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 ⦇s⦇mem:= ((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 ⦇s⦇mem:= ((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 ⦇s⦇mem:= ((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