The semantics represented by Fixpoint function

[channgo2203]

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]

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]

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

[channgo2203]

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 #6 (comment), or mute the thread https://github.com/notifications/unsubscribe-auth/ABsJyanH3WT_CShhKPl5ojNasL6YG7XRks5qzK71gaJpZM4KUKGP.

[pirapira]

@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.