path: root/src/Wasm/Data/Instruction.agda

{-# OPTIONS --safe --without-K #-}

module Wasm.Data.Instruction where

open import Data.Fin using (Fin)
open import Data.List using (List; []; _∷_; _++_; length; lookup)
open import Data.List.Membership.Propositional using (_∈_)
open import Data.List.Relation.Unary.All using (All)
open import Data.Maybe using (Maybe; just)
open import Data.Nat using (ℕ; suc; _>_)
open import Relation.Binary.PropositionalEquality using (_≡_)
open import Wasm.Type
open import Wasm.Value

record Context : Set where
  field
    funcs   : List FuncType
    tables  : List TableType
    mems    : List MemType
    globals : List GlobalType
    elems   : List RefType
    datas   : ℕ
    locals  : List ValType
    labels  : List (List ValType)
    return  : Maybe (List ValType)
    refs    : List (Fin (length funcs))

data Signedness : Set where
  signed   : Signedness
  unsigned : Signedness

module i32 where
  data Unary : Set where
    clz        : Unary
    ctz        : Unary
    popcnt     : Unary
    extend8-s  : Unary
    extend16-s : Unary

  data Binary : Set where
    add  : Binary
    sub  : Binary
    mul  : Binary
    div  : Signedness → Binary
    rem  : Signedness → Binary
    and  : Binary
    or   : Binary
    xor  : Binary
    shl  : Binary
    shr  : Signedness → Binary
    rotl : Binary
    rotr : Binary

  data Test : Set where
    eqz : Test

  data Rel : Set where
    eq : Rel
    ne : Rel
    lt : Signedness → Rel
    gt : Signedness → Rel
    le : Signedness → Rel
    ge : Signedness → Rel

  data Convert : NumType → Set where
    wrap          : Convert i64
    trunc-f32     : Signedness → Convert f32
    trunc-f64     : Signedness → Convert f64
    trunc-sat-f32 : Signedness → Convert f32
    trunc-sat-f64 : Signedness → Convert f64
    reinterpret   : Convert f32

module i64 where
  data Unary : Set where
    clz        : Unary
    ctz        : Unary
    popcnt     : Unary
    extend8-s  : Unary
    extend16-s : Unary
    extend32-s : Unary

  data Binary : Set where
    add  : Binary
    sub  : Binary
    mul  : Binary
    div  : Signedness → Binary
    rem  : Signedness → Binary
    and  : Binary
    or   : Binary
    xor  : Binary
    shl  : Binary
    shr  : Signedness → Binary
    rotl : Binary
    rotr : Binary

  data Test : Set where
    eqz : Test

  data Rel : Set where
    eq : Rel
    ne : Rel
    lt : Signedness → Rel
    gt : Signedness → Rel
    le : Signedness → Rel
    ge : Signedness → Rel

  data Convert : NumType → Set where
    extend        : Convert i32
    trunc-f32     : Signedness → Convert f32
    trunc-f64     : Signedness → Convert f64
    trunc-sat-f32 : Signedness → Convert f32
    trunc-sat-f64 : Signedness → Convert f64
    reinterpret   : Convert f64

module f32 where
  data Unary : Set where
    abs     : Unary
    neg     : Unary
    sqrt    : Unary
    ceil    : Unary
    floor   : Unary
    trunc   : Unary
    nearest : Unary

  data Binary : Set where
    add      : Binary
    sub      : Binary
    mul      : Binary
    div      : Binary
    min      : Binary
    max      : Binary
    copysign : Binary

  data Rel : Set where
    eq : Rel
    ne : Rel
    lt : Rel
    gt : Rel
    le : Rel
    ge : Rel

  data Convert : NumType → Set where
    demote      : Convert f64
    convert-i32 : Convert i32
    convert-i64 : Convert i64
    reinterpret : Convert i32

module f64 where
  data Unary : Set where
    abs     : Unary
    neg     : Unary
    sqrt    : Unary
    ceil    : Unary
    floor   : Unary
    trunc   : Unary
    nearest : Unary

  data Binary : Set where
    add      : Binary
    sub      : Binary
    mul      : Binary
    div      : Binary
    min      : Binary
    max      : Binary
    copysign : Binary

  data Rel : Set where
    eq : Rel
    ne : Rel
    lt : Rel
    gt : Rel
    le : Rel
    ge : Rel

  data Convert : NumType → Set where
    promote     : Convert f32
    convert-i32 : Convert i32
    convert-i64 : Convert i64
    reinterpret : Convert i64

record MemArg (t : ℕ): Set where
  field
    offset : I32
    align  : Fin (suc t)

data BlockType : Context → Set where
  idx : ∀ {C} → FuncType → BlockType C
  val : ∀ {C} → ValType → BlockType C
  nothing : ∀ {C} → BlockType C

blockTypeAsFunc : ∀ {C} → BlockType C → FuncType
blockTypeAsFunc {C} (idx τ) = τ
blockTypeAsFunc (val x) = [] ⟶ x ∷ []
blockTypeAsFunc nothing = [] ⟶ []

data Instruction : Context → FuncType → Set where
  ---- Numeric instructions
  -- const
  i32-const : ∀ {C} → (c : I32) → Instruction C ([] ⟶ num i32 ∷ [])
  i64-const : ∀ {C} → (c : I64) → Instruction C ([] ⟶ num i64 ∷ [])
  f32-const : ∀ {C} → (c : F32) → Instruction C ([] ⟶ num f32 ∷ [])
  f64-const : ∀ {C} → (c : F64) → Instruction C ([] ⟶ num f64 ∷ [])
  -- unop
  i32-unop : ∀ {C} → (op : i32.Unary) → Instruction C (num i32 ∷ [] ⟶ num i32 ∷ [])
  i64-unop : ∀ {C} → (op : i64.Unary) → Instruction C (num i64 ∷ [] ⟶ num i64 ∷ [])
  f32-unop : ∀ {C} → (op : f32.Unary) → Instruction C (num f32 ∷ [] ⟶ num f32 ∷ [])
  f64-unop : ∀ {C} → (op : f64.Unary) → Instruction C (num f64 ∷ [] ⟶ num f64 ∷ [])
  -- binop
  i32-binop : ∀ {C} → (op : i32.Binary) → Instruction C (num i32 ∷ num i32 ∷ [] ⟶ num i32 ∷ [])
  i64-binop : ∀ {C} → (op : i64.Binary) → Instruction C (num i64 ∷ num i64 ∷ [] ⟶ num i64 ∷ [])
  f32-binop : ∀ {C} → (op : f32.Binary) → Instruction C (num f32 ∷ num f32 ∷ [] ⟶ num f32 ∷ [])
  f64-binop : ∀ {C} → (op : f64.Binary) → Instruction C (num f64 ∷ num f64 ∷ [] ⟶ num f64 ∷ [])
  -- testop
  i32-testop : ∀ {C} → (op : i32.Test) → Instruction C (num i32 ∷ [] ⟶ num i32 ∷ [])
  i64-testop : ∀ {C} → (op : i64.Test) → Instruction C (num i64 ∷ [] ⟶ num i32 ∷ [])
  -- relop
  i32-relop : ∀ {C} → (op : i32.Rel) → Instruction C (num i32 ∷ num i32 ∷ [] ⟶ num i32 ∷ [])
  i64-relop : ∀ {C} → (op : i64.Rel) → Instruction C (num i64 ∷ num i64 ∷ [] ⟶ num i32 ∷ [])
  f32-relop : ∀ {C} → (op : f32.Rel) → Instruction C (num f32 ∷ num f32 ∷ [] ⟶ num i32 ∷ [])
  f64-relop : ∀ {C} → (op : f64.Rel) → Instruction C (num f64 ∷ num f64 ∷ [] ⟶ num i32 ∷ [])
  -- cvtop
  i32-cvtop : ∀ {C τ} → (op : i32.Convert τ) → Instruction C (num τ ∷ [] ⟶ num i32 ∷ [])
  i64-cvtop : ∀ {C τ} → (op : i64.Convert τ) → Instruction C (num τ ∷ [] ⟶ num i64 ∷ [])
  f32-cvtop : ∀ {C τ} → (op : f32.Convert τ) → Instruction C (num τ ∷ [] ⟶ num f32 ∷ [])
  f64-cvtop : ∀ {C τ} → (op : f64.Convert τ) → Instruction C (num τ ∷ [] ⟶ num f64 ∷ [])

  ---- Reference instructions
  ref-null : ∀ {C} τ → Instruction C ([] ⟶ ref τ ∷ [])
  ref-is-null : ∀ {C τ} → Instruction C (ref τ ∷ [] ⟶ num i32 ∷ [])
  ref-func : ∀ {C x} → (x∈refs : x ∈ Context.refs C) → Instruction C ([] ⟶ ref funcref ∷ [])

  ---- Parametric instructions
  drop : ∀ {C τ} → Instruction C (τ ∷ [] ⟶ [])
  select : ∀ {C τ} → Instruction C (num i32 ∷ τ ∷ τ ∷ [] ⟶ τ ∷ [])

  ---- Variable instructions
  local-get : ∀ {C} x → Instruction C ([] ⟶ lookup (Context.locals C) x ∷ [])
  local-set : ∀ {C} x → Instruction C (lookup (Context.locals C) x ∷ [] ⟶ [])
  local-tee : ∀ {C} x → Instruction C (lookup (Context.locals C) x ∷ [] ⟶ lookup (Context.locals C) x ∷ [])
  global-get : ∀ {C} x → Instruction C ([] ⟶ GlobalType.type (lookup (Context.globals C) x) ∷ [])
  global-set : ∀ {C} x → let g = lookup (Context.globals C) x in GlobalType.mut g ≡ var → Instruction C (GlobalType.type g ∷ [] ⟶ [])

  ---- Table instructions
  table-get : ∀ {C} x → Instruction C (num i32 ∷ [] ⟶ ref (TableType.type (lookup (Context.tables C) x)) ∷ [])
  table-set : ∀ {C} x → Instruction C (ref (TableType.type (lookup (Context.tables C) x)) ∷ num i32 ∷ [] ⟶ [])
  table-size : ∀ {C} (x : Fin (length (Context.tables C))) → Instruction C ([] ⟶ num i32 ∷ [])
  table-grow : ∀ {C} x → Instruction C (num i32 ∷ ref (TableType.type (lookup (Context.tables C) x)) ∷ [] ⟶ num i32 ∷ [])
  table-fill : ∀ {C} x → Instruction C (num i32 ∷ ref (TableType.type (lookup (Context.tables C) x)) ∷ num i32 ∷ [] ⟶ [])
  table-copy : ∀ {C} x y → TableType.type (lookup (Context.tables C) x) ≡ TableType.type (lookup (Context.tables C) y) → Instruction C (num i32 ∷ num i32 ∷ num i32 ∷ [] ⟶ [])
  table-init : ∀ {C} x y → TableType.type (lookup (Context.tables C) x) ≡ lookup (Context.elems C) y → Instruction C (num i32 ∷ num i32 ∷ num i32 ∷ [] ⟶ [])
  elem-drop : ∀ {C} (x : Fin (length (Context.elems C))) → Instruction C ([] ⟶ [])

  ---- Memory instructions
  -- load
  i32-load : ∀ {C} (m : MemArg 2) → length (Context.mems C) > 0 → Instruction C (num i32 ∷ [] ⟶ num i32 ∷ [])
  i64-load : ∀ {C} (m : MemArg 3) → length (Context.mems C) > 0 → Instruction C (num i32 ∷ [] ⟶ num i64 ∷ [])
  f32-load : ∀ {C} (m : MemArg 2) → length (Context.mems C) > 0 → Instruction C (num i32 ∷ [] ⟶ num f32 ∷ [])
  f64-load : ∀ {C} (m : MemArg 3) → length (Context.mems C) > 0 → Instruction C (num i32 ∷ [] ⟶ num f64 ∷ [])
  -- loadN
  i32-load8 : ∀ {C} (m : MemArg 0) → length (Context.mems C) > 0 → Signedness → Instruction C (num i32 ∷ [] ⟶ num i32 ∷ [])
  i32-load16 : ∀ {C} (m : MemArg 1) → length (Context.mems C) > 0 → Signedness → Instruction C (num i32 ∷ [] ⟶ num i32 ∷ [])
  i64-load8 : ∀ {C} (m : MemArg 0) → length (Context.mems C) > 0 → Signedness → Instruction C (num i32 ∷ [] ⟶ num i64 ∷ [])
  i64-load16 : ∀ {C} (m : MemArg 1) → length (Context.mems C) > 0 → Signedness → Instruction C (num i32 ∷ [] ⟶ num i64 ∷ [])
  i64-load32 : ∀ {C} (m : MemArg 2) → length (Context.mems C) > 0 → Signedness → Instruction C (num i32 ∷ [] ⟶ num i64 ∷ [])
  -- store
  i32-store : ∀ {C} (m : MemArg 2) → length (Context.mems C) > 0 → Instruction C (num i32 ∷ num i32 ∷ [] ⟶ [])
  i64-store : ∀ {C} (m : MemArg 3) → length (Context.mems C) > 0 → Instruction C (num i64 ∷ num i32 ∷ [] ⟶ [])
  f32-store : ∀ {C} (m : MemArg 2) → length (Context.mems C) > 0 → Instruction C (num f32 ∷ num i32 ∷ [] ⟶ [])
  f64-store : ∀ {C} (m : MemArg 3) → length (Context.mems C) > 0 → Instruction C (num f64 ∷ num i32 ∷ [] ⟶ [])
  -- storeN
  i32-store8 : ∀ {C} (m : MemArg 0) → length (Context.mems C) > 0 → Signedness → Instruction C (num i32 ∷ num i32 ∷ [] ⟶ [])
  i32-store16 : ∀ {C} (m : MemArg 1) → length (Context.mems C) > 0 → Signedness → Instruction C (num i32 ∷ num i32 ∷ [] ⟶ [])
  i64-store8 : ∀ {C} (m : MemArg 0) → length (Context.mems C) > 0 → Signedness → Instruction C (num i64 ∷ num i32 ∷ [] ⟶ [])
  i64-store16 : ∀ {C} (m : MemArg 1) → length (Context.mems C) > 0 → Signedness → Instruction C (num i64 ∷ num i32 ∷ [] ⟶ [])
  i64-store32 : ∀ {C} (m : MemArg 2) → length (Context.mems C) > 0 → Signedness → Instruction C (num i64 ∷ num i32 ∷ [] ⟶ [])
  -- other
  memory-size : ∀ {C} → length (Context.mems C) > 0 → Instruction C ([] ⟶ num i32 ∷ [])
  memory-grow : ∀ {C} → length (Context.mems C) > 0 → Instruction C (num i32 ∷ [] ⟶ num i32 ∷ [])
  memory-fill : ∀ {C} → length (Context.mems C) > 0 → Instruction C (num i32 ∷ num i32 ∷ num i32 ∷ [] ⟶ [])
  memory-copy : ∀ {C} → length (Context.mems C) > 0 → Instruction C (num i32 ∷ num i32 ∷ num i32 ∷ [] ⟶ [])
  memory-init : ∀ {C} (x : Fin (Context.datas C)) → length (Context.mems C) > 0 → Instruction C (num i32 ∷ num i32 ∷ num i32 ∷ [] ⟶ [])
  data-drop : ∀ {C} (x : Fin (Context.datas C)) → Instruction C ([] ⟶ [])

  ---- Control instructions
  nop : ∀ {C} → Instruction C ([] ⟶ [])
  unreachable : ∀ {C τ} → Instruction C τ
  block : ∀ {C} (bt : BlockType C) → let τ = blockTypeAsFunc bt in
    Instruction (record C {labels = FuncType.to τ ∷ Context.labels C}) τ → Instruction C τ
  loop : ∀ {C} (bt : BlockType C) → let τ = blockTypeAsFunc bt in
    Instruction (record C {labels = FuncType.from τ ∷ Context.labels C}) τ → Instruction C τ
  if : ∀ {C} (bt : BlockType C) → let τ = blockTypeAsFunc bt in
    (then else : Instruction (record C {labels = FuncType.to τ ∷ Context.labels C}) τ) → Instruction C (num i32 ∷ FuncType.from τ ⟶ FuncType.to τ)
  br : ∀ {C τ₁ τ₂} l → Instruction C (lookup (Context.labels C) l ++ τ₁ ⟶ τ₂)
  br_if : ∀ {C} l → let τ = lookup (Context.labels C) l in Instruction C (num i32 ∷ τ ⟶ τ)
  br_table : ∀ {C τ₁ τ₂} ls l → let τ = lookup (Context.labels C) l in All (λ l → lookup (Context.labels C) l ≡ τ) ls → Instruction C (τ ++ τ₁ ⟶ τ₂)
  return : ∀ {C τ τ₁ τ₂} → Context.return C ≡ just τ → Instruction C (τ ++ τ₁ ⟶ τ₂)
  call : ∀ {C} x → Instruction C (lookup (Context.funcs C) x)
  call_indirect : ∀ {C} x τ → TableType.type (lookup (Context.tables C) x) ≡ funcref → Instruction C (num i32 ∷ FuncType.from τ ⟶ FuncType.to τ)

  ---- Sequencing
  frame : ∀ {C τ τ₁ τ₂} → Instruction C (τ₁ ⟶ τ₂) → Instruction C (τ₁ ++ τ ⟶ τ₂ ++ τ)
  seq   : ∀ {C τ₁ τ₂ τ₃} → Instruction C (τ₁ ⟶ τ₂) → Instruction C (τ₂ ⟶ τ₃) → Instruction C (τ₁ ⟶ τ₃)

Expression : Context → List ValType → Set
Expression C τ = Instruction C ([] ⟶ τ)

data InstructionRef : ∀ {C τ} → Instruction C τ → Fin (length (Context.funcs C)) → Set where
  ---- Direct
  ref-func : ∀ {C x} x∈refs → InstructionRef (ref-func {C} {x} x∈refs) x
  call     : ∀ {C} x → InstructionRef (call {C} x) x

  ---- Structural
  block : ∀ {C x} bt {i} → InstructionRef i x → InstructionRef (block {C} bt i) x
  loop : ∀ {C x} bt {i} → InstructionRef i x → InstructionRef (loop {C} bt i) x
  if₁ : ∀ {C x} bt {i₁} → InstructionRef i₁ x → ∀ i₂ → InstructionRef (if {C} bt i₁ i₂) x
  if₂ : ∀ {C x} bt i₁ {i₂} → InstructionRef i₂ x → InstructionRef (if {C} bt i₁ i₂) x
  frame : ∀ {C x τ τ₁ τ₂} {i} → InstructionRef i x → InstructionRef (frame {C} {τ} {τ₁} {τ₂} i) x
  seq₁ : ∀ {C x τ₁ τ₂ τ₃} {i₁} → InstructionRef i₁ x → ∀ i₂ → InstructionRef (seq {C} {τ₁} {τ₂} {τ₃} i₁ i₂) x
  seq₂ : ∀ {C x τ₁ τ₂ τ₃} i₁ {i₂} → InstructionRef i₂ x → InstructionRef (seq {C} {τ₁} {τ₂} {τ₃} i₁ i₂) x

data Constant : ∀ {C τ} → Instruction C τ → Set where