Rewrite so only valid modules can be constructed.

4 files changed, 0 insertions, 546 deletions

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ℓ
-_≤ᵍ_ = _≡_