WebAssembly Specification Core

https://webassembly.github.io/spec/core
Admin
The official specification for the core WebAssembly binary instruction format, covering structure,...
Tokens:129,765
Snippets:805
Trust Score:8.3
Update:1 year ago
Show doc for...
Tokens:
Raw
### WebAssembly Start Function Definition

Source: https://webassembly.github.io/spec/core/text/modules

Specifies the syntax for defining a start function in WebAssembly, which is identified by its function index. It notes that only one start function can exist per module.

```WebAssembly
startI::= (start x:funcidxI) ⇒ {funcx}
```

--------------------------------

### WebAssembly Table Instructions

Source: https://webassembly.github.io/spec/core/syntax/instructions

Instructions for interacting with tables, including getting, setting, resizing, filling, copying, and initializing elements. Also covers dropping passive element segments.

```WebAssembly
table.get <tableidx>
table.set <tableidx>
table.size <tableidx>
table.grow <tableidx>
table.fill <tableidx>
table.copy <tableidx> <tableidx>
table.init <tableidx> <elemidx>
elem.drop <elemidx>
```

--------------------------------

### WebAssembly Variable Instructions

Source: https://webassembly.github.io/spec/core/syntax/instructions

Instructions for accessing and modifying local or global variables. Includes get, set, and tee operations for local variables, and get and set for global variables.

```WebAssembly
local.get <localidx>
local.set <localidx>
local.tee <localidx>
global.get <globalidx>
global.set <globalidx>
```

--------------------------------

### WebAssembly Example Reduction Sequence

Source: https://webassembly.github.io/spec/core/exec/runtime

Demonstrates a specific reduction scenario for a sequence of floating-point instructions using evaluation contexts. It highlights how the context is uniquely determined for applying reduction rules.

```WebAssembly
(f64.constx1)(f64.constx2)f64.neg(f64.constx3)f64.addf64.mul
```

--------------------------------

### WebAssembly Start Section

Source: https://webassembly.github.io/spec/core/binary/modules

Defines the start section (ID 8) in WebAssembly. This section decodes into an optional start function, specified by its function index, which is executed when the module is instantiated.

```WebAssembly
startsec::=st?:section8(start)⇒st?
start::=x:funcidx⇒{funcx}
```

--------------------------------

### WebAssembly f64 Arithmetic Reduction Sequence

Source: https://webassembly.github.io/spec/core/exec/conventions

Provides an example of a multi-step reduction sequence for a WebAssembly instruction stream involving f64 constants, negation, and addition. It shows the transformation of the configuration over three execution steps.

```WebAssembly
(f64.constx1)(f64.constx2)f64.neg(f64.constx3)f64.addf64.mul↪(f64.constx1)(f64.constx4)(f64.constx3)f64.addf64.mul↪(f64.constx1)(f64.constx5)f64.mul↪(f64.constx6)
```

--------------------------------

### WebAssembly Instruction Folding Example

Source: https://webassembly.github.io/spec/core/text/instructions

Demonstrates how a sequence of WebAssembly instructions can be folded into a nested S-expression format for improved readability.

```plaintext
Original: (local.get$x)(i32.const2)i32.add(i32.const3)i32.mul
Folded: (i32.mul(i32.add(local.get$x)(i32.const2))(i32.const3))
```

--------------------------------

### WebAssembly Branch Reduction Example

Source: https://webassembly.github.io/spec/core/exec/runtime

Illustrates the reduction of a simple branch instruction within a block context. It shows how a branch instruction replaces the targeted label and its associated instruction sequence with the label's continuation.

```WebAssembly
label0{instr∗}Bl[brl]end↪instr∗
```

--------------------------------

### WebAssembly Start Function Declaration

Source: https://webassembly.github.io/spec/core/syntax/modules

Declares a start function in WebAssembly that is automatically invoked after tables and memories are initialized during module instantiation. This function is intended for module state initialization.

```WebAssembly
start::={funcfuncidx}
```

--------------------------------

### WebAssembly Variable Access Instructions

Source: https://webassembly.github.io/spec/core/appendix/index-instructions

Documentation for WebAssembly variable access instructions: local.get_x, local.set_x, local.tee_x, global.get_x, global.set_x. These instructions are used to get and set local and global variables.

```WebAssembly
local.getx | 0x20 | []→[t] | validation | execution
local.setx | 0x21 | [t]→[] | validation | execution
local.teex | 0x22 | [t]→[t] | validation | execution
global.getx | 0x23 | []→[t] | validation | execution
global.setx | 0x24 | [t]→[] | validation | execution
```

--------------------------------

### WebAssembly Memory Management Instructions

Source: https://webassembly.github.io/spec/core/syntax/instructions

Instructions for managing linear memory, including getting size, growing memory, filling regions, copying data, initializing from segments, and dropping data segments.

```WebAssembly
memory.size
memory.grow
memory.fill
memory.copy
memory.init <dataidx>
data.drop <dataidx>
```

--------------------------------

### WebAssembly Table Get Instruction

Source: https://webassembly.github.io/spec/core/text/instructions

Represents the 'table.get' instruction in WebAssembly, which retrieves an element from a table by its index.

```WebAssembly
‘table.get’x:tableidxI⇒table.getx
```

--------------------------------

### WebAssembly Memory Management Instructions

Source: https://webassembly.github.io/spec/core/text/instructions

Instructions for managing WebAssembly memory, including getting the current size, growing the memory, filling memory regions, copying between regions, and initializing memory from data segments.

```WebAssembly
memory.size
memory.grow
memory.fill
memory.copy
memory.init
data.drop
```

--------------------------------

### WebAssembly Reference Instructions

Source: https://webassembly.github.io/spec/core/syntax/instructions

This section details WebAssembly instructions for managing references, including creating null references, checking for null values, and obtaining references to functions.

```WebAssembly
instr::=…|ref.nullreftype|ref.is_null|ref.funcfuncidx
```

--------------------------------

### WebAssembly Table Access Instructions

Source: https://webassembly.github.io/spec/core/appendix/index-instructions

Documentation for WebAssembly table access instructions: table.get_x and table.set_x. These instructions interact with the WebAssembly table.

```WebAssembly
table.getx | 0x25 | [i32]→[t] | validation | execution
table.setx | 0x26 | [i32t]→[] | validation | execution
```

--------------------------------

### WebAssembly Start Function Validation

Source: https://webassembly.github.io/spec/core/valid/modules

Validates a start function declaration, ensuring the specified function exists and has a type of []→[].

```WebAssembly
C.funcs[x]=[]→[]
C ⊢ {funcx} ok
```

--------------------------------

### WebAssembly Instantiation Process

Source: https://webassembly.github.io/spec/core/exec/modules

Describes the step-by-step process of instantiating a WebAssembly module, including validation, import matching, and initialization of memory and tables.

```WebAssembly
instantiate(S,module,externvalk)=S′;
F;runelem0(elemn[0])…runelemn−1(elemn[n−1])
rundata0(datam[0])…rundatam−1(datam[m−1])
(callstart.func)?
(if⊢module:externtypeimk→externtypeex∗ ∧
(S⊢externval:externtype)k ∧
(⊢externtype≤externtypeim)k ∧
module.globals=global∗ ∧
module.elems=elemn ∧
module.datas=datam ∧
module.start=start? ∧
(exprg=global.init)∗ ∧
(expre∗=elem.init)n ∧
S′,moduleinst=allocmodule(S,module,externvalk,val∗,(ref∗)n) ∧
F={modulemoduleinst,localsϵ} ∧
(S′;F;exprg↪∗S′;F;valend)∗ ∧
((S′;F;expre↪∗S′;F;refend)∗)n)
```

--------------------------------

### WebAssembly t2.cvtop_t1_sx? Instruction

Source: https://webassembly.github.io/spec/core/exec/instructions

Explains the t2.cvtop_t1_sx? instruction for type conversion. It covers stack assertions, popping a value, performing the conversion, and pushing the result or trapping.

```WebAssembly
t2.cvtop_t1_sx?
1. Assert: due to validation, a value of value type t1 is on the top of the stack.
2. Pop the value t1.constc1 from the stack.
3. If cvtopt1,t2sx?(c1) is defined:
    1. Let c2 be a possible result of computing cvtopt1,t2sx?(c1).
    2. Push the value t2.constc2 to the stack.
4. Else:
    1. Trap.

(t1.constc1)t2.cvtop_t1_sx?↪(t2.constc2)(ifc2∈cvtopt1,t2sx?(c1))
(t1.constc1)t2.cvtop_t1_sx?↪trap(ifcvtopt1,t2sx?(c1)={})
```

--------------------------------

### WebAssembly Global Get Instruction

Source: https://webassembly.github.io/spec/core/text/instructions

Represents the 'global.get' instruction in WebAssembly, which retrieves the value of a global variable by its index.

```WebAssembly
‘global.get’x:globalidxI⇒global.getx
```

--------------------------------

### WebAssembly Control Instructions Overview

Source: https://webassembly.github.io/spec/core/syntax/instructions

This snippet outlines the grammar for WebAssembly control instructions, including structured instructions and branching.

```WebAssembly
blocktype::=typeidx|valtype?
instr::=…|nop|unreachable|block blocktype instr* end|loop blocktype instr* end|if blocktype instr* else instr* end|br labelidx|br_if labelidx|br_table vec(labelidx) labelidx|return|call funcidx|call_indirect tableidx typeidx
```

--------------------------------

### WebAssembly Local Get Instruction

Source: https://webassembly.github.io/spec/core/text/instructions

Represents the 'local.get' instruction in WebAssembly, which retrieves the value of a local variable by its index.

```WebAssembly
‘local.get’x:localidxI⇒local.getx
```

--------------------------------

### WebAssembly i32.load Instructions

Source: https://webassembly.github.io/spec/core/text/instructions

Loads a 32-bit integer from memory. Supports signed and unsigned variants, with different byte alignments.

```WebAssembly
i32.load
i32.load8_s
i32.load8_u
i32.load16_s
i32.load16_u
```

--------------------------------

### WebAssembly Unary fabs Operator on Sequences

Source: https://webassembly.github.io/spec/core/exec/numerics

Shows an example of the unary fabs operator applied to a sequence of floating-point values, returning a sequence of floating-point results.

```WebAssembly
fabsN(zn)=fabsN(z[0])…fabsN(z[n])
```

--------------------------------

### WebAssembly Type Conversion and Promotion Instructions

Source: https://webassembly.github.io/spec/core/binary/instructions

This snippet includes WebAssembly instructions for converting between integer and floating-point types, as well as promoting and demoting floating-point values between different vector sizes. It covers saturating conversions and zero-extension.

```WebAssembly
0xFD248:u32⇒i32x4.trunc_sat_f32x4_s
0xFD249:u32⇒i32x4.trunc_sat_f32x4_u
0xFD250:u32⇒f32x4.convert_i32x4_s
0xFD251:u32⇒f32x4.convert_i32x4_u
0xFD252:u32⇒i32x4.trunc_sat_f64x2_s_zero
0xFD253:u32⇒i32x4.trunc_sat_f64x2_u_zero
0xFD254:u32⇒f64x2.convert_low_i32x4_s
0xFD255:u32⇒f64x2.convert_low_i32x4_u
0xFD94:u32⇒f32x4.demote_f64x2_zero
0xFD95:u32⇒f64x2.promote_low_f32x4
```

--------------------------------

### WebAssembly Numeric Instructions Overview

Source: https://webassembly.github.io/spec/core/syntax/instructions

Provides a grammar overview for WebAssembly numeric instructions, categorizing them by operation type and operand type. It includes shorthands for unary, binary, test, relation, and conversion operations.

```WebAssembly
nn,mm::=32|64
sx::=u|s
inst::=
inn.const
un
n|fnn.const
fnn|
inn.iunop|
fnn.funop|
inn.ibinop|
fnn.fbinop|
inn.itestop|
inn.irelop|
fnn.frelop|
inn.extend8_s|
inn.extend16_s|
i64.extend32_s|
i32.wrap_i64|
i64.extend_i32_sx|
inn.trunc_fmm_sx|
inn.trunc_sat_fmm_sx|
f32.demote_f64|
f64.promote_f32|
fnn.convert_imm_sx|
inn.reinterpret_fnn|
fnn.reinterpret_inn|
…
iunop::=clz|ctz|popcnt
ibinop::=add|sub|mul|div_sx|rem_sx|and|or|xor|shl|shr_sx|rotl|rotr
funop::=abs|neg|sqrt|ceil|floor|trunc|nearest
fbinop::=add|sub|mul|div|min|max|copysign
itestop::=eqz
irelop::=eq|ne|lt_sx|gt_sx|le_sx|ge_sx
frelop::=eq|ne|lt|gt|le|ge
```

--------------------------------

### WebAssembly Binary iadd Operator on Sequences

Source: https://webassembly.github.io/spec/core/exec/numerics

Provides an example of the binary iadd operator applied to two sequences of integers of the same length, returning a sequence of integer results.

```WebAssembly
iaddN(i1n,i2n)=iaddN(i1[0],i2[0])…iaddN(i1[n],i2[n])
```

--------------------------------

### WebAssembly f64 Comparison Operations

Source: https://webassembly.github.io/spec/core/text/instructions

Provides instructions for comparison operations on 64-bit floats, including equality, inequality, less than, greater than, less than or equal to, and greater than or equal to.

```WebAssembly
f64.eq
f64.ne
f64.lt
f64.gt
f64.le
f64.ge
```

--------------------------------

### WebAssembly Text Format: Number Type Grammar

Source: https://webassembly.github.io/spec/core/text/conventions

Example of a textual grammar rule for number types in WebAssembly, mapping string literals to abstract syntax types.

```Text
numtype::=‘i32’⇒i32|‘i64’⇒i64|‘f32’⇒f32|‘f64’⇒f64
```

--------------------------------

### WebAssembly f64x2 Maximum Operation

Source: https://webassembly.github.io/spec/core/appendix/index-instructions

No description

--------------------------------

### WebAssembly Name and Identifier Syntax

Source: https://webassembly.github.io/spec/core/text/values

Specifies the syntax for names and identifiers in WebAssembly. Names are UTF-8 strings, while identifiers are symbolic names starting with '$' followed by specific printable ASCII characters.

```WebAssembly
name::=b∗:string⇒c∗(ifb∗=utf8(c∗))
id::=‘$’idchar+
idchar::=‘0’|…|‘9’|‘A’|…|‘Z’|‘a’|…|‘z’|‘!’|‘#’|‘$’|‘%’|‘&’|‘’’|‘*’|‘+’|‘−’|‘.’|‘/’|‘:’|‘<’|‘=’|‘>’|‘?’|‘@’|‘\’|‘^’|‘_’|‘`’|‘|’|‘~’
```

--------------------------------

### WebAssembly i64 Comparison Operations

Source: https://webassembly.github.io/spec/core/text/instructions

Provides instructions for comparison operations on 64-bit integers, including equality, inequality, less than (signed and unsigned), greater than (signed and unsigned), less than or equal to (signed and unsigned), and greater than or equal to (signed and unsigned).

```WebAssembly
i64.eqz
i64.eq
i64.ne
i64.lt_s
i64.lt_u
i64.gt_s
i64.gt_u
i64.le_s
i64.le_u
i64.ge_s
i64.ge_u
```

--------------------------------

### WebAssembly Local Get Instruction (local.getx)

Source: https://webassembly.github.io/spec/core/exec/instructions

Retrieves the value of a local variable at a given index and pushes it onto the stack. It requires the local variable to exist within the current frame.

```wasm
F;(local.getx)↪F;val(ifF.locals[x]=val)
```

--------------------------------

### WebAssembly i64 Extension Instructions

Source: https://webassembly.github.io/spec/core/binary/instructions

Extends 64-bit integers with sign extension for smaller bit widths. These are plain opcodes without immediate values.

```WebAssembly
0xC2⇒i64.extend8_s
0xC3⇒i64.extend16_s
0xC4⇒i64.extend32_s
```

--------------------------------

### WebAssembly SIMD Vector Reduction Operations

Source: https://webassembly.github.io/spec/core/appendix/index-instructions

Includes operations that reduce a vector to a single scalar value. Examples are `any_true` for checking if any element is true and `all_true` for checking if all elements are true.

```Wasm
v128.any_true | 0xFD0x53 | [v128]→[i32]
i8x16.all_true | 0xFD0x63 | [v128]→[i32]
```

--------------------------------

### WebAssembly Integer Conversions

Source: https://webassembly.github.io/spec/core/text/instructions

Includes instructions for converting between integer types, truncating floats to integers (signed and unsigned, with and without saturation), extending integers, and converting integers to floats.

```WebAssembly
i32.wrap_i64
i32.trunc_f32_s
i32.trunc_f32_u
i32.trunc_f64_s
i32.trunc_f64_u
i32.trunc_sat_f32_s
i32.trunc_sat_f32_u
i32.trunc_sat_f64_s
i32.trunc_sat_f64_u
i64.extend_i32_s
i64.extend_i32_u
i64.trunc_f32_s
i64.trunc_f32_u
i64.trunc_f64_s
i64.trunc_f64_u
i64.trunc_sat_f32_s
i64.trunc_sat_f32_u
i64.trunc_sat_f64_s
i64.trunc_sat_f64_u
f32.convert_i32_s
f32.convert_i32_u
f32.convert_i64_s
f32.convert_i64_u
f64.convert_i32_s
f64.convert_i32_u
f64.convert_i64_s
f64.convert_i64_u
```

--------------------------------

### WebAssembly Text Format - Comment Definition

Source: https://webassembly.github.io/spec/core/text/lexical

Details the two types of comments allowed: line comments starting with ';;' and block comments enclosed in '(;' and ';)'. Block comments support nesting.

```WebAssembly Text Format
comment::=linecomment|blockcomment
linecomment::=‘;;’linechar*(newline|eof)
linechar::=c:char(ifc≠U+0A∧c≠U+0D)
blockcomment::=‘(;’blockchar*(‘;)’)
blockchar::=c:char(ifc≠‘;’∧c≠‘(’)|‘;’(ifthe next character is not‘)’)|‘(’(ifthe next character is not‘;’)|blockcomment
```

--------------------------------

### WebAssembly Floating-Point Conversions

Source: https://webassembly.github.io/spec/core/text/instructions

Includes instructions for converting between floating-point types, such as demoting f64 to f32 and promoting f32 to f64.

```WebAssembly
f32.demote_f64
f64.promote_f32
```

--------------------------------

### WebAssembly i64.load Instructions

Source: https://webassembly.github.io/spec/core/text/instructions

Loads a 64-bit integer from memory. Supports signed and unsigned variants for 8, 16, and 32-bit accesses, with different byte alignments.

```WebAssembly
i64.load
i64.load8_s
i64.load8_u
i64.load16_s
i64.load16_u
i64.load32_s
i64.load32_u
```

--------------------------------

### Get WebAssembly Module Imports

Source: https://webassembly.github.io/spec/core/appendix/embedding

Retrieves the imports of a WebAssembly module. This function returns a list of triples, each containing the module name, import name, and the external type of the import. It requires the module to be valid.

```WebAssembly
module_imports(module):(name,name,externtype)∗
module_imports(m)=(im.module,im.name,externtype)∗(ifim∗=m.imports∧⊢m:externtype∗→externtype′∗)
```

--------------------------------

### WebAssembly Reduction Rules with Evaluation Contexts

Source: https://webassembly.github.io/spec/core/exec/runtime

Details the reduction rules for WebAssembly, showing how computation progresses within evaluation contexts. This includes rules for instruction sequences and handling traps.

```WebAssembly
S;F;E[instr∗]↪S′;F′;E[instr′∗](ifS;F;instr∗↪S′;F′;instr′∗)
S;F;framen{F′}instr∗end↪S′;F;framen{F″}instr′∗end(ifS;F′;instr∗↪S′;F″;instr′∗)
S;F;E[trap]↪S;F;trap(ifE≠[_])
S;F;framen{F′}trapend↪S;F;trap
```

--------------------------------

### WebAssembly Reference Instructions Encoding

Source: https://webassembly.github.io/spec/core/binary/instructions

Details the single-byte opcode encoding for reference instructions, such as `ref.null` and `ref.is_null`, and `ref.func`.

```WebAssembly
instr::=…|0xD0t:reftype⇒ref.nullt|0xD1⇒ref.is_null|0xD2x:funcidx⇒ref.funcx
```

--------------------------------

### WebAssembly Structured Instructions: Block, Loop, If

Source: https://webassembly.github.io/spec/core/syntax/instructions

Explains the structured control flow instructions: block, loop, and if. These instructions bracket nested sequences of instructions and manage operand stack based on block types.

```WebAssembly
block blocktype instr* end
loop blocktype instr* end
if blocktype instr* else instr* end
```

--------------------------------

### WebAssembly Module Preamble and Structure

Source: https://webassembly.github.io/spec/core/binary/modules

Defines the magic number and version for WebAssembly binary modules, followed by the sequence of sections. It also details the structure of a module, including types, functions, tables, memories, globals, exports, start, elements, and data.

```WebAssembly
magic::=0x000x610x730x6D
version::=0x010x000x000x00
module::=magicversioncustomsec*functype*:typesec customsec*import*:importsec customsec*typeidx n:funcsec customsec*table*:tablesec customsec*mem*:memsec customsec*global*:globalsec customsec*export*:exportsec customsec*start?:startsec customsec*elem*:elemsec customsec*m?:datacountsec customsec*code n:codec customsec*data m:datasec* => {types type*, funcs func n, tables table*, mems mem*, globals global*, elem elem*, datas data m, start start?, imports import*, exports export*}
(if m? != ε ∨ dataidx(code n) = ∅)
where for each ti*, ei in code n,
func n[i] = {type typeidx n[i], locals ti*, body ei}
```

--------------------------------

### WebAssembly i64 Constants

Source: https://webassembly.github.io/spec/core/text/instructions

Defines the instruction for pushing a 64-bit integer constant onto the stack.

```WebAssembly
i64.const n:i64
```

--------------------------------

### WebAssembly Module Validation Rule

Source: https://webassembly.github.io/spec/core/valid/modules

Presents the formal validation rule for a WebAssembly module, denoted by ⊢module: it∗→et∗. This rule encompasses the validation of types, functions, tables, memories, globals, elements, data segments, start function, imports, and exports, subject to context constraints and type compatibility.

```WebAssembly
(⊢typeok)∗(C⊢func:ft)∗(C′⊢table:tt)∗(C′⊢mem:mt)∗(C′⊢global:gt)∗(C′⊢elem:rt)∗(C′⊢dataok)n(C⊢startok)?(C⊢import:it)∗(C⊢export:et)∗ift∗=funcs(it∗)itt∗=tables(it∗)imt∗=mems(it∗)igt∗=globals(it∗)x∗=funcidx(modulewithfuncs=ϵwithstart=ϵ)C={typestype∗,funcsift∗ft∗,tablesitt∗tt∗,memsimt∗mt∗,globalsigt∗gt∗,elemsrt∗,datasokn,refsx∗}C′=Cwithglobals=igt∗|C.mems|≤1(export.name)∗disjointmodule={typestype∗,funcsfunc∗,tablestable∗,memsmem∗,globalsglobal∗,elemselem∗,datasdatan,startstart?,importsimport∗,exportsexport∗}⊢module:it∗→et∗
```

--------------------------------

### WebAssembly Constant Instructions

Source: https://webassembly.github.io/spec/core/appendix/index-instructions

Documentation for WebAssembly constant instructions: i32.const, i64.const, f32.const, f64.const. These instructions push constant values onto the stack.

```WebAssembly
i32.consti32 | 0x41 | []→[i32] | validation | execution
i64.consti64 | 0x42 | []→[i64] | validation | execution
f32.constf32 | 0x43 | []→[f32] | validation | execution
f64.constf64 | 0x44 | []→[f64] | validation | execution
```

--------------------------------

### WebAssembly Static Constructs Typing Rules

Source: https://webassembly.github.io/spec/core/appendix/index-rules

This section outlines the typing rules for static constructs in WebAssembly, defining the judgements for limits, function types, block types, table types, memory types, global types, external types, instructions, instruction sequences, expressions, functions, tables, memories, globals, element segments, element modes, data segments, data modes, start functions, exports, export descriptions, imports, import descriptions, and modules.

```WebAssembly
Construct | Judgement
---
Limits | ⊢limits:k
Function type | ⊢functypeok
Block type | ⊢blocktypeok
Table type | ⊢tabletypeok
Memory type | ⊢memtypeok
Global type | ⊢globaltypeok
External type | ⊢externtypeok
Instruction | S;C⊢instr:stacktype
Instruction sequence | S;C⊢instr∗:stacktype
Expression | C⊢expr:resulttype
Function | C⊢func:functype
Table | C⊢table:tabletype
Memory | C⊢mem:memtype
Global | C⊢global:globaltype
Element segment | C⊢elem:reftype
Element mode | C⊢elemmode:reftype
Data segment | C⊢dataok
Data mode | C⊢datamodeok
Start function | C⊢startok
Export | C⊢export:externtype
Export description | C⊢exportdesc:externtype
Import | C⊢import:externtype
Import description | C⊢importdesc:externtype
Module | ⊢module:externtype∗→externtype∗
```

--------------------------------

### WebAssembly f64 Constants

Source: https://webassembly.github.io/spec/core/text/instructions

Defines the instruction for pushing a 64-bit floating-point constant onto the stack.

```WebAssembly
f64.const z:f64
```

--------------------------------

### WebAssembly f64.load Instructions

Source: https://webassembly.github.io/spec/core/text/instructions

Loads a 64-bit floating-point number from memory.

```WebAssembly
f64.load
```

--------------------------------

### WebAssembly i32 Comparison Operations

Source: https://webassembly.github.io/spec/core/text/instructions

Provides instructions for comparison operations on 32-bit integers, including equality, inequality, less than (signed and unsigned), greater than (signed and unsigned), less than or equal to (signed and unsigned), and greater than or equal to (signed and unsigned).

```WebAssembly
i32.eqz
i32.eq
i32.ne
i32.lt_s
i32.lt_u
i32.gt_s
i32.gt_u
i32.le_s
i32.le_u
i32.ge_s
i32.ge_u
```

--------------------------------

### WebAssembly Variable Instructions Encoding

Source: https://webassembly.github.io/spec/core/binary/instructions

Explains the encoding for variable instructions, which use byte codes followed by an index for operations like `local.get` and `global.set`.

```WebAssembly
instr::=…|0x20x:localidx⇒local.getx|0x21x:localidx⇒local.setx|0x22x:localidx⇒local.teex|0x23x:globalidx⇒global.getx|0x24x:globalidx⇒global.setx
```

--------------------------------

### WebAssembly Administrative Instructions

Source: https://webassembly.github.io/spec/core/exec/runtime

Extends the WebAssembly instruction syntax with administrative instructions used for formal notation, including 'trap', 'ref', 'ref.extern', 'invoke', 'label', and 'frame'. These model traps, references, function calls, and stack management.

```WebAssembly
instr::=...|trap|reffuncaddr|ref.externexternaddr|invokefuncaddr|labeln{instr*}instr*end|framen{framestate}instr*end
```

--------------------------------

### WebAssembly table.initxy Instruction

Source: https://webassembly.github.io/spec/core/valid/instructions

The table.initxy instruction initializes a range of elements in a table from an element segment. It requires the table and element segment to be defined, and their reference types must match. It takes destination index, source offset, and count as i32 inputs.

```WebAssembly
C.tables[x]=limitstC.elems[y]=tC⊢table.initxy:[i32i32i32]→[]
```

--------------------------------

### WebAssembly f32 Comparison Operations

Source: https://webassembly.github.io/spec/core/text/instructions

Provides instructions for comparison operations on 32-bit floats, including equality, inequality, less than, greater than, less than or equal to, and greater than or equal to.

```WebAssembly
f32.eq
f32.ne
f32.lt
f32.gt
f32.le
f32.ge
```

--------------------------------

### WebAssembly table.getx Instruction

Source: https://webassembly.github.io/spec/core/exec/instructions

Retrieves an element from a table at a specified index. It requires an i32 constant for the index, checks bounds, and pushes the table element onto the stack. Traps if the index is out of bounds.

```WebAssembly
S;F;(i32.consti)(table.getx)↪S;F;val(ifS.tables[F.module.tableaddrs[x]].elem[i]=val)S;F;(i32.consti)(table.getx)↪S;F;trap(otherwise)
```

--------------------------------

### WebAssembly Parametric Instructions Encoding

Source: https://webassembly.github.io/spec/core/binary/instructions

Describes the encoding for parametric instructions like `drop` and `select`, noting that some may include a type annotation.

```WebAssembly
instr::=…|0x1A⇒drop|0x1B⇒select|0x1Ct∗:vec(valtype)⇒selectt∗
```

--------------------------------

### WebAssembly memory.initx Instruction

Source: https://webassembly.github.io/spec/core/exec/instructions

Initializes a linear memory with data from a data segment. It takes offsets and length, and copies bytes from the data segment to the memory. Includes checks for bounds and handles zero length.

```WebAssembly
memory.initx
```

--------------------------------

### WebAssembly i32 Extension Instructions

Source: https://webassembly.github.io/spec/core/binary/instructions

Extends 32-bit integers with sign extension for smaller bit widths. These are plain opcodes without immediate values.

```WebAssembly
0xC0⇒i32.extend8_s
0xC1⇒i32.extend16_s
```

--------------------------------

### WebAssembly Host Function Invocation

Source: https://webassembly.github.io/spec/core/exec/instructions

Details the non-deterministic behavior of host functions in WebAssembly. It covers regular returns, potential traps, stack value consumption/production, and store modifications, ensuring the resulting store remains valid and an extension of the original.

```WebAssembly
S;valn(invokea)↪S′;result(ifS.funcs[a]={type[t1n]→[t2m],hostcodehf}∧(S′;result)∈hf(S;valn))
S;valn(invokea)↪S;valn(invokea)(ifS.funcs[a]={type[t1n]→[t2m],hostcodehf}∧⊥∈hf(S;valn))
```

--------------------------------

### WebAssembly f32.load Instructions

Source: https://webassembly.github.io/spec/core/text/instructions

Loads a 32-bit floating-point number from memory.

```WebAssembly
f32.load
```

--------------------------------

### WebAssembly Table Initialization and Manipulation Operators

Source: https://webassembly.github.io/spec/core/appendix/index-instructions

These operators manage table data in WebAssembly, including initializing table segments, dropping elements, copying table segments, growing tables, querying table size, and filling table regions with a specific element.

```WebAssembly
table.initxy | 0xFC0x0C | [i32i32i32]→[]
elem.dropx | 0xFC0x0D | []→[]
table.copyxy | 0xFC0x0E | [i32i32i32]→[]
table.growx | 0xFC0x0F | [ti32]→[i32]
table.sizex | 0xFC0x10 | []→[i32]
table.fillx | 0xFC0x11 | [i32ti32]→[]
```

--------------------------------

### WebAssembly ref.func Instruction

Source: https://webassembly.github.io/spec/core/exec/instructions

Explains the ref.func instruction, which pushes a function reference onto the stack. It involves asserting the existence of a function address and pushing the reference.

```WebAssembly
ref.funcx
1. Let F be the current frame.
2. Assert: due to validation, F.module.funcaddrs[x] exists.
3. Let a be the function address F.module.funcaddrs[x].
4. Push the value refa to the stack.

F;(ref.funcx)↪F;(refa)(ifa=F.module.funcaddrs[x])
```

--------------------------------

### WebAssembly Block Reduction Rule

Source: https://webassembly.github.io/spec/core/exec/runtime

Illustrates the reduction rule for a 'block' instruction in WebAssembly, showing how it is transformed into a 'label' instruction with an empty continuation, effectively pushing the label onto the stack.

```WebAssembly
block[tn]instr*end ↪labeln{ϵ}instr*end
```

--------------------------------

### WebAssembly t.binop Instruction

Source: https://webassembly.github.io/spec/core/exec/instructions

Explains the t.binop instruction for binary operations. It covers stack assertions, popping two operands, performing the binary operation, and pushing the result or trapping.

```WebAssembly
t.binop
1. Assert: due to validation, two values of value type t are on the top of the stack.
2. Pop the value t.constc2 from the stack.
3. Pop the value t.constc1 from the stack.
4. If binopt(c1,c2) is defined, then:
    1. Let c be a possible result of computing binopt(c1,c2).
    2. Push the value t.constc to the stack.
5. Else:
    1. Trap.

(t.constc1)(t.constc2)t.binop↪(t.constc)(ifc∈binopt(c1,c2))
(t.constc1)(t.constc2)t.binop↪trap(ifbinopt(c1,c2)={})
```

--------------------------------

### WebAssembly f32 Constants

Source: https://webassembly.github.io/spec/core/text/instructions

Defines the instruction for pushing a 32-bit floating-point constant onto the stack.

```WebAssembly
f32.const z:f32
```

--------------------------------

### WebAssembly i32 Constants

Source: https://webassembly.github.io/spec/core/text/instructions

Defines the instruction for pushing a 32-bit integer constant onto the stack.

```WebAssembly
i32.const n:i32
```

--------------------------------

### WebAssembly Nop and Unreachable Instructions

Source: https://webassembly.github.io/spec/core/syntax/instructions

Details the 'nop' instruction which does nothing and the 'unreachable' instruction which causes an unconditional trap.

```WebAssembly
nop
unreachable
```

--------------------------------

### WebAssembly Function Reference Instruction

Source: https://webassembly.github.io/spec/core/text/instructions

Represents the 'ref.func' instruction in WebAssembly, which pushes a reference to a specified function index onto the stack.

```WebAssembly
‘ref.func’x:funcidx⇒ref.funcx
```

--------------------------------

### WebAssembly Branch Instructions

Source: https://webassembly.github.io/spec/core/syntax/instructions

Describes various branch instructions: 'br' for unconditional branching, 'br_if' for conditional branching, 'br_table' for indirect branching, and 'return' as a shortcut for branching to the outermost block.

```WebAssembly
br labelidx
br_if labelidx
br_table vec(labelidx) labelidx
return
```

--------------------------------

### WebAssembly f64 Binary Floating-Point Operations

Source: https://webassembly.github.io/spec/core/text/instructions

Provides instructions for binary floating-point operations on 64-bit floats, including addition, subtraction, multiplication, division, minimum, maximum, and copy sign.

```WebAssembly
f64.add
f64.sub
f64.mul
f64.div
f64.min
f64.max
f64.copysign
```

--------------------------------

### WebAssembly Local Tee Instruction (local.teex)

Source: https://webassembly.github.io/spec/core/exec/instructions

Pops a value from the stack, pushes it back onto the stack, and then sets a local variable with that value. This is equivalent to a `local.set` after a `local.get` (or a duplicate).

```wasm
val(local.teex)↪valval(local.setx)
```

--------------------------------

### WebAssembly f64 Comparison Instructions

Source: https://webassembly.github.io/spec/core/binary/instructions

Performs equality and relational comparisons on 64-bit floating-point numbers. These are plain opcodes without immediate values.

```WebAssembly
0x61⇒f64.eq
0x62⇒f64.ne
0x63⇒f64.lt
0x64⇒f64.gt
0x65⇒f64.le
0x66⇒f64.ge
```

--------------------------------

### WebAssembly i64 Comparison Instructions

Source: https://webassembly.github.io/spec/core/binary/instructions

Performs equality and relational comparisons on 64-bit integers. These are plain opcodes without immediate values.

```WebAssembly
0x50⇒i64.eqz
0x51⇒i64.eq
0x52⇒i64.ne
0x53⇒i64.lt_s
0x54⇒i64.lt_u
0x55⇒i64.gt_s
0x56⇒i64.gt_u
0x57⇒i64.le_s
0x58⇒i64.le_u
0x59⇒i64.ge_s
0x5A⇒i64.ge_u
```

--------------------------------

### WebAssembly local.setx Instruction

Source: https://webassembly.github.io/spec/core/valid/instructions

Explains the 'local.setx' instruction for setting the value of a local variable 'x' of type 't'.

```WebAssembly
C.locals[x]=tC⊢local.setx:[t]→[]
```

--------------------------------

### WebAssembly Integer Comparison Instructions (i32)

Source: https://webassembly.github.io/spec/core/appendix/index-instructions

Documentation for WebAssembly i32 integer comparison instructions: eqz, eq, ne, lt_s, lt_u, gt_s, gt_u, le_s, le_u, ge_s, ge_u. These instructions compare two i32 values.

```WebAssembly
i32.eqz | 0x45 | [i32]→[i32] | validation | execution (operator)
i32.eq | 0x46 | [i32i32]→[i32] | validation | execution (operator)
i32.ne | 0x47 | [i32i32]→[i32] | validation | execution (operator)
i32.lt_s | 0x48 | [i32i32]→[i32] | validation | execution (operator)
i32.lt_u | 0x49 | [i32i32]→[i32] | validation | execution (operator)
i32.gt_s | 0x4A | [i32i32]→[i32] | validation | execution (operator)
i32.gt_u | 0x4B | [i32i32]→[i32] | validation | execution (operator)
i32.le_s | 0x4C | [i32i32]→[i32] | validation | execution (operator)
i32.le_u | 0x4D | [i32i32]→[i32] | validation | execution (operator)
i32.ge_s | 0x4E | [i32i32]→[i32] | validation | execution (operator)
i32.ge_u | 0x4F | [i32i32]→[i32] | validation | execution (operator)
```

--------------------------------

### WebAssembly i32.store Instructions

Source: https://webassembly.github.io/spec/core/text/instructions

Stores a 32-bit integer to memory. Supports different byte alignments.

```WebAssembly
i32.store
i32.store8
i32.store16
```

--------------------------------

### WebAssembly Integer Comparison Instructions (i64)

Source: https://webassembly.github.io/spec/core/appendix/index-instructions

Documentation for WebAssembly i64 integer comparison instructions: eqz, eq, ne, lt_s, lt_u, gt_s, gt_u, le_s, le_u, ge_s, ge_u. These instructions compare two i64 values.

```WebAssembly
i64.eqz | 0x50 | [i64]→[i32] | validation | execution (operator)
i64.eq | 0x51 | [i64i64]→[i32] | validation | execution (operator)
i64.ne | 0x52 | [i64i64]→[i32] | validation | execution (operator)
i64.lt_s | 0x53 | [i64i64]→[i32] | validation | execution (operator)
i64.lt_u | 0x54 | [i64i64]→[i32] | validation | execution (operator)
i64.gt_s | 0x55 | [i64i64]→[i32] | validation | execution (operator)
i64.gt_u | 0x56 | [i64i64]→[i32] | validation | execution (operator)
i64.le_s | 0x57 | [i64i64]→[i32] | validation | execution (operator)
i64.le_u | 0x58 | [i64i64]→[i32] | validation | execution (operator)
i64.ge_s | 0x59 | [i64i64]→[i32] | validation | execution (operator)
i64.ge_u | 0x5A | [i64i64]→[i32] | validation | execution (operator)
```

--------------------------------

### WebAssembly Stack Manipulation Instructions

Source: https://webassembly.github.io/spec/core/appendix/index-instructions

Documentation for WebAssembly stack manipulation instructions such as drop, select, and select_t. These instructions manage values on the operand stack.

```WebAssembly
drop | 0x1A | [t]→[] | validation | execution
select | 0x1B | [tti32]→[t] | validation | execution
selectt | 0x1C | [tti32]→[t] | validation | execution
```

--------------------------------

### WebAssembly i64.store Instructions

Source: https://webassembly.github.io/spec/core/text/instructions

Stores a 64-bit integer to memory. Supports different byte alignments for 8, 16, and 32-bit accesses.

```WebAssembly
i64.store
i64.store8
i64.store16
i64.store32
```

--------------------------------

### WebAssembly Operator Grouping Conventions

Source: https://webassembly.github.io/spec/core/syntax/instructions

Defines grammar shorthands used for grouping WebAssembly operators, simplifying the representation of common instruction patterns. This aids in understanding and defining instruction sets.

```WebAssembly
unop::=iunop|funop|extendN
binop::=ibinop|fbinop
testop::=itestop
relop::=irelop|frelop
cvtop::=wrap|extend|trunc|trunc_sat|convert|demote|promote|reinterpret
```
Tokens:
Raw