finite-wasm 0.6.1

Guarantee deterministic limits on execution time and space resources made available to the WebAssembly programs in a runtime-agnostic way.
# [Execution]()

The specific mechanism to instrument a WebAssembly module is implementation-specific. This section
describes the extensions to the [execution semantics]() of an instrumented WebAssembly module.

The specification extensions allow for various implementation strategies, including but not limited
to: transforming the WASM code to VM agnostic instrumented WASM code; built-in accounting in the VM
implementation itself; and others.

## [Runtime Structure]()

### [Module Instances]()

The `moduleinst` record is extended with the following entries:

* An amount of gas remaining `u64 gas`;
* Limit to the number of stack entries `u32 stacklimit`.

These additional entries may be emulated via instances of mutable global variables, if necessary.

### [Stack]()

โ€œStack heightโ€ is the height of the implicit stack. Stack height is a sum of:

1. The sum of sizes of the `value` stack entries; and
2. The sum of sizes of the `label` stack entries; and
3. The sum of sizes of the function activation frame stack entries.

**Note:** The size of each type of entry is not specified by this specification, however there are
some considerations to make when deciding on a function to compute the size of an entry:

* It may make sense to count each `value` as `1` slot or, alternatively, to consider their byte
  size (e.g. 4 for `i32` and 8 for `i64`);
* `labels` may be counted as `0` or `1` entry depending on the way theyโ€™re handled;
* In addition to the size inherent to all `activation` frames, the sizes of all local `value`s in
  `activation.frame.val` should be considered, as they may increase the size of the activation
  frames on the stack significantly.


## [Instructions]()

At each step before the WebAssembly instructions are reduced, the embedder-provided `fee` function
shall match a sequence of instructions and compute the gas price to execute the step. Each fee
decreases the `F.module.gas`. If subtracting from `f.module.gas` would cause the remaining gas pool
to decrease below zero, or to overflow, `F.module.gas` is set to 0 and the execution `trap`s.

For the given matched sequence of instructions, once the match occurs, the sequence is fully
evaluated before the fee matching occurs again.

**Note:** Specifying `fee` mapping is a responsibility of the embedder and is out of scope for this
specification.

**Note:** `fee` may match the operands the instruction would consume. This is particularly useful
for bulk instructions such as `memory.fill`. For example `fee((i32.const d) val (i32.const n)
memory.fill)` may take into the account that `n` bytes worth of memory would be written. Note that
`memory.fill` produces another `memory.fill` with a shorter range as a result of the reduction:

```
๐‘†; ๐น ; (i32.const ๐‘‘) val (i32.const ๐‘› + 1) memory.fill โ†’
๐‘†; ๐น ; (i32.const ๐‘‘) val (i32.store8 {offset 0, align 0})
(i32.const ๐‘‘ + 1) val (i32.const ๐‘›) memory.fill
```

However, since the fee for the original `memory.fill` was applied already, the execution of this
function and its reductions are not applied repeatedly until the entire sequence completes
reducing and executing.


### [Function calls]()

#### [Invocation of function address a]()

**Note**: Executing an instruction that invokes function instances must:

* Decrease the `F.module.gas` by `fee(frame๐‘› {frame} instr * end)`. This gives an opportunity to
  charge the gas fees necessary to construct the frame with a list of 0-values and to push it onto
  the native stack, if any. If subtracting the fee would cause `F.module.gas` to decrease below
  zero or to overflow, `F.module.gas` is set to 0 and the execution `trap`s.
* Ensure the sum of the current stack height and the maximum stack height required to execute the
  function do not exceed the `F.module.stacklimit`. Otherwise `trap`.

<!--
TODO:

#### [Host functions]()

Should we charge fees before calling out to a host function? Should this be a part of the spec?
-->

## [Modules]()

### [Instantiation]()

`moduleinst.gas` and `moduleinst.stacklimit` are initialized to their initial values during the
module allocation. This must occur before any instructions are evaluated as part of the
instantiation process.

### [Invocation]()

The external invocation of an exported function is augmented with the following operations:

0. Assert: Stack height is 0, before any stack operations occur.
9. Before function invocation:
  * Charge gas for each local of `funcaddr` and execution of this `call` instruction;

**Note**: Instrumentation may implement this via the export indirection mechanism specified in an
appendix, however implementations are required to _not_ utilize stack indirection if they implement
this behaviour in some other manner, as this may lead to double-charging.