WebAssembly Specification Release 1.1 (Draft 2021-12-18) - page 5

get

𝑥

• The table

𝐶.

𝑥

]

must be defined in the context.

• Let

𝑡

be the

𝐶.

𝑥

]

• Then the instruction is valid with type

[

𝑡

]

𝐶.

𝑥

] =

𝑡

𝑥

: [

[

𝑡

]

set

𝑥

• The table

𝐶.

𝑥

]

must be defined in the context.

• Let

𝑡

be the

𝐶.

𝑥

]

• Then the instruction is valid with type

𝑡

[]

𝐶.

𝑥

] =

𝑡

𝑥

: [

𝑡

[]

𝑥

• The table

𝐶.

𝑥

]

must be defined in the context.

• Then the instruction is valid with type

𝐶.

𝑥

] =

𝑥

: []

𝑥

• The table

𝐶.

𝑥

]

must be defined in the context.

• Let

𝑡

be the

𝐶.

𝑥

]

• Then the instruction is valid with type

[

𝑡

𝐶.

𝑥

] =

𝑡

𝑥

: [

𝑡

𝑥

• The table

𝐶.

𝑥

]

must be defined in the context.

• Let

𝑡

be the

𝐶.

𝑥

]

• Then the instruction is valid with type

𝑡

[]

𝐶.

𝑥

] =

𝑡

𝑥

: [

𝑡

[]

3.3. Instructions

copy

𝑥 𝑦

• The table

𝐶.

𝑥

]

must be defined in the context.

• Let

𝑡

be the

𝐶.

𝑥

]

• The table

𝐶.

𝑦

]

must be defined in the context.

• Let

𝑡

be the

𝐶.

𝑦

]

• The

𝑡

must be the same as

𝑡

• Then the instruction is valid with type

[]

𝐶.

𝑥

] =

𝑡

𝐶.

𝑥

] =

𝑡

𝑥 𝑦

: [

[]

𝑥 𝑦

• The table

𝐶.

𝑥

]

must be defined in the context.

• Let

𝑡

be the

𝐶.

𝑥

]

• The element segment

𝐶.

𝑦

]

must be defined in the context.

• Let

𝑡

be the

𝐶.

𝑦

]

• The

𝑡

must be the same as

𝑡

• Then the instruction is valid with type

[]

𝐶.

𝑥

] =

𝑡

𝐶.

𝑦

] =

𝑡

𝑥 𝑦

: [

[]

𝑥

• The element segment

𝐶.

𝑥

]

must be defined in the context.

• Then the instruction is valid with type

[]

𝐶.

𝑥

] =

𝑡

𝑥

: []

[]

3.3.7 Memory Instructions

𝑡.

load

• The memory

𝐶.

must be defined in the context.

• The alignment

must not be larger than the

bit width

𝑡

divided by

• Then the instruction is valid with type

[

𝑡

]

𝐶.

≤ |

𝑡

𝑡.

load

: [

[

𝑡

]

Chapter 3. Validation

• The memory

𝐶.

must be defined in the context.

• The alignment

must not be larger than

𝑁/

• Then the instruction is valid with type

[

𝑡

]

𝐶.

≤

𝑁/

𝑡.

load

𝑁

: [

[

𝑡

]

𝑡.

store

• The memory

𝐶.

must be defined in the context.

• The alignment

must not be larger than the

bit width

𝑡

divided by

• Then the instruction is valid with type

𝑡

[]

𝐶.

≤ |

𝑡

𝑡.

store

: [

𝑡

[]

• The memory

𝐶.

must be defined in the context.

• The alignment

must not be larger than

𝑁/

• Then the instruction is valid with type

𝑡

[]

𝐶.

≤

𝑁/

𝑡.

store

𝑁

: [

𝑡

[]

v128

load

𝑀

sx memarg

• The memory

𝐶.

must be defined in the context.

• The alignment

must not be larger than

𝑁/

𝑀

• Then the instruction is valid with type

𝐶.

≤

𝑁/

𝑀

v128

𝑀

: [

v128

splat

• The memory

𝐶.

must be defined in the context.

• The alignment

must not be larger than

𝑁/

• Then the instruction is valid with type

𝐶.

≤

𝑁/

v128

splat

: [

3.3. Instructions

v128

load

zero

• The memory

𝐶.

must be defined in the context.

• The alignment

must not be larger than

𝑁/

• Then the instruction is valid with type

𝐶.

≤

𝑁/

v128

zero

: [

v128

lane

• The lane index

must be smaller than

128

/𝑁

• The memory

𝐶.

must be defined in the context.

• The alignment

must not be larger than

𝑁/

• Then the instruction is valid with type

128

/𝑁

𝐶.

< 𝑁/

v128

lane

: [

v128

lane

• The lane index

must be smaller than

128

/𝑁

• The memory

𝐶.

must be defined in the context.

• The alignment

must not be larger than

𝑁/

• Then the instruction is valid with type

128

/𝑁

𝐶.

< 𝑁/

v128

lane

: [

[]

• The memory

𝐶.

must be defined in the context.

• Then the instruction is valid with type

𝐶.

: []

• The memory

𝐶.

must be defined in the context.

• Then the instruction is valid with type

𝐶.

𝐶

: [

Chapter 3. Validation

memory

fill

• The memory

𝐶.

must be defined in the context.

• Then the instruction is valid with type

[]

𝐶.

: [

[]

• The memory

𝐶.

must be defined in the context.

• Then the instruction is valid with type

[]

𝐶.

: [

[]

𝑥

• The memory

𝐶.

must be defined in the context.

• The data segment

𝐶.

𝑥

]

must be defined in the context.

• Then the instruction is valid with type

[]

𝐶.

𝐶.

𝑥

] =

𝑥

: [

[]

𝑥

• The data segment

𝐶.

𝑥

]

must be defined in the context.

• Then the instruction is valid with type

[]

𝐶.

𝑥

] =

𝑥

: []

[]

3.3.8 Control Instructions

nop

• The instruction is valid with type

[]

𝐶

: []

[]

• The instruction is valid with type

[

𝑡

[

𝑡

]

, for any sequences of

𝑡

and

𝑡

unreachable

: [

𝑡

[

𝑡

]

Note:

The

unreachable

instruction is

3.3. Instructions

• The

must be

as some

[

𝑡

[

𝑡

]

• Let

𝐶

′

be the same

𝐶

, but with the

[

𝑡

]

prepended to the

vector.

• Under context

𝐶

′

, the instruction sequence

must be

with type

[

𝑡

[

𝑡

]

• Then the compound instruction is valid with type

[

𝑡

[

𝑡

]

blocktype

: [

𝑡

[

𝑡

]

𝐶,

[

𝑡

: [

𝑡

[

𝑡

]

: [

𝑡

[

𝑡

]

Note:

The

notation

𝐶,

[

𝑡

]

inserts the new label type at index

, shifting all others.

• The

must be

as some

[

𝑡

[

𝑡

]

• Let

𝐶

′

be the same

𝐶

, but with the

[

𝑡

]

prepended to the

vector.

• Under context

𝐶

′

, the instruction sequence

must be

with type

[

𝑡

[

𝑡

]

• Then the compound instruction is valid with type

[

𝑡

[

𝑡

]

blocktype

: [

𝑡

[

𝑡

]

𝐶,

[

𝑡

: [

𝑡

[

𝑡

]

: [

𝑡

[

𝑡

]

Note:

The

notation

𝐶,

[

𝑡

]

inserts the new label type at index

, shifting all others.

• The

must be

as some

[

𝑡

[

𝑡

]

• Let

𝐶

′

be the same

𝐶

, but with the

[

𝑡

]

prepended to the

vector.

• Under context

𝐶

′

, the instruction sequence

must be

with type

[

𝑡

[

𝑡

]

• Under context

𝐶

′

, the instruction sequence

must be

with type

[

𝑡

[

𝑡

]

• Then the compound instruction is valid with type

[

𝑡

[

𝑡

]

blocktype

: [

𝑡

[

𝑡

]

𝐶,

[

𝑡

: [

𝑡

[

𝑡

]

𝐶,

[

𝑡

: [

𝑡

[

𝑡

]

: [

𝑡

[

𝑡

]

Note:

The

notation

𝐶,

[

𝑡

]

inserts the new label type at index

, shifting all others.

𝑙

• The label

𝐶.

𝑙

]

must be defined in the context.

• Let

[

𝑡

]

be the

𝐶.

𝑙

]

• Then the instruction is valid with type

[

𝑡

[

𝑡

]

, for any sequences of

𝑡

and

𝑡

Chapter 3. Validation

𝐶.

𝑙

] = [

𝑡

]

𝑙

: [

𝑡

[

𝑡

]

Note:

The

label index

space in the

𝐶

contains the most recent label first, so that

𝐶.

𝑙

]

performs a

relative lookup as expected.
The

instruction is

𝑙

• The label

𝐶.

𝑙

]

must be defined in the context.

• Let

[

𝑡

]

be the

𝐶.

𝑙

]

• Then the instruction is valid with type

[

𝑡

[

𝑡

]

𝐶.

𝑙

] = [

𝑡

]

𝑙

: [

𝑡

[

𝑡

]

Note:

The

label index

space in the

𝐶

contains the most recent label first, so that

𝐶.

𝑙

]

performs a

relative lookup as expected.

𝑙

𝑁

• The label

𝐶.

𝑙

𝑁

]

must be defined in the context.

• For all

𝑙

𝑖

𝑙

, the label

𝐶.

𝑙

𝑖

]

must be defined in the context.

• There must be a

[

𝑡

]

, such that:

–

For each

𝑡

𝑗

𝑡

and corresponding type

𝑡

′

𝑁 𝑗

𝐶.

𝑙

𝑁

]

𝑡

𝑗

𝑡

′

𝑁 𝑗

–

For all

𝑙

𝑖

𝑙

, and for each

𝑡

𝑗

𝑡

and corresponding type

𝑡

′

𝑖𝑗

𝐶.

𝑙

𝑖

]

𝑡

𝑗

𝑡

′

𝑖𝑗

• Then the instruction is valid with type

[

𝑡

[

𝑡

]

, for any sequences of

𝑡

and

𝑡

(

⊢

[

𝑡

]

≤

𝐶.

𝑙

])

⊢

[

𝑡

]

≤

𝐶.

𝑙

𝑁

]

𝑙

𝑁

: [

𝑡

[

𝑡

]

Note:

The

label index

space in the

𝐶

contains the most recent label first, so that

𝐶.

𝑙

𝑖

]

performs a

relative lookup as expected.
The

instruction is

• The return type

𝐶.

must not be absent in the context.

• Let

[

𝑡

]

be the

𝐶.

• Then the instruction is valid with type

[

𝑡

[

𝑡

]

, for any sequences of

𝑡

and

𝑡

𝐶.

= [

𝑡

]

: [

𝑡

[

𝑡

]

Note:

The

instruction is

3.3. Instructions

𝐶.

is absent (set to

𝜖

) when validating an

expression

that is not a function body. This differs from it being

set to the empty result type (

[

𝜖

]

), which is the case for functions not returning anything.

call

𝑥

• The function

𝐶.

𝑥

]

must be defined in the context.

• Then the instruction is valid with type

𝐶.

𝑥

]

𝐶.

𝑥

] = [

𝑡

[

𝑡

]

call

𝑥

: [

𝑡

[

𝑡

]

call

indirect

𝑥 𝑦

• The table

𝐶.

𝑥

]

must be defined in the context.

• Let

𝑡

be the

𝐶.

𝑥

]

• The

𝑡

must be

funcref

• The type

𝐶.

𝑦

]

must be defined in the context.

• Let

[

𝑡

[

𝑡

]

be the

function type

𝐶.

𝑦

]

• Then the instruction is valid with type

[

𝑡

[

𝑡

]

𝐶.

𝑥

] =

𝐶.

𝑦

] = [

𝑡

[

𝑡

]

𝑥 𝑦

: [

𝑡

[

𝑡

]

3.3.9 Instruction Sequences

Typing of instruction sequences is defined recursively.

Empty Instruction Sequence:

𝜖

• The empty instruction sequence is valid with type

[

𝑡

[

𝑡

]

, for any sequence of

operand types

𝑡

𝜖

: [

𝑡

[

𝑡

]

Non-empty Instruction Sequence:

• The instruction sequence

must be valid with type

[

𝑡

[

𝑡

]

, for some sequences of

𝑡

and

𝑡

• The instruction

must be valid with type

[

𝑡

[

𝑡

]

, for some sequences of

𝑡

and

𝑡

• There must be a sequence of

𝑡

, such that

𝑡

′*

where the type sequence

𝑡

′*

is as long as

𝑡

• For each

𝑡

′

𝑖

𝑡

′*

and corresponding type

𝑡

𝑖

𝑡

′

𝑖

𝑡

𝑖

• Then the combined instruction sequence is valid with type

[

𝑡

[

𝑡

]

: [

𝑡

[

𝑡

′*

]

⊢

[

𝑡

′*

]

≤

[

𝑡

]

: [

𝑡

[

𝑡

]

: [

𝑡

[

𝑡

]

Chapter 3. Validation

3.3.10 Expressions

Expressions

are classified by

result types

of the form

[

𝑡

]

end

• The instruction sequence

must be

with some

[

𝑡

′*

]

• For each

𝑡

′

𝑖

𝑡

′*

and corresponding

value type

type

𝑡

𝑖

𝑡

′

𝑖

𝑡

𝑖

• Then the expression is valid with

[

𝑡

]

: []

[

𝑡

′*

]

⊢

[

𝑡

′*

]

≤

[

𝑡

]

: [

𝑡

]

Constant Expressions

• In a

constant

expression

end

all instructions in

must be constant.

• A constant instruction

must be:

–

either of the form

𝑡.

const

𝑐

–

or of the form

ref

null

–

or of the form

ref

𝑥

–

or of the form

global

get

𝑥

, in which case

𝐶.

𝑥

]

must be a

global type

of the form

const

𝑡

(

𝐶.

𝑥

] =

𝑡

Note:

Currently, constant expressions occurring as initializers of

globals

are further constrained in that contained

global

get

instructions are only allowed to refer to

imported

globals. This is enforced in the

validation rule for

modules

by constraining the context

𝐶

accordingly.

The definition of constant expression may be extended in future versions of WebAssembly.

3.4 Modules

Modules

are valid when all the components they contain are valid. Furthermore, most definitions are themselves

classified with a suitable type.

3.4. Modules

3.4.1 Functions

Functions

are classified by

function types

of the form

[

𝑡

[

𝑡

]

𝑡

• The type

𝐶.

𝑥

]

must be defined in the context.

• Let

[

𝑡

[

𝑡

]

be the

function type

𝐶.

𝑥

]

• Let

𝐶

′

be the same

𝐶

, but with:

–

locals

set to the sequence of

𝑡

, concatenating parameters and locals,

–

set to the singular sequence containing only

[

𝑡

]

–

set to the

[

𝑡

]

• Under the context

𝐶

′

, the expression

must be valid with type

[

𝑡

]

• Then the function definition is valid with type

[

𝑡

[

𝑡

]

𝐶.

𝑥

] = [

𝑡

[

𝑡

]

𝐶,

locals

𝑡

[

𝑡

]

[

𝑡

: [

𝑡

]

𝑡

: [

𝑡

[

𝑡

]

3.4.2 Tables

Tables

are classified by

• The

must be

• Then the table definition is valid with type

3.4.3 Memories

Memories

are classified by

• The

must be

• Then the memory definition is valid with type

Chapter 3. Validation

3.4.4 Globals

Globals

are classified by

of the form

𝑡

• The

𝑡

must be

• The expression

must be

with

[

𝑡

]

• The expression

must be

constant

• Then the global definition is valid with type

mut

𝑡

mut

𝑡

𝐶

: [

𝑡

]

𝑡

3.4.5 Element Segments

Element segments

elem

are classified by the

of their elements.

𝑒

• For each

𝑒

𝑖

𝑒

–

The expression

𝑒

𝑖

must be

–

The expression

𝑒

𝑖

must be

constant

• The element mode

elemmode

must be valid with

𝑡

• Then the element segment is valid with

𝑡

(

𝑒

)

(

𝐶

𝑡

𝑒

𝑡

• The element mode is valid with any

• The table

𝐶.

𝑥

]

must be defined in the context.

• Let

𝑡

be the

𝐶.

𝑥

]

• The expression

must be

with

• The expression

must be

• Then the element mode is valid with

𝑡

𝐶.

𝑥

] =

𝑡

: [

𝐶

𝑡

3.4. Modules

declarative

• The element mode is valid with any

3.4.6 Data Segments

Data segments

data

are not classified by any type but merely checked for well-formedness.

𝑏

• The data mode

must be valid.

• Then the data segment is valid.

𝑏

• The data mode is valid.

• The memory

𝐶.

𝑥

]

must be defined in the context.

• The expression

must be

with

• The expression

must be

• Then the data mode is valid.

𝐶.

𝑥

] =

𝐶

: [

3.4.7 Start Function

Start function declarations

start

are not classified by any type.

{

𝑥

}

• The function

𝐶.

𝑥

]

must be defined in the context.

• The type of

𝐶.

𝑥

]

must be

[]

• Then the start function is valid.

𝐶.

𝑥

] = []

[]

𝑥

}

Chapter 3. Validation

3.4.8 Exports

Exports

export

and export descriptions

exportdesc

are classified by their

• The export description

exportdesc

must be valid with

external type

externtype

• Then the export is valid with

𝑥

• The function

𝐶.

𝑥

]

must be defined in the context.

• Then the export description is valid with

𝐶.

𝑥

]

𝐶.

𝑥

] =

𝑥

𝑥

• The table

𝐶.

𝑥

]

must be defined in the context.

• Then the export description is valid with

𝐶.

𝑥

]

𝐶.

𝑥

] =

𝑥

𝑥

• The memory

𝐶.

𝑥

]

must be defined in the context.

• Then the export description is valid with

𝐶.

𝑥

]

𝐶.

𝑥

] =

𝑥

𝑥

• The global

𝐶.

𝑥

]

must be defined in the context.

• Then the export description is valid with

𝐶.

𝑥

]

𝐶.

𝑥

] =

𝑥

3.4. Modules

3.4.9 Imports

Imports

import

and import descriptions

are classified by

• The import description

importdesc

must be valid with type

externtype

• Then the import is valid with type

𝑥

• The function

𝐶.

𝑥

]

must be defined in the context.

• Let

[

𝑡

[

𝑡

]

be the

function type

𝐶.

𝑥

]

• Then the import description is valid with type

[

𝑡

[

𝑡

]

𝐶.

𝑥

] = [

𝑡

[

𝑡

]

𝑥

[

𝑡

[

𝑡

]

• The table type

must be

• Then the import description is valid with type

• The memory type

must be

• Then the import description is valid with type

• The global type

must be

• Then the import description is valid with type

Chapter 3. Validation

3.4.10 Modules

Modules are classified by their mapping from the

of their

imports

to those of their

exports

A module is entirely

closed

, that is, its components can only refer to definitions that appear in the module itself.

Consequently, no initial

is required. Instead, the context

𝐶

for validation of the module’s content is con-

structed from the definitions in the module.

• Let

module

be the module to validate.

• Let

𝐶

be a

where:

–

𝐶.

module

–

𝐶.

)

concatenated with

, with the import’s

and the internal

func-

tion types

as determined below,

–

𝐶.

)

concatenated with

, with the import’s

and the internal

table

types

as determined below,

–

𝐶.

)

concatenated with

, with the import’s

and the internal

memory types

as determined below,

–

𝐶.

)

concatenated with

, with the import’s

and the internal

global types

as determined below,

–

𝐶.

as determined below,

–

𝐶.

is ok

𝑛

, where

𝑛

is the length of the vector

module

–

𝐶.

locals

is empty,

–

𝐶.

is empty,

–

𝐶.

is empty.

–

𝐶.

is the set

𝜖

)

, i.e., the set of

function indices

occurring in the module, except in its

functions

start function

• Let

𝐶

′

be the

where:

–

𝐶

′

is the sequence

)

–

𝐶

′

is the same as

𝐶.

–

𝐶

′

is the same as

𝐶.

–

all other fields are empty.

• Under the context

𝐶

–

For each

, the

must be

–

For each

, the definition

must be

with a

𝑖

–

For each

, the definition

must be

with a

𝑖

–

For each

, the definition

must be

with a

𝑖

–

For each

∗ Under the context

𝐶

′

, the definition

must be

with a

𝑖

–

For each

, the segment

must be

with

𝑖

–

For each

, the segment

must be

–

is non-empty, then

must be

–

For each

, the segment

must be

with an

𝑖

–

For each

, the segment

must be

with

𝑖

• The length of

𝐶.

must not be larger than

3.4. Modules

• All export names

export

𝑖

name

must be different.

• Let

be the concatenation of the internal

function types

𝑖

, in index order.

• Let

be the concatenation of the internal

table types

𝑖

, in index order.

• Let

be the concatenation of the internal

memory types

𝑖

, in index order.

• Let

be the concatenation of the internal

global types

𝑖

, in index order.

• Let

be the concatenation of the

reference types

𝑖

, in index order.

• Let

be the concatenation of

𝑖

of the imports, in index order.

• Let

be the concatenation of

𝑖

of the exports, in index order.

• Then the module is valid with

)

(

𝐶

)

(

)

(

mem

)

(

𝐶

′

global

)

(

elem

)

(

data

)

𝑛

(

start

)

(

import

)

(

export

)

ift

)

itt

)

imt

)

igt

)

𝑥

𝜖

)

𝐶

ift

itt

imt

igt

𝑛

𝑥

}

𝐶

′

{

igt

(

𝐶.

)

(

𝐶.

)

}

𝐶.

| ≤

disjoint

}

Note:

Most definitions in a module – particularly functions – are mutually recursive. Consequently, the definition

of the