Formal-spec style description of the EEI

[ehildenb]

https://github.com/ewasm/design/blob/master/eth_interface.md

We should be trying to follow the format of the WASM spec here, instead of having our own style/format. This will force us to disambiguate a lot of the behaviour here which is potentially ambiguous.

I can do this work if people would like, or at least start the branch doing the work. Just want to make sure there is agreement that this should happen.

[axic]

Can you give a short example of what format you'd like it to have? (There are so many versions of the "WAMS spec", I'm not entirely sure which one do you mean.)

[ehildenb]

https://github.com/WebAssembly/spec/blob/master/document/core/exec/instructions.rst

Looking at SELECT as a template.

So right now we have:

useGas

Subtracts an amount to the gas counter

Parameters

• amount i64 the amount to subtract to the gas counter

Returns

nothing

But we might think to have (I'm taking liberty with making my own notation for the system contract math notation at the end):

useGas

1. Assert: due to validation, that the top element of the stack is a value of type i64.
2. Pop the value i64.const g from the top of the stack.
3. Load the value i64.const G from EEI.gasAvailable.
4. If g <= G, then: i. Set EEI.gasAvailable to G - g.
5. Else: ii. Set EEI.trapReason to out of gas and Trap.

~\\[-1ex]
\begin{array}{l}
\begin{array}{lcl@{\qquad}l}
EEI; (\I32.\CONST g) (useGas) &\stepto& EEI'
\end{array}
\\ \qquad
(\iff EEI.gasAvailable = G \\
 \wedge G >= g \\
 \wedge EEI' = EEI \with gasAvailable = G - g \\
 )
\end{array}

\begin{array}{l}
\begin{array}{lcl@{\qquad}l}
EEI; (\I32.\CONST g) (useGas) &\stepto& EEI'; trap
\end{array}
\\ \qquad
(\iff EEI.gasAvailable = G \\
 \wedge G < g \\
 \wedge EEI' = EEI \with trapReason = "out of gas" \\
 )
\end{array}

This would give us a nice way to formalize/disambiguate issues like: https://github.com/ewasm/design/issues/72

[axic]

1. Assert: due to validation, that the top element of the stack is a value of type i64.
2. Pop the value i64.const g from the top of the stack.

I am not sure we actually have access to the stack.

External functions don’t receive access to the stack of the caller, just arguments, which were popped already off the stack.

[ehildenb]

Would the following make more sense? Note that I've switched (i32.const g) (useGas) to call EEI.useGas i64.const g to reflect that this is a function call.

call EEI.useGas i64.const g

1. Load the value i64.const G from EEI.gasAvailable.
2. If g <= G, then: i. Set EEI.gasAvailable to G - g.
3. Else: ii. Set EEI.trapReason to out of gas and Trap.

~\\[-1ex]
\begin{array}{l}
\begin{array}{lcl@{\qquad}l}
EEI; (call EEI.useGas i64.const g) &\stepto& EEI'
\end{array}
\\ \qquad
(\iff EEI.gasAvailable = G \\
 \wedge G >= g \\
 \wedge EEI' = EEI \with gasAvailable = G - g \\
 )
\end{array}

\begin{array}{l}
\begin{array}{lcl@{\qquad}l}
EEI; (call EEI.useGas i64.const g) &\stepto& EEI'; trap
\end{array}
\\ \qquad
(\iff EEI.gasAvailable = G \\
 \wedge G < g \\
 \wedge EEI' = EEI \with trapReason = "out of gas" \\
 )
\end{array}

[lrettig]

From the perspective of a lowly implementer, this would help a lot and would probably preempt a lot of the dumb questions I've asked e.g. https://gitter.im/ewasm/internal?at=5aac31dbc3c5f8b90d7e5e15.

[ehildenb]

https://docs.google.com/document/d/1z_u-hmQ6kF50rXbBEmT_tLOnyBGaBplpoOIe0FPEZ3s/edit?usp=sharing