Introduce type-safe instances and threadsHEADmaster

9 files changed, 419 insertions, 188 deletions

diff --git a/src/Wasm/Data.agda b/src/Wasm/Data.agda
index f7ed8da..d849cc6 100644
--- a/src/Wasm/Data.agda
+++ b/src/Wasm/Data.agda
@@ -14,9 +14,12 @@ open import Data.Product using (_×_; _,_; proj₁)
 open import Data.Sum using (_⊎_)
 open import Data.Unit using (⊤)
 open import Data.Vec using (Vec)
+open import Data.Vec.Relation.Unary.Any using () renaming (Any to VecAny)
 open import Function as _ using (_∋_)
 open import Relation.Binary.PropositionalEquality using (_≡_; _≢_)
-open import Wasm.Data.Instruction as Inst using (Expression; Constant)
+open import Wasm.Data.Instruction as Inst using (Expression; SequenceConstant)
+open import Wasm.Util.List.Map using (Map)
+open import Wasm.Util.List.Map.Any using () renaming (Any to MapAny)
 open import Wasm.Value using (Byte; Name)
 open import Wasm.Type
 
@@ -71,89 +74,69 @@ private
     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
+record Function (C : Inst.Context) (τ : FuncType) : Set where
   private
-    module Cₘ = Context Cₘ
-
-  type = lookup Cₘ.funcs idx
-
-  private
-    module type = FuncType type
+    module τ = FuncType τ
 
   field
     locals : List ValType
 
   private
-    C = Inst.Context ∋ record (makeContext Cᵢ Cₘ refs)
-      { locals  = type.from ++ locals
-      ; labels  = type.to ∷ []
-      ; return  = just type.to
+    C′ = Inst.Context ∋ record C
+      { locals  = τ.from ++ locals
+      ; labels  = τ.to ∷ []
+      ; return  = just τ.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
+    body : Expression C′ τ.to
 
+record Global (C : Inst.Context) (τ : GlobalType) : Set where
   private
-    module type = GlobalType type
+    module τ = GlobalType τ
 
   field
-    {body}   : Expression C (type.type ∷ [])
-    constant : Constant body
+    {body}   : Expression C (τ.type ∷ [])
+    constant : SequenceConstant 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
+GlobalRef : ∀ {C τ} → Global C τ → Fin (length (Inst.Context.funcs C)) → Set
+GlobalRef global x = Inst.SequenceRef (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))
+  active : ∀ table {offset : Expression C (num i32 ∷ [])} → SequenceConstant 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
+  activeRef : ∀ {x} table {offset} constant → Inst.SequenceRef offset x → ElemModeRef (active table {offset} constant) x
 
+record Elem (C : Inst.Context) (τ : RefType) : Set where
   field
-    {inits}  : List (Expression C (ref type ∷ []))
-    constant : All Constant inits
-    mode     : ElemMode C type
+    {inits}  : List (Expression C (ref τ ∷ []))
+    constant : All SequenceConstant inits
+    mode     : ElemMode C τ
 
-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
+data ElemRef {C τ} (elem : Elem C τ) (x : Fin (length (Inst.Context.funcs C))) : Set where
+  initsRef : Any (λ init → Inst.SequenceRef 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
+  active  : ∀ (memory : Fin (length (Inst.Context.mems C))) {offset : Expression C (num i32 ∷ [])} → SequenceConstant 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
+  activeRef : ∀ {x} memory {offset} constant → Inst.SequenceRef 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
+record Data (C : Inst.Context) : Set where
   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 : ∀ {C} → Data C → Fin (length (Inst.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
+record Exports (C : Inst.Context) (Cₑ : ExternTypes) : Set where
   private
-    C = Inst.Context ∋ makeContext Cᵢ Cₘ refs
     module Cₑ = ExternTypes Cₑ
     module C = Inst.Context C
   field
@@ -169,7 +152,7 @@ record Exports (Cᵢ : ExternTypes) (Cₘ : Context) (refs : List (Fin (length (
   field
     namesDisjoint : AllPairs _≢_ names
 
-ExportsRef : ∀ {Cᵢ Cₘ refs Cₑ} → Exports Cᵢ Cₘ refs Cₑ → Fin (length (ExternTypes.funcs Cᵢ ++ Context.funcs Cₘ)) → Set
+ExportsRef : ∀ {C Cₑ} → Exports C Cₑ → Fin (length (Inst.Context.funcs C)) → Set
 ExportsRef exports x = Any (λ (_ , y) → y ≡ x) (Exports.funcs exports)
 
 record Imports (Cᵢ : ExternTypes) : Set where
@@ -181,47 +164,42 @@ record Imports (Cᵢ : ExternTypes) : Set where
     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)))
+    {ft}     : List FuncType
+    tables   : List TableType
+    mems     : List MemType
+    {gt}     : List GlobalType
+    {rt}     : List RefType
+    {#datas} : ℕ
+    start    : Maybe (Fin (length (it.funcs ++ ft)))
+    refs     : List (Fin (length (it.funcs ++ ft)))
   private
     Cₘ = Context ∋ record
       { funcs   = ft
       ; tables  = tables
       ; mems    = mems
-      ; globals = it.globals
+      ; globals = gt
       ; elems   = rt
-      ; datas   = n
+      ; datas   = #datas
       }
+    C′ = makeGlobalContext it Cₘ refs
+
+  C = makeContext it Cₘ refs
+
   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)
+    funcs    : Map (Function C) ft
+    globals  : Map (Global C′) gt
+    elems    : Map (Elem C) rt
+    datas    : Vec (Data C) #datas
     startOk  : maybe (λ x → lookup (it.funcs ++ ft) x ≡ ([] ⟶ [])) ⊤ start
-    exports  : Exports it Cₘ refs et
+    exports  : Exports C 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
+    refsUsed : All (λ i → MapAny (λ g → GlobalRef g i) globals
+                        ⊎ MapAny (λ e → ElemRef e i) elems
+                        ⊎ VecAny (λ d → DataRef d i) datas
                         ⊎ ExportsRef exports i)
                    refs
 
@@ -230,7 +208,9 @@ private
     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 Data.Vec using ([])
     open import Relation.Binary.PropositionalEquality using (refl)
+    open import Wasm.Util.List.Map using (Map; []; _∷_)
     open Inst
 
     addTwoImports : ExternTypes
@@ -241,16 +221,12 @@ private
 
     addTwoModule : Module addTwoImports addTwoExports
     addTwoModule = record
-      { ft = (num i32 ∷ num i32 ∷ [] ⟶ num i32 ∷ []) ∷ []
-      ; tables = []
+      { 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))
+        ; body = local-get zero ∙ local-get (suc zero) ∙ i32-binop i32.add ∙ nop
         } ∷ []
       ; globals = []
       ; elems = []
diff --git a/src/Wasm/Data/Instruction.agda b/src/Wasm/Data/Instruction.agda
index 2e56368..8be89c6 100644
--- a/src/Wasm/Data/Instruction.agda
+++ b/src/Wasm/Data/Instruction.agda
@@ -12,6 +12,8 @@ open import Relation.Binary.PropositionalEquality using (_≡_)
 open import Wasm.Type
 open import Wasm.Value
 
+infixr 4 _∙_ _∙₁_ _∙₂_
+
 record Context : Set where
   field
     funcs   : List FuncType
@@ -193,146 +195,155 @@ blockTypeAsFunc {C} (idx τ) = τ
 blockTypeAsFunc (val x) = [] ⟶ x ∷ []
 blockTypeAsFunc nothing = [] ⟶ []
 
-data Instruction : Context → FuncType → Set where
+data Instruction (C : Context) : FuncType → Set
+data Sequence (C : Context) : FuncType → Set
+
+data Instruction C 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 ∷ [])
+  i32-const : (c : I32) → Instruction C ([] ⟶ num i32 ∷ [])
+  i64-const : (c : I64) → Instruction C ([] ⟶ num i64 ∷ [])
+  f32-const : (c : F32) → Instruction C ([] ⟶ num f32 ∷ [])
+  f64-const : (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 ∷ [])
+  i32-unop : (op : i32.Unary) → Instruction C (num i32 ∷ [] ⟶ num i32 ∷ [])
+  i64-unop : (op : i64.Unary) → Instruction C (num i64 ∷ [] ⟶ num i64 ∷ [])
+  f32-unop : (op : f32.Unary) → Instruction C (num f32 ∷ [] ⟶ num f32 ∷ [])
+  f64-unop : (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 ∷ [])
+  i32-binop : (op : i32.Binary) → Instruction C (num i32 ∷ num i32 ∷ [] ⟶ num i32 ∷ [])
+  i64-binop : (op : i64.Binary) → Instruction C (num i64 ∷ num i64 ∷ [] ⟶ num i64 ∷ [])
+  f32-binop : (op : f32.Binary) → Instruction C (num f32 ∷ num f32 ∷ [] ⟶ num f32 ∷ [])
+  f64-binop : (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 ∷ [])
+  i32-testop : (op : i32.Test) → Instruction C (num i32 ∷ [] ⟶ num i32 ∷ [])
+  i64-testop : (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 ∷ [])
+  i32-relop : (op : i32.Rel) → Instruction C (num i32 ∷ num i32 ∷ [] ⟶ num i32 ∷ [])
+  i64-relop : (op : i64.Rel) → Instruction C (num i64 ∷ num i64 ∷ [] ⟶ num i32 ∷ [])
+  f32-relop : (op : f32.Rel) → Instruction C (num f32 ∷ num f32 ∷ [] ⟶ num i32 ∷ [])
+  f64-relop : (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 ∷ [])
+  i32-cvtop : ∀ {τ} → (op : i32.Convert τ) → Instruction C (num τ ∷ [] ⟶ num i32 ∷ [])
+  i64-cvtop : ∀ {τ} → (op : i64.Convert τ) → Instruction C (num τ ∷ [] ⟶ num i64 ∷ [])
+  f32-cvtop : ∀ {τ} → (op : f32.Convert τ) → Instruction C (num τ ∷ [] ⟶ num f32 ∷ [])
+  f64-cvtop : ∀ {τ} → (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 ∷ [])
+  ref-null : ∀ τ → Instruction C ([] ⟶ ref τ ∷ [])
+  ref-is-null : ∀ {τ} → Instruction C (ref τ ∷ [] ⟶ num i32 ∷ [])
+  ref-func : ∀ {x} → (x∈refs : x ∈ Context.refs C) → Instruction C ([] ⟶ ref funcref ∷ [])
 
   ---- Parametric instructions
-  drop : ∀ {C τ} → Instruction C (τ ∷ [] ⟶ [])
-  select : ∀ {C τ} → Instruction C (num i32 ∷ τ ∷ τ ∷ [] ⟶ τ ∷ [])
+  drop : ∀ {τ} → Instruction C (τ ∷ [] ⟶ [])
+  select : ∀ {τ} → 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 ∷ [] ⟶ [])
+  local-get : ∀ x → Instruction C ([] ⟶ lookup (Context.locals C) x ∷ [])
+  local-set : ∀ x → Instruction C (lookup (Context.locals C) x ∷ [] ⟶ [])
+  local-tee : ∀ x → Instruction C (lookup (Context.locals C) x ∷ [] ⟶ lookup (Context.locals C) x ∷ [])
+  global-get : ∀ x → Instruction C ([] ⟶ GlobalType.type (lookup (Context.globals C) x) ∷ [])
+  global-set : ∀ 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 ([] ⟶ [])
+  table-get : ∀ x → Instruction C (num i32 ∷ [] ⟶ ref (TableType.type (lookup (Context.tables C) x)) ∷ [])
+  table-set : ∀ x → Instruction C (ref (TableType.type (lookup (Context.tables C) x)) ∷ num i32 ∷ [] ⟶ [])
+  table-size : ∀ (x : Fin (length (Context.tables C))) → Instruction C ([] ⟶ num i32 ∷ [])
+  table-grow : ∀ x → Instruction C (num i32 ∷ ref (TableType.type (lookup (Context.tables C) x)) ∷ [] ⟶ num i32 ∷ [])
+  table-fill : ∀ x → Instruction C (num i32 ∷ ref (TableType.type (lookup (Context.tables C) x)) ∷ num i32 ∷ [] ⟶ [])
+  table-copy : ∀ 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 : ∀ x y → TableType.type (lookup (Context.tables C) x) ≡ lookup (Context.elems C) y → Instruction C (num i32 ∷ num i32 ∷ num i32 ∷ [] ⟶ [])
+  elem-drop : ∀ (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 ∷ [])
+  i32-load : ∀ (m : MemArg 2) → length (Context.mems C) > 0 → Instruction C (num i32 ∷ [] ⟶ num i32 ∷ [])
+  i64-load : ∀ (m : MemArg 3) → length (Context.mems C) > 0 → Instruction C (num i32 ∷ [] ⟶ num i64 ∷ [])
+  f32-load : ∀ (m : MemArg 2) → length (Context.mems C) > 0 → Instruction C (num i32 ∷ [] ⟶ num f32 ∷ [])
+  f64-load : ∀ (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 ∷ [])
+  i32-load8 : ∀ (m : MemArg 0) → length (Context.mems C) > 0 → Signedness → Instruction C (num i32 ∷ [] ⟶ num i32 ∷ [])
+  i32-load16 : ∀ (m : MemArg 1) → length (Context.mems C) > 0 → Signedness → Instruction C (num i32 ∷ [] ⟶ num i32 ∷ [])
+  i64-load8 : ∀ (m : MemArg 0) → length (Context.mems C) > 0 → Signedness → Instruction C (num i32 ∷ [] ⟶ num i64 ∷ [])
+  i64-load16 : ∀ (m : MemArg 1) → length (Context.mems C) > 0 → Signedness → Instruction C (num i32 ∷ [] ⟶ num i64 ∷ [])
+  i64-load32 : ∀ (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 ∷ [] ⟶ [])
+  i32-store : ∀ (m : MemArg 2) → length (Context.mems C) > 0 → Instruction C (num i32 ∷ num i32 ∷ [] ⟶ [])
+  i64-store : ∀ (m : MemArg 3) → length (Context.mems C) > 0 → Instruction C (num i64 ∷ num i32 ∷ [] ⟶ [])
+  f32-store : ∀ (m : MemArg 2) → length (Context.mems C) > 0 → Instruction C (num f32 ∷ num i32 ∷ [] ⟶ [])
+  f64-store : ∀ (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 ∷ [] ⟶ [])
+  i32-store8 : ∀ (m : MemArg 0) → length (Context.mems C) > 0 → Signedness → Instruction C (num i32 ∷ num i32 ∷ [] ⟶ [])
+  i32-store16 : ∀ (m : MemArg 1) → length (Context.mems C) > 0 → Signedness → Instruction C (num i32 ∷ num i32 ∷ [] ⟶ [])
+  i64-store8 : ∀ (m : MemArg 0) → length (Context.mems C) > 0 → Signedness → Instruction C (num i64 ∷ num i32 ∷ [] ⟶ [])
+  i64-store16 : ∀ (m : MemArg 1) → length (Context.mems C) > 0 → Signedness → Instruction C (num i64 ∷ num i32 ∷ [] ⟶ [])
+  i64-store32 : ∀ (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 ([] ⟶ [])
+  memory-size : length (Context.mems C) > 0 → Instruction C ([] ⟶ num i32 ∷ [])
+  memory-grow : length (Context.mems C) > 0 → Instruction C (num i32 ∷ [] ⟶ num i32 ∷ [])
+  memory-fill : length (Context.mems C) > 0 → Instruction C (num i32 ∷ num i32 ∷ num i32 ∷ [] ⟶ [])
+  memory-copy : length (Context.mems C) > 0 → Instruction C (num i32 ∷ num i32 ∷ num i32 ∷ [] ⟶ [])
+  memory-init : (x : Fin (Context.datas C)) → length (Context.mems C) > 0 → Instruction C (num i32 ∷ num i32 ∷ num i32 ∷ [] ⟶ [])
+  data-drop : (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 (τ₁ ⟶ τ₃)
+  block : (bt : BlockType C) → let τ = blockTypeAsFunc bt in
+    Sequence (record C {labels = FuncType.to τ ∷ Context.labels C}) τ → Instruction C τ
+  loop : (bt : BlockType C) → let τ = blockTypeAsFunc bt in
+    Sequence (record C {labels = FuncType.from τ ∷ Context.labels C}) τ → Instruction C τ
+  if : (bt : BlockType C) → let τ = blockTypeAsFunc bt in
+    (then else : Sequence (record C {labels = FuncType.to τ ∷ Context.labels C}) τ) → Instruction C (num i32 ∷ FuncType.from τ ⟶ FuncType.to τ)
+  br_if : ∀ l → let τ = lookup (Context.labels C) l in Instruction C (num i32 ∷ τ ⟶ τ)
+  call : ∀ x → Instruction C (lookup (Context.funcs C) x)
+  call_indirect : ∀ x τ → TableType.type (lookup (Context.tables C) x) ≡ funcref → Instruction C (num i32 ∷ FuncType.from τ ⟶ FuncType.to τ)
+
+data Sequence C where
+  nop         : ∀ {τ} → Sequence C (τ ⟶ τ)
+  unreachable : ∀ {τ} → Sequence C τ
+  br          : ∀ {τ₁ τ₂} l → Sequence C (lookup (Context.labels C) l ++ τ₁ ⟶ τ₂)
+  br_table    : ∀ {τ₁ τ₂} ls l → let τ = lookup (Context.labels C) l in All (λ l → lookup (Context.labels C) l ≡ τ) ls → Sequence C (τ ++ τ₁ ⟶ τ₂)
+  return      : ∀ {τ τ₁ τ₂} → Context.return C ≡ just τ → Sequence C (τ ++ τ₁ ⟶ τ₂)
+  _∙_         : ∀ {τ₀ τ₁ τ₂ τ₃} → Instruction C (τ₁ ⟶ τ₂) → Sequence C (τ₂ ++ τ₀ ⟶ τ₃) → Sequence C (τ₁ ++ τ₀ ⟶ τ₃)
 
 Expression : Context → List ValType → Set
-Expression C τ = Instruction C ([] ⟶ τ)
+Expression C τ = Sequence C ([] ⟶ τ)
 
-data InstructionRef {C} : ∀ {τ} → Instruction C τ → Fin (length (Context.funcs C)) → Set where
+data InstructionRef {C} : ∀ {τ} → Instruction C τ → Fin (length (Context.funcs C)) → Set
+data SequenceRef {C} : ∀ {τ} → Sequence C τ → Fin (length (Context.funcs C)) → Set
+
+data InstructionRef {C} where
   ---- Direct
   ref-func : ∀ {x} x∈refs → InstructionRef (ref-func {C} {x} x∈refs) x
   call     : ∀ x → InstructionRef (call {C} x) x
 
   ---- Structural
-  block : ∀ {x} bt {i} → InstructionRef i x → InstructionRef (block {C} bt i) x
-  loop : ∀ {x} bt {i} → InstructionRef i x → InstructionRef (loop {C} bt i) x
-  if₁ : ∀ {x} bt {i₁} → InstructionRef i₁ x → ∀ i₂ → InstructionRef (if {C} bt i₁ i₂) x
-  if₂ : ∀ {x} bt i₁ {i₂} → InstructionRef i₂ x → InstructionRef (if {C} bt i₁ i₂) x
-  frame : ∀ {x τ τ₁ τ₂} {i} → InstructionRef i x → InstructionRef (frame {C} {τ} {τ₁} {τ₂} i) x
-  seq₁ : ∀ {x τ₁ τ₂ τ₃} {i₁} → InstructionRef i₁ x → ∀ i₂ → InstructionRef (seq {C} {τ₁} {τ₂} {τ₃} i₁ i₂) x
-  seq₂ : ∀ {x τ₁ τ₂ τ₃} i₁ {i₂} → InstructionRef i₂ x → InstructionRef (seq {C} {τ₁} {τ₂} {τ₃} i₁ i₂) x
-
-data Constant {C} : ∀ {τ} → Instruction C τ → Set where
+  block : ∀ {x} bt {i} → SequenceRef i x → InstructionRef (block {C} bt i) x
+  loop : ∀ {x} bt {i} → SequenceRef i x → InstructionRef (loop {C} bt i) x
+  if₁ : ∀ {x} bt {i₁} → SequenceRef i₁ x → ∀ i₂ → InstructionRef (if {C} bt i₁ i₂) x
+  if₂ : ∀ {x} bt i₁ {i₂} → SequenceRef i₂ x → InstructionRef (if {C} bt i₁ i₂) x
+
+data SequenceRef {C} where
+  _∙₁_ : ∀ {x τ₀ τ₁ τ₂ τ₃ i} → InstructionRef i x → ∀ i* → SequenceRef (_∙_ {C} {τ₀} {τ₁} {τ₂} {τ₃} i i*) x
+  _∙₂_ : ∀ {x τ₀ τ₁ τ₂ τ₃} i {i*} → SequenceRef i* x → SequenceRef (_∙_ {C} {τ₀} {τ₁} {τ₂} {τ₃} i i*) x
+
+data InstructionConstant {C} : ∀ {τ} → Instruction C τ → Set
+data SequenceConstant {C} : ∀ {τ} → Sequence C τ → Set
+
+data InstructionConstant {C} where
   ---- Direct
   -- const
-  i32-const : ∀ c → Constant (i32-const c)
-  i64-const : ∀ c → Constant (i64-const c)
-  f32-const : ∀ c → Constant (f32-const c)
-  f64-const : ∀ c → Constant (f64-const c)
+  i32-const : ∀ c → InstructionConstant (i32-const c)
+  i64-const : ∀ c → InstructionConstant (i64-const c)
+  f32-const : ∀ c → InstructionConstant (f32-const c)
+  f64-const : ∀ c → InstructionConstant (f64-const c)
 
   -- refs
-  ref-null : ∀ τ → Constant (ref-null τ)
-  ref-func : ∀ {x} x∈refs → Constant (ref-func {x = x} x∈refs)
+  ref-null : ∀ τ → InstructionConstant (ref-null τ)
+  ref-func : ∀ {x} x∈refs → InstructionConstant (ref-func {x = x} x∈refs)
 
   -- global
-  global-get : ∀ {x} → GlobalType.mut (lookup (Context.globals C) x) ≡ const → Constant (global-get x)
+  global-get : ∀ {x} → GlobalType.mut (lookup (Context.globals C) x) ≡ const → InstructionConstant (global-get x)
 
-  ---- Structural
-  frame : ∀ {τ τ₁ τ₂ i} → Constant i → Constant (frame {C} {τ} {τ₁} {τ₂} i)
-  seq   : ∀ {τ₁ τ₂ τ₃ i₁ i₂} → Constant i₁ → Constant i₂ → Constant (seq {C} {τ₁} {τ₂} {τ₃} i₁ i₂)
+data SequenceConstant {C} where
+  nop : ∀ {τ} → SequenceConstant (nop {C} {τ})
+  _∙_ : ∀ {τ₀ τ₁ τ₂ τ₃ i i*} → InstructionConstant i → SequenceConstant i* → SequenceConstant (_∙_ {C} {τ₀} {τ₁} {τ₂} {τ₃} i i*)
diff --git a/src/Wasm/Semantics.agda b/src/Wasm/Semantics.agda
new file mode 100644
index 0000000..68f4219
--- /dev/null
+++ b/src/Wasm/Semantics.agda
@@ -0,0 +1,147 @@
+{-# OPTIONS --safe --without-K #-}
+
+module Wasm.Semantics
+  {a} (ExternAddr : Set a)
+  where
+
+open import Data.Fin using (Fin; zero; toℕ; inject≤)
+open import Data.List using (List; []; _∷_; _++_; length; lookup; allFin)
+open import Data.List.Relation.Unary.Linked using (Linked)
+open import Data.Maybe using (Maybe; maybe; map)
+open import Data.Nat using (ℕ; _≤_; _≥?_; _≤?_)
+open import Data.Product using (_×_; ∃; ∃₂; _,_; proj₁; proj₂)
+open import Data.Sum using (_⊎_)
+open import Data.Unit using (⊤)
+open import Data.Vec as Vec using (Vec)
+open import Level using () renaming (suc to ℓsuc)
+open import Relation.Binary using (REL)
+open import Relation.Binary.PropositionalEquality using (_≡_; cong; subst; module ≡-Reasoning)
+open import Relation.Nary using (substₙ)
+open import Relation.Nullary.Decidable using (True)
+open import Wasm.Data
+open import Wasm.Type hiding (_,_)
+open import Wasm.Util.List.Map as Map using (Map)
+open import Wasm.Util.List.Prefix as Prefix using (Prefix; length≤) renaming (Map to PrefixMap)
+open import Wasm.Value
+
+open import Wasm.Data.Instruction as Inst using ()
+
+record StoreTypes : Set₁ where
+  field
+    hostFuncs : List FuncType
+    funcs     : List FuncType
+    tables    : List TableType
+    mems      : List MemType
+    globals   : List GlobalType
+    elems     : List RefType
+    datas     : ℕ
+
+data Num : NumType → Set where
+  i32 : I32 → Num i32
+  i64 : I64 → Num i64
+  f32 : F32 → Num f32
+  f64 : F64 → Num f64
+
+data Ref (S : StoreTypes) : RefType → Set a where
+  null   : ∀ τ → Ref S τ
+  func   : Fin (length (StoreTypes.funcs S)) → Ref S funcref
+  extern : ExternAddr → Ref S externref
+
+data Value (S : StoreTypes) : ValType → Set a where
+  num : ∀ {τ} → Num τ → Value S (num τ)
+  ref : ∀ {τ} → Ref S τ → Value S (ref τ)
+
+default : ∀ {S} τ → Value S τ
+default (num i32) = num (i32 zero)
+default (num i64) = num (i64 zero)
+default (num f32) = num (f32 0f32)
+default (num f64) = num (f64 0f64)
+default (ref τ)   = ref (null τ)
+
+data Result (S : StoreTypes) : List ValType → Set a where
+  [_]  : ∀ {τs} → Map (Value S) τs → Result S τs
+  trap : ∀ {τs} → Result S τs
+
+record ExportsInst (S : StoreTypes) (Cₑ : ExternTypes) : Set where
+  private
+    module S = StoreTypes S
+    module Cₑ = ExternTypes Cₑ
+  field
+    funcs   : Map (λ τ → ∃ λ i → lookup S.funcs i ≡ τ) Cₑ.funcs
+    tables  : Map (λ τ → ∃ λ i → lookup S.tables i ≡ τ) Cₑ.tables
+    mems    : Map (λ τ → ∃ λ i → lookup S.mems i ≡ τ) Cₑ.mems
+    globals : Map (λ τ → ∃ λ i → lookup S.globals i ≡ τ) Cₑ.globals
+
+record ModuleInst (S : StoreTypes) (C : Inst.Context) : Set₁ where
+  private
+    module S = StoreTypes S
+    module C = Inst.Context C
+  field
+    {et}    : ExternTypes
+    funcs   : Map (λ τ → ∃ λ i → lookup S.funcs i ≡ τ) C.funcs
+    tables  : Map (λ τ → ∃ λ i → lookup S.tables i ≡ τ) C.tables
+    mems    : Map (λ τ → ∃ λ i → lookup S.mems i ≡ τ) C.mems
+    globals : Map (λ τ → ∃ λ i → lookup S.globals i ≡ τ) C.globals
+    elems   : Map (λ τ → ∃ λ i → lookup S.elems i ≡ τ) C.elems
+    datas   : Vec (Fin S.datas) C.datas
+    exports : ExportsInst S et
+
+record TableInst (S : StoreTypes) (τ : TableType) : Set a where
+  private
+    module τ = TableType τ
+  field
+    elems      : List (Ref S τ.type)
+    {minBound} : True (length elems ≥? toℕ (Limits.min′ τ.limits))
+    {maxBound} : maybe (λ max → True (length elems ≤? toℕ max)) ⊤ (Limits.max τ.limits)
+
+record MemInst (τ : MemType) : Set where
+  private
+    module τ = MemType τ
+  field
+    pages      : List (Vec Byte 65536)
+    {minBound} : True (length pages ≥? toℕ (Limits.min′ τ.limits))
+    {maxBound} : maybe (λ max → True (length pages ≤? toℕ max)) ⊤ (Limits.max τ.limits)
+
+record WasmFuncInst (S : StoreTypes) (τ : FuncType) : Set₁ where
+  field
+    {context} : Inst.Context
+    modinst   : ModuleInst S context
+    code      : Function context τ
+
+data FunctionInst (S : StoreTypes) (τ : FuncType) : Set₁ where
+  host : ∀ {i} → lookup (StoreTypes.hostFuncs S) i ≡ τ → FunctionInst S τ
+  wasm : WasmFuncInst S τ → FunctionInst S τ
+
+record Store (types : StoreTypes) : Set (ℓsuc a) where
+  inductive
+  private
+    module types = StoreTypes types
+  field
+    funcs   : Map (FunctionInst types) types.funcs
+    tables  : Map (TableInst types) types.tables
+    mems    : Map MemInst types.mems
+    globals : Map (λ g → Value types (GlobalType.type g)) types.globals
+    elems   : Map (λ τ → List (Ref types τ)) types.elems
+    datas   : Vec (List Byte) types.datas
+
+data FrameInstruction (C : Inst.Context) : (stackTy labelTy : List (List ValType)) (τ : FuncType) → Set where
+  [_] : ∀ {τ₁ τ₂ τ₃} → Inst.Sequence (record C {labels = []}) (τ₂ ++ τ₁ ⟶ τ₃) → FrameInstruction C (τ₁ ∷ []) [] (τ₂ ⟶ τ₃)
+  _∷_ : ∀ {τs₁ τs₂ τ₁′ τ₂′ τ′ τ} → let C′ = record C { labels = τ₂′ ∷ (Inst.Context.labels C) } in Inst.Sequence C′ (τ′ ++ τ₁′ ⟶ τ₂′) → FrameInstruction C τs₁ τs₂ (τ₁′ ⟶ τ) → FrameInstruction C (τ₁′ ∷ τs₁) (τ₂′ ∷ τs₂) (τ′ ⟶ τ)
+
+record Frame (S : StoreTypes) (τ : FuncType) : Set (ℓsuc a) where
+  field
+    context   : Inst.Context
+  private
+    module context = Inst.Context context
+  field
+    modinst   : ModuleInst S context
+    {stackTy} : List (List ValType)
+    {labelTy} : List (List ValType)
+    locals    : Map (Value S) (context.locals)
+    stack     : Map (Map (Value S)) stackTy
+    insts     : FrameInstruction context stackTy labelTy τ
+
+record Thread (S : StoreTypes) (τ : List ValType) : Set (ℓsuc a) where
+  field
+    {frameTy} : List (List ValType)
+    frames    : Linked (λ τ₁ τ₂ → Frame S (τ₁ ⟶ τ₂)) ([] ∷ frameTy ++ τ ∷ [])
diff --git a/src/Wasm/Semantics/Instruction.agda b/src/Wasm/Semantics/Instruction.agda
new file mode 100644
index 0000000..5edd58b
--- /dev/null
+++ b/src/Wasm/Semantics/Instruction.agda
@@ -0,0 +1,5 @@
+{-# OPTIONS --safe --without-K #-}
+
+module Wasm.Semantics.Instruction where
+
+
diff --git a/src/Wasm/Type.agda b/src/Wasm/Type.agda
index 7a82aa8..6e94a71 100644
--- a/src/Wasm/Type.agda
+++ b/src/Wasm/Type.agda
@@ -2,9 +2,9 @@
 
 module Wasm.Type where
 
-open import Data.Fin using (Fin; Fin′)
+open import Data.Fin using (Fin; Fin′; inject)
 open import Data.List using (List)
-open import Data.Maybe using (Maybe; maybe)
+open import Data.Maybe using (Maybe; nothing; just; maybe)
 open import Data.Nat using (ℕ)
 open import Wasm.Value using (I32)
 
@@ -16,6 +16,11 @@ record Limits (k : ℕ) : Set where
     max     : Maybe (Fin k)
     min     : maybe Fin′ (Fin k) max
 
+  min′ : Fin k
+  min′ with max     | min
+  ...     | nothing | m = m
+  ...     | just _  | m = inject m
+
 data NumType : Set where
   i32 : NumType
   i64 : NumType
diff --git a/src/Wasm/Util/List/Map.agda b/src/Wasm/Util/List/Map.agda
new file mode 100644
index 0000000..a6da0d0
--- /dev/null
+++ b/src/Wasm/Util/List/Map.agda
@@ -0,0 +1,33 @@
+{-# OPTIONS --safe --without-K #-}
+
+-- List where element types depend on another list.
+module Wasm.Util.List.Map where
+
+open import Data.Fin using (Fin; zero; suc)
+open import Data.List as List using (List; []; _∷_)
+open import Data.Nat using (ℕ)
+open import Level using (Level; _⊔_)
+
+infixr 5 _∷_
+
+private
+  variable
+    a b : Level
+    A : Set a
+    B : A → Set b
+    xs : List A
+
+data Map {A : Set a} (B : A → Set b) : List A → Set (a ⊔ b) where
+  [] : Map B []
+  _∷_ : ∀ {x xs} (y : B x) (ys : Map B xs) → Map B (x ∷ xs)
+
+length : Map B xs → ℕ
+length {xs = xs} ys = List.length xs
+
+lookup : (ys : Map B xs) → (i : Fin (length ys)) → B (List.lookup xs i)
+lookup (y ∷ ys) zero    = y
+lookup (y ∷ ys) (suc i) = lookup ys i
+
+map : ∀ {c} {C : A → Set c} → (∀ {x} → B x → C x) → Map B xs → Map C xs
+map f []       = []
+map f (y ∷ ys) = f y ∷ map f ys
diff --git a/src/Wasm/Util/List/Map/Any.agda b/src/Wasm/Util/List/Map/Any.agda
new file mode 100644
index 0000000..196ecc5
--- /dev/null
+++ b/src/Wasm/Util/List/Map/Any.agda
@@ -0,0 +1,12 @@
+{-# OPTIONS --safe --without-K #-}
+
+module Wasm.Util.List.Map.Any where
+
+open import Data.List using (_∷_)
+open import Level using (_⊔_)
+open import Relation.Unary using (Pred)
+open import Wasm.Util.List.Map
+
+data Any {a b p} {A : Set a} {B : A → Set b} (P : ∀ {x} → Pred (B x) p) : ∀ {xs} → Pred (Map B xs) (a ⊔ b ⊔ p) where
+  here : ∀ {x xs y ys} (py : P y) → Any P {x ∷ xs} (y ∷ ys)
+  there : ∀ {x xs y ys} (pys : Any P ys) → Any P {x ∷ xs} (y ∷ ys)
diff --git a/src/Wasm/Util/List/Prefix.agda b/src/Wasm/Util/List/Prefix.agda
new file mode 100644
index 0000000..6216c39
--- /dev/null
+++ b/src/Wasm/Util/List/Prefix.agda
@@ -0,0 +1,36 @@
+{-# OPTIONS --safe --without-K #-}
+
+module Wasm.Util.List.Prefix where
+
+open import Data.Fin using (Fin; zero; suc; inject≤)
+open import Data.List as L using (List; []; _∷_; _++_; length; take)
+open import Data.List.Relation.Binary.Pointwise using (Pointwise; []; _∷_)
+open import Data.Nat using (_≤_; z≤n; s≤s)
+open import Level using (Level; _⊔_)
+open import Relation.Binary using (Rel)
+open import Relation.Binary.PropositionalEquality using (_≡_)
+open import Wasm.Util.List.Map as M using ([]; _∷_)
+
+private
+  variable
+    a b c q r : Level
+    A : Set a
+    x y : A
+    xs ys : List A
+    R : Rel A r
+
+Prefix : ∀ {A : Set a} (R : Rel A r) (xs ys : List A) → Set (a ⊔ r)
+Prefix R xs ys = Pointwise R xs (take (length xs) ys)
+
+data Map {A : Set a} {B : A → Set b} {C : A → Set c} {R : Rel A r} (Q : ∀ {x y} → R x y → B x → C y → Set q) : Prefix R xs ys → M.Map B xs → M.Map C ys → Set (a ⊔ b ⊔ c ⊔ q ⊔ r) where
+  [] : ∀ {ws : M.Map C ys} → Map Q [] [] ws
+  _∷_ : ∀ {z : B x} {w : C y} {zs : M.Map B xs} {ws : M.Map C ys} {r} {rs} → (q : Q r z w) → (qs : Map Q rs zs ws) → Map Q (r ∷ rs) (z ∷ zs) (w ∷ ws)
+
+length≤ : Prefix R xs ys → length xs ≤ length ys
+length≤ {ys = []}     []            = z≤n
+length≤ {ys = y ∷ ys} []            = z≤n
+length≤ {ys = y ∷ ys} (x∼y ∷ xs∼ys) = s≤s (length≤ xs∼ys)
+
+lookup : ∀ {xs ys} → (rs : Prefix R xs ys) → (i : Fin (length xs)) → R (L.lookup xs i) (L.lookup ys (inject≤ i (length≤ rs)))
+lookup {ys = y ∷ ys} (x∼y ∷ xs∼ys) zero    = x∼y
+lookup {ys = y ∷ ys} (x∼y ∷ xs∼ys) (suc i) = lookup xs∼ys i
diff --git a/src/Wasm/Value.agda b/src/Wasm/Value.agda
index 9dfc24e..b28a5c8 100644
--- a/src/Wasm/Value.agda
+++ b/src/Wasm/Value.agda
@@ -2,7 +2,7 @@
 
 module Wasm.Value where
 
-open import Data.Fin using (Fin)
+open import Data.Fin using (Fin; zero)
 open import Data.String using (String)
 
 Name : Set
@@ -22,3 +22,9 @@ F32 = Fin 4294967296
 
 F64 : Set
 F64 = Fin 18446744073709551616
+
+0f32 : F32
+0f32 = zero
+
+0f64 : F64
+0f64 = zero