Theory Wasm_Base_Defs
section ‹WebAssembly Base Definitions›
theory Wasm_Base_Defs imports Wasm_Ast Wasm_Type_Abs begin
instantiation i32 :: wasm_int begin instance .. end
instantiation i64 :: wasm_int begin instance .. end
instantiation f32 :: wasm_float begin instance .. end
instantiation f64 :: wasm_float begin instance .. end
consts
ui32_trunc_f32 :: "f32 ⇒ i32 option"
si32_trunc_f32 :: "f32 ⇒ i32 option"
ui32_trunc_f64 :: "f64 ⇒ i32 option"
si32_trunc_f64 :: "f64 ⇒ i32 option"
ui64_trunc_f32 :: "f32 ⇒ i64 option"
si64_trunc_f32 :: "f32 ⇒ i64 option"
ui64_trunc_f64 :: "f64 ⇒ i64 option"
si64_trunc_f64 :: "f64 ⇒ i64 option"
f32_convert_ui32 :: "i32 ⇒ f32"
f32_convert_si32 :: "i32 ⇒ f32"
f32_convert_ui64 :: "i64 ⇒ f32"
f32_convert_si64 :: "i64 ⇒ f32"
f64_convert_ui32 :: "i32 ⇒ f64"
f64_convert_si32 :: "i32 ⇒ f64"
f64_convert_ui64 :: "i64 ⇒ f64"
f64_convert_si64 :: "i64 ⇒ f64"
wasm_wrap :: "i64 ⇒ i32"
wasm_extend_u :: "i32 ⇒ i64"
wasm_extend_s :: "i32 ⇒ i64"
wasm_demote :: "f64 ⇒ f32"
wasm_promote :: "f32 ⇒ f64"
serialise_i32 :: "i32 ⇒ bytes"
serialise_i64 :: "i64 ⇒ bytes"
serialise_f32 :: "f32 ⇒ bytes"
serialise_f64 :: "f64 ⇒ bytes"
wasm_bool :: "bool ⇒ i32"
int32_minus_one :: i32
definition mem_size :: "mem ⇒ nat" where
"mem_size m = length (Rep_mem m)"
definition mem_grow :: "mem ⇒ nat ⇒ mem" where
"mem_grow m n = mem_append m (bytes_replicate (n * 64000) 0)"
definition load :: "mem ⇒ nat ⇒ off ⇒ nat ⇒ bytes option" where
"load m n off l = (if (mem_size m ≥ (n+off+l))
then Some (read_bytes m (n+off) l)
else None)"
definition sign_extend :: "sx ⇒ nat ⇒ bytes ⇒ bytes" where
"sign_extend sx l bytes = (let msb = msb (msbyte bytes) in
let byte = (case sx of U ⇒ 0 | S ⇒ if msb then -1 else 0) in
bytes_takefill byte l bytes)"
definition load_packed :: "sx ⇒ mem ⇒ nat ⇒ off ⇒ nat ⇒ nat ⇒ bytes option" where
"load_packed sx m n off lp l = map_option (sign_extend sx l) (load m n off lp)"
definition store :: "mem ⇒ nat ⇒ off ⇒ bytes ⇒ nat ⇒ mem option" where
"store m n off bs l = (if (mem_size m ≥ (n+off+l))
then Some (write_bytes m (n+off) (bytes_takefill 0 l bs))
else None)"
definition store_packed :: "mem ⇒ nat ⇒ off ⇒ bytes ⇒ nat ⇒ mem option" where
"store_packed = store"
consts
wasm_deserialise :: "bytes ⇒ t ⇒ v"
host_apply :: "s ⇒ tf ⇒ host ⇒ v list ⇒ host_state ⇒ (s × v list) option"
definition typeof :: " v ⇒ t" where
"typeof v = (case v of
ConstInt32 _ ⇒ T_i32
| ConstInt64 _ ⇒ T_i64
| ConstFloat32 _ ⇒ T_f32
| ConstFloat64 _ ⇒ T_f64)"
definition option_projl :: "('a × 'b) option ⇒ 'a option" where
"option_projl x = map_option fst x"
definition option_projr :: "('a × 'b) option ⇒ 'b option" where
"option_projr x = map_option snd x"
definition t_length :: "t ⇒ nat" where
"t_length t = (case t of
T_i32 ⇒ 4
| T_i64 ⇒ 8
| T_f32 ⇒ 4
| T_f64 ⇒ 8)"
definition tp_length :: "tp ⇒ nat" where
"tp_length tp = (case tp of
Tp_i8 ⇒ 1
| Tp_i16 ⇒ 2
| Tp_i32 ⇒ 4)"
definition is_int_t :: "t ⇒ bool" where
"is_int_t t = (case t of
T_i32 ⇒ True
| T_i64 ⇒ True
| T_f32 ⇒ False
| T_f64 ⇒ False)"
definition is_float_t :: "t ⇒ bool" where
"is_float_t t = (case t of
T_i32 ⇒ False
| T_i64 ⇒ False
| T_f32 ⇒ True
| T_f64 ⇒ True)"
definition is_mut :: "tg ⇒ bool" where
"is_mut tg = (tg_mut tg = T_mut)"
definition app_unop_i :: "unop_i ⇒ 'i::wasm_int ⇒ 'i::wasm_int" where
"app_unop_i iop c =
(case iop of
Ctz ⇒ int_ctz c
| Clz ⇒ int_clz c
| Popcnt ⇒ int_popcnt c)"
definition app_unop_f :: "unop_f ⇒ 'f::wasm_float ⇒ 'f::wasm_float" where
"app_unop_f fop c =
(case fop of
Neg ⇒ float_neg c
| Abs ⇒ float_abs c
| Ceil ⇒ float_ceil c
| Floor ⇒ float_floor c
| Trunc ⇒ float_trunc c
| Nearest ⇒ float_nearest c
| Sqrt ⇒ float_sqrt c)"
definition app_binop_i :: "binop_i ⇒ 'i::wasm_int ⇒ 'i::wasm_int ⇒ ('i::wasm_int) option" where
"app_binop_i iop c1 c2 = (case iop of
Add ⇒ Some (int_add c1 c2)
| Sub ⇒ Some (int_sub c1 c2)
| Mul ⇒ Some (int_mul c1 c2)
| Div U ⇒ int_div_u c1 c2
| Div S ⇒ int_div_s c1 c2
| Rem U ⇒ int_rem_u c1 c2
| Rem S ⇒ int_rem_s c1 c2
| And ⇒ Some (int_and c1 c2)
| Or ⇒ Some (int_or c1 c2)
| Xor ⇒ Some (int_xor c1 c2)
| Shl ⇒ Some (int_shl c1 c2)
| Shr U ⇒ Some (int_shr_u c1 c2)
| Shr S ⇒ Some (int_shr_s c1 c2)
| Rotl ⇒ Some (int_rotl c1 c2)
| Rotr ⇒ Some (int_rotr c1 c2))"
definition app_binop_f :: "binop_f ⇒ 'f::wasm_float ⇒ 'f::wasm_float ⇒ ('f::wasm_float) option" where
"app_binop_f fop c1 c2 = (case fop of
Addf ⇒ Some (float_add c1 c2)
| Subf ⇒ Some (float_sub c1 c2)
| Mulf ⇒ Some (float_mul c1 c2)
| Divf ⇒ Some (float_div c1 c2)
| Min ⇒ Some (float_min c1 c2)
| Max ⇒ Some (float_max c1 c2)
| Copysign ⇒ Some (float_copysign c1 c2))"
definition app_testop_i :: "testop ⇒ 'i::wasm_int ⇒ bool" where
"app_testop_i testop c = (case testop of Eqz ⇒ int_eqz c)"
definition app_relop_i :: "relop_i ⇒ 'i::wasm_int ⇒ 'i::wasm_int ⇒ bool" where
"app_relop_i rop c1 c2 = (case rop of
Eq ⇒ int_eq c1 c2
| Ne ⇒ int_ne c1 c2
| Lt U ⇒ int_lt_u c1 c2
| Lt S ⇒ int_lt_s c1 c2
| Gt U ⇒ int_gt_u c1 c2
| Gt S ⇒ int_gt_s c1 c2
| Le U ⇒ int_le_u c1 c2
| Le S ⇒ int_le_s c1 c2
| Ge U ⇒ int_ge_u c1 c2
| Ge S ⇒ int_ge_s c1 c2)"
definition app_relop_f :: "relop_f ⇒ 'f::wasm_float ⇒ 'f::wasm_float ⇒ bool" where
"app_relop_f rop c1 c2 = (case rop of
Eqf ⇒ float_eq c1 c2
| Nef ⇒ float_ne c1 c2
| Ltf ⇒ float_lt c1 c2
| Gtf ⇒ float_gt c1 c2
| Lef ⇒ float_le c1 c2
| Gef ⇒ float_ge c1 c2)"
definition types_agree :: "t ⇒ v ⇒ bool" where
"types_agree t v = (typeof v = t)"
definition cl_type :: "cl ⇒ tf" where
"cl_type cl = (case cl of Func_native _ tf _ _ ⇒ tf | Func_host tf _ ⇒ tf)"
definition rglob_is_mut :: "global ⇒ bool" where
"rglob_is_mut g = (g_mut g = T_mut)"
definition stypes :: "s ⇒ nat ⇒ nat ⇒ tf" where
"stypes s i j = ((types ((inst s)!i))!j)"
definition sfunc_ind :: "s ⇒ nat ⇒ nat ⇒ nat" where
"sfunc_ind s i j = ((inst.funcs ((inst s)!i))!j)"
definition sfunc :: "s ⇒ nat ⇒ nat ⇒ cl" where
"sfunc s i j = (funcs s)!(sfunc_ind s i j)"
definition sglob_ind :: "s ⇒ nat ⇒ nat ⇒ nat" where
"sglob_ind s i j = ((inst.globs ((inst s)!i))!j)"
definition sglob :: "s ⇒ nat ⇒ nat ⇒ global" where
"sglob s i j = (globs s)!(sglob_ind s i j)"
definition sglob_val :: "s ⇒ nat ⇒ nat ⇒ v" where
"sglob_val s i j = g_val (sglob s i j)"
definition smem_ind :: "s ⇒ nat ⇒ nat option" where
"smem_ind s i = (inst.mem ((inst s)!i))"
definition stab_s :: "s ⇒ nat ⇒ nat ⇒ cl option" where
"stab_s s i j = (let stabinst = ((tab s)!i) in (if (length (stabinst) > j) then (stabinst!j) else None))"
definition stab :: "s ⇒ nat ⇒ nat ⇒ cl option" where
"stab s i j = (case (inst.tab ((inst s)!i)) of Some k => stab_s s k j | None => None)"
definition supdate_glob_s :: "s ⇒ nat ⇒ v ⇒ s" where
"supdate_glob_s s k v = s⦇globs := (globs s)[k:=((globs s)!k)⦇g_val := v⦈]⦈"
definition supdate_glob :: "s ⇒ nat ⇒ nat ⇒ v ⇒ s" where
"supdate_glob s i j v = (let k = sglob_ind s i j in supdate_glob_s s k v)"
definition is_const :: "e ⇒ bool" where
"is_const e = (case e of Basic (C _) ⇒ True | _ ⇒ False)"
definition const_list :: "e list ⇒ bool" where
"const_list xs = list_all is_const xs"
inductive store_extension :: "s ⇒ s ⇒ bool" where
"⟦insts = insts'; fs = fs'; tclss = tclss'; list_all2 (λbs bs'. mem_size bs ≤ mem_size bs') bss bss'; gs = gs'⟧ ⟹
store_extension ⦇s.inst = insts, s.funcs = fs, s.tab = tclss, s.mem = bss, s.globs = gs⦈
⦇s.inst = insts', s.funcs = fs', s.tab = tclss', s.mem = bss', s.globs = gs'⦈"
abbreviation to_e_list :: "b_e list ⇒ e list" (‹$* _› 60) where
"to_e_list b_es ≡ map Basic b_es"
abbreviation v_to_e_list :: "v list ⇒ e list" (‹$$* _› 60) where
"v_to_e_list ves ≡ map (λv. $C v) ves"
inductive Lfilled :: "nat ⇒ Lholed ⇒ e list ⇒ e list ⇒ bool" where
L0:"⟦const_list vs; lholed = (LBase vs es')⟧ ⟹ Lfilled 0 lholed es (vs @ es @ es')"
| LN:"⟦const_list vs; lholed = (LRec vs n es' l es''); Lfilled k l es lfilledk⟧ ⟹ Lfilled (k+1) lholed es (vs @ [Label n es' lfilledk] @ es'')"
inductive Lfilled_exact :: "nat ⇒ Lholed ⇒ e list ⇒ e list ⇒ bool" where
L0:"⟦lholed = (LBase [] [])⟧ ⟹ Lfilled_exact 0 lholed es es"
| LN:"⟦const_list vs; lholed = (LRec vs n es' l es''); Lfilled_exact k l es lfilledk⟧ ⟹ Lfilled_exact (k+1) lholed es (vs @ [Label n es' lfilledk] @ es'')"
definition load_store_t_bounds :: "a ⇒ tp option ⇒ t ⇒ bool" where
"load_store_t_bounds a tp t = (case tp of
None ⇒ 2^a ≤ t_length t
| Some tp ⇒ 2^a ≤ tp_length tp ∧ tp_length tp < t_length t ∧ is_int_t t)"
definition cvt_i32 :: "sx option ⇒ v ⇒ i32 option" where
"cvt_i32 sx v = (case v of
ConstInt32 c ⇒ None
| ConstInt64 c ⇒ Some (wasm_wrap c)
| ConstFloat32 c ⇒ (case sx of
Some U ⇒ ui32_trunc_f32 c
| Some S ⇒ si32_trunc_f32 c
| None ⇒ None)
| ConstFloat64 c ⇒ (case sx of
Some U ⇒ ui32_trunc_f64 c
| Some S ⇒ si32_trunc_f64 c
| None ⇒ None))"
definition cvt_i64 :: "sx option ⇒ v ⇒ i64 option" where
"cvt_i64 sx v = (case v of
ConstInt32 c ⇒ (case sx of
Some U ⇒ Some (wasm_extend_u c)
| Some S ⇒ Some (wasm_extend_s c)
| None ⇒ None)
| ConstInt64 c ⇒ None
| ConstFloat32 c ⇒ (case sx of
Some U ⇒ ui64_trunc_f32 c
| Some S ⇒ si64_trunc_f32 c
| None ⇒ None)
| ConstFloat64 c ⇒ (case sx of
Some U ⇒ ui64_trunc_f64 c
| Some S ⇒ si64_trunc_f64 c
| None ⇒ None))"
definition cvt_f32 :: "sx option ⇒ v ⇒ f32 option" where
"cvt_f32 sx v = (case v of
ConstInt32 c ⇒ (case sx of
Some U ⇒ Some (f32_convert_ui32 c)
| Some S ⇒ Some (f32_convert_si32 c)
| _ ⇒ None)
| ConstInt64 c ⇒ (case sx of
Some U ⇒ Some (f32_convert_ui64 c)
| Some S ⇒ Some (f32_convert_si64 c)
| _ ⇒ None)
| ConstFloat32 c ⇒ None
| ConstFloat64 c ⇒ Some (wasm_demote c))"
definition cvt_f64 :: "sx option ⇒ v ⇒ f64 option" where
"cvt_f64 sx v = (case v of
ConstInt32 c ⇒ (case sx of
Some U ⇒ Some (f64_convert_ui32 c)
| Some S ⇒ Some (f64_convert_si32 c)
| _ ⇒ None)
| ConstInt64 c ⇒ (case sx of
Some U ⇒ Some (f64_convert_ui64 c)
| Some S ⇒ Some (f64_convert_si64 c)
| _ ⇒ None)
| ConstFloat32 c ⇒ Some (wasm_promote c)
| ConstFloat64 c ⇒ None)"
definition cvt :: "t ⇒ sx option ⇒ v ⇒ v option" where
"cvt t sx v = (case t of
T_i32 ⇒ (case (cvt_i32 sx v) of Some c ⇒ Some (ConstInt32 c) | None ⇒ None)
| T_i64 ⇒ (case (cvt_i64 sx v) of Some c ⇒ Some (ConstInt64 c) | None ⇒ None)
| T_f32 ⇒ (case (cvt_f32 sx v) of Some c ⇒ Some (ConstFloat32 c) | None ⇒ None)
| T_f64 ⇒ (case (cvt_f64 sx v) of Some c ⇒ Some (ConstFloat64 c) | None ⇒ None))"
definition bits :: "v ⇒ bytes" where
"bits v = (case v of
ConstInt32 c ⇒ (serialise_i32 c)
| ConstInt64 c ⇒ (serialise_i64 c)
| ConstFloat32 c ⇒ (serialise_f32 c)
| ConstFloat64 c ⇒ (serialise_f64 c))"
definition bitzero :: "t ⇒ v" where
"bitzero t = (case t of
T_i32 ⇒ ConstInt32 0
| T_i64 ⇒ ConstInt64 0
| T_f32 ⇒ ConstFloat32 0
| T_f64 ⇒ ConstFloat64 0)"
definition n_zeros :: "t list ⇒ v list" where
"n_zeros ts = (map (λt. bitzero t) ts)"
lemma is_int_t_exists:
assumes "is_int_t t"
shows "t = T_i32 ∨ t = T_i64"
using assms
by (cases t) (auto simp add: is_int_t_def)
lemma is_float_t_exists:
assumes "is_float_t t"
shows "t = T_f32 ∨ t = T_f64"
using assms
by (cases t) (auto simp add: is_float_t_def)
lemma int_float_disjoint: "is_int_t t = -(is_float_t t)"
by simp (metis is_float_t_def is_int_t_def t.exhaust t.simps(13-16))
lemma stab_unfold:
assumes "stab s i j = Some cl"
shows "∃k. inst.tab ((inst s)!i) = Some k ∧ length ((tab s)!k) > j ∧((tab s)!k)!j = Some cl"
proof -
obtain k where have_k:"(inst.tab ((inst s)!i)) = Some k"
using assms
unfolding stab_def
by fastforce
hence s_o:"stab s i j = stab_s s k j"
using assms
unfolding stab_def
by simp
then obtain stabinst where stabinst_def:"stabinst = ((tab s)!k)"
by blast
hence "stab_s s k j = (stabinst!j) ∧ (length stabinst > j)"
using assms s_o
unfolding stab_s_def
by (cases "(length stabinst > j)", auto)
thus ?thesis
using have_k stabinst_def assms s_o
by auto
qed
lemma inj_basic: "inj Basic"
by (meson e.inject(1) injI)
lemma inj_basic_econst: "inj (λv. $C v)"
by (meson b_e.inject(16) e.inject(1) injI)
lemma to_e_list_1:"[$ a] = $* [a]"
by simp
lemma to_e_list_2:"[$ a, $ b] = $* [a, b]"
by simp
lemma to_e_list_3:"[$ a, $ b, $ c] = $* [a, b, c]"
by simp
lemma v_exists_b_e:"∃ves. ($$*vs) = ($*ves)"
proof (induction vs)
case (Cons a vs)
thus ?case
by (metis list.simps(9))
qed auto
lemma Lfilled_exact_imp_Lfilled:
assumes "Lfilled_exact n lholed es LI"
shows "Lfilled n lholed es LI"
using assms
proof (induction rule: Lfilled_exact.induct)
case (L0 lholed es)
thus ?case
using const_list_def Lfilled.intros(1)
by fastforce
next
case (LN vs lholed n es' l es'' k es lfilledk)
thus ?case
using Lfilled.intros(2)
by fastforce
qed
lemma Lfilled_exact_app_imp_exists_Lfilled:
assumes "const_list ves"
"Lfilled_exact n lholed (ves@es) LI"
shows "∃lholed'. Lfilled n lholed' es LI"
using assms(2,1)
proof (induction "(ves@es)" LI rule: Lfilled_exact.induct)
case (L0 lholed)
show ?case
using Lfilled.intros(1)[OF L0(2), of _ "[]"]
by fastforce
next
case (LN vs lholed n es' l es'' k lfilledk)
thus ?case
using Lfilled.intros(2)
by fastforce
qed
lemma Lfilled_imp_exists_Lfilled_exact:
assumes "Lfilled n lholed es LI"
shows "∃lholed' ves es_c. const_list ves ∧ Lfilled_exact n lholed' (ves@es@es_c) LI"
using assms Lfilled_exact.intros
by (induction rule: Lfilled.induct) fastforce+
lemma n_zeros_typeof:
"n_zeros ts = vs ⟹ (ts = map typeof vs)"
proof (induction ts arbitrary: vs)
case Nil
thus ?case
unfolding n_zeros_def
by simp
next
case (Cons t ts)
obtain vs' where "n_zeros ts = vs'"
using n_zeros_def
by blast
moreover
have "typeof (bitzero t) = t"
unfolding typeof_def bitzero_def
by (cases t, simp_all)
ultimately
show ?case
using Cons
unfolding n_zeros_def
by auto
qed
end