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

7.1.3 Pre- and Post-Conditions

Some operations state

pre-conditions

about their arguments or

post-conditions

about their results. It is the embed-

der’s responsibility to meet the pre-conditions. If it does, the post conditions are guaranteed by the semantics.
In addition to pre- and post-conditions explicitly stated with each operation, the specification adopts the following

conventions for

runtime objects

(

𝑠𝑡𝑜𝑟𝑒

moduleinst

externval

addresses

• Every runtime object passed as a parameter must be

valid

per an implicit pre-condition.

• Every runtime object returned as a result is

valid

per an implicit post-condition.

Note:

As long as an embedder treats runtime objects as abstract and only creates and manipulates them through

the interface defined here, all implicit pre-conditions are automatically met.

7.1.4 Store

store

init() :

store

1. Return the empty

store

store

init()

𝜖,

𝜖,

𝜖,

𝜖

}

7.1.5 Modules

module

decode(

byte

) :

module

error

1. If there exists a derivation for the

sequence

as a

according to the

, yielding a

𝑚

, then return

𝑚

2. Else, return

error

module

decode(

𝑏

)

𝑚

(

module

⇒

𝑚

𝑏

)

module

decode(

𝑏

)

error

(

otherwise

)

module

) :

1. If there exists a derivation for the

source

char

as a

module

according to the

text grammar for modules

yielding a

module

𝑚

, then return

𝑚

2. Else, return

error

module

parse(

𝑐

)

𝑚

(

module

⇒

𝑚

𝑐

)

module

parse(

𝑐

)

error

(

otherwise

)

184

Chapter 7. Appendix

module

1. If

, then return nothing.

2. Else, return

error

module

validate(

𝑚

)

𝜖

(

𝑚

′*

)

module

validate(

𝑚

)

error

(

otherwise

)

module

instantiate(

) : (

1. Try

with

as imports:

a. If it succeeds with a

module instance

moduleinst

, then let

result

moduleinst

b. Else, let

result

error

2. Return the new store paired with

result

module

instantiate(

𝑆, 𝑚,

)

(

𝑆

′

, 𝐹.

(

𝑆, 𝑚,

𝑆

′

;

𝐹

;

𝜖

)

module

instantiate(

𝑆, 𝑚,

)

(

𝑆

′

(

𝑆, 𝑚,

𝑆

′

;

𝐹

;

trap

)

Note:

The store may be modified even in case of an error.

module

imports(

) : (

1. Pre-condition:

with external import types

externtype

and external export types

externtype

′*

2. Let

be the

3. Assert: the length of

equals the length of

4. For each

and corresponding

, do:

a. Let

result

𝑖

be the triple

)

5. Return the concatenation of all

result

𝑖

, in index order.

6. Post-condition: each

externtype

𝑖

valid

module

imports(

𝑚

)

(

(

∧

𝑚

′*

)

module

exports(

) : (

1. Pre-condition:

with external import types

externtype

and external export types

externtype

′*

2. Let

be the

3. Assert: the length of

export

equals the length of

externtype

′*

4. For each

and corresponding

′*

, do:

a. Let

result

𝑖

be the pair

)

5. Return the concatenation of all

result

𝑖

, in index order.

6. Post-condition: each

7.1. Embedding

185

module

exports(

𝑚

)

(

name

externtype

′

)

(

∧

𝑚

′*

)

7.1.6 Module Instances

instance

export(

1. Assert: due to

of the

, all its

are different.

2. If there exists an

such that

equals

, then:

a. Return the

3. Else, return

instance

export(

𝑖

]

(

𝑖

]

name

)

instance

export(

(

otherwise

)

7.1.7 Functions

func

alloc(

) : (

1. Pre-condition:

𝑣𝑎𝑙𝑖𝑑 < 𝑣𝑎𝑙𝑖𝑑

−

𝑓 𝑢𝑛𝑐𝑡𝑦𝑝𝑒 >

2. Let

funcaddr

be the result of

allocating a host function

store

with

function type

functype

and host function

code

hostfunc

3. Return the new store paired with

funcaddr

func

alloc(

𝑆,

code

)

(

𝑆

′

)

(

allochostfunc

(

𝑆,

code

) =

𝑆

′

)

Note:

This operation assumes that

hostfunc

satisfies the

pre- and post-conditions

required for a function instance

with type

functype

Regular (non-host) function instances can only be created indirectly through

module instantiation

func

type(

1. Return

𝑆.

funcs

[

𝑎

]

type

2. Post-condition: the returned

function type

valid

func

type(

𝑆, 𝑎

)

𝑆.

funcs

[

𝑎

]

type

186

Chapter 7. Appendix

func

invoke(

) : (

1. Try

the function

with

as arguments:

a. If it succeeds with

values

val

′*

as results, then let

result

val

′*

b. Else it has trapped, hence let

result

error

2. Return the new store paired with

result

func

invoke(

𝑆, 𝑎, 𝑣

)

(

𝑆

′

, 𝑣

′*

)

(

𝑆, 𝑎, 𝑣

𝑆

′

;

𝐹

;

𝑣

′*

)

func

invoke(

𝑆, 𝑎, 𝑣

)

(

𝑆

′

(

𝑆, 𝑎, 𝑣

𝑆

′

;

𝐹

;

trap

)

Note:

The store may be modified even in case of an error.

7.1.8 Tables

table

alloc(

) : (

1. Pre-condition:

𝑣𝑎𝑙𝑖𝑑 < 𝑣𝑎𝑙𝑖𝑑

−

𝑡𝑎𝑏𝑙𝑒𝑡𝑦𝑝𝑒 >

2. Let

be the result of

with

and initialization value

ref

3. Return the new store paired with

tableaddr

table

alloc(

𝑆,

, 𝑟

)

(

𝑆

′

)

(

alloctable

(

𝑆,

, 𝑟

) =

𝑆

′

)

table

type(

1. Return

𝑆.

tables

[

𝑎

]

type

2. Post-condition: the returned

table type

𝑣𝑎𝑙𝑖𝑑 < 𝑣𝑎𝑙𝑖𝑑

−

𝑡𝑎𝑏𝑙𝑒𝑡𝑦𝑝𝑒 >

table

type(

𝑆, 𝑎

)

𝑆.

tables

[

𝑎

]

table

, 𝑖

1. Let

be the

2. If

𝑖

is larger than or equal to the length of

, then return

3. Else, return the

𝑖

]

table

read(

𝑆, 𝑎, 𝑖

)

𝑟

(

𝑆.

tables

[

𝑎

]

elem

[

𝑖

] =

𝑟

)

table

read(

𝑆, 𝑎, 𝑖

)

error

(

otherwise

)

table

, 𝑖

1. Let

be the

2. If

𝑖

is larger than or equal to the length of

, then return

3. Replace

𝑖

]

with the

reference value

ref

4. Return the updated store.

table

write(

𝑆, 𝑎, 𝑖, 𝑟

)

𝑆

′

(

𝑆

′

𝑎

]

elem

[

𝑖

] =

𝑟

)

table

write(

𝑆, 𝑎, 𝑖, 𝑟

)

error

(

otherwise

)

7.1. Embedding

187

table

1. Return the length of

table

size(

𝑆, 𝑎

)

𝑛

(

𝑆.

tables

[

𝑎

]

elem

𝑛

)

table

grow(

, 𝑛

1. Try

the

𝑛

elements with initialization value

ref

a. If it succeeds, return the updated store.

b. Else, return

error

table

grow(

𝑆, 𝑎, 𝑛, 𝑟

)

𝑆

′

(

𝑆

′

𝑎

] =

𝑆.

𝑎

]

, 𝑛, 𝑟

))

table

grow(

𝑆, 𝑎, 𝑛, 𝑟

)

error

(

otherwise

)

7.1.9 Memories

mem

alloc(

) : (

1. Pre-condition:

𝑣𝑎𝑙𝑖𝑑 < 𝑣𝑎𝑙𝑖𝑑

−

𝑚𝑒𝑚𝑡𝑦𝑝𝑒 >

2. Let

memaddr

be the result of

allocating a memory

store

with

memory type

memtype

3. Return the new store paired with

memaddr

mem

alloc(

𝑆,

)

(

𝑆

′

)

(

allocmem

(

𝑆,

) =

𝑆

′

)

mem

type(

1. Return

𝑆.

mems

[

𝑎

]

type

2. Post-condition: the returned

memory type

𝑣𝑎𝑙𝑖𝑑 < 𝑣𝑎𝑙𝑖𝑑

−

𝑚𝑒𝑚𝑡𝑦𝑝𝑒 >

mem

type(

𝑆, 𝑎

)

𝑆.

mems

[

𝑎

]

mem

, 𝑖

1. Let

be the

2. If

𝑖

is larger than or equal to the length of

, then return

3. Else, return the

𝑖

]

mem

read(

𝑆, 𝑎, 𝑖

)

𝑏

(

𝑆.

mems

[

𝑎

]

data

[

𝑖

] =

𝑏

)

mem

read(

𝑆, 𝑎, 𝑖

)

error

(

otherwise

)

188

Chapter 7. Appendix

mem

, 𝑖

1. Let

be the

2. If

is larger than or equal to the length of

, then return

3. Replace

𝑖

]

with

byte

4. Return the updated store.

mem

write(

𝑆, 𝑎, 𝑖, 𝑏

)

𝑆

′

(

𝑆

′

𝑎

]

data

[

𝑖

] =

𝑏

)

mem

write(

𝑆, 𝑎, 𝑖, 𝑏

)

error

(

otherwise

)

mem

1. Return the length of

divided by the

mem

size(

𝑆, 𝑎

)

𝑛

(

𝑆.

mems

[

𝑎

]

data

𝑛

64 Ki)

mem

grow(

, 𝑛

1. Try

the

𝑛

a. If it succeeds, return the updated store.

b. Else, return

error

mem

grow(

𝑆, 𝑎, 𝑛

)

𝑆

′

(

𝑆

′

𝑎

] =

𝑆.

𝑎

]

, 𝑛

))

mem

grow(

𝑆, 𝑎, 𝑛

)

error

(

otherwise

)

7.1.10 Globals

global

alloc(

) : (

1. Pre-condition:

𝑣𝑎𝑙𝑖𝑑 < 𝑣𝑎𝑙𝑖𝑑

−

𝑔𝑙𝑜𝑏𝑎𝑙𝑡𝑦𝑝𝑒 >

2. Let

globaladdr

be the result of

allocating a global

store

with

global type

globaltype

and initialization

value

val

3. Return the new store paired with

globaladdr

global

alloc(

𝑆,

, 𝑣

)

(

𝑆

′

)

(

allocglobal

(

𝑆,

, 𝑣

) =

𝑆

′

)

global

type(

1. Return

𝑆.

globals

[

𝑎

]

type

2. Post-condition: the returned

global type

𝑣𝑎𝑙𝑖𝑑 < 𝑣𝑎𝑙𝑖𝑑

−

𝑔𝑙𝑜𝑏𝑎𝑙𝑡𝑦𝑝𝑒 >

global

type(

𝑆, 𝑎

)

𝑆.

globals

[

𝑎

]

type

7.1. Embedding

189

global

1. Let

be the

2. Return the

global

read(

𝑆, 𝑎

)

𝑣

(

𝑆.

globals

[

𝑎

]

value

𝑣

)

global

1. Let

be the

2. Let

𝑡

be the structure of the

3. If

is not

, then return

4. Replace

with the

5. Return the updated store.

global

write(

𝑆, 𝑎, 𝑣

)

𝑆

′

(

𝑆.

globals

[

𝑎

]

type

var

𝑡

∧

𝑆

′

𝑎

]

value

𝑣

)

global

write(

𝑆, 𝑎, 𝑣

)

error

(

otherwise

)

7.2 Implementation Limitations

Implementations typically impose additional restrictions on a number of aspects of a WebAssembly module or

execution. These may stem from:

• physical resource limits,
• constraints imposed by the embedder or its environment,
• limitations of selected implementation strategies.

This section lists allowed limitations. Where restrictions take the form of numeric limits, no minimum requirements

are given, nor are the limits assumed to be concrete, fixed numbers. However, it is expected that all implementations

have “reasonably” large limits to enable common applications.

Note:

A conforming implementation is not allowed to leave out individual

features

. However, designated subsets

of WebAssembly may be specified in the future.

7.2.1 Syntactic Limits

Structure

An implementation may impose restrictions on the following dimensions of a module:

• the number of

in a

• the number of

in a

, including imports

• the number of

tables

in a

module

, including imports

• the number of

memories

in a

module

, including imports

• the number of

globals

in a

module

, including imports

• the number of

in a

• the number of

in a

190

Chapter 7. Appendix

• the number of

to a

• the number of

from a

• the number of parameters in a

function type

• the number of results in a

function type

• the number of parameters in a

block type

• the number of results in a

• the number of

in a

• the size of a

body

• the size of a

structured control instruction

• the number of

structured control instructions

in a

function

• the nesting depth of

structured control instructions

• the number of

label indices

in a

table

instruction

• the length of an

• the length of a

• the length of a

• the range of

in a

If the limits of an implementation are exceeded for a given module, then the implementation may reject the

vali-

dation

, compilation, or

instantiation

of that module with an embedder-specific error.

Note:

The last item allows

embedders

that operate in limited environments without support for

Unicode

to limit

the names of

imports

and

exports

to common subsets like

ASCII

Binary Format

For a module given in

binary format

, additional limitations may be imposed on the following dimensions:

• the size of a

module

• the size of any

section

• the size of an individual function’s

code

• the number of

sections

Text Format

For a module given in

text format

, additional limitations may be imposed on the following dimensions:

• the size of the

source text

• the size of any syntactic element
• the size of an individual

token

• the nesting depth of

folded instructions

• the length of symbolic

identifiers

• the range of literal

characters

allowed in the

source text

https://www.unicode.org/versions/latest/

https://webstore.ansi.org/RecordDetail.aspx?sku=INCITS+4-1986%5bR2012%5d

7.2. Implementation Limitations

191

7.2.2 Validation

An implementation may defer

validation

of individual

functions

until they are first

invoked

If a function turns out to be invalid, then the invocation, and every consecutive call to the same function, results in

trap

Note:

This is to allow implementations to use interpretation or just-in-time compilation for functions. The function

must still be fully validated before execution of its body begins.

7.2.3 Execution

Restrictions on the following dimensions may be imposed during

execution

of a WebAssembly program:

• the number of allocated

module instances

• the number of allocated

function instances

• the number of allocated

table instances

• the number of allocated

memory instances

• the number of allocated

• the size of a

• the size of a

• the number of

on the

• the number of

on the

• the number of

on the

If the runtime limits of an implementation are exceeded during execution of a computation, then it may terminate

that computation and report an embedder-specific error to the invoking code.
Some of the above limits may already be verified during instantiation, in which case an implementation may report

exceedance in the same manner as for

syntactic limits

Note:

Concrete limits are usually not fixed but may be dependent on specifics, interdependent, vary over time, or

depend on other implementation- or embedder-specific situations or events.

7.3 Validation Algorithm

The specification of WebAssembly

validation

is purely

declarative

. It describes the constraints that must be met

by a

module

instruction

sequence to be valid.

This section sketches the skeleton of a sound and complete

algorithm

for effectively validating code, i.e., sequences

instructions

. (Other aspects of validation are straightforward to implement.)

In fact, the algorithm is expressed over the flat sequence of opcodes as occurring in the

binary format

, and performs

only a single pass over it. Consequently, it can be integrated directly into a decoder.
The algorithm is expressed in typed pseudo code whose semantics is intended to be self-explanatory.

192

Chapter 7. Appendix

7.3.1 Data Structures

Types are representable as an enumeration.

type

val_type

= I32 | I64 | F32 | F64 | V128 | Funcref | Externref

func

is_num

(

: val_type | Unknown) : bool =

return

t = I32 || t = I64 || t = F32 || t = F64 || t = Unknown

func

is_vec

(

: val_type | Unknown) : bool =

return

t = V128 || t = Unknown

func

is_ref

(

: val_type | Unknown) : bool =

return

t = Funcref || t = Externref || t = Unknown

The algorithm uses two separate stacks: the

value stack

and the

control stack

. The former tracks the

types

operand values on the

stack

, the latter surrounding

structured control instructions

and their associated

blocks

type

val_stack

= stack(val_type | Unknown)

type

ctrl_stack

= stack(ctrl_frame)

type

ctrl_frame

= {

opcode

: opcode

start_types

: list(val_type)

end_types

: list(val_type)

height

: nat

unreachable

: bool

}

For each value, the value stack records its

value type

, or

Unknown

when the type is not known.

For each entered block, the control stack records a

control frame

with the originating opcode, the types on the top

of the operand stack at the start and end of the block (used to check its result as well as branches), the height of

the operand stack at the start of the block (used to check that operands do not underflow the current block), and a

flag recording whether the remainder of the block is unreachable (used to handle

stack-polymorphic

typing after

branches).
For the purpose of presenting the algorithm, the operand and control stacks are simply maintained as global vari-

ables:

var

vals

: val_stack

var

ctrls

: ctrl_stack

However, these variables are not manipulated directly by the main checking function, but through a set of auxiliary

functions:

func

push_val

(

type

: val_type | Unknown) =

vals.push(type)

func

pop_val

() : val_type | Unknown =

(vals.size() = ctrls[0].height && ctrls[0].unreachable)

return

Unknown

error_if(vals.size() = ctrls[0].height)

return

vals.pop()

func

pop_val

(

expect

: val_type | Unknown) : val_type | Unknown =

let

actual

= pop_val()

error_if(actual =/= expect && actual =/= Unknown && expect =/= Unknown)

return

actual

(continues on next page)

7.3. Validation Algorithm

193

(continued from previous page)

func

push_vals

(

types

: list(val_type)) =

foreach

types) push_val(t)

func

pop_vals

(

types

: list(val_type)) : list(val_type) =

var

popped

:= []

foreach

reverse(types)) popped.prepend(pop_val(t))

return

popped

Pushing an operand value simply pushes the respective type to the value stack.
Popping an operand value checks that the value stack does not underflow the current block and then removes

one type. But first, a special case is handled where the block contains no known values, but has been marked as

unreachable. That can occur after an unconditional branch, when the stack is typed

polymorphically

. In that case,

an unknown type is returned.
A second function for popping an operand value takes an expected type, which the actual operand type is checked

against. The types may differ in case one of them is Unknown. The function returns the actual type popped from

the stack.
Finally, there are accumulative functions for pushing or popping multiple operand types.

Note:

The notation

stack[i]

is meant to index the stack from the top, so that, e.g.,

ctrls[0]

accesses the

element pushed last.

The control stack is likewise manipulated through auxiliary functions:

func

push_ctrl

(

opcode

: opcode,

: list(val_type),

out

: list(val_type)) =

let

frame

= ctrl_frame(opcode,

, out, vals.size(), false)

ctrls.push(frame)
push_vals(

)

func

pop_ctrl

() : ctrl_frame =

error_if(ctrls.is_empty())

let

frame

= ctrls[0]

pop_vals(frame.end_types)
error_if(vals.size() =/= frame.height)
ctrls.pop()

return

frame

func

label_types

(

frame

: ctrl_frame) : list(val_types) =

return

(if frame.opcode == loop then frame.start_types else frame.end_types)

func

unreachable

() =

vals.resize(ctrls[0].height)
ctrls[0].unreachable := true

Pushing a control frame takes the types of the label and result values. It allocates a new frame record recording

them along with the current height of the operand stack and marks the block as reachable.
Popping a frame first checks that the control stack is not empty. It then verifies that the operand stack contains the

right types of values expected at the end of the exited block and pops them off the operand stack. Afterwards, it

checks that the stack has shrunk back to its initial height.
The type of the

label

associated with a control frame is either that of the stack at the start or the end of the frame,

determined by the opcode that it originates from.
Finally, the current frame can be marked as unreachable. In that case, all existing operand types are purged from

the value stack, in order to allow for the

stack-polymorphism

logic in

pop_val

to take effect.

Note:

Even with the unreachable flag set, consecutive operands are still pushed to and popped from the operand

stack. That is necessary to detect invalid

. However, a polymorphic

194

Chapter 7. Appendix

(continued from previous page)

case

(else)

let

frame

= pop_ctrl()

error_if(frame.opcode =/=

)

push_ctrl(else, frame.start_types, frame.end_types)

case

(br n)

error_if(ctrls.size() < n)
pop_vals(label_types(ctrls[n]))
unreachable()

case

(br_if n)

error_if(ctrls.size() < n)
pop_val(I32)
pop_vals(label_types(ctrls[n]))
push_vals(label_types(ctrls[n]))

case

(br_table n* m)

pop_val(I32)
error_if(ctrls.size() < m)

let

arity

= label_types(ctrls[m]).size()

foreach

n*)

error_if(ctrls.size() < n)
error_if(label_types(ctrls[n]).size() =/= arity)
push_vals(pop_vals(label_types(ctrls[n])))

pop_vals(label_types(ctrls[m]))
unreachable()

Note:

It is an invariant under the current WebAssembly instruction set that an operand of

Unknown

type is never

duplicated on the stack. This would change if the language were extended with stack instructions like

dup

. Under

such an extension, the above algorithm would need to be refined by replacing the

Unknown

type with proper

type

variables

to ensure that all uses are consistent.

7.4 Custom Sections

This appendix defines dedicated

custom sections

for WebAssembly’s

binary format

. Such sections do not con-

tribute to, or otherwise affect, the WebAssembly semantics, and like any custom section they may be ignored by

an implementation. However, they provide useful meta data that implementations can make use of to improve user

experience or take compilation hints.
Currently, only one dedicated custom section is defined, the

name section

7.4.1 Name Section

The

name section

is a

custom section

whose name string is itself ‘

name

’. The name section should appear only

once in a module, and only after the

data section

The purpose of this section is to attach printable names to definitions in a module, which e.g. can be used by a

debugger or when parts of the module are to be rendered in

text form

Note:

All

names

are represented in

Unicode

encoded in UTF-8. Names need not be unique.

https://www.unicode.org/versions/latest/

196

Chapter 7. Appendix

Memory

Instance

meminst

• The

memory type

meminst

type

must remain unchanged.

• The length of

meminst

data

must not shrink.

𝑛

≤

𝑛

𝑏

𝑛

𝑏

𝑛

}

Global Instance

• The

must remain unchanged.

• Let

mut

𝑡

be the structure of

• If

, then the

must remain unchanged.

𝑡

)

𝑡

)

value

val

}

Element Instance

eleminst

• The vector

eleminst

elem

must either remain unchanged or shrink to length

∨

𝜖

}

Data Instance

datainst

• The vector

datainst

data

must either remain unchanged or shrink to length

𝑏

∨

𝑏

𝜖

𝑏

𝑏

}

7.5.6 Theorems

Given the definition of

valid configurations

, the standard soundness theorems hold.

Theorem (Preservation).

If a

configuration

𝑆

;

𝑇

valid

with

result type

[

𝑡

]

(i.e.,

⊢

𝑆

;

𝑇

: [

𝑡

]

), and steps to

𝑆

′

;

𝑇

′

(i.e.,

𝑆

;

𝑇

→

𝑆

′

;

𝑇

′

), then

𝑆

′

;

𝑇

′

is a valid configuration with the same result type (i.e.,

⊢

𝑆

′

;

𝑇

′

: [

𝑡

]

Furthermore,

𝑆

′

is an

extension

𝑆

(i.e.,

⊢

𝑆

⪯

𝑆

′

terminal

thread

is one whose sequence of

instructions

is a

result

. A terminal configuration is a configuration

whose thread is terminal.

Theorem (Progress).

If a

configuration

𝑆

;

𝑇

valid

(i.e.,

⊢

𝑆

;

𝑇

: [

𝑡

]

for some

result type

[

𝑡

]

), then either it is

terminal, or it can step to some configuration

𝑆

′

;

𝑇

′

(i.e.,

𝑆

;

𝑇

→

𝑆

′

;

𝑇

′

From Preservation and Progress the soundness of the WebAssembly type system follows directly.

Corollary (Soundness).

If a

configuration

𝑆

;

𝑇

valid

(i.e.,

⊢

𝑆

;

𝑇

: [

𝑡

]

for some

result type

[

𝑡

]

), then it either

diverges or takes a finite number of steps to reach a terminal configuration

𝑆

′

;

𝑇

′

(i.e.,

𝑆

;

𝑇

→

𝑆

′

;

𝑇

′

) that is

valid with the same result type (i.e.,

⊢

𝑆

′

;

𝑇

′

: [

𝑡

]

) and where

𝑆

′

is an

extension

𝑆

(i.e.,

⊢

𝑆

⪯

𝑆

′

A machine-verified version of the formalization and soundness proof is described in the following article: Conrad Watt.

Mechanising

and Verifying the WebAssembly Specification

. Proceedings of the 7th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP

2018). ACM 2018.

https://dl.acm.org/citation.cfm?id=3167082

In other words, every thread in a valid configuration either runs forever, traps, or terminates with a result that has

the expected type. Consequently, given a

valid store

, no computation defined by

instantiation

invocation

of a

valid module can “crash” or otherwise (mis)behave in ways not covered by the

execution

semantics given in this

specification.

7.6 Change History

Since the original release 1.0 of the WebAssembly specification, a number of proposals for extensions have been

integrated. The following sections provide an overview of what has changed.

7.6.1 Release 1.1

Sign extension instructions

Added new numeric instructions for performing sign extension within integer representations

• New

numeric instructions

extend

Non-trapping float-to-int conversions

Added new conversion instructions that avoid trapping when converting a floating-point number to an integer

• New

numeric instructions

trunc

sat

Multiple values

Generalized the result type of blocks and functions to allow for multiple values; in addition, introduced the ability

to have block parameters

•

Function types

allow more than one result

•

Block types

can be arbitrary function types

Reference types

Added

funcref

and

externref

as new value types and respective instructions

• New

and

• New

reference instructions

• Enrich

parametric instruction

select

with optional type immediate

• New

declarative

form of

element segment

https://github.com/WebAssembly/spec/tree/main/proposals/sign-extension-ops/

https://github.com/WebAssembly/spec/tree/main/proposals/nontrapping-float-to-int-conversion/

https://github.com/WebAssembly/spec/tree/main/proposals/multi-value/

https://github.com/WebAssembly/spec/tree/main/proposals/reference-types/

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