Introduce type-safe instances and threadsHEADmaster

1 files changed, 147 insertions, 0 deletions

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 ++ τ ∷ [])