diff options
Diffstat (limited to 'src/Wasm/Validation/Instructions.agda')
| -rw-r--r-- | src/Wasm/Validation/Instructions.agda | 197 |
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 |