spec: Runtime spec for gas and stack accounting

[nagisa]

Split out from #2

[nagisa]

I’m… no longer finding a way to set PR as a draft...

[Ekleog]

Just carrying one leftover comment from the previous PR, and I also noticed that the wording was not exactly right yet for stack height metering. It was written as though the check was supposed to validate the whole call tree.

[matklad]

Note that today it is gas(u32) where u32 measures opcodes rather than gas cost directly. Ie, it's conceptually the host who multiplies ops by gas-cost.

Spec-wise it seems easier to count instructions, but that might close the door to differently-weighting instructions. Or at least make that doorframe narrower -- even with ops, we can say that sqrt is 2x usual op.

[nagisa]

I don’t believe the spec should specify a specific scheme in that regard. I adjusted the wording to use a fee(insn) mechanism where fee is defined by the embedder – this way they can specify whatever they want – counting instructions (fee = 1), or something else entirely.

However, in practice it is impossible to continue counting each instruction as 1. Some instructions, even today, scale linearly depending on the operands they pop (memory.grow) and they will only continue increasing (e.g. memory.fill).

And either way, we’ve had problems with fitting some things into u32, so making the gas limit an u64 seems like an obvious improvement in flexibility.

[nagisa]

I went ahead and reworded the specification to achieve the following:

• Both gas and stack limits are, for the purposes of the specification ensured at each charged operation (for each instruction executed for gas, for each stack push/pop for stack size). These can then be optimized by the implementation by collapsing within basic blocks etc. cf. used_gas: how can we provide exact measure of gas used/remaining gas back to the contract? #3
• We don’t talk about implementation details anywhere except side notes. Implementation details is for the implementation to decide on ^^
• Fixed the wording to allow for stack entries to be counted however the impementation prefers;
• Fixed the wording charging gas for local initialization – this is now part of semantics for invoking a function address, exactly where it belongs.

This new wording however has some interesting implications. For example, as written, we ought to charge some gas when evaluating the i32.const 0 in

(data (offset (i32.const 0)) ...)

which clearly requires involvement of the VM. Implementation wise, we can also charge this after the fact too in e.g. the start function, much like we might need to do for local initialization.

[nagisa]

This I believe effectively requires special handling for these kinds of instructions in the instrumentation or the VM. That is, you can’t just

(call $gas (i32.const 1))
(memory.grow (i32.const 123))

You actually need either a variadic $gas that is able to take all the operands as an argument (before returning them) or maybe some other nasty hack…

[matklad]

Yeah, I think our current impl rewrites memory.grow into a funciton call.

[matklad]

Overal, LGTM! Fees surprisingly simple even

[matklad]

Might be worth to explicitly mention that

the specification aims to support at least two general implementation strategies: desugaring in the terms of core WASM, or built-in accounting in the VM itself.

[matklad]

Yeah, I think our current impl rewrites memory.grow into a funciton call.

[matklad]

incomplete sentence

[nagisa]

Aha, because this is no longer necessary due to this logic having moved to the “Invocation of function address a” portion of the spec. Nice catch, removed.