Rewrite so only valid modules can be constructed.

1 files changed, 0 insertions, 197 deletions

diff --git a/src/Wasm/Validation/Instructions.agda b/src/Wasm/Validation/Instructions.agda
deleted file mode 100644
index 7aa9411..0000000
--- a/src/Wasm/Validation/Instructions.agda
+++ /dev/null
@@ -1,197 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-------------------------------------------------------------------------
--- 3.3 Instructions
-
-module Wasm.Validation.Instructions where
-
-open import Data.Fin using (zero; toℕ)
-open import Data.List using (List; []; _∷_; _++_; map)
-open import Data.List.Membership.Propositional using (_∈_)
-open import Data.List.Relation.Binary.Pointwise using (Pointwise)
-open import Data.List.Relation.Unary.All using (All)
-open import Data.Maybe using (just; nothing)
-open import Data.Nat using (_+_; _^_) renaming (_≤_ to _≤ⁿ_)
-open import Data.Product using (_,_; _×_; ∃)
-open import Data.Sum using (inj₁; inj₂)
-open import Data.Vec.Bounded using (toList)
-open import Level using (0ℓ)
-open import Relation.Binary using (Rel)
-open import Relation.Binary.PropositionalEquality using (_≡_)
-open import Wasm.Expression.Instructions
-open import Wasm.Expression.Types
-open import Wasm.Expression.Utilities using (BitWidth; 32Bit; 64Bit; module BitWidth′)
-open import Wasm.Validation.Context
-open import Wasm.Validation.Types
-
-infix 4 _≤_ _⟶_
-
-data OpdType : Set where
-  [_] : ValType → OpdType
-  ⊥   : OpdType
-
-record StackType : Set where
-  constructor _⟶_
-  field
-    from : List OpdType
-    to   : List OpdType
-
-fromResult : ResultType → List OpdType
-fromResult t = map [_] (toList t)
-
-fromFunc : FuncType → StackType
-fromFunc (from ⟶ to) = fromResult from ⟶ fromResult to
-
-data _≤_ : Rel OpdType 0ℓ where
-  ⊥≤τ  : ∀ {τ} → ⊥ ≤ τ
-  refl : ∀ {τ τ′} → τ ≡ τ′ → τ ≤ τ′
-
-------------------------------------------------------------------------
--- 3.3.1 Numeric Instructions
-
-intType : BitWidth → OpdType
-intType 32Bit = [ inj₁ i32 ]
-intType 64Bit = [ inj₁ i64 ]
-
-floatType : BitWidth → OpdType
-floatType 32Bit = [ inj₁ f32 ]
-floatType 64Bit = [ inj₁ f64 ]
-
-typeOfNum : NumInstr → StackType
-typeOfNum (int (ixx w (IntOp.const _))) = [] ⟶ intType w ∷ []
-typeOfNum (int (ixx w (IntOp.iunop _))) = intType w ∷ [] ⟶ intType w ∷ []
-typeOfNum (int (ixx w (IntOp.ibinop _))) = intType w ∷ intType w ∷ [] ⟶ intType w ∷ []
-typeOfNum (int (ixx w (IntOp.itestop _))) = intType w ∷ [] ⟶ [ inj₁ i32 ] ∷ []
-typeOfNum (int (ixx w (IntOp.irelop _))) = intType w ∷ intType w ∷ [] ⟶ [ inj₁ i32 ] ∷ []
-typeOfNum (int (ixx w IntOp.extend8-s)) = intType w ∷ [] ⟶ intType w ∷ []
-typeOfNum (int (ixx w IntOp.extend16-s)) = intType w ∷ [] ⟶ intType w ∷ []
-typeOfNum (int (ixx w (IntOp.trunc-f w′ _))) = floatType w′ ∷ [] ⟶ intType w ∷ []
-typeOfNum (int (ixx w (IntOp.trunc-sat-f w′ _))) = floatType w′ ∷ [] ⟶ intType w ∷ []
-typeOfNum (int (ixx w IntOp.reinterpret-f)) = floatType w ∷ [] ⟶ intType w ∷ []
-typeOfNum (int i64-extend32-s) = [ inj₁ i64 ] ∷ [] ⟶ [ inj₁ i64 ] ∷ []
-typeOfNum (int i32-wrap-i64) = [ inj₁ i64 ] ∷ [] ⟶ [ inj₁ i32 ] ∷ []
-typeOfNum (int (i64-extend-i32 _)) = [ inj₁ i32 ] ∷ [] ⟶ [ inj₁ i64 ] ∷ []
-typeOfNum (float (fxx w (FloatOp.const _))) = [] ⟶ floatType w ∷ []
-typeOfNum (float (fxx w (FloatOp.funop _))) = floatType w ∷ [] ⟶ floatType w ∷ []
-typeOfNum (float (fxx w (FloatOp.fbinop _))) = floatType w ∷ floatType w ∷ [] ⟶ floatType w ∷ []
-typeOfNum (float (fxx w (FloatOp.frelop _))) = floatType w ∷ floatType w ∷ [] ⟶ [ inj₁ i32 ] ∷ []
-typeOfNum (float (fxx w (FloatOp.convert-i w′ _))) = intType w′ ∷ [] ⟶ floatType w ∷ []
-typeOfNum (float (fxx w FloatOp.reinterpret-i)) = intType w ∷ [] ⟶ floatType w ∷ []
-typeOfNum (float f32-demote-f64) = [ inj₁ f64 ] ∷ [] ⟶ [ inj₁ f32 ] ∷ []
-typeOfNum (float f64-promote-f32) = [ inj₁ f32 ] ∷ [] ⟶ [ inj₁ f64 ] ∷ []
-
-------------------------------------------------------------------------
--- 3.3.2 Reference Instructions
-
-data RefInstrType : Context → RefInstr → StackType → Set where
-  null : ∀ {C t} → RefInstrType C (null t) ([] ⟶ [ inj₂ t ] ∷ [])
-  is-null : ∀ {C t} → RefInstrType C is-null ([ inj₂ t ] ∷ [] ⟶ [ inj₁ i32 ] ∷ [])
-  func : ∀ {C x t} → Context.getFunc C x ≡ just t → x ∈ Context.refs C → RefInstrType C (func x) ([] ⟶ [ inj₂ funcref ] ∷ [])
-
-------------------------------------------------------------------------
--- 3.3.3 Parametric Instructions
-
-data ParametricInstrType : Context → ParametricInstr → StackType → Set where
-  drop : ∀ {C t} → ParametricInstrType C drop ([ t ] ∷ [] ⟶ [])
-  select-t : ∀ {C t} → ParametricInstrType C (select (just (t ∷ []))) ([ inj₁ i32 ] ∷ [ t ] ∷ [ t ] ∷ [] ⟶ [ t ] ∷ [])
-  select-no-t : ∀ {C t} → ParametricInstrType C (select nothing) ([ inj₁ i32 ] ∷ [ inj₁ t ] ∷ [ inj₁  t ] ∷ [] ⟶ [ inj₁ t ] ∷ [])
-
-------------------------------------------------------------------------
--- 3.3.4 Variable Instructions
-
-data VarInstrType : Context → VarInstr → StackType → Set where
-  local-get : ∀ {C x t} → Context.getLocal C x ≡ just t → VarInstrType C (local-get x) ([] ⟶ [ t ] ∷ [])
-  local-set : ∀ {C x t} → Context.getLocal C x ≡ just t → VarInstrType C (local-set x) ([ t ] ∷ [] ⟶ [])
-  local-tee : ∀ {C x t} → Context.getLocal C x ≡ just t → VarInstrType C (local-tee x) ([ t ] ∷ [] ⟶ [ t ] ∷ [])
-  global-get : ∀ {C x m t} → Context.getGlobal C x ≡ just (m , t) → VarInstrType C (global-get x) ([] ⟶ [ t ] ∷ [])
-  global-set : ∀ {C x t} → Context.getGlobal C x ≡ just (var , t) → VarInstrType C (global-set x) ([ t ] ∷ [] ⟶ [])
-
-------------------------------------------------------------------------
--- 3.3.5 Table Instructions
-
-data TableInstrType : Context → TableInstr → StackType → Set where
-  get : ∀ {C x lim t} → Context.getTable C x ≡ just (lim , t) → TableInstrType C (get x) ([ inj₁ i32 ] ∷ [] ⟶ [ inj₂ t ] ∷ [])
-  set : ∀ {C x lim t} → Context.getTable C x ≡ just (lim , t) → TableInstrType C (set x) ([ inj₂ t ] ∷ [ inj₁ i32 ] ∷ [] ⟶ [])
-  size : ∀ {C x lim,t} → Context.getTable C x ≡ just lim,t → TableInstrType C (size x) ([] ⟶ [ inj₁ i32 ] ∷ [])
-  grow : ∀ {C x lim t} → Context.getTable C x ≡ just (lim , t) → TableInstrType C (grow x) ([ inj₁ i32 ] ∷ [ inj₂ t ] ∷ [] ⟶ [ inj₁ i32 ] ∷ [])
-  fill : ∀ {C x lim t} → Context.getTable C x ≡ just (lim , t) → TableInstrType C (fill x) ([ inj₁ i32 ] ∷ [ inj₂ t ] ∷ [ inj₁ i32 ] ∷ [] ⟶ [])
-  copy : ∀ {C x y lim₁ lim₂ t} → Context.getTable C x ≡ just (lim₁ , t) → Context.getTable C y ≡ just (lim₂ , t) → TableInstrType C (copy x y) ([ inj₁ i32 ] ∷ [ inj₁ i32 ] ∷ [ inj₁ i32 ] ∷ [] ⟶ [])
-  init : ∀ {C x y lim₁ t} → Context.getTable C x ≡ just (lim₁ , t) → Context.getElem C y ≡ just t → TableInstrType C (init x y) ([ inj₁ i32 ] ∷ [ inj₁ i32 ] ∷ [ inj₁ i32 ] ∷ [] ⟶ [])
-  drop : ∀ {C x t} → Context.getElem C x ≡ just t → TableInstrType C (drop x) ([] ⟶ [])
-
-------------------------------------------------------------------------
--- 3.3.6 Memory Instructions
-
-data MemInstrType : Context → MemInstr → StackType → Set where
-  int-load : ∀ {C w arg lim} → Context.getMem C zero ≡ just lim → 2 ^ (3 + toℕ (MemArg.align arg)) ≤ⁿ BitWidth′.toℕ w → MemInstrType C (int (ixx w (IntMem.load arg))) ([ inj₁ i32 ] ∷ [] ⟶ intType w ∷ [])
-  int-load8 : ∀ {C w s arg lim} → Context.getMem C zero ≡ just lim → MemArg.align arg ≡ zero → MemInstrType C (int (ixx w (IntMem.load8 s arg))) ([ inj₁ i32 ] ∷ [] ⟶ intType w ∷ [])
-  int-load16 : ∀ {C w s arg lim} → Context.getMem C zero ≡ just lim → toℕ (MemArg.align arg) ≤ⁿ 1 → MemInstrType C (int (ixx w (IntMem.load16 s arg))) ([ inj₁ i32 ] ∷ [] ⟶ intType w ∷ [])
-  int-load32 : ∀ {C s arg lim} → Context.getMem C zero ≡ just lim → toℕ (MemArg.align arg) ≤ⁿ 2 → MemInstrType C (int (i64-load32 s arg)) ([ inj₁ i32 ] ∷ [] ⟶ [ inj₁ i64 ] ∷ [])
-  int-store : ∀ {C w arg lim} → Context.getMem C zero ≡ just lim → 2 ^ (3 + toℕ (MemArg.align arg)) ≤ⁿ BitWidth′.toℕ w → MemInstrType C (int (ixx w (IntMem.store arg))) (intType w ∷ [ inj₁ i32 ] ∷ [] ⟶ [])
-  int-store8 : ∀ {C w arg lim} → Context.getMem C zero ≡ just lim → MemArg.align arg ≡ zero → MemInstrType C (int (ixx w (IntMem.store8 arg))) (intType w ∷ [ inj₁ i32 ] ∷ [] ⟶ [])
-  int-store16 : ∀ {C w arg lim} → Context.getMem C zero ≡ just lim → toℕ (MemArg.align arg) ≤ⁿ 1 → MemInstrType C (int (ixx w (IntMem.store16 arg))) (intType w ∷ [ inj₁ i32 ] ∷ [] ⟶ [])
-  int-store32 : ∀ {C arg lim} → Context.getMem C zero ≡ just lim → toℕ (MemArg.align arg) ≤ⁿ 2 → MemInstrType C (int (i64-store32 arg)) ([ inj₁ i64 ] ∷ [ inj₁ i32 ] ∷ [] ⟶ [])
-  float-load : ∀ {C w arg lim} → Context.getMem C zero ≡ just lim → 2 ^ (3 + toℕ (MemArg.align arg)) ≤ⁿ BitWidth′.toℕ w → MemInstrType C (float (w , (FloatMem.load arg))) ([ inj₁ i32 ] ∷ [] ⟶ floatType w ∷ [])
-  float-store : ∀ {C w arg lim} → Context.getMem C zero ≡ just lim → 2 ^ (3 + toℕ (MemArg.align arg)) ≤ⁿ BitWidth′.toℕ w → MemInstrType C (float (w , (FloatMem.store arg))) ([ inj₁ i32 ] ∷ floatType w ∷ [] ⟶ [])
-  size : ∀ {C lim} → Context.getMem C zero ≡ just lim → MemInstrType C size ([] ⟶ [ inj₁ i32 ] ∷ [])
-  grow : ∀ {C lim} → Context.getMem C zero ≡ just lim → MemInstrType C grow ([ inj₁ i32 ] ∷ [] ⟶ [ inj₁ i32 ] ∷ [])
-  fill : ∀ {C lim} → Context.getMem C zero ≡ just lim → MemInstrType C fill ([ inj₁ i32 ] ∷ [ inj₁ i32 ] ∷ [ inj₁ i32 ] ∷ [] ⟶ [])
-  copy : ∀ {C lim} → Context.getMem C zero ≡ just lim → MemInstrType C copy ([ inj₁ i32 ] ∷ [ inj₁ i32 ] ∷ [ inj₁ i32 ] ∷ [] ⟶ [])
-  init : ∀ {C x lim} → Context.getMem C zero ≡ just lim → Context.getData C x ≡ just _ → MemInstrType C (init x) ([ inj₁ i32 ] ∷ [ inj₁ i32 ] ∷ [ inj₁ i32 ] ∷ [] ⟶ [])
-  drop : ∀ {C x} → Context.getData C x ≡ just _ → MemInstrType C (drop x) ([] ⟶ [])
-
-------------------------------------------------------------------------
--- 3.3.7 Control Instructions
-
-infix 2 _⊢_∶_ _⊢*_∶_
-
-data _⊢_∶_ : Context → Instr → StackType → Set
-data _⊢*_∶_ : Context → List Instr → StackType → Set
-
-data _⊢_∶_ where
-  num : ∀ {C i} → C ⊢ num i ∶ typeOfNum i
-  ref : ∀ {C i t} → RefInstrType C i t → C ⊢ ref i ∶ t
-  parametric : ∀ {C i t} → ParametricInstrType C i t → C ⊢ parametric i ∶ t
-  var : ∀ {C i t} → VarInstrType C i t → C ⊢ var i ∶ t
-  table : ∀ {C i t} → TableInstrType C i t → C ⊢ table i ∶ t
-  mem : ∀ {C i t} → MemInstrType C i t → C ⊢ mem i ∶ t
-  nop : ∀ {C} → C ⊢ nop ∶ [] ⟶ []
-  unreachable : ∀ {C ts₁ ts₂} → C ⊢ unreachable ∶ ts₁ ⟶ ts₂
-  block : ∀ {C bt t₁ t₂ is} → blockType C bt ≡ just (t₁ ⟶ t₂) → record C { labels = t₂ ∷ Context.labels C } ⊢* is ∶ fromFunc (t₁ ⟶ t₂) → C ⊢ block bt is ∶ fromFunc (t₁ ⟶ t₂)
-  loop : ∀ {C bt t₁ t₂ is} → blockType C bt ≡ just (t₁ ⟶ t₂) → record C { labels = t₁ ∷ Context.labels C } ⊢* is ∶ fromFunc (t₁ ⟶ t₂) → C ⊢ block bt is ∶ fromFunc (t₁ ⟶ t₂)
-  if-else : ∀ {C bt t₁ t₂ is₁ is₂} → blockType C bt ≡ just (t₁ ⟶ t₂) → record C { labels = t₂ ∷ Context.labels C } ⊢* is₁ ∶ fromFunc (t₁ ⟶ t₂) → record C { labels = t₂ ∷ Context.labels C } ⊢* is₂ ∶ fromFunc (t₁ ⟶ t₂) → C ⊢ if-else bt is₁ is₂ ∶ [ inj₁ i32 ] ∷ fromResult t₁ ⟶ fromResult t₂
-  br : ∀ {C l t t₁ t₂} → Context.getLabel C l ≡ just t → C ⊢ br l ∶ fromResult t ++ t₁ ⟶ t₂
-  br_if : ∀ {C l t} → Context.getLabel C l ≡ just t → C ⊢ br l ∶ [ inj₁ i32 ] ∷ fromResult t ⟶ fromResult t
-  br_table : ∀ {C ls l t t′ t₁ t₂} → Context.getLabel C l ≡ just t′ → Pointwise _≤_ t (fromResult t′) → All (λ l′ → ∃ λ t′ → Context.getLabel C l′ ≡ just t′ × Pointwise _≤_ t (fromResult t′)) (toList ls) → C ⊢ br-table ls l ∶ t ++ t₁ ⟶ t₂
-  return : ∀ {C t t₁ t₂} → Context.return C ≡ just t → C ⊢ return ∶ (fromResult t) ++ t₁ ⟶ t₂
-  call : ∀ {C x t} → Context.getFunc C x ≡ just t → C ⊢ call x ∶ fromFunc t
-  call-indirect : ∀ {C x y lim t₁ t₂} → Context.getTable C x ≡ just (lim , funcref) → Context.getType C y ≡ just (t₁ ⟶ t₂) → C ⊢ call-indirect x y ∶ [ inj₁ i32 ] ∷ fromResult t₁ ⟶ fromResult t₂
-
-------------------------------------------------------------------------
--- 3.3.8 Instruction Sequences
-
--- NOTE: fold is in reverse due to nature of lists in Agda.
-
-data _⊢*_∶_ where
-  empty : ∀ {C t} → C ⊢* [] ∶ t ⟶ t
-  step : ∀ {C i is t₀ t₁ t′ t t₃} → Pointwise _≤_ t′ t → C ⊢ i ∶ t ⟶ t₁ → C ⊢* is ∶ (t₁ ++ t₀) ⟶ t₃ → C ⊢* i ∷ is ∶ (t′ ++ t₀) ⟶ t₃
-
-------------------------------------------------------------------------
--- 3.3.9 Expressions
-
-infix 2 _⊢ᵉ_∶_ _⊢*_const _⊢_const
-
-_⊢ᵉ_∶_ : Context → Expr → ResultType → Set
-C ⊢ᵉ expr ∶ t = ∃ λ t′ → (C ⊢* expr ∶ [] ⟶ t′) × Pointwise _≤_ t′ (fromResult t)
-
-data _⊢_const : Context → Instr → Set
-_⊢*_const : Context → Expr → Set
-
-data _⊢_const where
-  int-const : ∀ {C w x} → C ⊢ num (int (ixx w (IntOp.const x))) const
-  float-const : ∀ {C w x} → C ⊢ num (float (fxx w (FloatOp.const x))) const
-  ref-null : ∀ {C t} → C ⊢ ref (null t) const
-  ref-func : ∀ {C x} → C ⊢ ref (func x) const
-  global-get : ∀ {C x t} → Context.getGlobal C x ≡ just (const , t) → C ⊢ var (global-get x) const
-
-C ⊢* expr const = All (C ⊢_const) expr