search

pirapira / evmverif

An EVM code verification framework in Coq
Apache License 2.0
44 stars 8 forks source link

The semantics represented by Fixpoint function #6

Open channgo2203 opened 7 years ago

channgo2203 commented 7 years ago

The semantics represented by Fixpoint function decreases on the number of step is not good. Since if a bytecode program uses jump instructions that loop, you cannot predict statically how many steps to evaluate. As my implementation (using fixpoint is "big-step" semantics style), it is decreases on the availabe gas.

pirapira commented 7 years ago

This is not a problem because whenever we use the fixpoint function, we can say "for any number of steps, the fixpoint function does not do this." Or, "there exists a number of steps after which the fixpoint function does this".

pirapira commented 7 years ago

@channgo2203 My usage of Fixpoint function with steps comes from here. Eventually I will replace the steps with gas.

channgo2203 commented 7 years ago

An other ways that is more flexible is to express the step evaluation as a relation instead of fixpoin function (you can look at some information at Software Foundations https://www.cis.upenn.edu/~bcpierce/sf/current/Smallstep.html https://www.cis.upenn.edu/~bcpierce/sf/current/Smallstep.html).

On Oct 12, 2016, at 5:57 AM, Yoichi Hirai notifications@github.com wrote:

This is not a problem because whenever we use the fixpoint function, we can say "for any number of steps, the fixpoint function does not do this." Or, "there exists a number of steps after which the fixpoint function does this".

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/pirapira/evmverif/issues/6#issuecomment-253170474, or mute the thread https://github.com/notifications/unsubscribe-auth/ABsJyanH3WT_CShhKPl5ojNasL6YG7XRks5qzK71gaJpZM4KUKGP.

pirapira commented 7 years ago

@channgo2203 Yes. That allows nondeterminism. Actually we need nondeterminism for CALL instruction because the result of CALL is out of control of the contract under verification. By default I'm going to wrap the currently existing Fixpoint function as a relation.