Complete Section 2 - Structure.

5 files changed, 604 insertions, 0 deletions

diff --git a/src/Wasm/Expression/Instructions.agda b/src/Wasm/Expression/Instructions.agda
new file mode 100644
index 0000000..6cd006b
--- /dev/null
+++ b/src/Wasm/Expression/Instructions.agda
@@ -0,0 +1,219 @@
+{-# 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 : 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
+  table-get  : Indices.TableIdx → TableInstr
+  table-set  : Indices.TableIdx → TableInstr
+  table-size : Indices.TableIdx → TableInstr
+  table-grow : Indices.TableIdx → TableInstr
+  table-fill : Indices.TableIdx → TableInstr
+  table-copy : Indices.TableIdx → Indices.TableIdx → TableInstr
+  table-init : Indices.TableIdx → Indices.ElemIdx → TableInstr
+  elem-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
new file mode 100644
index 0000000..912d6da
--- /dev/null
+++ b/src/Wasm/Expression/Modules.agda
@@ -0,0 +1,128 @@
+{-# 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
new file mode 100644
index 0000000..f72df93
--- /dev/null
+++ b/src/Wasm/Expression/Types.agda
@@ -0,0 +1,88 @@
+{-# OPTIONS --without-K --safe #-}
+
+------------------------------------------------------------------------
+-- 2.3 Types
+
+module Wasm.Expression.Types where
+
+open import Data.Maybe using (Maybe)
+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
diff --git a/src/Wasm/Expression/Utilities.agda b/src/Wasm/Expression/Utilities.agda
new file mode 100644
index 0000000..b7f9af4
--- /dev/null
+++ b/src/Wasm/Expression/Utilities.agda
@@ -0,0 +1,51 @@
+{-# 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≤)
+
+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
new file mode 100644
index 0000000..d6bce60
--- /dev/null
+++ b/src/Wasm/Expression/Values.agda
@@ -0,0 +1,118 @@
+{-# 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.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