From a3a8a44b4bc0d60164452826645066a5ffed5bc5 Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Wed, 28 Jul 2021 16:56:07 +0100 Subject: Complete Section 3 - Validation. --- src/Wasm/Validation/Modules.agda | 191 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 191 insertions(+) create mode 100644 src/Wasm/Validation/Modules.agda (limited to 'src/Wasm/Validation/Modules.agda') 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)) -- cgit v1.2.3