Complete Section 3 - Validation.

1 files changed, 191 insertions, 0 deletions

diff --git a/src/Wasm/Validation/Modules.agda b/src/Wasm/Validation/Modules.agda
new file mode 100644
index 0000000..1e0ca0a
--- /dev/null
+++ b/src/Wasm/Validation/Modules.agda
@@ -0,0 +1,191 @@
+{-# 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))