Kwasm.validation.instruction

Validator of Expression nodes.

From the docs:

Expressions expr are classified by result types of the form [t?].

instr* end

• The instruction sequence instr* must be valid with type [] => [t?], for some optional value type t?.
• Then the expression is valid with result type [t?].

Constant Expressions

• In a constant expression instr* end all instructions in instr* must be constant.

• A constant instruction instr must be:

  • either of the form t.const c,
  • or of the form global.get x, in which case C.globals\[x] must be a global type of the form const t.

Validator of sequences of Instruction nodes.

From

Typing of instruction sequences is defined recursively.

Empty Instruction Sequence: ϵ

• The empty instruction sequence is valid with type [t*] => [t*], for any sequence of value types t*.

Non-empty Instruction Sequence: instr* instrN

• The instruction sequence instr* must be valid with type [t*^1] => [t*2], for some sequences of value types t*^1 and t*^2.
• The instruction instrN must be valid with type [t*] => [t*^3], for some sequences of value types t* and t*^3.
• There must be a sequence of value types t*^0, such that t*^2 = t*^0 t*.
• Then the combined instruction sequence is valid with type [t*^1] => [t*^0 t*^3].

Validates Instruction nodes by multiplexing out to implementation-specific variants.

Validator of MemoryInstruction nodes by multiplexing into specific validators for each type.

See: LoadIntValidator, StoreIntValidator, LoadFloatValidator, StoreFloatValidator,

Validates NumericConstantInstruction nodes.

From the docs:

t.const c

• The instruction is valid with type [] => \[t].

Validates NumericInstruction nodes.

From the docs:

t.unop

• The NumericInstruction is valid with type [t] => [t].

t.binop

• The NumericInstruction is valid with type [t t] => [t].

t.testop

• The NumericInstruction is valid with type [t] => [i32].

t.relop

• The NumericInstruction is valid with type [t t] => [i32].

t2.cvtop_t1_sx?

• The NumericInstruction is valid with type \[t1] => \[t2].

Validator of ParametricInstruction nodes.

From the docs:

ParametricInstruction.Drop

• The instruction is valid with type [t] =>[], for any value type t.

ParametricInstruction.Select

• The instruction is valid with type [t t i32] => [t], for any value type t.

Validator of VariableInstruction nodes.

From

VariableInstruction.LocalGet

• The local C.locals\[x] must be defined in the context.
• Let t be the value type C.locals\[x].
• Then the instruction is valid with type [] => \[t].

VariableInstruction.LocalSet

• The local C.locals\[x] must be defined in the context.
• Let t be the value type C.locals\[x].
• Then the instruction is valid with type \[t] => [].

VariableInstruction.LocalTee

• The local C.locals\[x] must be defined in the context.
• Let t be the value type C.locals\[x].
• Then the instruction is valid with type \[t] => \[t].

VariableInstruction.GlobalGet

• The global C.globals\[x] must be defined in the context.
• Let mut t be the global type C.globals\[x].
• Then the instruction is valid with type [] => \[t].

VariableInstruction.GlobalSet

• The global C.globals\[x] must be defined in the context.
• Let mut t be the global type C.globals\[x].
• The mutability mut must be var.
• Then the instruction is valid with type \[t] => [].