diff --git a/tests/ulm-with-contract/erc_20_token.1.run b/tests/ulm-with-contract/erc_20_token.1.run index b3388e7..94e4dd0 100644 --- a/tests/ulm-with-contract/erc_20_token.1.run +++ b/tests/ulm-with-contract/erc_20_token.1.run @@ -8,11 +8,11 @@ list_mock GetAccountStorageHook ( storageKey("balances", 1010101_u160:u160) ) ul list_mock SetAccountStorageHook ( storageKey("balances", 1010101_u160:u160) , 9900_u256 ) ulmNoResult(); list_mock GetAccountStorageHook ( storageKey("balances", 2020202_u160:u160) ) ulmIntResult(0, u256); list_mock SetAccountStorageHook ( storageKey("balances", 2020202_u160:u160) , 100_u256 ) 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 Log3Hook ( eventSignature("Transfer(address,address,uint256)") , 1010101 , 2020202 , encodeValues(100_u256:u256) ) ulmNoResult(); list_mock GetAccountStorageHook ( storageKey("balances", 1010101_u160:u160) ) ulmIntResult(9900, u256); list_mock GetAccountStorageHook ( storageKey("balances", 2020202_u160:u160) ) ulmIntResult(100, u256); list_mock SetAccountStorageHook ( storageKey("allowances", 1010101_u160:u160, 3030303_u160:u160) , 200_u256 ) 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 Log3Hook ( eventSignature("Approval(address,address,uint256)") , 1010101 , 3030303 , encodeValues(200_u256:u256) ) ulmNoResult(); list_mock GetAccountStorageHook ( storageKey("allowances", 1010101_u160:u160, 3030303_u160:u160) ) ulmIntResult(200, u256); list_mock SetAccountStorageHook ( storageKey("allowances", 1010101_u160:u160, 3030303_u160:u160) , 0_u256 ) ulmNoResult(); list_mock GetAccountStorageHook ( storageKey("balances", 1010101_u160:u160) ) ulmIntResult(9900, u256); @@ -20,7 +20,7 @@ list_mock GetAccountStorageHook ( storageKey("balances", 1010101_u160:u160) ) ul list_mock SetAccountStorageHook ( storageKey("balances", 1010101_u160:u160) , 9700_u256 ) ulmNoResult(); list_mock GetAccountStorageHook ( storageKey("balances", 2020202_u160:u160) ) ulmIntResult(100, u256); list_mock SetAccountStorageHook ( storageKey("balances", 2020202_u160:u160) , 300_u256 ) 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 Log3Hook ( eventSignature("Transfer(address,address,uint256)") , 1010101 , 2020202 , encodeValues(200_u256:u256) ) ulmNoResult(); list_mock GetAccountStorageHook ( storageKey("balances", 1010101_u160:u160) ) ulmIntResult(9700, u256); list_mock GetAccountStorageHook ( storageKey("balances", 2020202_u160:u160) ) ulmIntResult(300, u256); diff --git a/ulm-semantics/main/hooks/ulm.md b/ulm-semantics/main/hooks/ulm.md index af09a70..c6b06f6 100644 --- a/ulm-semantics/main/hooks/ulm.md +++ b/ulm-semantics/main/hooks/ulm.md @@ -8,8 +8,6 @@ module ULM-SEMANTICS-HOOKS-ULM-SYNTAX | CallerHook() | SetAccountStorageHook(Int, Int) | GetAccountStorageHook(Int) - // TODO: Build mocks for all the hooks below in a meaningful - // way in tests (right now we just use opaque values). | Log0Hook(Bytes) | Log1Hook(Int, Bytes) | Log2Hook(Int, Int, Bytes) diff --git a/ulm-semantics/test/execution.md b/ulm-semantics/test/execution.md index 4b3df80..6f6c0c6 100644 --- a/ulm-semantics/test/execution.md +++ b/ulm-semantics/test/execution.md @@ -44,8 +44,11 @@ module ULM-TEST-SYNTAX syntax UlmTestHook ::= SetAccountStorageHook(StorageKey, Expression) [seqstrict, result(TestResult)] | GetAccountStorageHook(StorageKey) [seqstrict, result(TestResult)] + | Log3Hook(EventSignature, Int, Int, EncodeValues) [seqstrict(1, 4), result(TestResult)] syntax StorageKey ::= storageKey(String, EncodeArgs) + syntax EventSignature ::= eventSignature(String) + syntax EncodeValues ::= encodeValues(EncodeArgs) endmodule module ULM-TEST-EXECUTION @@ -68,7 +71,7 @@ module ULM-TEST-EXECUTION syntax UlmTestHook ::= #SetAccountStorageHook(Int, IntOrError) | #GetAccountStorageHook(Int) - + | #Log3Hook(Int, Int, Int, Bytes) syntax Mockable ::= UlmHook syntax BytesOrError ::= extractCallSignature(EncodeCall) [function, total] @@ -208,9 +211,12 @@ module ULM-TEST-EXECUTION syntax Bool ::= isTestResult(K) [symbol(isTestResult), function] rule isTestResult(_:K) => false [owise] rule isTestResult(evaluatedStorageKey(_:Bytes)) => true + rule isTestResult(evaluatedEventSignature(_:Int)) => true + rule isTestResult(encodedValues(_:Bytes)) => true rule isTestResult(_:PtrValue) => true rule isTestResult(#SetAccountStorageHook(_:Int, _:Int)) => true rule isTestResult(#GetAccountStorageHook(_:Int)) => true + rule isTestResult(#Log3Hook(_:Int, _:Int, _:Int, _:Bytes)) => true syntax StorageKey ::= storageKey(NonEmptyStatementsOrError) | storageKey(Expression) [strict(1)] @@ -232,6 +238,30 @@ module ULM-TEST-EXECUTION rule storageKey(ptrValue(_, u64(BytesId))) => storageKey(ulmBytesId(BytesId)) rule storageKey(ulmBytesValue(B:Bytes)) => evaluatedStorageKey(B) + syntax EventSignature ::= evaluatedEventSignature(Int) + rule eventSignature(Signature:String) + => evaluatedEventSignature(Bytes2Int(Keccak256raw(String2Bytes(Signature)), BE, Unsigned)) + + syntax EncodeValues ::= encodeValues(NonEmptyStatementsOrError) + | encodeValues(Expression) [strict(1)] + | encodeValues(UlmExpression) [strict(1)] + | encodedValues(Bytes) + rule encodeValues(Args:EncodeArgs) + => encodeValues + ( concat + ( let buffer_id = :: bytes_hooks :: empty( .CallParamsList ); + .NonEmptyStatements + , encodeStatements + ( buffer_id + , encodeArgsToEncodeValues(Args) + ) + ) + ) + rule encodeValues(Statements:NonEmptyStatements) + => encodeValues({.InnerAttributes Statements buffer_id }) + rule encodeValues(ptrValue(_, u64(BytesId))) => encodeValues(ulmBytesId(BytesId)) + rule encodeValues(ulmBytesValue(B:Bytes)) => encodedValues(B) + rule SetAccountStorageHook(evaluatedStorageKey(B:Bytes), ptrValue(_, Value:Value)) => #SetAccountStorageHook ( Bytes2Int(Keccak256raw(B), BE, Unsigned) @@ -257,6 +287,18 @@ module ULM-TEST-EXECUTION GetAccountStorageHook(Key) Result + rule Log3Hook(evaluatedEventSignature(I:Int), A:Int, C:Int, encodedValues(B2:Bytes)) + => #Log3Hook + ( I + , A + , C + , B2 + ) + rule list_mock #Log3Hook(V1:Int, V2:Int, V3:Int, B:Bytes) Result:UlmHookResult + => list_mock + Log3Hook(V1, V2, V3, B) + Result + // This may seem stupid, but it's a workaround for // https://github.com/runtimeverification/k/issues/4683 rule isKResult(X) => true requires isTestResult(X)