Rewrite so only valid modules can be constructed.

1 files changed, 321 insertions, 0 deletions

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