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

------------------------------------------------------------------------
-- 3.3 Instructions

module Wasm.Validation.Instructions where

open import Data.Fin using (zero; toℕ)
open import Data.List using (List; []; _∷_; _++_; map)
open import Data.List.Membership.Propositional using (_∈_)
open import Data.List.Relation.Binary.Pointwise using (Pointwise)
open import Data.List.Relation.Unary.All using (All)
open import Data.Maybe using (just; nothing)
open import Data.Nat using (_+_; _^_) renaming (_≤_ to _≤ⁿ_)
open import Data.Product using (_,_; _×_; ∃)
open import Data.Sum using (inj₁; inj₂)
open import Data.Vec.Bounded using (toList)
open import Level using (0ℓ)
open import Relation.Binary using (Rel)
open import Relation.Binary.PropositionalEquality using (_≡_)
open import Wasm.Expression.Instructions
open import Wasm.Expression.Types
open import Wasm.Expression.Utilities using (BitWidth; 32Bit; 64Bit; module BitWidth′)
open import Wasm.Validation.Context
open import Wasm.Validation.Types

infix 4 _≤_ _⟶_

data OpdType : Set where
  [_] : ValType → OpdType
  ⊥   : OpdType

record StackType : Set where
  constructor _⟶_
  field
    from : List OpdType
    to   : List OpdType

fromResult : ResultType → List OpdType
fromResult t = map [_] (toList t)

fromFunc : FuncType → StackType
fromFunc (from ⟶ to) = fromResult from ⟶ fromResult to

data _≤_ : Rel OpdType 0ℓ where
  ⊥≤τ  : ∀ {τ} → ⊥ ≤ τ
  refl : ∀ {τ τ′} → τ ≡ τ′ → τ ≤ τ′

------------------------------------------------------------------------
-- 3.3.1 Numeric Instructions

intType : BitWidth → OpdType
intType 32Bit = [ inj₁ i32 ]
intType 64Bit = [ inj₁ i64 ]

floatType : BitWidth → OpdType
floatType 32Bit = [ inj₁ f32 ]
floatType 64Bit = [ inj₁ f64 ]

typeOfNum : NumInstr → StackType
typeOfNum (int (ixx w (IntOp.const _))) = [] ⟶ intType w ∷ []
typeOfNum (int (ixx w (IntOp.iunop _))) = intType w ∷ [] ⟶ intType w ∷ []
typeOfNum (int (ixx w (IntOp.ibinop _))) = intType w ∷ intType w ∷ [] ⟶ intType w ∷ []
typeOfNum (int (ixx w (IntOp.itestop _))) = intType w ∷ [] ⟶ [ inj₁ i32 ] ∷ []
typeOfNum (int (ixx w (IntOp.irelop _))) = intType w ∷ intType w ∷ [] ⟶ [ inj₁ i32 ] ∷ []
typeOfNum (int (ixx w IntOp.extend8-s)) = intType w ∷ [] ⟶ intType w ∷ []
typeOfNum (int (ixx w IntOp.extend16-s)) = intType w ∷ [] ⟶ intType w ∷ []
typeOfNum (int (ixx w (IntOp.trunc-f w′ _))) = floatType w′ ∷ [] ⟶ intType w ∷ []
typeOfNum (int (ixx w (IntOp.trunc-sat-f w′ _))) = floatType w′ ∷ [] ⟶ intType w ∷ []
typeOfNum (int (ixx w IntOp.reinterpret-f)) = floatType w ∷ [] ⟶ intType w ∷ []
typeOfNum (int i64-extend32-s) = [ inj₁ i64 ] ∷ [] ⟶ [ inj₁ i64 ] ∷ []
typeOfNum (int i32-wrap-i64) = [ inj₁ i64 ] ∷ [] ⟶ [ inj₁ i32 ] ∷ []
typeOfNum (int (i64-extend-i32 _)) = [ inj₁ i32 ] ∷ [] ⟶ [ inj₁ i64 ] ∷ []
typeOfNum (float (fxx w (FloatOp.const _))) = [] ⟶ floatType w ∷ []
typeOfNum (float (fxx w (FloatOp.funop _))) = floatType w ∷ [] ⟶ floatType w ∷ []
typeOfNum (float (fxx w (FloatOp.fbinop _))) = floatType w ∷ floatType w ∷ [] ⟶ floatType w ∷ []
typeOfNum (float (fxx w (FloatOp.frelop _))) = floatType w ∷ floatType w ∷ [] ⟶ [ inj₁ i32 ] ∷ []
typeOfNum (float (fxx w (FloatOp.convert-i w′ _))) = intType w′ ∷ [] ⟶ floatType w ∷ []
typeOfNum (float (fxx w FloatOp.reinterpret-i)) = intType w ∷ [] ⟶ floatType w ∷ []
typeOfNum (float f32-demote-f64) = [ inj₁ f64 ] ∷ [] ⟶ [ inj₁ f32 ] ∷ []
typeOfNum (float f64-promote-f32) = [ inj₁ f32 ] ∷ [] ⟶ [ inj₁ f64 ] ∷ []

------------------------------------------------------------------------
-- 3.3.2 Reference Instructions

data RefInstrType : Context → RefInstr → StackType → Set where
  null : ∀ {C t} → RefInstrType C (null t) ([] ⟶ [ inj₂ t ] ∷ [])
  is-null : ∀ {C t} → RefInstrType C is-null ([ inj₂ t ] ∷ [] ⟶ [ inj₁ i32 ] ∷ [])
  func : ∀ {C x t} → Context.getFunc C x ≡ just t → x ∈ Context.refs C → RefInstrType C (func x) ([] ⟶ [ inj₂ funcref ] ∷ [])

------------------------------------------------------------------------
-- 3.3.3 Parametric Instructions

data ParametricInstrType : Context → ParametricInstr → StackType → Set where
  drop : ∀ {C t} → ParametricInstrType C drop ([ t ] ∷ [] ⟶ [])
  select-t : ∀ {C t} → ParametricInstrType C (select (just (t ∷ []))) ([ inj₁ i32 ] ∷ [ t ] ∷ [ t ] ∷ [] ⟶ [ t ] ∷ [])
  select-no-t : ∀ {C t} → ParametricInstrType C (select nothing) ([ inj₁ i32 ] ∷ [ inj₁ t ] ∷ [ inj₁  t ] ∷ [] ⟶ [ inj₁ t ] ∷ [])

------------------------------------------------------------------------
-- 3.3.4 Variable Instructions

data VarInstrType : Context → VarInstr → StackType → Set where
  local-get : ∀ {C x t} → Context.getLocal C x ≡ just t → VarInstrType C (local-get x) ([] ⟶ [ t ] ∷ [])
  local-set : ∀ {C x t} → Context.getLocal C x ≡ just t → VarInstrType C (local-set x) ([ t ] ∷ [] ⟶ [])
  local-tee : ∀ {C x t} → Context.getLocal C x ≡ just t → VarInstrType C (local-tee x) ([ t ] ∷ [] ⟶ [ t ] ∷ [])
  global-get : ∀ {C x m t} → Context.getGlobal C x ≡ just (m , t) → VarInstrType C (global-get x) ([] ⟶ [ t ] ∷ [])
  global-set : ∀ {C x t} → Context.getGlobal C x ≡ just (var , t) → VarInstrType C (global-set x) ([ t ] ∷ [] ⟶ [])

------------------------------------------------------------------------
-- 3.3.5 Table Instructions

data TableInstrType : Context → TableInstr → StackType → Set where
  get : ∀ {C x lim t} → Context.getTable C x ≡ just (lim , t) → TableInstrType C (get x) ([ inj₁ i32 ] ∷ [] ⟶ [ inj₂ t ] ∷ [])
  set : ∀ {C x lim t} → Context.getTable C x ≡ just (lim , t) → TableInstrType C (set x) ([ inj₂ t ] ∷ [ inj₁ i32 ] ∷ [] ⟶ [])
  size : ∀ {C x lim,t} → Context.getTable C x ≡ just lim,t → TableInstrType C (size x) ([] ⟶ [ inj₁ i32 ] ∷ [])
  grow : ∀ {C x lim t} → Context.getTable C x ≡ just (lim , t) → TableInstrType C (grow x) ([ inj₁ i32 ] ∷ [ inj₂ t ] ∷ [] ⟶ [ inj₁ i32 ] ∷ [])
  fill : ∀ {C x lim t} → Context.getTable C x ≡ just (lim , t) → TableInstrType C (fill x) ([ inj₁ i32 ] ∷ [ inj₂ t ] ∷ [ inj₁ i32 ] ∷ [] ⟶ [])
  copy : ∀ {C x y lim₁ lim₂ t} → Context.getTable C x ≡ just (lim₁ , t) → Context.getTable C y ≡ just (lim₂ , t) → TableInstrType C (copy x y) ([ inj₁ i32 ] ∷ [ inj₁ i32 ] ∷ [ inj₁ i32 ] ∷ [] ⟶ [])
  init : ∀ {C x y lim₁ t} → Context.getTable C x ≡ just (lim₁ , t) → Context.getElem C y ≡ just t → TableInstrType C (init x y) ([ inj₁ i32 ] ∷ [ inj₁ i32 ] ∷ [ inj₁ i32 ] ∷ [] ⟶ [])
  drop : ∀ {C x t} → Context.getElem C x ≡ just t → TableInstrType C (drop x) ([] ⟶ [])

------------------------------------------------------------------------
-- 3.3.6 Memory Instructions

data MemInstrType : Context → MemInstr → StackType → Set where
  int-load : ∀ {C w arg lim} → Context.getMem C zero ≡ just lim → 2 ^ (3 + toℕ (MemArg.align arg)) ≤ⁿ BitWidth′.toℕ w → MemInstrType C (int (ixx w (IntMem.load arg))) ([ inj₁ i32 ] ∷ [] ⟶ intType w ∷ [])
  int-load8 : ∀ {C w s arg lim} → Context.getMem C zero ≡ just lim → MemArg.align arg ≡ zero → MemInstrType C (int (ixx w (IntMem.load8 s arg))) ([ inj₁ i32 ] ∷ [] ⟶ intType w ∷ [])
  int-load16 : ∀ {C w s arg lim} → Context.getMem C zero ≡ just lim → toℕ (MemArg.align arg) ≤ⁿ 1 → MemInstrType C (int (ixx w (IntMem.load16 s arg))) ([ inj₁ i32 ] ∷ [] ⟶ intType w ∷ [])
  int-load32 : ∀ {C s arg lim} → Context.getMem C zero ≡ just lim → toℕ (MemArg.align arg) ≤ⁿ 2 → MemInstrType C (int (i64-load32 s arg)) ([ inj₁ i32 ] ∷ [] ⟶ [ inj₁ i64 ] ∷ [])
  int-store : ∀ {C w arg lim} → Context.getMem C zero ≡ just lim → 2 ^ (3 + toℕ (MemArg.align arg)) ≤ⁿ BitWidth′.toℕ w → MemInstrType C (int (ixx w (IntMem.store arg))) (intType w ∷ [ inj₁ i32 ] ∷ [] ⟶ [])
  int-store8 : ∀ {C w arg lim} → Context.getMem C zero ≡ just lim → MemArg.align arg ≡ zero → MemInstrType C (int (ixx w (IntMem.store8 arg))) (intType w ∷ [ inj₁ i32 ] ∷ [] ⟶ [])
  int-store16 : ∀ {C w arg lim} → Context.getMem C zero ≡ just lim → toℕ (MemArg.align arg) ≤ⁿ 1 → MemInstrType C (int (ixx w (IntMem.store16 arg))) (intType w ∷ [ inj₁ i32 ] ∷ [] ⟶ [])
  int-store32 : ∀ {C arg lim} → Context.getMem C zero ≡ just lim → toℕ (MemArg.align arg) ≤ⁿ 2 → MemInstrType C (int (i64-store32 arg)) ([ inj₁ i64 ] ∷ [ inj₁ i32 ] ∷ [] ⟶ [])
  float-load : ∀ {C w arg lim} → Context.getMem C zero ≡ just lim → 2 ^ (3 + toℕ (MemArg.align arg)) ≤ⁿ BitWidth′.toℕ w → MemInstrType C (float (w , (FloatMem.load arg))) ([ inj₁ i32 ] ∷ [] ⟶ floatType w ∷ [])
  float-store : ∀ {C w arg lim} → Context.getMem C zero ≡ just lim → 2 ^ (3 + toℕ (MemArg.align arg)) ≤ⁿ BitWidth′.toℕ w → MemInstrType C (float (w , (FloatMem.store arg))) ([ inj₁ i32 ] ∷ floatType w ∷ [] ⟶ [])
  size : ∀ {C lim} → Context.getMem C zero ≡ just lim → MemInstrType C size ([] ⟶ [ inj₁ i32 ] ∷ [])
  grow : ∀ {C lim} → Context.getMem C zero ≡ just lim → MemInstrType C grow ([ inj₁ i32 ] ∷ [] ⟶ [ inj₁ i32 ] ∷ [])
  fill : ∀ {C lim} → Context.getMem C zero ≡ just lim → MemInstrType C fill ([ inj₁ i32 ] ∷ [ inj₁ i32 ] ∷ [ inj₁ i32 ] ∷ [] ⟶ [])
  copy : ∀ {C lim} → Context.getMem C zero ≡ just lim → MemInstrType C copy ([ inj₁ i32 ] ∷ [ inj₁ i32 ] ∷ [ inj₁ i32 ] ∷ [] ⟶ [])
  init : ∀ {C x lim} → Context.getMem C zero ≡ just lim → Context.getData C x ≡ just _ → MemInstrType C (init x) ([ inj₁ i32 ] ∷ [ inj₁ i32 ] ∷ [ inj₁ i32 ] ∷ [] ⟶ [])
  drop : ∀ {C x} → Context.getData C x ≡ just _ → MemInstrType C (drop x) ([] ⟶ [])

------------------------------------------------------------------------
-- 3.3.7 Control Instructions

infix 2 _⊢_∶_ _⊢*_∶_

data _⊢_∶_ : Context → Instr → StackType → Set
data _⊢*_∶_ : Context → List Instr → StackType → Set

data _⊢_∶_ where
  num : ∀ {C i} → C ⊢ num i ∶ typeOfNum i
  ref : ∀ {C i t} → RefInstrType C i t → C ⊢ ref i ∶ t
  parametric : ∀ {C i t} → ParametricInstrType C i t → C ⊢ parametric i ∶ t
  var : ∀ {C i t} → VarInstrType C i t → C ⊢ var i ∶ t
  table : ∀ {C i t} → TableInstrType C i t → C ⊢ table i ∶ t
  mem : ∀ {C i t} → MemInstrType C i t → C ⊢ mem i ∶ t
  nop : ∀ {C} → C ⊢ nop ∶ [] ⟶ []
  unreachable : ∀ {C ts₁ ts₂} → C ⊢ unreachable ∶ ts₁ ⟶ ts₂
  block : ∀ {C bt t₁ t₂ is} → blockType C bt ≡ just (t₁ ⟶ t₂) → record C { labels = t₂ ∷ Context.labels C } ⊢* is ∶ fromFunc (t₁ ⟶ t₂) → C ⊢ block bt is ∶ fromFunc (t₁ ⟶ t₂)
  loop : ∀ {C bt t₁ t₂ is} → blockType C bt ≡ just (t₁ ⟶ t₂) → record C { labels = t₁ ∷ Context.labels C } ⊢* is ∶ fromFunc (t₁ ⟶ t₂) → C ⊢ block bt is ∶ fromFunc (t₁ ⟶ t₂)
  if-else : ∀ {C bt t₁ t₂ is₁ is₂} → blockType C bt ≡ just (t₁ ⟶ t₂) → record C { labels = t₂ ∷ Context.labels C } ⊢* is₁ ∶ fromFunc (t₁ ⟶ t₂) → record C { labels = t₂ ∷ Context.labels C } ⊢* is₂ ∶ fromFunc (t₁ ⟶ t₂) → C ⊢ if-else bt is₁ is₂ ∶ [ inj₁ i32 ] ∷ fromResult t₁ ⟶ fromResult t₂
  br : ∀ {C l t t₁ t₂} → Context.getLabel C l ≡ just t → C ⊢ br l ∶ fromResult t ++ t₁ ⟶ t₂
  br_if : ∀ {C l t} → Context.getLabel C l ≡ just t → C ⊢ br l ∶ [ inj₁ i32 ] ∷ fromResult t ⟶ fromResult t
  br_table : ∀ {C ls l t t′ t₁ t₂} → Context.getLabel C l ≡ just t′ → Pointwise _≤_ t (fromResult t′) → All (λ l′ → ∃ λ t′ → Context.getLabel C l′ ≡ just t′ × Pointwise _≤_ t (fromResult t′)) (toList ls) → C ⊢ br-table ls l ∶ t ++ t₁ ⟶ t₂
  return : ∀ {C t t₁ t₂} → Context.return C ≡ just t → C ⊢ return ∶ (fromResult t) ++ t₁ ⟶ t₂
  call : ∀ {C x t} → Context.getFunc C x ≡ just t → C ⊢ call x ∶ fromFunc t
  call-indirect : ∀ {C x y lim t₁ t₂} → Context.getTable C x ≡ just (lim , funcref) → Context.getType C y ≡ just (t₁ ⟶ t₂) → C ⊢ call-indirect x y ∶ [ inj₁ i32 ] ∷ fromResult t₁ ⟶ fromResult t₂

------------------------------------------------------------------------
-- 3.3.8 Instruction Sequences

-- NOTE: fold is in reverse due to nature of lists in Agda.

data _⊢*_∶_ where
  empty : ∀ {C t} → C ⊢* [] ∶ t ⟶ t
  step : ∀ {C i is t₀ t₁ t′ t t₃} → Pointwise _≤_ t′ t → C ⊢ i ∶ t ⟶ t₁ → C ⊢* is ∶ (t₁ ++ t₀) ⟶ t₃ → C ⊢* i ∷ is ∶ (t′ ++ t₀) ⟶ t₃

------------------------------------------------------------------------
-- 3.3.9 Expressions

infix 2 _⊢ᵉ_∶_ _⊢*_const _⊢_const

_⊢ᵉ_∶_ : Context → Expr → ResultType → Set
C ⊢ᵉ expr ∶ t = ∃ λ t′ → (C ⊢* expr ∶ [] ⟶ t′) × Pointwise _≤_ t′ (fromResult t)

data _⊢_const : Context → Instr → Set
_⊢*_const : Context → Expr → Set

data _⊢_const where
  int-const : ∀ {C w x} → C ⊢ num (int (ixx w (IntOp.const x))) const
  float-const : ∀ {C w x} → C ⊢ num (float (fxx w (FloatOp.const x))) const
  ref-null : ∀ {C t} → C ⊢ ref (null t) const
  ref-func : ∀ {C x} → C ⊢ ref (func x) const
  global-get : ∀ {C x t} → Context.getGlobal C x ≡ just (const , t) → C ⊢ var (global-get x) const

C ⊢* expr const = All (C ⊢_const) expr