Rewrite so only valid modules can be constructed.

14 files changed, 673 insertions, 1190 deletions

diff --git a/src/Wasm/Constants.agda b/src/Wasm/Constants.agda
deleted file mode 100644
index 74682a8..0000000
--- a/src/Wasm/Constants.agda
+++ /dev/null
@@ -1,11 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-------------------------------------------------------------------------
--- Big constant values
-
-module Wasm.Constants where
-
-open import Data.Nat using (ℕ)
-
-2^32 : ℕ
-2^32 = 4294967296
diff --git a/src/Wasm/Data.agda b/src/Wasm/Data.agda
new file mode 100644
index 0000000..f7ed8da
--- /dev/null
+++ b/src/Wasm/Data.agda
@@ -0,0 +1,272 @@
+{-# OPTIONS --safe --without-K #-}
+
+module Wasm.Data where
+
+open import Data.Fin using (Fin; zero; suc)
+open import Data.List using (List; []; _∷_; _++_; length; lookup; map)
+open import Data.List.Relation.Binary.Pointwise using (Pointwise)
+open import Data.List.Relation.Unary.All using (All)
+open import Data.List.Relation.Unary.Any using (Any)
+open import Data.List.Relation.Unary.AllPairs using (AllPairs)
+open import Data.Maybe using (Maybe; just; nothing; maybe)
+open import Data.Nat using (ℕ; suc; _+_; _≤_; z≤n)
+open import Data.Product using (_×_; _,_; proj₁)
+open import Data.Sum using (_⊎_)
+open import Data.Unit using (⊤)
+open import Data.Vec using (Vec)
+open import Function as _ using (_∋_)
+open import Relation.Binary.PropositionalEquality using (_≡_; _≢_)
+open import Wasm.Data.Instruction as Inst using (Expression; Constant)
+open import Wasm.Value using (Byte; Name)
+open import Wasm.Type
+
+record ExternTypes : Set where
+  field
+    funcs   : List FuncType
+    tables  : List TableType
+    mems    : List MemType
+    globals : List GlobalType
+
+record Context : Set where
+  field
+    funcs   : List FuncType
+    tables  : List TableType
+    mems    : List MemType
+    globals : List GlobalType
+    elems   : List RefType
+    datas   : ℕ
+
+private
+  makeContext : (Cᵢ : ExternTypes) → (Cₘ : Context) → (refs : List (Fin (length (ExternTypes.funcs Cᵢ ++ Context.funcs Cₘ)))) → Inst.Context
+  makeContext Cᵢ Cₘ refs = record
+    { funcs   = Cᵢ.funcs ++ Cₘ.funcs
+    ; tables  = Cᵢ.tables ++ Cₘ.tables
+    ; mems    = Cᵢ.mems ++ Cₘ.mems
+    ; globals = Cᵢ.globals ++ Cₘ.globals
+    ; elems   = Cₘ.elems
+    ; datas   = Cₘ.datas
+    ; locals  = []
+    ; labels  = []
+    ; return  = nothing
+    ; refs    = refs
+    }
+    where
+    module Cᵢ = ExternTypes Cᵢ
+    module Cₘ = Context Cₘ
+
+  makeGlobalContext : (Cᵢ : ExternTypes) → (Cₘ : Context) → (refs : List (Fin (length (ExternTypes.funcs Cᵢ ++ Context.funcs Cₘ)))) → Inst.Context
+  makeGlobalContext Cᵢ Cₘ refs = record
+    { funcs   = Cᵢ.funcs ++ Cₘ.funcs
+    ; tables  = []
+    ; mems    = []
+    ; globals = Cᵢ.globals
+    ; elems   = []
+    ; datas   = 0
+    ; locals  = []
+    ; labels  = []
+    ; return  = nothing
+    ; refs    = refs
+    }
+    where
+    module Cᵢ = ExternTypes Cᵢ
+    module Cₘ = Context Cₘ
+
+record Function (Cᵢ : ExternTypes) (Cₘ : Context) (refs : List (Fin (length (ExternTypes.funcs Cᵢ ++ Context.funcs Cₘ)))) (idx : Fin (length (Context.funcs Cₘ))) : Set where
+  private
+    module Cₘ = Context Cₘ
+
+  type = lookup Cₘ.funcs idx
+
+  private
+    module type = FuncType type
+
+  field
+    locals : List ValType
+
+  private
+    C = Inst.Context ∋ record (makeContext Cᵢ Cₘ refs)
+      { locals  = type.from ++ locals
+      ; labels  = type.to ∷ []
+      ; return  = just type.to
+      }
+  field
+    body : Expression C type.to
+
+record Global (Cᵢ : ExternTypes) (Cₘ : Context) (refs : List (Fin (length (ExternTypes.funcs Cᵢ ++ Context.funcs Cₘ)))) (idx : Fin (length (Context.globals Cₘ))) : Set where
+  private
+    module Cₘ = Context Cₘ
+    C = Inst.Context ∋ makeGlobalContext Cᵢ Cₘ refs
+
+  type = lookup Cₘ.globals idx
+
+  private
+    module type = GlobalType type
+
+  field
+    {body}   : Expression C (type.type ∷ [])
+    constant : Constant body
+
+GlobalRef : ∀ {Cᵢ Cₘ refs idx} → Global Cᵢ Cₘ refs idx → Fin (length (ExternTypes.funcs Cᵢ ++ Context.funcs Cₘ)) → Set
+GlobalRef global x = Inst.InstructionRef (Global.body global) x
+
+data ElemMode (C : Inst.Context) : RefType → Set where
+  passive : ∀ {τ} → ElemMode C τ
+  active : ∀ table {offset : Expression C (num i32 ∷ [])} → Constant offset → ElemMode C (TableType.type (lookup (Inst.Context.tables C) table))
+  declarative : ∀ {τ} → ElemMode C τ
+
+data ElemModeRef {C : Inst.Context} : ∀ {τ} → ElemMode C τ → Fin (length (Inst.Context.funcs C)) → Set where
+  activeRef : ∀ {x} table {offset} constant → Inst.InstructionRef offset x → ElemModeRef (active table {offset} constant) x
+
+record Elem (Cᵢ : ExternTypes) (Cₘ : Context) (refs : List (Fin (length (ExternTypes.funcs Cᵢ ++ Context.funcs Cₘ)))) (idx : Fin (length (Context.elems Cₘ))) : Set where
+  private
+    module Cₘ = Context Cₘ
+    C = Inst.Context ∋ makeContext Cᵢ Cₘ refs
+
+  type = lookup Cₘ.elems idx
+
+  field
+    {inits}  : List (Expression C (ref type ∷ []))
+    constant : All Constant inits
+    mode     : ElemMode C type
+
+data ElemRef {Cᵢ} {Cₘ} {refs} {idx} (elem : Elem Cᵢ Cₘ refs idx) (x : Fin (length (ExternTypes.funcs Cᵢ ++ Context.funcs Cₘ))) : Set where
+  initsRef : Any (λ init → Inst.InstructionRef init x) (Elem.inits elem) → ElemRef elem x
+  modeRef  : ElemModeRef (Elem.mode elem) x → ElemRef elem x
+
+data DataMode (C : Inst.Context) : Set where
+  passive : DataMode C
+  active  : ∀ (memory : Fin (length (Inst.Context.mems C))) {offset : Expression C (num i32 ∷ [])} → Constant offset → DataMode C
+
+
+data DataModeRef {C : Inst.Context} : DataMode C → Fin (length (Inst.Context.funcs C)) → Set where
+  activeRef : ∀ {x} memory {offset} constant → Inst.InstructionRef offset x → DataModeRef (active memory {offset} constant) x
+
+record Data (Cᵢ : ExternTypes) (Cₘ : Context) (refs : List (Fin (length (ExternTypes.funcs Cᵢ ++ Context.funcs Cₘ)))) (idx : Fin (Context.datas Cₘ)) : Set where
+  private
+    C = Inst.Context ∋ makeContext Cᵢ Cₘ refs
+  field
+    init : List Byte
+    mode : DataMode C
+
+DataRef : ∀ {Cᵢ Cₘ refs idx} → Data Cᵢ Cₘ refs idx → Fin (length (ExternTypes.funcs Cᵢ ++ Context.funcs Cₘ)) → Set
+DataRef dta x = DataModeRef (Data.mode dta) x
+
+record Exports (Cᵢ : ExternTypes) (Cₘ : Context) (refs : List (Fin (length (ExternTypes.funcs Cᵢ ++ Context.funcs Cₘ)))) (Cₑ : ExternTypes) : Set where
+  private
+    C = Inst.Context ∋ makeContext Cᵢ Cₘ refs
+    module Cₑ = ExternTypes Cₑ
+    module C = Inst.Context C
+  field
+    funcs     : List (Name × Fin (length (C.funcs)))
+    tables    : List (Name × Fin (length (C.tables)))
+    mems      : List (Name × Fin (length (C.mems)))
+    globals   : List (Name × Fin (length (C.globals)))
+    funcsOk   : Pointwise (λ (_ , x) τ → lookup C.funcs x ≡ τ) funcs Cₑ.funcs
+    tablesOk  : Pointwise (λ (_ , x) τ → lookup C.tables x ≡ τ) tables Cₑ.tables
+    memsOk    : Pointwise (λ (_ , x) τ → lookup C.mems x ≡ τ) mems Cₑ.mems
+    globalsOk : Pointwise (λ (_ , x) τ → lookup C.globals x ≡ τ) globals Cₑ.globals
+  names = map proj₁ funcs ++ map proj₁ tables ++ map proj₁ mems ++ map proj₁ globals
+  field
+    namesDisjoint : AllPairs _≢_ names
+
+ExportsRef : ∀ {Cᵢ Cₘ refs Cₑ} → Exports Cᵢ Cₘ refs Cₑ → Fin (length (ExternTypes.funcs Cᵢ ++ Context.funcs Cₘ)) → Set
+ExportsRef exports x = Any (λ (_ , y) → y ≡ x) (Exports.funcs exports)
+
+record Imports (Cᵢ : ExternTypes) : Set where
+  private
+    module Cᵢ = ExternTypes Cᵢ
+  field
+    funcs   : Vec (Name × Name) (length Cᵢ.funcs)
+    tables  : Vec (Name × Name) (length Cᵢ.tables)
+    mems    : Vec (Name × Name) (length Cᵢ.mems)
+    globals : Vec (Name × Name) (length Cᵢ.globals)
+
+infixr 5 _∷_
+
+data DList : ∀ {n} → (A : Fin n → Set) → Set₁ where
+  [] : ∀ {A} → DList {0} A
+  _∷_ : ∀ {n A} → A zero → DList {n} (λ i → A (suc i)) → DList A
+
+data DAny : ∀ {n A} → (∀ {i} → A i → Set) → DList {n} A → Set₁ where
+  here  : ∀ {n A} {P : ∀ {i} → A i → Set} {x xs} → P x → DAny {suc n} {A} P (x ∷ xs)
+  there : ∀ {n A} {P : ∀ {i} → A i → Set} {x xs} → DAny (λ {i} → P {suc i}) xs → DAny {suc n} {A} P (x ∷ xs)
+
+record Module (it et : ExternTypes) : Set₁ where
+  private
+    module it = ExternTypes it
+  field
+    ft     : List FuncType
+    tables : List TableType
+    mems   : List MemType
+    rt     : List RefType
+    n      : ℕ
+    start  : Maybe (Fin (length (it.funcs ++ ft)))
+  private
+    Cₘ = Context ∋ record
+      { funcs   = ft
+      ; tables  = tables
+      ; mems    = mems
+      ; globals = it.globals
+      ; elems   = rt
+      ; datas   = n
+      }
+  field
+    refs     : List (Fin (length (it.funcs ++ ft)))
+    funcs    : DList (Function it Cₘ refs)
+    globals  : DList (Global it Cₘ refs)
+    elems    : DList (Elem it Cₘ refs)
+    datas    : DList (Data it Cₘ refs)
+    startOk  : maybe (λ x → lookup (it.funcs ++ ft) x ≡ ([] ⟶ [])) ⊤ start
+    exports  : Exports it Cₘ refs et
+    memCount : length it.mems + length mems ≤ 1
+    refsUsed : All (λ i → DAny (λ g → GlobalRef g i) globals
+                        ⊎ DAny (λ e → ElemRef e i) elems
+                        ⊎ DAny (λ d → DataRef d i) datas
+                        ⊎ ExportsRef exports i)
+                   refs
+
+private
+  module Test where
+    open import Data.List.Relation.Binary.Pointwise using ([]; _∷_)
+    open import Data.List.Relation.Unary.All using ([])
+    open import Data.List.Relation.Unary.AllPairs using ([]; _∷_)
+    open import Relation.Binary.PropositionalEquality using (refl)
+    open Inst
+
+    addTwoImports : ExternTypes
+    addTwoImports = record { funcs = [] ; tables = [] ; mems = [] ; globals = [] }
+
+    addTwoExports : ExternTypes
+    addTwoExports = record { funcs = (num i32 ∷ num i32 ∷ [] ⟶ num i32 ∷ []) ∷ [] ; tables = [] ; mems = [] ; globals = [] }
+
+    addTwoModule : Module addTwoImports addTwoExports
+    addTwoModule = record
+      { ft = (num i32 ∷ num i32 ∷ [] ⟶ num i32 ∷ []) ∷ []
+      ; tables = []
+      ; mems = []
+      ; rt = []
+      ; n = 0
+      ; start = nothing
+      ; refs = []
+      ; funcs = record
+        { locals = []
+        ; body = seq (local-get zero) (seq (frame (local-get (suc zero))) (i32-binop i32.add))
+        } ∷ []
+      ; globals = []
+      ; elems = []
+      ; datas = []
+      ; startOk = _
+      ; exports = record
+        { funcs = ("addTwo" , zero) ∷ []
+        ; tables = []
+        ; mems = []
+        ; globals = []
+        ; funcsOk = refl ∷ []
+        ; tablesOk = []
+        ; memsOk = []
+        ; globalsOk = []
+        ; namesDisjoint = [] ∷ []
+        }
+      ; memCount = z≤n
+      ; refsUsed = []
+      }
diff --git a/src/Wasm/Data/Instruction.agda b/src/Wasm/Data/Instruction.agda
new file mode 100644
index 0000000..69853f0
--- /dev/null
+++ b/src/Wasm/Data/Instruction.agda
@@ -0,0 +1,321 @@
+{-# 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
diff --git a/src/Wasm/Expression/Instructions.agda b/src/Wasm/Expression/Instructions.agda
deleted file mode 100644
index 3fa96be..0000000
--- a/src/Wasm/Expression/Instructions.agda
+++ /dev/null
@@ -1,219 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-------------------------------------------------------------------------
--- 2.4 Types
-
-module Wasm.Expression.Instructions where
-
-open import Data.List using (List)
-open import Data.Maybe using (Maybe)
-open import Data.Product using (∃)
-open import Data.Sum using (_⊎_)
-open import Wasm.Expression.Values using (UnsignedInteger; UninterpretedInteger; Float)
-open import Wasm.Expression.Types using (ValType; RefType)
-open import Wasm.Expression.Utilities
-
-------------------------------------------------------------------------
--- 2.4.1 Numeric Instructions
-
-module IntOp (w : BitWidth) where
-  data Unary : Set where
-    clz    : Unary
-    ctz    : Unary
-    popcnt : 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 IntInstr : Set where
-    const         : UninterpretedInteger (BitWidth′.toℕ w) → IntInstr
-    iunop         : Unary → IntInstr
-    ibinop        : Binary → IntInstr
-    itestop       : Test → IntInstr
-    irelop        : Rel → IntInstr
-    extend8-s     : IntInstr
-    extend16-s    : IntInstr
-    trunc-f       : BitWidth → Signedness → IntInstr
-    trunc-sat-f   : BitWidth → Signedness → IntInstr
-    reinterpret-f : IntInstr
-
-data IntInstr : Set where
-  ixx            : ∀ w → IntOp.IntInstr w → IntInstr
-  i64-extend32-s : IntInstr
-  i32-wrap-i64   : IntInstr
-  i64-extend-i32 : Signedness → IntInstr
-
-module FloatOp (w : BitWidth) 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 FloatInstr : Set where
-    const         : Float w → FloatInstr
-    funop         : Unary → FloatInstr
-    fbinop        : Binary → FloatInstr
-    frelop        : Rel → FloatInstr
-    convert-i     : BitWidth → Signedness → FloatInstr
-    reinterpret-i : FloatInstr
-
-data FloatInstr : Set where
-  fxx             : ∀ w → FloatOp.FloatInstr w → FloatInstr
-  f32-demote-f64  : FloatInstr
-  f64-promote-f32 : FloatInstr
-
-data NumInstr : Set where
-  int   : IntInstr → NumInstr
-  float : FloatInstr → NumInstr
-
-------------------------------------------------------------------------
--- 2.4.2 Reference Instructions
-
-data RefInstr : Set where
-  null    : RefType → RefInstr
-  is-null : RefInstr
-  func    : Indices.FuncIdx → RefInstr
-
-------------------------------------------------------------------------
--- 2.4.3 Parametric Instructions
-
-data ParametricInstr : Set where
-  drop   : ParametricInstr
-  select : Maybe (List ValType) → ParametricInstr
-
-------------------------------------------------------------------------
--- 2.4.4 Variable Instructions
-
-data VarInstr : Set where
-  local-get  : Indices.LocalIdx → VarInstr
-  local-set  : Indices.LocalIdx → VarInstr
-  local-tee  : Indices.LocalIdx → VarInstr
-  global-get : Indices.GlobalIdx → VarInstr
-  global-set : Indices.GlobalIdx → VarInstr
-
-------------------------------------------------------------------------
--- 2.4.5 Table Instructions
-
-data TableInstr : Set where
-  get  : Indices.TableIdx → TableInstr
-  set  : Indices.TableIdx → TableInstr
-  size : Indices.TableIdx → TableInstr
-  grow : Indices.TableIdx → TableInstr
-  fill : Indices.TableIdx → TableInstr
-  copy : Indices.TableIdx → Indices.TableIdx → TableInstr
-  init : Indices.TableIdx → Indices.ElemIdx → TableInstr
-  drop  : Indices.ElemIdx → TableInstr
-
-------------------------------------------------------------------------
--- 2.4.6 Memory Instructions
-
-record MemArg : Set where
-  field
-    offset : UnsignedInteger 32
-    align  : UnsignedInteger 32
-
-module IntMem (w : BitWidth) where
-  data IntMemInstr : Set where
-    load    : MemArg → IntMemInstr
-    store   : MemArg → IntMemInstr
-    load8   : Signedness → MemArg → IntMemInstr
-    load16  : Signedness → MemArg → IntMemInstr
-    store8  : MemArg → IntMemInstr
-    store16 : MemArg → IntMemInstr
-
-data IntMemInstr : Set where
-  ixx         : ∀ w → IntMem.IntMemInstr w → IntMemInstr
-  i64-load32  : Signedness → MemArg → IntMemInstr
-  i64-store32 : MemArg → IntMemInstr
-
-module FloatMem (w : BitWidth) where
-  data FloatMemInstr : Set where
-    load  : MemArg → FloatMemInstr
-    store : MemArg → FloatMemInstr
-
-FloatMemInstr : Set
-FloatMemInstr = ∃ FloatMem.FloatMemInstr
-
-data MemInstr : Set where
-  int   : IntMemInstr → MemInstr
-  float : FloatMemInstr → MemInstr
-  size  : MemInstr
-  grow  : MemInstr
-  fill  : MemInstr
-  copy  : MemInstr
-  init  : Indices.DataIdx → MemInstr
-  drop  : Indices.DataIdx → MemInstr
-
-------------------------------------------------------------------------
--- 2.4.7 Control Instructions
-
-BlockType : Set
-BlockType = Indices.TypeIdx ⊎ Maybe ValType
-
-data Instr : Set where
-  num           : NumInstr → Instr
-  ref           : RefInstr → Instr
-  parametric    : ParametricInstr → Instr
-  var           : VarInstr → Instr
-  table         : TableInstr → Instr
-  mem           : MemInstr → Instr
-  nop           : Instr
-  unreachable   : Instr
-  block         : BlockType → List Instr → Instr
-  loop          : BlockType → List Instr → Instr
-  if-else       : BlockType → List Instr → List Instr → Instr
-  br            : Indices.LabelIdx → Instr
-  br-if         : Indices.LabelIdx → Instr
-  br-table      : Vec′ Indices.LabelIdx → Indices.LabelIdx → Instr
-  return        : Instr
-  call          : Indices.FuncIdx → Instr
-  call-indirect : Indices.TableIdx → Indices.TypeIdx → Instr
-
-------------------------------------------------------------------------
--- 2.4.8 Expressions
-
-Expr : Set
-Expr = List Instr
diff --git a/src/Wasm/Expression/Modules.agda b/src/Wasm/Expression/Modules.agda
deleted file mode 100644
index 912d6da..0000000
--- a/src/Wasm/Expression/Modules.agda
+++ /dev/null
@@ -1,128 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-------------------------------------------------------------------------
--- 2.5 Modules
-
-module Wasm.Expression.Modules where
-
-open import Data.Maybe using (Maybe)
-open import Wasm.Expression.Types
-open import Wasm.Expression.Utilities using (Vec′; module Indices)
-open import Wasm.Expression.Values using (Byte; Name)
-open import Wasm.Expression.Instructions using (Expr)
-
-------------------------------------------------------------------------
--- 2.5.1 Indices
-
--- NOTE: defined in Wasm.Expression.Utilities
-
-------------------------------------------------------------------------
--- 2.5.2 Types
-
--- NOTE: no new definitions
-
-------------------------------------------------------------------------
--- 2.5.3 Functions
-
-record Func : Set where
-  field
-    type   : Indices.TypeIdx
-    locals : Vec′ ValType
-    body   : Expr
-
-------------------------------------------------------------------------
--- 2.5.4 Tables
-
-Table : Set
-Table = TableType
-
-------------------------------------------------------------------------
--- 2.5.5 Memories
-
-Mem : Set
-Mem = MemType
-
-------------------------------------------------------------------------
--- 2.5.6 Globals
-
-record Global : Set where
-  field
-    type : GlobalType
-    init : Expr
-
-------------------------------------------------------------------------
--- 2.5.7 Element Segments
-
-data ElemMode : Set where
-  passive     : ElemMode
-  active      : (table : Indices.TableIdx) → (offset : Expr) → ElemMode
-  declarative : ElemMode
-
-record Elem : Set where
-  field
-    type : RefType
-    init : Vec′ Expr
-    mode : ElemMode
-
-------------------------------------------------------------------------
--- 2.5.8 Data Segments
-
-data DataMode : Set where
-  passive : DataMode
-  active  : (memory : Indices.MemIdx) → (offset : Expr) → DataMode
-
-record Data : Set where
-  field
-    init : Vec′ Byte
-    mode : DataMode
-
-------------------------------------------------------------------------
--- 2.5.9 Start Function
-
-Start : Set
-Start = Indices.FuncIdx
-
-------------------------------------------------------------------------
--- 2.5.10 Exports
-
-data ExportDesc : Set where
-  func   : Indices.FuncIdx → ExportDesc
-  table  : Indices.TableIdx → ExportDesc
-  mem    : Indices.MemIdx → ExportDesc
-  global : Indices.GlobalIdx → ExportDesc
-
-record Export : Set where
-  field
-    name : Name
-    desc : ExportDesc
-
-------------------------------------------------------------------------
--- 2.5.11 Imports
-
-data ImportDesc : Set where
-  func   : Indices.TypeIdx → ImportDesc
-  table  : TableType → ImportDesc
-  mem    : MemType → ImportDesc
-  global : GlobalType → ImportDesc
-
-record Import : Set where
-  field
-    mod  : Name
-    name : Name
-    desc : ImportDesc
-
-------------------------------------------------------------------------
--- Module definition
-
-record Mod : Set where
-  field
-    types   : Vec′ FuncType
-    funcs   : Vec′ Func
-    tables  : Vec′ Table
-    mems    : Vec′ Mem
-    globals : Vec′ Global
-    elems   : Vec′ Elem
-    datas   : Vec′ Data
-    start   : Maybe Start
-    imports : Vec′ Import
-    exports : Vec′ Export
diff --git a/src/Wasm/Expression/Types.agda b/src/Wasm/Expression/Types.agda
deleted file mode 100644
index 02661e8..0000000
--- a/src/Wasm/Expression/Types.agda
+++ /dev/null
@@ -1,112 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-------------------------------------------------------------------------
--- 2.3 Types
-
-module Wasm.Expression.Types where
-
-open import Data.Maybe using (Maybe; just; nothing)
-open import Data.Product using (_×_)
-open import Data.Sum using (_⊎_)
-open import Wasm.Expression.Values using (UnsignedInteger)
-open import Wasm.Expression.Utilities using (Vec′)
-
-------------------------------------------------------------------------
--- 2.3.1 Number Types
-
-data NumType : Set where
-  i32 : NumType
-  i64 : NumType
-  f32 : NumType
-  f64 : NumType
-
-------------------------------------------------------------------------
--- 2.3.2 Reference Types
-
-data RefType : Set where
-  funcref   : RefType
-  externref : RefType
-
-------------------------------------------------------------------------
--- 2.3.3 Value Types
-
-ValType : Set
-ValType = NumType ⊎ RefType
-
-------------------------------------------------------------------------
--- 2.3.4 Result Types
-
-ResultType : Set
-ResultType = Vec′ ValType
-
-------------------------------------------------------------------------
--- 2.3.5 Function Types
-
-record FuncType : Set where
-  constructor _⟶_
-  field
-    from : ResultType
-    to   : ResultType
-
-------------------------------------------------------------------------
--- 2.3.6 Limits
-
-record Limits : Set where
-  field
-    min : UnsignedInteger 32
-    max : Maybe (UnsignedInteger 32)
-
-------------------------------------------------------------------------
--- 2.3.7 Memory Types
-
-MemType : Set
-MemType = Limits
-
-------------------------------------------------------------------------
--- 2.3.8 Table Types
-
-TableType : Set
-TableType = Limits × RefType
-
-------------------------------------------------------------------------
--- 2.3.9 Global Types
-
-data Mut : Set where
-  const : Mut
-  var   : Mut
-
-GlobalType : Set
-GlobalType = Mut × ValType
-
-------------------------------------------------------------------------
--- 2.3.10 External Types
-
-data ExternType : Set where
-  func   : FuncType → ExternType
-  table  : TableType → ExternType
-  mem    : MemType → ExternType
-  global : GlobalType → ExternType
-
-func? : ExternType → Maybe FuncType
-func? (func t)   = just t
-func? (table t)  = nothing
-func? (mem t)    = nothing
-func? (global t) = nothing
-
-table? : ExternType → Maybe TableType
-table? (func t)   = nothing
-table? (table t)  = just t
-table? (mem t)    = nothing
-table? (global t) = nothing
-
-mem? : ExternType → Maybe MemType
-mem? (func t)   = nothing
-mem? (table t)  = nothing
-mem? (mem t)    = just t
-mem? (global t) = nothing
-
-global? : ExternType → Maybe GlobalType
-global? (func t)   = nothing
-global? (table t)  = nothing
-global? (mem t)    = nothing
-global? (global t) = just t
diff --git a/src/Wasm/Expression/Utilities.agda b/src/Wasm/Expression/Utilities.agda
deleted file mode 100644
index 129af14..0000000
--- a/src/Wasm/Expression/Utilities.agda
+++ /dev/null
@@ -1,52 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-module Wasm.Expression.Utilities where
-
-open import Data.Fin using (Fin)
-open import Data.Nat using (ℕ; _^_)
-open import Data.Vec.Bounded using (Vec≤)
-open import Wasm.Constants
-
-Vec′ : ∀ {a} → Set a → Set a
-Vec′ A = Vec≤ A 2^32
-
-data Signedness : Set where
-  Signed   : Signedness
-  Unsigned : Signedness
-
-data BitWidth : Set where
-  32Bit : BitWidth
-  64Bit : BitWidth
-
-module BitWidth′ where
-  toℕ : BitWidth → ℕ
-  toℕ 32Bit = 32
-  toℕ 64Bit = 64
-
-module Indices where
-  TypeIdx : Set
-  TypeIdx = Fin 2^32
-
-  FuncIdx : Set
-  FuncIdx = Fin 2^32
-
-  TableIdx : Set
-  TableIdx = Fin 2^32
-
-  MemIdx : Set
-  MemIdx = Fin 2^32
-
-  GlobalIdx : Set
-  GlobalIdx = Fin 2^32
-
-  ElemIdx : Set
-  ElemIdx = Fin 2^32
-
-  DataIdx : Set
-  DataIdx = Fin 2^32
-
-  LocalIdx : Set
-  LocalIdx = Fin 2^32
-
-  LabelIdx : Set
-  LabelIdx = Fin 2^32
diff --git a/src/Wasm/Expression/Values.agda b/src/Wasm/Expression/Values.agda
deleted file mode 100644
index 283e325..0000000
--- a/src/Wasm/Expression/Values.agda
+++ /dev/null
@@ -1,122 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-------------------------------------------------------------------------
--- 2.2 Values
-
-module Wasm.Expression.Values where
-
-open import Data.Char using (Char; toℕ)
-open import Data.Empty using (⊥)
-open import Data.Fin using (Fin)
-open import Data.Nat using (ℕ; zero; suc; _^_; pred)
-open import Wasm.Constants
-open import Wasm.Expression.Utilities using (BitWidth; 32Bit; 64Bit)
-
-infix 8 +_ -_
-
-------------------------------------------------------------------------
--- 2.2.1 Bytes
-
-Byte : Set
-Byte = Fin 256
-
-------------------------------------------------------------------------
--- 2.2.2 Integers
-
-UnsignedInteger : ℕ → Set
-UnsignedInteger n = Fin (2 ^ n)
-
-data SignedInteger : ℕ → Set where
-  +_     : ∀ {n} → Fin n → SignedInteger (suc n)
-  -[1+_] : ∀ {n} → Fin n → SignedInteger (suc n)
-
-UninterpretedInteger : ℕ → Set
-UninterpretedInteger = UnsignedInteger
-
-------------------------------------------------------------------------
--- 2.2.3 Floating-Point
-
-signif : BitWidth → ℕ
-signif 32Bit = 23
-signif 64Bit = 52
-
-expon : BitWidth → ℕ
-expon 32Bit = 8
-expon 64Bit = 11
-
-data FloatMag : BitWidth → Set where
-  nan       : ∀ {w} → (n : Fin (pred (2 ^ (signif w)))) → FloatMag w
-  ∞         : ∀ {w} → FloatMag w
-  normal    : ∀ {w} → (e : Fin (pred (pred (2 ^ (expon w))))) → (t : Fin (2 ^ (signif w))) → FloatMag w
-  subnormal : ∀ {w} → (t : Fin (pred (2 ^ (signif w)))) → FloatMag w
-  zero      : ∀ {w} → FloatMag w
-
-data Float : BitWidth → Set where
-  +_ : ∀ {w} → FloatMag w → Float w
-  -_ : ∀ {w} → FloatMag w → Float w
-
-------------------------------------------------------------------------
--- 2.2.4 Names
-
-module _ where
-  open import Data.Bool using (Bool; true; false; if_then_else_)
-  open import Data.List using (List; []; _∷_; length; map; sum)
-  open import Data.Nat using (_≤ᵇ_; _<_; z≤n; s≤s)
-  open import Data.Nat.Properties using (≤-step)
-  open import Data.Product using (_×_; _,_; proj₂; map₂)
-  open import Data.String using (String; toList)
-
-  halfEven? : ℕ → Bool × ℕ
-  halfEven? zero          = true , 0
-  halfEven? (suc zero)    = false , 0
-  halfEven? (suc (suc n)) = map₂ suc (halfEven? n)
-
-  n≢0⇒halfEven?<n : ∀ n → proj₂ (halfEven? (suc n)) < (suc n)
-  n≢0⇒halfEven?<n zero = s≤s z≤n
-  n≢0⇒halfEven?<n (suc zero) = s≤s (n≢0⇒halfEven?<n zero)
-  n≢0⇒halfEven?<n (suc (suc n)) = s≤s (≤-step (n≢0⇒halfEven?<n n))
-
-  asBits : ℕ → List Bool
-  asBits n = All.wfRec <-wellFounded _ Pred helper n
-    where
-    open import Data.Nat.Induction using (<-wellFounded)
-    open import Data.Nat.Properties using (module ≤-Reasoning)
-    open import Induction.WellFounded using (WfRec; module All)
-    open import Relation.Binary.PropositionalEquality using (cong; inspect; [_])
-
-    open ≤-Reasoning
-
-    Pred : ℕ → Set
-    Pred n = List Bool
-
-    helper : ∀ n → WfRec _<_ Pred n → List Bool
-    helper zero rec = []
-    helper (suc n) rec with halfEven? (suc n) | inspect halfEven? (suc n)
-    ...                   | true , m  | [ m≡n+1/2 ] = false ∷ rec m (begin-strict
-                                                        m ≡˘⟨ cong proj₂ m≡n+1/2 ⟩
-                                                        proj₂ (halfEven? (suc n)) <⟨ n≢0⇒halfEven?<n n ⟩
-                                                        suc n ∎)
-    ...                   | false , m | [ m≡n/2 ]   = true ∷ rec m (begin-strict
-                                                        m ≡˘⟨ cong proj₂ m≡n/2 ⟩
-                                                        proj₂ (halfEven? (suc n)) <⟨ n≢0⇒halfEven?<n n ⟩
-                                                        suc n ∎)
-
-  utf8Bytes : Char → ℕ
-  utf8Bytes c with asBits (toℕ c)
-  ... | bits = if length bits ≤ᵇ 7 then
-                  1
-               else if length bits ≤ᵇ 11 then
-                  2
-               else if length bits ≤ᵇ 16 then
-                  3
-               else
-                  4
-
-  byteLength : String → ℕ
-  byteLength s = sum (map utf8Bytes (toList s))
-
-  data Name : Set where
-    name : ∀ s → {len : byteLength s < 2^32} → Name
-
-  toString : Name → String
-  toString (name s) = s
diff --git a/src/Wasm/Type.agda b/src/Wasm/Type.agda
new file mode 100644
index 0000000..7a82aa8
--- /dev/null
+++ b/src/Wasm/Type.agda
@@ -0,0 +1,56 @@
+{-# OPTIONS --safe --without-K #-}
+
+module Wasm.Type where
+
+open import Data.Fin using (Fin; Fin′)
+open import Data.List using (List)
+open import Data.Maybe using (Maybe; maybe)
+open import Data.Nat using (ℕ)
+open import Wasm.Value using (I32)
+
+infix 4 _⟶_ _,_
+
+record Limits (k : ℕ) : Set where
+  constructor _,_
+  field
+    max     : Maybe (Fin k)
+    min     : maybe Fin′ (Fin k) max
+
+data NumType : Set where
+  i32 : NumType
+  i64 : NumType
+  f32 : NumType
+  f64 : NumType
+
+data RefType : Set where
+  funcref   : RefType
+  externref : RefType
+
+data ValType : Set where
+  num : NumType → ValType
+  ref : RefType → ValType
+
+record FuncType : Set where
+  constructor _⟶_
+  field
+    from : List ValType
+    to   : List ValType
+
+data Mutability : Set where
+  const : Mutability
+  var   : Mutability
+
+record GlobalType : Set where
+  constructor _,_
+  field
+    mut  : Mutability
+    type : ValType
+
+record TableType : Set where
+  field
+    limits : Limits 4294967295
+    type   : RefType
+
+record MemType : Set where
+  field
+    limits : Limits 65536
diff --git a/src/Wasm/Validation/Context.agda b/src/Wasm/Validation/Context.agda
deleted file mode 100644
index f7c2564..0000000
--- a/src/Wasm/Validation/Context.agda
+++ /dev/null
@@ -1,63 +0,0 @@
-{-# 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
deleted file mode 100644
index 7aa9411..0000000
--- a/src/Wasm/Validation/Instructions.agda
+++ /dev/null
@@ -1,197 +0,0 @@
-{-# 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
deleted file mode 100644
index 1e0ca0a..0000000
--- a/src/Wasm/Validation/Modules.agda
+++ /dev/null
@@ -1,191 +0,0 @@
-{-# 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
deleted file mode 100644
index 3ee78c0..0000000
--- a/src/Wasm/Validation/Types.agda
+++ /dev/null
@@ -1,95 +0,0 @@
-{-# 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ℓ
-_≤ᵍ_ = _≡_
diff --git a/src/Wasm/Value.agda b/src/Wasm/Value.agda
new file mode 100644
index 0000000..9dfc24e
--- /dev/null
+++ b/src/Wasm/Value.agda
@@ -0,0 +1,24 @@
+{-# OPTIONS --safe --without-K #-}
+
+module Wasm.Value where
+
+open import Data.Fin using (Fin)
+open import Data.String using (String)
+
+Name : Set
+Name = String
+
+Byte : Set
+Byte = Fin 256
+
+I32 : Set
+I32 = Fin 4294967296
+
+I64 : Set
+I64 = Fin 18446744073709551616
+
+F32 : Set
+F32 = Fin 4294967296
+
+F64 : Set
+F64 = Fin 18446744073709551616