MERGE symoblic-pr to master: STEP one #294
Conversation
evm.md
Outdated
| @@ -15,6 +15,7 @@ module EVM | |||
| imports STRING | |||
| imports EVM-DATA | |||
| imports NETWORK | |||
| imports K-REFLECTION | |||
There was a problem hiding this comment.
i think this can be dropped now.
evm-symbolic.md
Outdated
|
|
||
| ```k | ||
| endmodule | ||
| ``` |
There was a problem hiding this comment.
if we do not have much thing to add in this module, i think we can just move these two syntax declarations into EDSL.
There was a problem hiding this comment.
I added a few other things in the later commits. Lets keep it for now
There was a problem hiding this comment.
@yzhang90 I'm not comfortable merging this without seeing how these are being used. Can you point me to some example usages?
There was a problem hiding this comment.
There was a problem hiding this comment.
@ehildenb this is for abstracting ECREC that has two cases: ec-recover success and failure (i.e., the #sender may return .Account if the ECDSA recover fails for some reason. see the two rules for #ecrec.) so, we need a kind of flag that distinguishes the two cases, which is #ecrecEmpty. and #symEcrec is the symbolic address resulted from the ec-recover for the success case.
note that in theory, ECREC can return 0 for both success and failure cases. but we don't want to have #symEcrec to cover both.
yzhang90
force-pushed
the
imap
branch
2 times, most recently
from
f18bde7
to
e5d7816
Compare
edsl.md
Outdated
| | byteStack2IntList ( WordStack , Int ) [function] | ||
|
|
||
| syntax Int ::= bytesInNextInt ( WordStack , Int ) [function] //how many bytes will go into next Int. | ||
| // ------------------------------------------------------------ |
There was a problem hiding this comment.
i think this ---- needs to be aligned
|
Jenkins: test mantis |
|
@ehildenb |
|
Jenkins: test this please |
symbolic: Created module symbolic.md, Symbolic rules for ECREC.
edsl, symbolic: added generalized byteStack2IntList(), refactoring of module dependencies. Now EVM-SYMBOLIC imports EDSL.