diff options
| -rw-r--r-- | src/Wasm/Data.agda | 138 | ||||
| -rw-r--r-- | src/Wasm/Data/Instruction.agda | 219 | ||||
| -rw-r--r-- | src/Wasm/Semantics.agda | 147 | ||||
| -rw-r--r-- | src/Wasm/Semantics/Instruction.agda | 5 | ||||
| -rw-r--r-- | src/Wasm/Type.agda | 9 | ||||
| -rw-r--r-- | src/Wasm/Util/List/Map.agda | 33 | ||||
| -rw-r--r-- | src/Wasm/Util/List/Map/Any.agda | 12 | ||||
| -rw-r--r-- | src/Wasm/Util/List/Prefix.agda | 36 | ||||
| -rw-r--r-- | src/Wasm/Value.agda | 8 |
9 files changed, 419 insertions, 188 deletions
diff --git a/src/Wasm/Data.agda b/src/Wasm/Data.agda index f7ed8da..d849cc6 100644 --- a/src/Wasm/Data.agda +++ b/src/Wasm/Data.agda @@ -14,9 +14,12 @@ open import Data.Product using (_×_; _,_; proj₁) open import Data.Sum using (_⊎_) open import Data.Unit using (⊤) open import Data.Vec using (Vec) +open import Data.Vec.Relation.Unary.Any using () renaming (Any to VecAny) open import Function as _ using (_∋_) open import Relation.Binary.PropositionalEquality using (_≡_; _≢_) -open import Wasm.Data.Instruction as Inst using (Expression; Constant) +open import Wasm.Data.Instruction as Inst using (Expression; SequenceConstant) +open import Wasm.Util.List.Map using (Map) +open import Wasm.Util.List.Map.Any using () renaming (Any to MapAny) open import Wasm.Value using (Byte; Name) open import Wasm.Type @@ -71,89 +74,69 @@ private module Cᵢ = ExternTypes Cᵢ module Cₘ = Context Cₘ -record Function (Cᵢ : ExternTypes) (Cₘ : Context) (refs : List (Fin (length (ExternTypes.funcs Cᵢ ++ Context.funcs Cₘ)))) (idx : Fin (length (Context.funcs Cₘ))) : Set where +record Function (C : Inst.Context) (τ : FuncType) : Set where private - module Cₘ = Context Cₘ - - type = lookup Cₘ.funcs idx - - private - module type = FuncType type + module τ = FuncType τ field locals : List ValType private - C = Inst.Context ∋ record (makeContext Cᵢ Cₘ refs) - { locals = type.from ++ locals - ; labels = type.to ∷ [] - ; return = just type.to + C′ = Inst.Context ∋ record C + { locals = τ.from ++ locals + ; labels = τ.to ∷ [] + ; return = just τ.to } field - body : Expression C type.to - -record Global (Cᵢ : ExternTypes) (Cₘ : Context) (refs : List (Fin (length (ExternTypes.funcs Cᵢ ++ Context.funcs Cₘ)))) (idx : Fin (length (Context.globals Cₘ))) : Set where - private - module Cₘ = Context Cₘ - C = Inst.Context ∋ makeGlobalContext Cᵢ Cₘ refs - - type = lookup Cₘ.globals idx + body : Expression C′ τ.to +record Global (C : Inst.Context) (τ : GlobalType) : Set where private - module type = GlobalType type + module τ = GlobalType τ field - {body} : Expression C (type.type ∷ []) - constant : Constant body + {body} : Expression C (τ.type ∷ []) + constant : SequenceConstant body -GlobalRef : ∀ {Cᵢ Cₘ refs idx} → Global Cᵢ Cₘ refs idx → Fin (length (ExternTypes.funcs Cᵢ ++ Context.funcs Cₘ)) → Set -GlobalRef global x = Inst.InstructionRef (Global.body global) x +GlobalRef : ∀ {C τ} → Global C τ → Fin (length (Inst.Context.funcs C)) → Set +GlobalRef global x = Inst.SequenceRef (Global.body global) x data ElemMode (C : Inst.Context) : RefType → Set where passive : ∀ {τ} → ElemMode C τ - active : ∀ table {offset : Expression C (num i32 ∷ [])} → Constant offset → ElemMode C (TableType.type (lookup (Inst.Context.tables C) table)) + active : ∀ table {offset : Expression C (num i32 ∷ [])} → SequenceConstant offset → ElemMode C (TableType.type (lookup (Inst.Context.tables C) table)) declarative : ∀ {τ} → ElemMode C τ data ElemModeRef {C : Inst.Context} : ∀ {τ} → ElemMode C τ → Fin (length (Inst.Context.funcs C)) → Set where - activeRef : ∀ {x} table {offset} constant → Inst.InstructionRef offset x → ElemModeRef (active table {offset} constant) x - -record Elem (Cᵢ : ExternTypes) (Cₘ : Context) (refs : List (Fin (length (ExternTypes.funcs Cᵢ ++ Context.funcs Cₘ)))) (idx : Fin (length (Context.elems Cₘ))) : Set where - private - module Cₘ = Context Cₘ - C = Inst.Context ∋ makeContext Cᵢ Cₘ refs - - type = lookup Cₘ.elems idx + activeRef : ∀ {x} table {offset} constant → Inst.SequenceRef offset x → ElemModeRef (active table {offset} constant) x +record Elem (C : Inst.Context) (τ : RefType) : Set where field - {inits} : List (Expression C (ref type ∷ [])) - constant : All Constant inits - mode : ElemMode C type + {inits} : List (Expression C (ref τ ∷ [])) + constant : All SequenceConstant inits + mode : ElemMode C τ -data ElemRef {Cᵢ} {Cₘ} {refs} {idx} (elem : Elem Cᵢ Cₘ refs idx) (x : Fin (length (ExternTypes.funcs Cᵢ ++ Context.funcs Cₘ))) : Set where - initsRef : Any (λ init → Inst.InstructionRef init x) (Elem.inits elem) → ElemRef elem x +data ElemRef {C τ} (elem : Elem C τ) (x : Fin (length (Inst.Context.funcs C))) : Set where + initsRef : Any (λ init → Inst.SequenceRef init x) (Elem.inits elem) → ElemRef elem x modeRef : ElemModeRef (Elem.mode elem) x → ElemRef elem x data DataMode (C : Inst.Context) : Set where passive : DataMode C - active : ∀ (memory : Fin (length (Inst.Context.mems C))) {offset : Expression C (num i32 ∷ [])} → Constant offset → DataMode C + active : ∀ (memory : Fin (length (Inst.Context.mems C))) {offset : Expression C (num i32 ∷ [])} → SequenceConstant offset → DataMode C data DataModeRef {C : Inst.Context} : DataMode C → Fin (length (Inst.Context.funcs C)) → Set where - activeRef : ∀ {x} memory {offset} constant → Inst.InstructionRef offset x → DataModeRef (active memory {offset} constant) x + activeRef : ∀ {x} memory {offset} constant → Inst.SequenceRef offset x → DataModeRef (active memory {offset} constant) x -record Data (Cᵢ : ExternTypes) (Cₘ : Context) (refs : List (Fin (length (ExternTypes.funcs Cᵢ ++ Context.funcs Cₘ)))) (idx : Fin (Context.datas Cₘ)) : Set where - private - C = Inst.Context ∋ makeContext Cᵢ Cₘ refs +record Data (C : Inst.Context) : Set where field init : List Byte mode : DataMode C -DataRef : ∀ {Cᵢ Cₘ refs idx} → Data Cᵢ Cₘ refs idx → Fin (length (ExternTypes.funcs Cᵢ ++ Context.funcs Cₘ)) → Set +DataRef : ∀ {C} → Data C → Fin (length (Inst.Context.funcs C)) → Set DataRef dta x = DataModeRef (Data.mode dta) x -record Exports (Cᵢ : ExternTypes) (Cₘ : Context) (refs : List (Fin (length (ExternTypes.funcs Cᵢ ++ Context.funcs Cₘ)))) (Cₑ : ExternTypes) : Set where +record Exports (C : Inst.Context) (Cₑ : ExternTypes) : Set where private - C = Inst.Context ∋ makeContext Cᵢ Cₘ refs module Cₑ = ExternTypes Cₑ module C = Inst.Context C field @@ -169,7 +152,7 @@ record Exports (Cᵢ : ExternTypes) (Cₘ : Context) (refs : List (Fin (length ( field namesDisjoint : AllPairs _≢_ names -ExportsRef : ∀ {Cᵢ Cₘ refs Cₑ} → Exports Cᵢ Cₘ refs Cₑ → Fin (length (ExternTypes.funcs Cᵢ ++ Context.funcs Cₘ)) → Set +ExportsRef : ∀ {C Cₑ} → Exports C Cₑ → Fin (length (Inst.Context.funcs C)) → Set ExportsRef exports x = Any (λ (_ , y) → y ≡ x) (Exports.funcs exports) record Imports (Cᵢ : ExternTypes) : Set where @@ -181,47 +164,42 @@ record Imports (Cᵢ : ExternTypes) : Set where mems : Vec (Name × Name) (length Cᵢ.mems) globals : Vec (Name × Name) (length Cᵢ.globals) -infixr 5 _∷_ - -data DList : ∀ {n} → (A : Fin n → Set) → Set₁ where - [] : ∀ {A} → DList {0} A - _∷_ : ∀ {n A} → A zero → DList {n} (λ i → A (suc i)) → DList A - -data DAny : ∀ {n A} → (∀ {i} → A i → Set) → DList {n} A → Set₁ where - here : ∀ {n A} {P : ∀ {i} → A i → Set} {x xs} → P x → DAny {suc n} {A} P (x ∷ xs) - there : ∀ {n A} {P : ∀ {i} → A i → Set} {x xs} → DAny (λ {i} → P {suc i}) xs → DAny {suc n} {A} P (x ∷ xs) - record Module (it et : ExternTypes) : Set₁ where private module it = ExternTypes it field - ft : List FuncType - tables : List TableType - mems : List MemType - rt : List RefType - n : ℕ - start : Maybe (Fin (length (it.funcs ++ ft))) + {ft} : List FuncType + tables : List TableType + mems : List MemType + {gt} : List GlobalType + {rt} : List RefType + {#datas} : ℕ + start : Maybe (Fin (length (it.funcs ++ ft))) + refs : List (Fin (length (it.funcs ++ ft))) private Cₘ = Context ∋ record { funcs = ft ; tables = tables ; mems = mems - ; globals = it.globals + ; globals = gt ; elems = rt - ; datas = n + ; datas = #datas } + C′ = makeGlobalContext it Cₘ refs + + C = makeContext it Cₘ refs + field - refs : List (Fin (length (it.funcs ++ ft))) - funcs : DList (Function it Cₘ refs) - globals : DList (Global it Cₘ refs) - elems : DList (Elem it Cₘ refs) - datas : DList (Data it Cₘ refs) + funcs : Map (Function C) ft + globals : Map (Global C′) gt + elems : Map (Elem C) rt + datas : Vec (Data C) #datas startOk : maybe (λ x → lookup (it.funcs ++ ft) x ≡ ([] ⟶ [])) ⊤ start - exports : Exports it Cₘ refs et + exports : Exports C et memCount : length it.mems + length mems ≤ 1 - refsUsed : All (λ i → DAny (λ g → GlobalRef g i) globals - ⊎ DAny (λ e → ElemRef e i) elems - ⊎ DAny (λ d → DataRef d i) datas + refsUsed : All (λ i → MapAny (λ g → GlobalRef g i) globals + ⊎ MapAny (λ e → ElemRef e i) elems + ⊎ VecAny (λ d → DataRef d i) datas ⊎ ExportsRef exports i) refs @@ -230,7 +208,9 @@ private open import Data.List.Relation.Binary.Pointwise using ([]; _∷_) open import Data.List.Relation.Unary.All using ([]) open import Data.List.Relation.Unary.AllPairs using ([]; _∷_) + open import Data.Vec using ([]) open import Relation.Binary.PropositionalEquality using (refl) + open import Wasm.Util.List.Map using (Map; []; _∷_) open Inst addTwoImports : ExternTypes @@ -241,16 +221,12 @@ private addTwoModule : Module addTwoImports addTwoExports addTwoModule = record - { ft = (num i32 ∷ num i32 ∷ [] ⟶ num i32 ∷ []) ∷ [] - ; tables = [] + { tables = [] ; mems = [] - ; rt = [] - ; n = 0 ; start = nothing - ; refs = [] ; funcs = record { locals = [] - ; body = seq (local-get zero) (seq (frame (local-get (suc zero))) (i32-binop i32.add)) + ; body = local-get zero ∙ local-get (suc zero) ∙ i32-binop i32.add ∙ nop } ∷ [] ; globals = [] ; elems = [] diff --git a/src/Wasm/Data/Instruction.agda b/src/Wasm/Data/Instruction.agda index 2e56368..8be89c6 100644 --- a/src/Wasm/Data/Instruction.agda +++ b/src/Wasm/Data/Instruction.agda @@ -12,6 +12,8 @@ open import Relation.Binary.PropositionalEquality using (_≡_) open import Wasm.Type open import Wasm.Value +infixr 4 _∙_ _∙₁_ _∙₂_ + record Context : Set where field funcs : List FuncType @@ -193,146 +195,155 @@ blockTypeAsFunc {C} (idx τ) = τ blockTypeAsFunc (val x) = [] ⟶ x ∷ [] blockTypeAsFunc nothing = [] ⟶ [] -data Instruction : Context → FuncType → Set where +data Instruction (C : Context) : FuncType → Set +data Sequence (C : Context) : FuncType → Set + +data Instruction C where ---- Numeric instructions -- const - i32-const : ∀ {C} → (c : I32) → Instruction C ([] ⟶ num i32 ∷ []) - i64-const : ∀ {C} → (c : I64) → Instruction C ([] ⟶ num i64 ∷ []) - f32-const : ∀ {C} → (c : F32) → Instruction C ([] ⟶ num f32 ∷ []) - f64-const : ∀ {C} → (c : F64) → Instruction C ([] ⟶ num f64 ∷ []) + i32-const : (c : I32) → Instruction C ([] ⟶ num i32 ∷ []) + i64-const : (c : I64) → Instruction C ([] ⟶ num i64 ∷ []) + f32-const : (c : F32) → Instruction C ([] ⟶ num f32 ∷ []) + f64-const : (c : F64) → Instruction C ([] ⟶ num f64 ∷ []) -- unop - i32-unop : ∀ {C} → (op : i32.Unary) → Instruction C (num i32 ∷ [] ⟶ num i32 ∷ []) - i64-unop : ∀ {C} → (op : i64.Unary) → Instruction C (num i64 ∷ [] ⟶ num i64 ∷ []) - f32-unop : ∀ {C} → (op : f32.Unary) → Instruction C (num f32 ∷ [] ⟶ num f32 ∷ []) - f64-unop : ∀ {C} → (op : f64.Unary) → Instruction C (num f64 ∷ [] ⟶ num f64 ∷ []) + i32-unop : (op : i32.Unary) → Instruction C (num i32 ∷ [] ⟶ num i32 ∷ []) + i64-unop : (op : i64.Unary) → Instruction C (num i64 ∷ [] ⟶ num i64 ∷ []) + f32-unop : (op : f32.Unary) → Instruction C (num f32 ∷ [] ⟶ num f32 ∷ []) + f64-unop : (op : f64.Unary) → Instruction C (num f64 ∷ [] ⟶ num f64 ∷ []) -- binop - i32-binop : ∀ {C} → (op : i32.Binary) → Instruction C (num i32 ∷ num i32 ∷ [] ⟶ num i32 ∷ []) - i64-binop : ∀ {C} → (op : i64.Binary) → Instruction C (num i64 ∷ num i64 ∷ [] ⟶ num i64 ∷ []) - f32-binop : ∀ {C} → (op : f32.Binary) → Instruction C (num f32 ∷ num f32 ∷ [] ⟶ num f32 ∷ []) - f64-binop : ∀ {C} → (op : f64.Binary) → Instruction C (num f64 ∷ num f64 ∷ [] ⟶ num f64 ∷ []) + i32-binop : (op : i32.Binary) → Instruction C (num i32 ∷ num i32 ∷ [] ⟶ num i32 ∷ []) + i64-binop : (op : i64.Binary) → Instruction C (num i64 ∷ num i64 ∷ [] ⟶ num i64 ∷ []) + f32-binop : (op : f32.Binary) → Instruction C (num f32 ∷ num f32 ∷ [] ⟶ num f32 ∷ []) + f64-binop : (op : f64.Binary) → Instruction C (num f64 ∷ num f64 ∷ [] ⟶ num f64 ∷ []) -- testop - i32-testop : ∀ {C} → (op : i32.Test) → Instruction C (num i32 ∷ [] ⟶ num i32 ∷ []) - i64-testop : ∀ {C} → (op : i64.Test) → Instruction C (num i64 ∷ [] ⟶ num i32 ∷ []) + i32-testop : (op : i32.Test) → Instruction C (num i32 ∷ [] ⟶ num i32 ∷ []) + i64-testop : (op : i64.Test) → Instruction C (num i64 ∷ [] ⟶ num i32 ∷ []) -- relop - i32-relop : ∀ {C} → (op : i32.Rel) → Instruction C (num i32 ∷ num i32 ∷ [] ⟶ num i32 ∷ []) - i64-relop : ∀ {C} → (op : i64.Rel) → Instruction C (num i64 ∷ num i64 ∷ [] ⟶ num i32 ∷ []) - f32-relop : ∀ {C} → (op : f32.Rel) → Instruction C (num f32 ∷ num f32 ∷ [] ⟶ num i32 ∷ []) - f64-relop : ∀ {C} → (op : f64.Rel) → Instruction C (num f64 ∷ num f64 ∷ [] ⟶ num i32 ∷ []) + i32-relop : (op : i32.Rel) → Instruction C (num i32 ∷ num i32 ∷ [] ⟶ num i32 ∷ []) + i64-relop : (op : i64.Rel) → Instruction C (num i64 ∷ num i64 ∷ [] ⟶ num i32 ∷ []) + f32-relop : (op : f32.Rel) → Instruction C (num f32 ∷ num f32 ∷ [] ⟶ num i32 ∷ []) + f64-relop : (op : f64.Rel) → Instruction C (num f64 ∷ num f64 ∷ [] ⟶ num i32 ∷ []) -- cvtop - i32-cvtop : ∀ {C τ} → (op : i32.Convert τ) → Instruction C (num τ ∷ [] ⟶ num i32 ∷ []) - i64-cvtop : ∀ {C τ} → (op : i64.Convert τ) → Instruction C (num τ ∷ [] ⟶ num i64 ∷ []) - f32-cvtop : ∀ {C τ} → (op : f32.Convert τ) → Instruction C (num τ ∷ [] ⟶ num f32 ∷ []) - f64-cvtop : ∀ {C τ} → (op : f64.Convert τ) → Instruction C (num τ ∷ [] ⟶ num f64 ∷ []) + i32-cvtop : ∀ {τ} → (op : i32.Convert τ) → Instruction C (num τ ∷ [] ⟶ num i32 ∷ []) + i64-cvtop : ∀ {τ} → (op : i64.Convert τ) → Instruction C (num τ ∷ [] ⟶ num i64 ∷ []) + f32-cvtop : ∀ {τ} → (op : f32.Convert τ) → Instruction C (num τ ∷ [] ⟶ num f32 ∷ []) + f64-cvtop : ∀ {τ} → (op : f64.Convert τ) → Instruction C (num τ ∷ [] ⟶ num f64 ∷ []) ---- Reference instructions - ref-null : ∀ {C} τ → Instruction C ([] ⟶ ref τ ∷ []) - ref-is-null : ∀ {C τ} → Instruction C (ref τ ∷ [] ⟶ num i32 ∷ []) - ref-func : ∀ {C x} → (x∈refs : x ∈ Context.refs C) → Instruction C ([] ⟶ ref funcref ∷ []) + ref-null : ∀ τ → Instruction C ([] ⟶ ref τ ∷ []) + ref-is-null : ∀ {τ} → Instruction C (ref τ ∷ [] ⟶ num i32 ∷ []) + ref-func : ∀ {x} → (x∈refs : x ∈ Context.refs C) → Instruction C ([] ⟶ ref funcref ∷ []) ---- Parametric instructions - drop : ∀ {C τ} → Instruction C (τ ∷ [] ⟶ []) - select : ∀ {C τ} → Instruction C (num i32 ∷ τ ∷ τ ∷ [] ⟶ τ ∷ []) + drop : ∀ {τ} → Instruction C (τ ∷ [] ⟶ []) + select : ∀ {τ} → Instruction C (num i32 ∷ τ ∷ τ ∷ [] ⟶ τ ∷ []) ---- Variable instructions - local-get : ∀ {C} x → Instruction C ([] ⟶ lookup (Context.locals C) x ∷ []) - local-set : ∀ {C} x → Instruction C (lookup (Context.locals C) x ∷ [] ⟶ []) - local-tee : ∀ {C} x → Instruction C (lookup (Context.locals C) x ∷ [] ⟶ lookup (Context.locals C) x ∷ []) - global-get : ∀ {C} x → Instruction C ([] ⟶ GlobalType.type (lookup (Context.globals C) x) ∷ []) - global-set : ∀ {C} x → let g = lookup (Context.globals C) x in GlobalType.mut g ≡ var → Instruction C (GlobalType.type g ∷ [] ⟶ []) + local-get : ∀ x → Instruction C ([] ⟶ lookup (Context.locals C) x ∷ []) + local-set : ∀ x → Instruction C (lookup (Context.locals C) x ∷ [] ⟶ []) + local-tee : ∀ x → Instruction C (lookup (Context.locals C) x ∷ [] ⟶ lookup (Context.locals C) x ∷ []) + global-get : ∀ x → Instruction C ([] ⟶ GlobalType.type (lookup (Context.globals C) x) ∷ []) + global-set : ∀ x → let g = lookup (Context.globals C) x in GlobalType.mut g ≡ var → Instruction C (GlobalType.type g ∷ [] ⟶ []) ---- Table instructions - table-get : ∀ {C} x → Instruction C (num i32 ∷ [] ⟶ ref (TableType.type (lookup (Context.tables C) x)) ∷ []) - table-set : ∀ {C} x → Instruction C (ref (TableType.type (lookup (Context.tables C) x)) ∷ num i32 ∷ [] ⟶ []) - table-size : ∀ {C} (x : Fin (length (Context.tables C))) → Instruction C ([] ⟶ num i32 ∷ []) - table-grow : ∀ {C} x → Instruction C (num i32 ∷ ref (TableType.type (lookup (Context.tables C) x)) ∷ [] ⟶ num i32 ∷ []) - table-fill : ∀ {C} x → Instruction C (num i32 ∷ ref (TableType.type (lookup (Context.tables C) x)) ∷ num i32 ∷ [] ⟶ []) - table-copy : ∀ {C} x y → TableType.type (lookup (Context.tables C) x) ≡ TableType.type (lookup (Context.tables C) y) → Instruction C (num i32 ∷ num i32 ∷ num i32 ∷ [] ⟶ []) - table-init : ∀ {C} x y → TableType.type (lookup (Context.tables C) x) ≡ lookup (Context.elems C) y → Instruction C (num i32 ∷ num i32 ∷ num i32 ∷ [] ⟶ []) - elem-drop : ∀ {C} (x : Fin (length (Context.elems C))) → Instruction C ([] ⟶ []) + table-get : ∀ x → Instruction C (num i32 ∷ [] ⟶ ref (TableType.type (lookup (Context.tables C) x)) ∷ []) + table-set : ∀ x → Instruction C (ref (TableType.type (lookup (Context.tables C) x)) ∷ num i32 ∷ [] ⟶ []) + table-size : ∀ (x : Fin (length (Context.tables C))) → Instruction C ([] ⟶ num i32 ∷ []) + table-grow : ∀ x → Instruction C (num i32 ∷ ref (TableType.type (lookup (Context.tables C) x)) ∷ [] ⟶ num i32 ∷ []) + table-fill : ∀ x → Instruction C (num i32 ∷ ref (TableType.type (lookup (Context.tables C) x)) ∷ num i32 ∷ [] ⟶ []) + table-copy : ∀ x y → TableType.type (lookup (Context.tables C) x) ≡ TableType.type (lookup (Context.tables C) y) → Instruction C (num i32 ∷ num i32 ∷ num i32 ∷ [] ⟶ []) + table-init : ∀ x y → TableType.type (lookup (Context.tables C) x) ≡ lookup (Context.elems C) y → Instruction C (num i32 ∷ num i32 ∷ num i32 ∷ [] ⟶ []) + elem-drop : ∀ (x : Fin (length (Context.elems C))) → Instruction C ([] ⟶ []) ---- Memory instructions -- load - i32-load : ∀ {C} (m : MemArg 2) → length (Context.mems C) > 0 → Instruction C (num i32 ∷ [] ⟶ num i32 ∷ []) - i64-load : ∀ {C} (m : MemArg 3) → length (Context.mems C) > 0 → Instruction C (num i32 ∷ [] ⟶ num i64 ∷ []) - f32-load : ∀ {C} (m : MemArg 2) → length (Context.mems C) > 0 → Instruction C (num i32 ∷ [] ⟶ num f32 ∷ []) - f64-load : ∀ {C} (m : MemArg 3) → length (Context.mems C) > 0 → Instruction C (num i32 ∷ [] ⟶ num f64 ∷ []) + i32-load : ∀ (m : MemArg 2) → length (Context.mems C) > 0 → Instruction C (num i32 ∷ [] ⟶ num i32 ∷ []) + i64-load : ∀ (m : MemArg 3) → length (Context.mems C) > 0 → Instruction C (num i32 ∷ [] ⟶ num i64 ∷ []) + f32-load : ∀ (m : MemArg 2) → length (Context.mems C) > 0 → Instruction C (num i32 ∷ [] ⟶ num f32 ∷ []) + f64-load : ∀ (m : MemArg 3) → length (Context.mems C) > 0 → Instruction C (num i32 ∷ [] ⟶ num f64 ∷ []) -- loadN - i32-load8 : ∀ {C} (m : MemArg 0) → length (Context.mems C) > 0 → Signedness → Instruction C (num i32 ∷ [] ⟶ num i32 ∷ []) - i32-load16 : ∀ {C} (m : MemArg 1) → length (Context.mems C) > 0 → Signedness → Instruction C (num i32 ∷ [] ⟶ num i32 ∷ []) - i64-load8 : ∀ {C} (m : MemArg 0) → length (Context.mems C) > 0 → Signedness → Instruction C (num i32 ∷ [] ⟶ num i64 ∷ []) - i64-load16 : ∀ {C} (m : MemArg 1) → length (Context.mems C) > 0 → Signedness → Instruction C (num i32 ∷ [] ⟶ num i64 ∷ []) - i64-load32 : ∀ {C} (m : MemArg 2) → length (Context.mems C) > 0 → Signedness → Instruction C (num i32 ∷ [] ⟶ num i64 ∷ []) + i32-load8 : ∀ (m : MemArg 0) → length (Context.mems C) > 0 → Signedness → Instruction C (num i32 ∷ [] ⟶ num i32 ∷ []) + i32-load16 : ∀ (m : MemArg 1) → length (Context.mems C) > 0 → Signedness → Instruction C (num i32 ∷ [] ⟶ num i32 ∷ []) + i64-load8 : ∀ (m : MemArg 0) → length (Context.mems C) > 0 → Signedness → Instruction C (num i32 ∷ [] ⟶ num i64 ∷ []) + i64-load16 : ∀ (m : MemArg 1) → length (Context.mems C) > 0 → Signedness → Instruction C (num i32 ∷ [] ⟶ num i64 ∷ []) + i64-load32 : ∀ (m : MemArg 2) → length (Context.mems C) > 0 → Signedness → Instruction C (num i32 ∷ [] ⟶ num i64 ∷ []) -- store - i32-store : ∀ {C} (m : MemArg 2) → length (Context.mems C) > 0 → Instruction C (num i32 ∷ num i32 ∷ [] ⟶ []) - i64-store : ∀ {C} (m : MemArg 3) → length (Context.mems C) > 0 → Instruction C (num i64 ∷ num i32 ∷ [] ⟶ []) - f32-store : ∀ {C} (m : MemArg 2) → length (Context.mems C) > 0 → Instruction C (num f32 ∷ num i32 ∷ [] ⟶ []) - f64-store : ∀ {C} (m : MemArg 3) → length (Context.mems C) > 0 → Instruction C (num f64 ∷ num i32 ∷ [] ⟶ []) + i32-store : ∀ (m : MemArg 2) → length (Context.mems C) > 0 → Instruction C (num i32 ∷ num i32 ∷ [] ⟶ []) + i64-store : ∀ (m : MemArg 3) → length (Context.mems C) > 0 → Instruction C (num i64 ∷ num i32 ∷ [] ⟶ []) + f32-store : ∀ (m : MemArg 2) → length (Context.mems C) > 0 → Instruction C (num f32 ∷ num i32 ∷ [] ⟶ []) + f64-store : ∀ (m : MemArg 3) → length (Context.mems C) > 0 → Instruction C (num f64 ∷ num i32 ∷ [] ⟶ []) -- storeN - i32-store8 : ∀ {C} (m : MemArg 0) → length (Context.mems C) > 0 → Signedness → Instruction C (num i32 ∷ num i32 ∷ [] ⟶ []) - i32-store16 : ∀ {C} (m : MemArg 1) → length (Context.mems C) > 0 → Signedness → Instruction C (num i32 ∷ num i32 ∷ [] ⟶ []) - i64-store8 : ∀ {C} (m : MemArg 0) → length (Context.mems C) > 0 → Signedness → Instruction C (num i64 ∷ num i32 ∷ [] ⟶ []) - i64-store16 : ∀ {C} (m : MemArg 1) → length (Context.mems C) > 0 → Signedness → Instruction C (num i64 ∷ num i32 ∷ [] ⟶ []) - i64-store32 : ∀ {C} (m : MemArg 2) → length (Context.mems C) > 0 → Signedness → Instruction C (num i64 ∷ num i32 ∷ [] ⟶ []) + i32-store8 : ∀ (m : MemArg 0) → length (Context.mems C) > 0 → Signedness → Instruction C (num i32 ∷ num i32 ∷ [] ⟶ []) + i32-store16 : ∀ (m : MemArg 1) → length (Context.mems C) > 0 → Signedness → Instruction C (num i32 ∷ num i32 ∷ [] ⟶ []) + i64-store8 : ∀ (m : MemArg 0) → length (Context.mems C) > 0 → Signedness → Instruction C (num i64 ∷ num i32 ∷ [] ⟶ []) + i64-store16 : ∀ (m : MemArg 1) → length (Context.mems C) > 0 → Signedness → Instruction C (num i64 ∷ num i32 ∷ [] ⟶ []) + i64-store32 : ∀ (m : MemArg 2) → length (Context.mems C) > 0 → Signedness → Instruction C (num i64 ∷ num i32 ∷ [] ⟶ []) -- other - memory-size : ∀ {C} → length (Context.mems C) > 0 → Instruction C ([] ⟶ num i32 ∷ []) - memory-grow : ∀ {C} → length (Context.mems C) > 0 → Instruction C (num i32 ∷ [] ⟶ num i32 ∷ []) - memory-fill : ∀ {C} → length (Context.mems C) > 0 → Instruction C (num i32 ∷ num i32 ∷ num i32 ∷ [] ⟶ []) - memory-copy : ∀ {C} → length (Context.mems C) > 0 → Instruction C (num i32 ∷ num i32 ∷ num i32 ∷ [] ⟶ []) - memory-init : ∀ {C} (x : Fin (Context.datas C)) → length (Context.mems C) > 0 → Instruction C (num i32 ∷ num i32 ∷ num i32 ∷ [] ⟶ []) - data-drop : ∀ {C} (x : Fin (Context.datas C)) → Instruction C ([] ⟶ []) + memory-size : length (Context.mems C) > 0 → Instruction C ([] ⟶ num i32 ∷ []) + memory-grow : length (Context.mems C) > 0 → Instruction C (num i32 ∷ [] ⟶ num i32 ∷ []) + memory-fill : length (Context.mems C) > 0 → Instruction C (num i32 ∷ num i32 ∷ num i32 ∷ [] ⟶ []) + memory-copy : length (Context.mems C) > 0 → Instruction C (num i32 ∷ num i32 ∷ num i32 ∷ [] ⟶ []) + memory-init : (x : Fin (Context.datas C)) → length (Context.mems C) > 0 → Instruction C (num i32 ∷ num i32 ∷ num i32 ∷ [] ⟶ []) + data-drop : (x : Fin (Context.datas C)) → Instruction C ([] ⟶ []) ---- Control instructions - nop : ∀ {C} → Instruction C ([] ⟶ []) - unreachable : ∀ {C τ} → Instruction C τ - block : ∀ {C} (bt : BlockType C) → let τ = blockTypeAsFunc bt in - Instruction (record C {labels = FuncType.to τ ∷ Context.labels C}) τ → Instruction C τ - loop : ∀ {C} (bt : BlockType C) → let τ = blockTypeAsFunc bt in - Instruction (record C {labels = FuncType.from τ ∷ Context.labels C}) τ → Instruction C τ - if : ∀ {C} (bt : BlockType C) → let τ = blockTypeAsFunc bt in - (then else : Instruction (record C {labels = FuncType.to τ ∷ Context.labels C}) τ) → Instruction C (num i32 ∷ FuncType.from τ ⟶ FuncType.to τ) - br : ∀ {C τ₁ τ₂} l → Instruction C (lookup (Context.labels C) l ++ τ₁ ⟶ τ₂) - br_if : ∀ {C} l → let τ = lookup (Context.labels C) l in Instruction C (num i32 ∷ τ ⟶ τ) - br_table : ∀ {C τ₁ τ₂} ls l → let τ = lookup (Context.labels C) l in All (λ l → lookup (Context.labels C) l ≡ τ) ls → Instruction C (τ ++ τ₁ ⟶ τ₂) - return : ∀ {C τ τ₁ τ₂} → Context.return C ≡ just τ → Instruction C (τ ++ τ₁ ⟶ τ₂) - call : ∀ {C} x → Instruction C (lookup (Context.funcs C) x) - call_indirect : ∀ {C} x τ → TableType.type (lookup (Context.tables C) x) ≡ funcref → Instruction C (num i32 ∷ FuncType.from τ ⟶ FuncType.to τ) - - ---- Sequencing - frame : ∀ {C τ τ₁ τ₂} → Instruction C (τ₁ ⟶ τ₂) → Instruction C (τ₁ ++ τ ⟶ τ₂ ++ τ) - seq : ∀ {C τ₁ τ₂ τ₃} → Instruction C (τ₁ ⟶ τ₂) → Instruction C (τ₂ ⟶ τ₃) → Instruction C (τ₁ ⟶ τ₃) + block : (bt : BlockType C) → let τ = blockTypeAsFunc bt in + Sequence (record C {labels = FuncType.to τ ∷ Context.labels C}) τ → Instruction C τ + loop : (bt : BlockType C) → let τ = blockTypeAsFunc bt in + Sequence (record C {labels = FuncType.from τ ∷ Context.labels C}) τ → Instruction C τ + if : (bt : BlockType C) → let τ = blockTypeAsFunc bt in + (then else : Sequence (record C {labels = FuncType.to τ ∷ Context.labels C}) τ) → Instruction C (num i32 ∷ FuncType.from τ ⟶ FuncType.to τ) + br_if : ∀ l → let τ = lookup (Context.labels C) l in Instruction C (num i32 ∷ τ ⟶ τ) + call : ∀ x → Instruction C (lookup (Context.funcs C) x) + call_indirect : ∀ x τ → TableType.type (lookup (Context.tables C) x) ≡ funcref → Instruction C (num i32 ∷ FuncType.from τ ⟶ FuncType.to τ) + +data Sequence C where + nop : ∀ {τ} → Sequence C (τ ⟶ τ) + unreachable : ∀ {τ} → Sequence C τ + br : ∀ {τ₁ τ₂} l → Sequence C (lookup (Context.labels C) l ++ τ₁ ⟶ τ₂) + br_table : ∀ {τ₁ τ₂} ls l → let τ = lookup (Context.labels C) l in All (λ l → lookup (Context.labels C) l ≡ τ) ls → Sequence C (τ ++ τ₁ ⟶ τ₂) + return : ∀ {τ τ₁ τ₂} → Context.return C ≡ just τ → Sequence C (τ ++ τ₁ ⟶ τ₂) + _∙_ : ∀ {τ₀ τ₁ τ₂ τ₃} → Instruction C (τ₁ ⟶ τ₂) → Sequence C (τ₂ ++ τ₀ ⟶ τ₃) → Sequence C (τ₁ ++ τ₀ ⟶ τ₃) Expression : Context → List ValType → Set -Expression C τ = Instruction C ([] ⟶ τ) +Expression C τ = Sequence C ([] ⟶ τ) -data InstructionRef {C} : ∀ {τ} → Instruction C τ → Fin (length (Context.funcs C)) → Set where +data InstructionRef {C} : ∀ {τ} → Instruction C τ → Fin (length (Context.funcs C)) → Set +data SequenceRef {C} : ∀ {τ} → Sequence C τ → Fin (length (Context.funcs C)) → Set + +data InstructionRef {C} where ---- Direct ref-func : ∀ {x} x∈refs → InstructionRef (ref-func {C} {x} x∈refs) x call : ∀ x → InstructionRef (call {C} x) x ---- Structural - block : ∀ {x} bt {i} → InstructionRef i x → InstructionRef (block {C} bt i) x - loop : ∀ {x} bt {i} → InstructionRef i x → InstructionRef (loop {C} bt i) x - if₁ : ∀ {x} bt {i₁} → InstructionRef i₁ x → ∀ i₂ → InstructionRef (if {C} bt i₁ i₂) x - if₂ : ∀ {x} bt i₁ {i₂} → InstructionRef i₂ x → InstructionRef (if {C} bt i₁ i₂) x - frame : ∀ {x τ τ₁ τ₂} {i} → InstructionRef i x → InstructionRef (frame {C} {τ} {τ₁} {τ₂} i) x - seq₁ : ∀ {x τ₁ τ₂ τ₃} {i₁} → InstructionRef i₁ x → ∀ i₂ → InstructionRef (seq {C} {τ₁} {τ₂} {τ₃} i₁ i₂) x - seq₂ : ∀ {x τ₁ τ₂ τ₃} i₁ {i₂} → InstructionRef i₂ x → InstructionRef (seq {C} {τ₁} {τ₂} {τ₃} i₁ i₂) x - -data Constant {C} : ∀ {τ} → Instruction C τ → Set where + block : ∀ {x} bt {i} → SequenceRef i x → InstructionRef (block {C} bt i) x + loop : ∀ {x} bt {i} → SequenceRef i x → InstructionRef (loop {C} bt i) x + if₁ : ∀ {x} bt {i₁} → SequenceRef i₁ x → ∀ i₂ → InstructionRef (if {C} bt i₁ i₂) x + if₂ : ∀ {x} bt i₁ {i₂} → SequenceRef i₂ x → InstructionRef (if {C} bt i₁ i₂) x + +data SequenceRef {C} where + _∙₁_ : ∀ {x τ₀ τ₁ τ₂ τ₃ i} → InstructionRef i x → ∀ i* → SequenceRef (_∙_ {C} {τ₀} {τ₁} {τ₂} {τ₃} i i*) x + _∙₂_ : ∀ {x τ₀ τ₁ τ₂ τ₃} i {i*} → SequenceRef i* x → SequenceRef (_∙_ {C} {τ₀} {τ₁} {τ₂} {τ₃} i i*) x + +data InstructionConstant {C} : ∀ {τ} → Instruction C τ → Set +data SequenceConstant {C} : ∀ {τ} → Sequence C τ → Set + +data InstructionConstant {C} where ---- Direct -- const - i32-const : ∀ c → Constant (i32-const c) - i64-const : ∀ c → Constant (i64-const c) - f32-const : ∀ c → Constant (f32-const c) - f64-const : ∀ c → Constant (f64-const c) + i32-const : ∀ c → InstructionConstant (i32-const c) + i64-const : ∀ c → InstructionConstant (i64-const c) + f32-const : ∀ c → InstructionConstant (f32-const c) + f64-const : ∀ c → InstructionConstant (f64-const c) -- refs - ref-null : ∀ τ → Constant (ref-null τ) - ref-func : ∀ {x} x∈refs → Constant (ref-func {x = x} x∈refs) + ref-null : ∀ τ → InstructionConstant (ref-null τ) + ref-func : ∀ {x} x∈refs → InstructionConstant (ref-func {x = x} x∈refs) -- global - global-get : ∀ {x} → GlobalType.mut (lookup (Context.globals C) x) ≡ const → Constant (global-get x) + global-get : ∀ {x} → GlobalType.mut (lookup (Context.globals C) x) ≡ const → InstructionConstant (global-get x) - ---- Structural - frame : ∀ {τ τ₁ τ₂ i} → Constant i → Constant (frame {C} {τ} {τ₁} {τ₂} i) - seq : ∀ {τ₁ τ₂ τ₃ i₁ i₂} → Constant i₁ → Constant i₂ → Constant (seq {C} {τ₁} {τ₂} {τ₃} i₁ i₂) +data SequenceConstant {C} where + nop : ∀ {τ} → SequenceConstant (nop {C} {τ}) + _∙_ : ∀ {τ₀ τ₁ τ₂ τ₃ i i*} → InstructionConstant i → SequenceConstant i* → SequenceConstant (_∙_ {C} {τ₀} {τ₁} {τ₂} {τ₃} i i*) 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 ++ τ ∷ []) diff --git a/src/Wasm/Semantics/Instruction.agda b/src/Wasm/Semantics/Instruction.agda new file mode 100644 index 0000000..5edd58b --- /dev/null +++ b/src/Wasm/Semantics/Instruction.agda @@ -0,0 +1,5 @@ +{-# OPTIONS --safe --without-K #-} + +module Wasm.Semantics.Instruction where + + diff --git a/src/Wasm/Type.agda b/src/Wasm/Type.agda index 7a82aa8..6e94a71 100644 --- a/src/Wasm/Type.agda +++ b/src/Wasm/Type.agda @@ -2,9 +2,9 @@ module Wasm.Type where -open import Data.Fin using (Fin; Fin′) +open import Data.Fin using (Fin; Fin′; inject) open import Data.List using (List) -open import Data.Maybe using (Maybe; maybe) +open import Data.Maybe using (Maybe; nothing; just; maybe) open import Data.Nat using (ℕ) open import Wasm.Value using (I32) @@ -16,6 +16,11 @@ record Limits (k : ℕ) : Set where max : Maybe (Fin k) min : maybe Fin′ (Fin k) max + min′ : Fin k + min′ with max | min + ... | nothing | m = m + ... | just _ | m = inject m + data NumType : Set where i32 : NumType i64 : NumType diff --git a/src/Wasm/Util/List/Map.agda b/src/Wasm/Util/List/Map.agda new file mode 100644 index 0000000..a6da0d0 --- /dev/null +++ b/src/Wasm/Util/List/Map.agda @@ -0,0 +1,33 @@ +{-# OPTIONS --safe --without-K #-} + +-- List where element types depend on another list. +module Wasm.Util.List.Map where + +open import Data.Fin using (Fin; zero; suc) +open import Data.List as List using (List; []; _∷_) +open import Data.Nat using (ℕ) +open import Level using (Level; _⊔_) + +infixr 5 _∷_ + +private + variable + a b : Level + A : Set a + B : A → Set b + xs : List A + +data Map {A : Set a} (B : A → Set b) : List A → Set (a ⊔ b) where + [] : Map B [] + _∷_ : ∀ {x xs} (y : B x) (ys : Map B xs) → Map B (x ∷ xs) + +length : Map B xs → ℕ +length {xs = xs} ys = List.length xs + +lookup : (ys : Map B xs) → (i : Fin (length ys)) → B (List.lookup xs i) +lookup (y ∷ ys) zero = y +lookup (y ∷ ys) (suc i) = lookup ys i + +map : ∀ {c} {C : A → Set c} → (∀ {x} → B x → C x) → Map B xs → Map C xs +map f [] = [] +map f (y ∷ ys) = f y ∷ map f ys diff --git a/src/Wasm/Util/List/Map/Any.agda b/src/Wasm/Util/List/Map/Any.agda new file mode 100644 index 0000000..196ecc5 --- /dev/null +++ b/src/Wasm/Util/List/Map/Any.agda @@ -0,0 +1,12 @@ +{-# OPTIONS --safe --without-K #-} + +module Wasm.Util.List.Map.Any where + +open import Data.List using (_∷_) +open import Level using (_⊔_) +open import Relation.Unary using (Pred) +open import Wasm.Util.List.Map + +data Any {a b p} {A : Set a} {B : A → Set b} (P : ∀ {x} → Pred (B x) p) : ∀ {xs} → Pred (Map B xs) (a ⊔ b ⊔ p) where + here : ∀ {x xs y ys} (py : P y) → Any P {x ∷ xs} (y ∷ ys) + there : ∀ {x xs y ys} (pys : Any P ys) → Any P {x ∷ xs} (y ∷ ys) diff --git a/src/Wasm/Util/List/Prefix.agda b/src/Wasm/Util/List/Prefix.agda new file mode 100644 index 0000000..6216c39 --- /dev/null +++ b/src/Wasm/Util/List/Prefix.agda @@ -0,0 +1,36 @@ +{-# OPTIONS --safe --without-K #-} + +module Wasm.Util.List.Prefix where + +open import Data.Fin using (Fin; zero; suc; inject≤) +open import Data.List as L using (List; []; _∷_; _++_; length; take) +open import Data.List.Relation.Binary.Pointwise using (Pointwise; []; _∷_) +open import Data.Nat using (_≤_; z≤n; s≤s) +open import Level using (Level; _⊔_) +open import Relation.Binary using (Rel) +open import Relation.Binary.PropositionalEquality using (_≡_) +open import Wasm.Util.List.Map as M using ([]; _∷_) + +private + variable + a b c q r : Level + A : Set a + x y : A + xs ys : List A + R : Rel A r + +Prefix : ∀ {A : Set a} (R : Rel A r) (xs ys : List A) → Set (a ⊔ r) +Prefix R xs ys = Pointwise R xs (take (length xs) ys) + +data Map {A : Set a} {B : A → Set b} {C : A → Set c} {R : Rel A r} (Q : ∀ {x y} → R x y → B x → C y → Set q) : Prefix R xs ys → M.Map B xs → M.Map C ys → Set (a ⊔ b ⊔ c ⊔ q ⊔ r) where + [] : ∀ {ws : M.Map C ys} → Map Q [] [] ws + _∷_ : ∀ {z : B x} {w : C y} {zs : M.Map B xs} {ws : M.Map C ys} {r} {rs} → (q : Q r z w) → (qs : Map Q rs zs ws) → Map Q (r ∷ rs) (z ∷ zs) (w ∷ ws) + +length≤ : Prefix R xs ys → length xs ≤ length ys +length≤ {ys = []} [] = z≤n +length≤ {ys = y ∷ ys} [] = z≤n +length≤ {ys = y ∷ ys} (x∼y ∷ xs∼ys) = s≤s (length≤ xs∼ys) + +lookup : ∀ {xs ys} → (rs : Prefix R xs ys) → (i : Fin (length xs)) → R (L.lookup xs i) (L.lookup ys (inject≤ i (length≤ rs))) +lookup {ys = y ∷ ys} (x∼y ∷ xs∼ys) zero = x∼y +lookup {ys = y ∷ ys} (x∼y ∷ xs∼ys) (suc i) = lookup xs∼ys i diff --git a/src/Wasm/Value.agda b/src/Wasm/Value.agda index 9dfc24e..b28a5c8 100644 --- a/src/Wasm/Value.agda +++ b/src/Wasm/Value.agda @@ -2,7 +2,7 @@ module Wasm.Value where -open import Data.Fin using (Fin) +open import Data.Fin using (Fin; zero) open import Data.String using (String) Name : Set @@ -22,3 +22,9 @@ F32 = Fin 4294967296 F64 : Set F64 = Fin 18446744073709551616 + +0f32 : F32 +0f32 = zero + +0f64 : F64 +0f64 = zero |