Quelle  Wasm.thy

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

inductive cl_typing :: "[s_context, cl, tf] ==> bool" where
   "[i < length (s_inst S); ((s_inst S)!i) = C; tf = (t1s _> t2s); C(local := (local C) @ t1s @ ts, label := ([t2s] @ (label C)), return := Some t2s) ⊨ es : ([] _> t2s)] ==> cl_typing S (Func_native i tf ts es) (t1s _> t2s)"
|  "cl_typing S (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 *)
  "C ⊨ b_es : tf ==> S∙C ⊨ $*b_es : tf"
  (* composition *)
| "[S∙C ⊨ es : (t1s _> t2s); S∙C ⊨ [e] : (t2s _> t3s)] ==> S∙C ⊨ es @ [e] : (t1s _> t3s)"
  (* weakening *)
| "S∙C ⊨ es : (t1s _> t2s) ==>S∙C ⊨ es : (ts @ t1s _> ts @ t2s)"
  (* trap *)
| "S∙C ⊨ [Trap] : tf"
  (* local *)
| "[S∙Some ts ⊨!!!_i vs;es : ts; length ts = n] ==> S∙C ⊨ [Local n i vs es] : ([] _> ts)"
  (* callcl *)
| "[cl_typing S cl tf] ==> S∙C ⊨ [Callcl cl] : tf"
  (* label *)
| "[S∙C ⊨ e0s : (ts _> t2s); S∙C(label := ([ts] @ (label C))) ⊨ es : ([] _> t2s); length ts = n] ==> S∙C ⊨ [Label n e0s es] : ([] _> t2s)"
(* section: s_typing *)
| "[i < (length (s_inst S)); tvs = map typeof vs; C =((s_inst S)!i)(local := (local ((s_inst S)!i) @ tvs), return := rs); S∙C ⊨ es : ([] _> ts); (rs = Some ts) ∨ rs = None] ==> S∙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 S)) fs tfs; list_all2 (globi_agree (s_globs S)) gs tgs; (i = Some i' ∧ i' < length (s_tab S) ∧ (s_tab S)!i' = (the n)) ∨ (i = None ∧ n = None); memi_agree (s_mem S) j m] ==> inst_typing S (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 S tcl = (case tcl of None ==> True | Some cl ==> ∃tf. cl_typing S cl tf)"

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

inductive store_typing :: "[s, s_context] ==> bool" where
  "[S = (s_inst = Cs, s_funcs = tfs, s_tab = ns, s_mem = ms, s_globs = tgs); list_all2 (inst_typing S) insts Cs; list_all2 (cl_typing S) fs tfs; list_all (tab_agree S) (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) S"

inductive config_typing :: "[nat, s, v list, e list, t list] ==> bool" (‹⊨'_ _ _;_;_ : _› 60) where
  "[store_typing s S; 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