Theory Wasm

theory Wasm imports Wasm_Base_Defs begin

(* TYPING RELATION *)
inductive b_e_typing :: "[t_context, b_e list, tf]  bool" ("_  _ : _" 60) where
  ― ‹num ops›
  const:"𝒞  [C v]         : ([]    _> [(typeof v)])"
| unop_i:"is_int_t t    𝒞  [Unop_i t _]  : ([t]   _> [t])"
| unop_f:"is_float_t t  𝒞  [Unop_f t _]  : ([t]   _> [t])"
| binop_i:"is_int_t t    𝒞  [Binop_i t iop] : ([t,t] _> [t])"
| binop_f:"is_float_t t  𝒞  [Binop_f t _] : ([t,t] _> [t])"
| testop:"is_int_t t    𝒞  [Testop t _]  : ([t]   _> [T_i32])"
| relop_i:"is_int_t t    𝒞  [Relop_i t _] : ([t,t] _> [T_i32])"
| relop_f:"is_float_t t  𝒞  [Relop_f t _] : ([t,t] _> [T_i32])"
  ― ‹convert›
| convert:"(t1  t2); (sx = None) = ((is_float_t t1  is_float_t t2)  (is_int_t t1  is_int_t t2  (t_length t1 < t_length t2)))  𝒞  [Cvtop t1 Convert t2 sx] : ([t2] _> [t1])"
  ― ‹reinterpret›
| reinterpret:"(t1  t2); t_length t1 = t_length t2  𝒞  [Cvtop t1 Reinterpret t2 None] : ([t2] _> [t1])"
  ― ‹unreachable, nop, drop, select›
| unreachable:"𝒞  [Unreachable] : (ts _> ts')"
| nop:"𝒞  [Nop] : ([] _> [])"
| drop:"𝒞  [Drop] : ([t] _> [])"
| select:"𝒞  [Select] : ([t,t,T_i32] _> [t])"
  ― ‹block›
| block:"tf = (tn _> tm); 𝒞label := ([tm] @ (label 𝒞))  es : (tn _> tm)  𝒞  [Block tf es] : (tn _> tm)"
  ― ‹loop›
| loop:"tf = (tn _> tm); 𝒞label := ([tn] @ (label 𝒞))  es : (tn _> tm)  𝒞  [Loop tf es] : (tn _> tm)"
  ― ‹if then else›
| if_wasm:"tf = (tn _> tm); 𝒞label := ([tm] @ (label 𝒞))  es1 : (tn _> tm); 𝒞label := ([tm] @ (label 𝒞))  es2 : (tn _> tm)  𝒞  [If tf es1 es2] : (tn @ [T_i32] _> tm)"
  ― ‹br›
| br:"i < length(label 𝒞); (label 𝒞)!i = ts  𝒞  [Br i] : (t1s @ ts _> t2s)"
  ― ‹br_if›
| br_if:"i < length(label 𝒞); (label 𝒞)!i = ts  𝒞  [Br_if i] : (ts @ [T_i32] _> ts)"
  ― ‹br_table›
| br_table:"list_all (λi. i < length(label 𝒞)  (label 𝒞)!i = ts) (is@[i])  𝒞  [Br_table is i] : (t1s @ ts @ [T_i32] _> t2s)"
  ― ‹return›
| return:"(return 𝒞) = Some ts  𝒞  [Return] : (t1s @ ts _> t2s)"
  ― ‹call›
| call:"i < length(func_t 𝒞); (func_t 𝒞)!i = tf  𝒞  [Call i] : tf"
  ― ‹call_indirect›
| call_indirect:"i < length(types_t 𝒞); (types_t 𝒞)!i = (t1s _> t2s); (table 𝒞)  None  𝒞  [Call_indirect i] : (t1s @ [T_i32] _> t2s)"
  ― ‹get_local›
| get_local:"i < length(local 𝒞); (local 𝒞)!i = t  𝒞  [Get_local i] : ([] _> [t])"
  ― ‹set_local›
| set_local:"i < length(local 𝒞); (local 𝒞)!i = t  𝒞  [Set_local i] : ([t] _> [])"
  ― ‹tee_local›
| tee_local:"i < length(local 𝒞); (local 𝒞)!i = t  𝒞  [Tee_local i] : ([t] _> [t])"
  ― ‹get_global›
| get_global:"i < length(global 𝒞); tg_t ((global 𝒞)!i) = t  𝒞  [Get_global i] : ([] _> [t])"
  ― ‹set_global›
| set_global:"i < length(global 𝒞); tg_t ((global 𝒞)!i) = t; is_mut ((global 𝒞)!i)  𝒞  [Set_global i] : ([t] _> [])"
  ― ‹load›
| load:"(memory 𝒞) = Some n; load_store_t_bounds a (option_projl tp_sx) t  𝒞  [Load t tp_sx a off] : ([T_i32] _> [t])"
  ― ‹store›
| store:"(memory 𝒞) = Some n; load_store_t_bounds a tp t  𝒞  [Store t tp a off] : ([T_i32,t] _> [])"
  ― ‹current_memory›
| current_memory:"(memory 𝒞) = Some n  𝒞  [Current_memory] : ([] _> [T_i32])"
  ― ‹Grow_memory›
| grow_memory:"(memory 𝒞) = Some n  𝒞  [Grow_memory] : ([T_i32] _> [T_i32])"
  ― ‹empty program›
| empty:"𝒞  [] : ([] _> [])"
  ― ‹composition›
| composition:"𝒞  es : (t1s _> t2s); 𝒞  [e] : (t2s _> t3s)  𝒞  es @ [e] : (t1s _> t3s)"
  ― ‹weakening›
| weakening:"𝒞  es : (t1s _> t2s)  𝒞  es : (ts @ t1s _> ts @ t2s)"

inductive cl_typing :: "[s_context, cl, tf]  bool" where
   "i < length (s_inst 𝒮); ((s_inst 𝒮)!i) = 𝒞; tf = (t1s _> t2s); 𝒞local := (local 𝒞) @ t1s @ ts, label := ([t2s] @ (label 𝒞)), return := Some t2s  es : ([] _> t2s)  cl_typing 𝒮 (Func_native i tf ts es) (t1s _> t2s)"
|  "cl_typing 𝒮 (Func_host tf h) tf"

(* lifting the b_e_typing relation to the administrative operators *)
inductive e_typing :: "[s_context, t_context, e list, tf]  bool" ("__  _ : _" 60)
and       s_typing :: "[s_context, (t list) option, nat, v list, e list, t list]  bool" ("__ ⊩'_ _ _;_ : _" 60) where
(* section: e_typing *)
  (* lifting *)
  "𝒞  b_es : tf  𝒮𝒞  $*b_es : tf"
  (* composition *)
| "𝒮𝒞  es : (t1s _> t2s); 𝒮𝒞  [e] : (t2s _> t3s)  𝒮𝒞  es @ [e] : (t1s _> t3s)"
  (* weakening *)
| "𝒮𝒞  es : (t1s _> t2s) 𝒮𝒞  es : (ts @ t1s _> ts @ t2s)"
  (* trap *)
| "𝒮𝒞  [Trap] : tf"
  (* local *)
| "𝒮Some ts ⊩_i vs;es : ts; length ts = n  𝒮𝒞  [Local n i vs es] : ([] _> ts)"
  (* callcl *)
| "cl_typing 𝒮 cl tf  𝒮𝒞   [Callcl cl] : tf"
  (* label *)
| "𝒮𝒞  e0s : (ts _> t2s); 𝒮𝒞label := ([ts] @ (label 𝒞))  es : ([] _> t2s); length ts = n  𝒮𝒞  [Label n e0s es] : ([] _> t2s)"
(* section: s_typing *)
| "i < (length (s_inst 𝒮)); tvs = map typeof vs; 𝒞 =((s_inst 𝒮)!i)local := (local ((s_inst 𝒮)!i) @ tvs), return := rs; 𝒮𝒞  es : ([] _> ts); (rs = Some ts)  rs = None  𝒮rs ⊩_i vs;es : ts"

definition "globi_agree gs n g = (n < length gs  gs!n = g)"

definition "memi_agree sm j m = ((j' m'. j = Some j'  j' < length sm   m = Some m'  sm!j' = m')  j = None  m = None)"

definition "funci_agree fs n f = (n < length fs  fs!n = f)"

inductive inst_typing :: "[s_context, inst, t_context]  bool" where
  "list_all2 (funci_agree (s_funcs 𝒮)) fs tfs; list_all2 (globi_agree (s_globs 𝒮)) gs tgs; (i = Some i'  i' < length (s_tab 𝒮)  (s_tab 𝒮)!i' = (the n))  (i = None  n = None); memi_agree (s_mem 𝒮) j m  inst_typing 𝒮 types = ts, funcs = fs, tab = i, mem = j, globs = gs types_t = ts, func_t = tfs, global = tgs, table = n, memory = m, local = [], label = [], return = None"

definition "glob_agree g tg = (tg_mut tg = g_mut g  tg_t tg = typeof (g_val g))"

definition "tab_agree 𝒮 tcl = (case tcl of None  True | Some cl  tf. cl_typing 𝒮 cl tf)"

definition "mem_agree bs m = (λ bs m. m  mem_size bs) bs m"

inductive store_typing :: "[s, s_context]  bool" where
  "𝒮 = s_inst = 𝒞s, s_funcs = tfs, s_tab = ns, s_mem = ms, s_globs = tgs; list_all2 (inst_typing 𝒮) insts 𝒞s; list_all2 (cl_typing 𝒮) fs tfs; list_all (tab_agree 𝒮) (concat tclss); list_all2 (λ tcls n. n  length tcls) tclss ns; list_all2 mem_agree bss ms; list_all2 glob_agree gs tgs  store_typing s.inst = insts, s.funcs = fs, s.tab = tclss, s.mem = bss, s.globs = gs 𝒮"

inductive config_typing :: "[nat, s, v list, e list, t list]  bool" ("⊢'_ _ _;_;_ : _" 60) where
  "store_typing s 𝒮; 𝒮None ⊩_i vs;es : ts  ⊢_i s;vs;es : ts"

(* REDUCTION RELATION *)

inductive reduce_simple :: "[e list, e list]  bool" ("_  _" 60) where
  ― ‹integer unary ops›
  unop_i32:"[$C (ConstInt32 c), $(Unop_i T_i32 iop)]  [$C (ConstInt32 (app_unop_i iop c))]"
| unop_i64:"[$C (ConstInt64 c), $(Unop_i T_i64 iop)]  [$C (ConstInt64 (app_unop_i iop c))]"
  ― ‹float unary ops›
| unop_f32:"[$C (ConstFloat32 c), $(Unop_f T_f32 fop)]  [$C (ConstFloat32 (app_unop_f fop c))]"
| unop_f64:"[$C (ConstFloat64 c), $(Unop_f T_f64 fop)]  [$C (ConstFloat64 (app_unop_f fop c))]"
  ― ‹int32 binary ops›
| binop_i32_Some:"app_binop_i iop c1 c2 = (Some c)  [$C (ConstInt32 c1), $C (ConstInt32 c2), $(Binop_i T_i32 iop)]  [$C (ConstInt32 c)]"
| binop_i32_None:"app_binop_i iop c1 c2 = None  [$C (ConstInt32 c1), $C (ConstInt32 c2), $(Binop_i T_i32 iop)]  [Trap]"
  ― ‹int64 binary ops›
| binop_i64_Some:"app_binop_i iop c1 c2 = (Some c)  [$C (ConstInt64 c1), $C (ConstInt64 c2), $(Binop_i T_i64 iop)]  [$C (ConstInt64 c)]"
| binop_i64_None:"app_binop_i iop c1 c2 = None  [$C (ConstInt64 c1), $C (ConstInt64 c2), $(Binop_i T_i64 iop)]  [Trap]"
  ― ‹float32 binary ops›
| binop_f32_Some:"app_binop_f fop c1 c2 = (Some c)  [$C (ConstFloat32 c1), $C (ConstFloat32 c2), $(Binop_f T_f32 fop)]  [$C (ConstFloat32 c)]"
| binop_f32_None:"app_binop_f fop c1 c2 = None  [$C (ConstFloat32 c1), $C (ConstFloat32 c2), $(Binop_f T_f32 fop)]  [Trap]"
  ― ‹float64 binary ops›
| binop_f64_Some:"app_binop_f fop c1 c2 = (Some c)  [$C (ConstFloat64 c1), $C (ConstFloat64 c2), $(Binop_f T_f64 fop)]  [$C (ConstFloat64 c)]"
| binop_f64_None:"app_binop_f fop c1 c2 = None  [$C (ConstFloat64 c1), $C (ConstFloat64 c2), $(Binop_f T_f64 fop)]  [Trap]"
  ― ‹testops›
| testop_i32:"[$C (ConstInt32 c), $(Testop T_i32 testop)]  [$C ConstInt32 (wasm_bool (app_testop_i testop c))]"
| testop_i64:"[$C (ConstInt64 c), $(Testop T_i64 testop)]  [$C ConstInt32 (wasm_bool (app_testop_i testop c))]"
  ― ‹int relops›
| relop_i32:"[$C (ConstInt32 c1), $C (ConstInt32 c2), $(Relop_i T_i32 iop)]  [$C (ConstInt32 (wasm_bool (app_relop_i iop c1 c2)))]"
| relop_i64:"[$C (ConstInt64 c1), $C (ConstInt64 c2), $(Relop_i T_i64 iop)]  [$C (ConstInt32 (wasm_bool (app_relop_i iop c1 c2)))]"
  ― ‹float relops›
| relop_f32:"[$C (ConstFloat32 c1), $C (ConstFloat32 c2), $(Relop_f T_f32 fop)]  [$C (ConstInt32 (wasm_bool (app_relop_f fop c1 c2)))]"
| relop_f64:"[$C (ConstFloat64 c1), $C (ConstFloat64 c2), $(Relop_f T_f64 fop)]  [$C (ConstInt32 (wasm_bool (app_relop_f fop c1 c2)))]"
  ― ‹convert›
| convert_Some:"types_agree t1 v; cvt t2 sx v = (Some v')  [$(C v), $(Cvtop t2 Convert t1 sx)]  [$(C v')]"
| convert_None:"types_agree t1 v; cvt t2 sx v = None  [$(C v), $(Cvtop t2 Convert t1 sx)]  [Trap]"
  ― ‹reinterpret›
| reinterpret:"types_agree t1 v  [$(C v), $(Cvtop t2 Reinterpret t1 None)]  [$(C (wasm_deserialise (bits v) t2))]"
  ― ‹unreachable›
| unreachable:"[$ Unreachable]  [Trap]"
  ― ‹nop›
| nop:"[$ Nop]  []"
  ― ‹drop›
| drop:"[$(C v), ($ Drop)]  []"
  ― ‹select›
| select_false:"int_eq n 0  [$(C v1), $(C v2), $C (ConstInt32 n), ($ Select)]  [$(C v2)]"
| select_true:"int_ne n 0  [$(C v1), $(C v2), $C (ConstInt32 n), ($ Select)]  [$(C v1)]"
  ― ‹block›
| block:"const_list vs; length vs = n; length t1s = n; length t2s = m  vs @ [$(Block (t1s _> t2s) es)]  [Label m [] (vs @ ($* es))]"
  ― ‹loop›
| loop:"const_list vs; length vs = n; length t1s = n; length t2s = m  vs @ [$(Loop (t1s _> t2s) es)]  [Label n [$(Loop (t1s _> t2s) es)] (vs @ ($* es))]"
  ― ‹if›
| if_false:"int_eq n 0  [$C (ConstInt32 n), $(If tf e1s e2s)]  [$(Block tf e2s)]"
| if_true:"int_ne n 0  [$C (ConstInt32 n), $(If tf e1s e2s)]  [$(Block tf e1s)]"
  ― ‹label›
| label_const:"const_list vs  [Label n es vs]  vs"
| label_trap:"[Label n es [Trap]]  [Trap]"
  ― ‹br›
| br:"const_list vs; length vs = n; Lfilled i lholed (vs @ [$(Br i)]) LI  [Label n es LI]  vs @ es"
  ― ‹br_if›
| br_if_false:"int_eq n 0  [$C (ConstInt32 n), $(Br_if i)]  []"
| br_if_true:"int_ne n 0  [$C (ConstInt32 n), $(Br_if i)]  [$(Br i)]"
  ― ‹br_table›
| br_table:"length is > (nat_of_int c)  [$C (ConstInt32 c), $(Br_table is i)]  [$(Br (is!(nat_of_int c)))]"
| br_table_length:"length is  (nat_of_int c)  [$C (ConstInt32 c), $(Br_table is i)]  [$(Br i)]"
  ― ‹local›
| local_const:"const_list es; length es = n  [Local n i vs es]  es"
| local_trap:"[Local n i vs [Trap]]  [Trap]"
  ― ‹return›
| return:"const_list vs; length vs = n; Lfilled j lholed (vs @ [$Return]) es   [Local n i vls es]  vs"
  ― ‹tee_local›
| tee_local:"is_const v  [v, $(Tee_local i)]  [v, v, $(Set_local i)]"
| trap:"es  [Trap]; Lfilled 0 lholed [Trap] es  es  [Trap]"

(* full reduction rule *)
inductive reduce :: "[s, v list, e list, nat, s, v list, e list]  bool" ("_;_;_ ↝'_ _ _;_;_" 60) where
  ― ‹lifting basic reduction›
  basic:"e  e'  s;vs;e ↝_i s;vs;e'"
  ― ‹call›
| call:"s;vs;[$(Call j)] ↝_i s;vs;[Callcl (sfunc s i j)]"
  ― ‹call_indirect›
| call_indirect_Some:"stab s i (nat_of_int c) = Some cl; stypes s i j = tf; cl_type cl = tf  s;vs;[$C (ConstInt32 c), $(Call_indirect j)] ↝_i s;vs;[Callcl cl]"
| call_indirect_None:"(stab s i (nat_of_int c) = Some cl  stypes s i j  cl_type cl)  stab s i (nat_of_int c) = None  s;vs;[$C (ConstInt32 c), $(Call_indirect j)] ↝_i s;vs;[Trap]"
  ― ‹call›
| callcl_native:"cl = Func_native j (t1s _> t2s) ts es; ves = ($$* vcs); length vcs = n; length ts = k; length t1s = n; length t2s = m; (n_zeros ts = zs)   s;vs;ves @ [Callcl cl] ↝_i s;vs;[Local m j (vcs@zs) [$(Block ([] _> t2s) es)]]"
| callcl_host_Some:"cl = Func_host (t1s _> t2s) f; ves = ($$* vcs); length vcs = n; length t1s = n; length t2s = m; host_apply s (t1s _> t2s) f vcs hs = Some (s', vcs')  s;vs;ves @ [Callcl cl] ↝_i s';vs;($$* vcs')"
| callcl_host_None:"cl = Func_host (t1s _> t2s) f; ves = ($$* vcs); length vcs = n; length t1s = n; length t2s = m  s;vs;ves @ [Callcl cl] ↝_i s;vs;[Trap]"
  ― ‹get_local›
| get_local:"length vi = j  s;(vi @ [v] @ vs);[$(Get_local j)] ↝_i s;(vi @ [v] @ vs);[$(C v)]"
  ― ‹set_local›
| set_local:"length vi = j  s;(vi @ [v] @ vs);[$(C v'), $(Set_local j)] ↝_i s;(vi @ [v'] @ vs);[]"
  ― ‹get_global›
| get_global:"s;vs;[$(Get_global j)] ↝_i s;vs;[$ C(sglob_val s i j)]"
  ― ‹set_global›
| set_global:"supdate_glob s i j v = s'  s;vs;[$(C v), $(Set_global j)] ↝_i s';vs;[]"
  ― ‹load›
| load_Some:"smem_ind s i = Some j; ((mem s)!j) = m; load m (nat_of_int k) off (t_length t) = Some bs  s;vs;[$C (ConstInt32 k), $(Load t None a off)] ↝_i s;vs;[$C (wasm_deserialise bs t)]"
| load_None:"smem_ind s i = Some j; ((mem s)!j) = m; load m (nat_of_int k) off (t_length t) = None  s;vs;[$C (ConstInt32 k), $(Load t None a off)] ↝_i s;vs;[Trap]"
  ― ‹load packed›
| load_packed_Some:"smem_ind s i = Some j; ((mem s)!j) = m; load_packed sx m (nat_of_int k) off (tp_length tp) (t_length t) = Some bs  s;vs;[$C (ConstInt32 k), $(Load t (Some (tp, sx)) a off)] ↝_i s;vs;[$C (wasm_deserialise bs t)]"
| load_packed_None:"smem_ind s i = Some j; ((mem s)!j) = m; load_packed sx m (nat_of_int k) off (tp_length tp) (t_length t) = None  s;vs;[$C (ConstInt32 k), $(Load t (Some (tp, sx)) a off)] ↝_i s;vs;[Trap]"
  ― ‹store›
| store_Some:"types_agree t v; smem_ind s i = Some j; ((mem s)!j) = m; store m (nat_of_int k) off (bits v) (t_length t) = Some mem'  s;vs;[$C (ConstInt32 k), $C v, $(Store t None a off)] ↝_i smem:= ((mem s)[j := mem']);vs;[]"
| store_None:"types_agree t v; smem_ind s i = Some j; ((mem s)!j) = m; store m (nat_of_int k) off (bits v) (t_length t) = None  s;vs;[$C (ConstInt32 k), $C v, $(Store t None a off)] ↝_i s;vs;[Trap]"
  ― ‹store packed› (* take only (tp_length tp) lower order bytes *)
| store_packed_Some:"types_agree t v; smem_ind s i = Some j; ((mem s)!j) = m; store_packed m (nat_of_int k) off (bits v) (tp_length tp) = Some mem'  s;vs;[$C (ConstInt32 k), $C v, $(Store t (Some tp) a off)] ↝_i smem:= ((mem s)[j := mem']);vs;[]"
| store_packed_None:"types_agree t v; smem_ind s i = Some j; ((mem s)!j) = m; store_packed m (nat_of_int k) off (bits v) (tp_length tp) = None  s;vs;[$C (ConstInt32 k), $C v, $(Store t (Some tp) a off)] ↝_i s;vs;[Trap]"
  ― ‹current_memory›
| current_memory:"smem_ind s i = Some j; ((mem s)!j) = m; mem_size m = n  s;vs;[ $(Current_memory)] ↝_i s;vs;[$C (ConstInt32 (int_of_nat n))]"
  ― ‹grow_memory›
| grow_memory:"smem_ind s i = Some j; ((mem s)!j) = m; mem_size m = n; mem_grow m (nat_of_int c) = mem'  s;vs;[$C (ConstInt32 c), $(Grow_memory)] ↝_i smem:= ((mem s)[j := mem']);vs;[$C (ConstInt32 (int_of_nat n))]"
  ― ‹grow_memory fail›
| grow_memory_fail:"smem_ind s i = Some j; ((mem s)!j) = m; mem_size m = n  s;vs;[$C (ConstInt32 c),$(Grow_memory)] ↝_i s;vs;[$C (ConstInt32 int32_minus_one)]"
  (* The bad ones. *)
  ― ‹inductive label reduction›
| label:"s;vs;es ↝_i s';vs';es'; Lfilled k lholed es les; Lfilled k lholed es' les'  s;vs;les ↝_i s';vs';les'"
  ― ‹inductive local reduction›
| local:"s;vs;es ↝_i s';vs';es'  s;v0s;[Local n i vs es] ↝_j s';v0s;[Local n i vs' es']"

end