More clear tests #187
More clear tests #187
Conversation
virgil-serbanuta
force-pushed
the
str-encoding
branch
2 times, most recently
from
10f243a to
d40e15d
Compare
virgil-serbanuta
force-pushed
the
clear-tests
branch
from
d049999 to
0830a70
Compare
virgil-serbanuta
force-pushed
the
clear-tests
branch
from
c9831b9 to
34a6e09
Compare
| rule encode_call_data C:EncodeCall | ||
| => encodeCallData(extractCallSignature(C), encodeInstructions(C)) | ||
|
|
||
| syntax ExecutionItem ::= encodeCallData(BytesOrError, NonEmptyStatementsOrError) |
There was a problem hiding this comment.
Should this have function, total attrs?
There was a problem hiding this comment.
It can't have a "total" attribute because it's not defined when either the first or the second argument is an error. Since partial functions have all sorts of problems (e.g. having a Left => Right rewrite rule in a semantics where Right may be undefined makes the entire semantics unsound, or whatever is the proper word for it), I would prefer to use them only when absolutely needed.
Even if we ignore that, I would argue that not making this a function makes the code more debugable. When evaluating an undefined function, the LLVM backend will print the function that it can't evaluate, which is sort of nice. However, it's harder to get the entire context in which this happened (i.e., the entire configuration). If encodeCallData is not a function, you get the entire configuration.
With the Haskell backend, if we make this a function, it depends. If there is a #Ceil definition for this, then proving would just succeed (since bottom implies everything), although that's certainly not what we want here (although I think that they may have added a warning for this case, or something like that). Without a #Ceil definition, you'd get the full configuration with an unevaluated function, which is fine for debugging.
| <ulm-bytes-buffers> | ||
| Buffers:Map | ||
| </ulm-bytes-buffers> | ||
| requires B:Bytes:KItem ==K Buffers[MInt2Unsigned(V)] orDefault 0 |
There was a problem hiding this comment.
I'm not quite sure how the orDefault case here works --- the types don't seem to match up how I expect --- is this clause intended to always be false in the orDefault case?
There was a problem hiding this comment.
Yes. I added a comment saying that explicitly.
| => ulmBytesNew(encodeConstructorData(PTYPES, ARGS)) | ||
| ... | ||
| </k> | ||
| syntax ExecutionItem ::= encodeConstructorData(NonEmptyStatementsOrError) |
There was a problem hiding this comment.
Should this have function, total attrs?
There was a problem hiding this comment.
Same answer as above.
ulm-semantics/test/execution.md
Outdated
| rule encodeArgsToEncodeValues(E:Expression : T:Type , Es:EncodeArgs) | ||
| => E : T , encodeArgsToEncodeValues(Es) |
There was a problem hiding this comment.
It looks like EncodeArg and EncodeValue have the same syntax. Is this the intended behavior? At the moment I don't fully understand how these sorts are being used.
There was a problem hiding this comment.
They are mostly the same thing. There are some obscure reasons for keeping them separate (mostly I was hesitant about using EncodeValues for parsing), but I think that you're probably right and I should merge them. See the last commit of this PR. If you decide that, for some reasons, they should be separate, I can create a new PR undoing that commit.
| rule SetAccountStorageHook(evaluatedStorageKey(B:Bytes), ptrValue(_, Value:Value)) | ||
| => #SetAccountStorageHook | ||
| ( Bytes2Int(Keccak256raw(B), BE, Unsigned) | ||
| , valueToInteger(Value) |
There was a problem hiding this comment.
It seems that, in the case valueToInteger returns error, the rules below on 270 and 274 will not cover all possible cases and evaluation will get stuck.
There was a problem hiding this comment.
Yes, it gets stuck, and valueToInteger evaluates to a term containing an error message somewhat explaining what went wrong. That's by design. I mean, is there a better option if the user asks to add a mock for a SetAccountStorage(key, non-integer-value) call?
Of course, one option would be to provide an Int directly to SetAccountStorageHook instead of an Expression, and I'll do that if you think it's better, but this PR attempted to make tests more readable, and I'm assuming that using Expression helps.
ulm-semantics/test/execution.md
Outdated
| rule SetAccountStorageHook(evaluatedStorageKey(B:Bytes), ptrValue(_, Value:Value)) | ||
| => #SetAccountStorageHook | ||
| ( Bytes2Int(Keccak256raw(B), BE, Unsigned) | ||
| , valueToInteger(Value) | ||
| ) | ||
| rule mock #SetAccountStorageHook(Key:Int, Value:Int) Result:UlmHookResult | ||
| => mock | ||
| SetAccountStorageHook(Key, Value) | ||
| Result | ||
| rule list_mock #SetAccountStorageHook(Key:Int, Value:Int) Result:UlmHookResult | ||
| => list_mock | ||
| SetAccountStorageHook(Key, Value) | ||
| Result | ||
|
|
||
| rule GetAccountStorageHook(evaluatedStorageKey(B:Bytes)) | ||
| => #GetAccountStorageHook(Bytes2Int(Keccak256raw(B), BE, Unsigned)) | ||
| rule mock #GetAccountStorageHook(Key:Int) Result:UlmHookResult | ||
| => mock | ||
| GetAccountStorageHook(Key) | ||
| Result | ||
| rule list_mock #GetAccountStorageHook(Key:Int) Result:UlmHookResult | ||
| => list_mock | ||
| GetAccountStorageHook(Key) | ||
| Result |
There was a problem hiding this comment.
The use of overloaded names Set/GetAccountStorageHook and #Set/GetAccountStorageHook both in this file and in ulm-semantics/main/hooks/ulm.md makes the logic a bit hard to follow in these rules.
It looks in this file the declared sharp versions are intermediate forms --- perhaps they could be renamed to avoid conflict with the overloaded version in ulm-semantics/main/hooks/ulm.md?
I understand that the non-sharp version in this file is designed to make the test files look like the underlying functions in the semantics, so the overloading there seems to have a potentially bigger payoff in test readability.
virgil-serbanuta
force-pushed
the
clear-tests
branch
from
879b8c4 to
639b43d
Compare
No description provided.