From a3a8a44b4bc0d60164452826645066a5ffed5bc5 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Wed, 28 Jul 2021 16:56:07 +0100
Subject: Complete Section 3 - Validation.

---
 src/Wasm/Validation/Context.agda      |  63 +++++++++++
 src/Wasm/Validation/Instructions.agda | 197 ++++++++++++++++++++++++++++++++++
 src/Wasm/Validation/Modules.agda      | 191 ++++++++++++++++++++++++++++++++
 src/Wasm/Validation/Types.agda        |  95 ++++++++++++++++
 4 files changed, 546 insertions(+)
 create mode 100644 src/Wasm/Validation/Context.agda
 create mode 100644 src/Wasm/Validation/Instructions.agda
 create mode 100644 src/Wasm/Validation/Modules.agda
 create mode 100644 src/Wasm/Validation/Types.agda

(limited to 'src/Wasm')

diff --git a/src/Wasm/Validation/Context.agda b/src/Wasm/Validation/Context.agda
new file mode 100644
index 0000000..f7c2564
--- /dev/null
+++ b/src/Wasm/Validation/Context.agda
@@ -0,0 +1,63 @@
+{-# OPTIONS --without-K --safe #-}
+
+------------------------------------------------------------------------
+-- Type Context
+
+module Wasm.Validation.Context where
+
+open import Data.Fin using (Fin; toℕ; fromℕ<)
+open import Data.List using (List; length; lookup)
+open import Data.Maybe using (Maybe; just; nothing)
+open import Data.Nat using (_<?_; _^_)
+open import Data.Unit using (⊤)
+open import Relation.Nullary using (yes; no)
+open import Wasm.Constants
+open import Wasm.Expression.Types
+open import Wasm.Expression.Utilities using (module Indices)
+
+record Context : Set where
+  field
+    types : List FuncType
+    funcs : List FuncType
+    tables : List TableType
+    mems   : List MemType
+    globals : List GlobalType
+    elems   : List RefType
+    datas   : List ⊤
+    locals  : List ValType
+    labels  : List ResultType
+    return  : Maybe ResultType
+    refs    : List Indices.FuncIdx
+
+  private
+    get : ∀ {A} → List A → Fin 2^32 → Maybe A
+    get xs idx with toℕ idx <? length xs
+    ... | yes idx<∣xs∣ = just (lookup xs (fromℕ< idx<∣xs∣))
+    ... | no _         = nothing
+
+  getType : Indices.TypeIdx → Maybe FuncType
+  getType = get types
+
+  getFunc : Indices.FuncIdx → Maybe FuncType
+  getFunc = get funcs
+
+  getTable : Indices.TableIdx → Maybe TableType
+  getTable = get tables
+
+  getMem : Indices.MemIdx → Maybe MemType
+  getMem = get mems
+
+  getGlobal : Indices.GlobalIdx → Maybe GlobalType
+  getGlobal = get globals
+
+  getElem : Indices.ElemIdx → Maybe RefType
+  getElem = get elems
+
+  getData : Indices.DataIdx → Maybe ⊤
+  getData = get datas
+
+  getLocal : Indices.LocalIdx → Maybe ValType
+  getLocal = get locals
+
+  getLabel : Indices.LabelIdx → Maybe ResultType
+  getLabel = get labels
diff --git a/src/Wasm/Validation/Instructions.agda b/src/Wasm/Validation/Instructions.agda
new file mode 100644
index 0000000..7aa9411
--- /dev/null
+++ b/src/Wasm/Validation/Instructions.agda
@@ -0,0 +1,197 @@
+{-# 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
diff --git a/src/Wasm/Validation/Modules.agda b/src/Wasm/Validation/Modules.agda
new file mode 100644
index 0000000..1e0ca0a
--- /dev/null
+++ b/src/Wasm/Validation/Modules.agda
@@ -0,0 +1,191 @@
+{-# OPTIONS --without-K --safe #-}
+
+------------------------------------------------------------------------
+-- 3.4 Modules
+
+module Wasm.Validation.Modules where
+
+open import Data.List using (List; []; _∷_; _++_; map; mapMaybe; allFin; replicate)
+open import Data.List.Relation.Unary.All using (All)
+open import Data.List.Relation.Unary.AllPairs using (AllPairs)
+open import Data.List.Relation.Binary.Pointwise using (Pointwise)
+open import Data.Maybe using (just; nothing; maybe)
+open import Data.Nat using (_≤_; z≤n; s≤s; _^_)
+open import Data.Product using (_×_; ∃; _,_; proj₁; proj₂)
+open import Data.Sum using (inj₁)
+open import Data.Unit using (⊤)
+open import Data.Vec using ([]; _∷_)
+open import Data.Vec.Bounded using (Vec≤; _,_; toList)
+open import Relation.Binary.PropositionalEquality using (_≡_; _≢_)
+open import Wasm.Constants
+open import Wasm.Expression.Modules
+open import Wasm.Expression.Types
+open import Wasm.Expression.Utilities using (module Indices)
+open import Wasm.Expression.Values using (toString)
+open import Wasm.Validation.Context
+open import Wasm.Validation.Instructions hiding (_≤_)
+open import Wasm.Validation.Types
+
+------------------------------------------------------------------------
+-- 3.4.1 Functions
+
+record FuncOk (C : Context) (F : Func) (τ : FuncType) : Set where
+  private
+    module C = Context C
+    module F = Func F
+    module τ = FuncType τ
+
+  field
+    typeEq : C.getType F.type ≡ just τ
+    exprOk : record C
+      { locals = toList F.locals ++ toList τ.from
+      ; labels = τ.to ∷ []
+      ; return = just τ.to
+      } ⊢ᵉ F.body ∶ τ.to
+
+------------------------------------------------------------------------
+-- 3.4.2 Tables
+
+TableOk : Context → Table → TableType → Set
+TableOk C tbl τ = tbl ≡ τ × TableTypeOk τ
+
+------------------------------------------------------------------------
+-- 3.4.3 Memories
+
+MemOk : Context → Mem → MemType → Set
+MemOk C mry τ = mry ≡ τ × MemTypeOk τ
+
+------------------------------------------------------------------------
+-- 3.4.4 Globals
+
+record GlobalOk (C : Context) (G : Global) (τ : GlobalType) : Set where
+  private
+    module C = Context C
+    module G = Global G
+    mut = proj₁ τ
+    t = proj₂ τ
+
+  field
+    typeEq    : G.type ≡ τ
+    typeOk    : GlobalTypeOk τ
+    initOk    : C ⊢ᵉ G.init ∶ t ∷ [] , s≤s z≤n
+    initConst : C ⊢* G.init const
+
+------------------------------------------------------------------------
+-- 3.4.5 Element Segments
+
+data ElemModeOk : Context → ElemMode → RefType → Set where
+  passive : ∀ {C τ} → ElemModeOk C passive τ
+  active : ∀ {C x lim off t} → Context.getTable C x ≡ just (lim , t) → C ⊢ᵉ off ∶ inj₁ i32 ∷ [] , s≤s z≤n → C ⊢* off const → ElemModeOk C (active x off) t
+  declarative : ∀ {C τ} → ElemModeOk C declarative τ
+
+record ElemOk (C : Context) (E : Elem) (τ : RefType) : Set where
+  private
+    module C = Context C
+    module E = Elem E
+
+  field
+    typeEq     : E.type ≡ τ
+    initsOk    : All (λ e → ∃ (C ⊢ᵉ e ∶_)) (toList E.init)
+    initsConst : All (C ⊢*_const) (toList E.init)
+    modeOk     : ElemModeOk C E.mode E.type
+
+------------------------------------------------------------------------
+-- 3.4.6 Data Segments
+
+data DataModeOk : Context → DataMode → Set where
+  passive : ∀ {C} → DataModeOk C passive
+  active : ∀ {C x lim off} → Context.getMem C x ≡ just lim → C ⊢ᵉ off ∶ inj₁ i32 ∷ [] , s≤s z≤n → C ⊢* off const → DataModeOk C (active x off)
+
+DataOk : Context → Data → Set
+DataOk C D = DataModeOk C (Data.mode D)
+
+------------------------------------------------------------------------
+-- 3.4.7 Start Function
+
+StartOk : Context → Start → Set
+StartOk C x = Context.getFunc C x ≡ just (([] , z≤n) ⟶ ([] , z≤n))
+
+------------------------------------------------------------------------
+-- 3.4.8 Exports
+
+data ExportDescOk : Context → ExportDesc → ExternType → Set where
+  func   : ∀ {C x t} → Context.getFunc C x ≡ just t → ExportDescOk C (func x) (func t)
+  table  : ∀ {C x t} → Context.getTable C x ≡ just t → ExportDescOk C (table x) (table t)
+  mem    : ∀ {C x t} → Context.getMem C x ≡ just t → ExportDescOk C (mem x) (mem t)
+  global : ∀ {C x t} → Context.getGlobal C x ≡ just t → ExportDescOk C (global x) (global t)
+
+ExportOk : Context → Export → ExternType → Set
+ExportOk C exp t = ExportDescOk C (Export.desc exp) t
+
+------------------------------------------------------------------------
+-- 3.4.9 Imports
+
+data ImportDescOk : Context → ImportDesc → ExternType → Set where
+  func   : ∀ {C x t} → Context.getType C x ≡ just t → ImportDescOk C (func x) (func t)
+  table  : ∀ {C t} → TableTypeOk t → ImportDescOk C (table t) (table t)
+  mem    : ∀ {C t} → MemTypeOk t → ImportDescOk C (mem t) (mem t)
+  global : ∀ {C t} → GlobalTypeOk t → ImportDescOk C (global t) (global t)
+
+ImportOk : Context → Import → ExternType → Set
+ImportOk C imp t = ImportDescOk C (Import.desc imp) t
+
+------------------------------------------------------------------------
+-- 3.4.10 Modules
+
+record _⊢ᴹ_∶_⟶_ (M : Mod) (it : List ExternType) (et : List ExternType) : Set where
+  field
+    {ft} : List FuncType
+    {tt} : List TableType
+    {mt} : List MemType
+    {gt} : List GlobalType
+    {rt} : List RefType
+
+  private
+    module M = Mod M
+    ift = mapMaybe func? it
+    itt = mapMaybe table? it
+    imt = mapMaybe mem? it
+    igt = mapMaybe global? it
+    -- FIXME: find real references
+    x = []
+    C = record
+      { types = toList M.types
+      ; funcs = ft ++ ift
+      ; tables = tt ++ itt
+      ; mems = mt ++ imt
+      ; globals = gt ++ igt
+      ; elems = rt
+      ; datas = replicate (Vec≤.length M.datas) _
+      ; locals = []
+      ; labels = []
+      ; return = nothing
+      ; refs = x
+      }
+    C′ = record
+       { types = []
+       ; funcs = Context.funcs C
+       ; tables = []
+       ; mems = []
+       ; globals = igt
+       ; elems = []
+       ; datas = []
+       ; locals = []
+       ; labels = []
+       ; return = nothing
+       ; refs = Context.refs C
+       }
+
+  field
+    typesOk        : All FuncTypeOk (toList M.types)
+    funcsOk        : Pointwise (FuncOk C) (toList M.funcs) ft
+    tablesOk       : Pointwise (TableOk C) (toList M.tables) tt
+    memsOk         : Pointwise (MemOk C) (toList M.mems) mt
+    globalsOk      : Pointwise (GlobalOk C′) (toList M.globals) gt
+    elemsOk        : Pointwise (ElemOk C) (toList M.elems) rt
+    datasOk        : All (DataOk C) (toList M.datas)
+    startOk        : maybe (StartOk C) ⊤ M.start
+    importsOk      : Pointwise (ImportOk C) (toList M.imports) it
+    exportsOk      : Pointwise (ExportOk C) (toList M.exports) et
+    memsCount      : Vec≤.length M.mems ≤ 1
+    exportDisjoint : AllPairs _≢_ (map (λ x → toString (Export.name x)) (toList M.exports))
diff --git a/src/Wasm/Validation/Types.agda b/src/Wasm/Validation/Types.agda
new file mode 100644
index 0000000..3ee78c0
--- /dev/null
+++ b/src/Wasm/Validation/Types.agda
@@ -0,0 +1,95 @@
+{-# OPTIONS --without-K --safe #-}
+
+------------------------------------------------------------------------
+-- 3.2 Types
+
+module Wasm.Validation.Types where
+
+open import Data.Fin using (toℕ)
+open import Data.Maybe using (Maybe; just; nothing)
+open import Data.Nat using (ℕ; _≤_; _≥_; z≤n; s≤s; _^_; pred)
+open import Data.Product using (_×_; _,_)
+open import Data.Sum using (inj₁; inj₂)
+open import Data.Unit using (⊤)
+open import Data.Vec using ([]; _∷_)
+open import Data.Vec.Bounded using (_,_)
+open import Level using (0ℓ)
+open import Relation.Binary using (Rel)
+open import Relation.Binary.PropositionalEquality using (_≡_)
+open import Wasm.Constants
+open import Wasm.Expression.Instructions using (BlockType)
+open import Wasm.Expression.Types
+open import Wasm.Validation.Context
+
+infix 2 ⊢ˡ_∶_
+infix 4 _≤ˡ_ _≤ᶠ_ _≤ᵗ_ _≤ᵐ_ _≤ᵍ_
+
+IsOk : Set → Set₁
+IsOk A = A → Set
+
+------------------------------------------------------------------------
+-- 3.2.1 Limits
+
+data ⊢ˡ_∶_ : Limits → ℕ → Set where
+  noMax   : ∀ {k n} → toℕ n ≤ k → ⊢ˡ record { min = n ; max = nothing } ∶ k
+  withMax : ∀ {k m n} → toℕ n ≤ toℕ m → toℕ m ≤ k → ⊢ˡ record { min = n ; max = just m } ∶ k
+
+------------------------------------------------------------------------
+-- 3.2.2 Block Types
+
+blockType : Context → BlockType → Maybe FuncType
+blockType C (inj₁ x) = Context.getType C x
+blockType C (inj₂ (just t)) = just (([] , z≤n) ⟶ (t ∷ [] , s≤s z≤n))
+blockType C (inj₂ nothing) = just (([] , z≤n) ⟶ ([] , z≤n))
+
+------------------------------------------------------------------------
+-- 3.2.3 Function Types
+
+FuncTypeOk : IsOk FuncType
+FuncTypeOk _ = ⊤
+
+------------------------------------------------------------------------
+-- 3.2.4 Table Types
+
+TableTypeOk : IsOk TableType
+TableTypeOk (limits , reftype) = ⊢ˡ limits ∶ pred 2^32
+
+------------------------------------------------------------------------
+-- 3.2.5 Memory Types
+
+MemTypeOk : IsOk MemType
+MemTypeOk limits = ⊢ˡ limits ∶ 2 ^ 16
+
+------------------------------------------------------------------------
+-- 3.2.6 Global Types
+
+GlobalTypeOk : IsOk GlobalType
+GlobalTypeOk t = ⊤
+
+------------------------------------------------------------------------
+-- 3.2.7 External Types
+
+data ExternTypeOk : IsOk ExternType where
+  func : ∀ {t} → FuncTypeOk t → ExternTypeOk (func t)
+  table : ∀ {t} → TableTypeOk t → ExternTypeOk (table t)
+  mem : ∀ {t} → MemTypeOk t → ExternTypeOk (mem t)
+  global : ∀ {t} → GlobalTypeOk t → ExternTypeOk (global t)
+
+------------------------------------------------------------------------
+-- 3.2.8 Import Subtyping
+
+data _≤ˡ_ : Rel Limits 0ℓ where
+  noMax : ∀ {m₁? n₁ n₂} → toℕ n₁ ≥ toℕ n₂ → record { min = n₁ ; max = m₁? } ≤ˡ record { min = n₂ ; max = nothing }
+  withMax : ∀ {m₁ m₂ n₁ n₂} → toℕ n₁ ≥ toℕ n₂ → toℕ m₁ ≤ toℕ m₂ → record { min = n₁ ; max = just m₁ } ≤ˡ record { min = n₂ ; max = just m₂ }
+
+_≤ᶠ_ : Rel FuncType 0ℓ
+_≤ᶠ_ = _≡_
+
+_≤ᵗ_ : Rel TableType 0ℓ
+(limits₁ , reftype₁) ≤ᵗ (limits₂ , reftype₂) = limits₁ ≤ˡ limits₂ × reftype₁ ≡ reftype₂
+
+_≤ᵐ_ : Rel MemType 0ℓ
+_≤ᵐ_ = _≤ˡ_
+
+_≤ᵍ_ : Rel GlobalType 0ℓ
+_≤ᵍ_ = _≡_
-- 
cgit v1.2.3