-
Notifications
You must be signed in to change notification settings - Fork 0
/
Wasm.thy
236 lines (220 loc) · 26.8 KB
/
Wasm.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
theory Wasm imports Wasm_Base_Defs begin
(* TYPING RELATION *)
inductive b_e_typing :: "[t_context, b_e list, tf] \<Rightarrow> bool" ("_ \<turnstile> _ : _" 60) where
--"\<open>num ops\<close>"
const:"\<C> \<turnstile> [C v] : ([] _> [(typeof v)])"
| unop_i:"is_int_t t \<Longrightarrow> \<C> \<turnstile> [Unop_i t _] : ([t] _> [t])"
| unop_f:"is_float_t t \<Longrightarrow> \<C> \<turnstile> [Unop_f t _] : ([t] _> [t])"
| binop_i:"\<lbrakk>is_int_t t; (is_secret_t t \<longrightarrow> safe_binop_i iop)\<rbrakk> \<Longrightarrow> \<C> \<turnstile> [Binop_i t iop] : ([t,t] _> [t])"
| binop_f:"is_float_t t \<Longrightarrow> \<C> \<turnstile> [Binop_f t _] : ([t,t] _> [t])"
| testop:"is_int_t t \<Longrightarrow> \<C> \<turnstile> [Testop t _] : ([t] _> [(T_i32 (t_sec t))])"
| relop_i:"is_int_t t \<Longrightarrow> \<C> \<turnstile> [Relop_i t _] : ([t,t] _> [(T_i32 (t_sec t))])"
| relop_f:"is_float_t t \<Longrightarrow> \<C> \<turnstile> [Relop_f t _] : ([t,t] _> [(T_i32 (t_sec t))])"
--"\<open>convert\<close>"
| convert:"\<lbrakk>(t1 \<noteq> t2); t_sec t1 = t_sec t2; (sx = None) = ((is_float_t t1 \<and> is_float_t t2) \<or> (is_int_t t1 \<and> is_int_t t2 \<and> (t_length t1 < t_length t2)))\<rbrakk> \<Longrightarrow> \<C> \<turnstile> [Cvtop t1 Convert t2 sx] : ([t2] _> [t1])"
--"\<open>reinterpret\<close>"
| reinterpret:"\<lbrakk>(t1 \<noteq> t2); t_sec t1 = t_sec t2; t_length t1 = t_length t2\<rbrakk> \<Longrightarrow> \<C> \<turnstile> [Cvtop t1 Reinterpret t2 None] : ([t2] _> [t1])"
--"\<open>classify\<close>"
| classify:"\<lbrakk>is_int_t t2; is_public_t t2; classify_t t2 = t1\<rbrakk> \<Longrightarrow> \<C> \<turnstile> [Cvtop t1 Classify t2 None] : ([t2] _> [t1])"
--"\<open>declassify\<close>"
| declassify:"\<lbrakk>(trust_t \<C>) = Trusted; is_int_t t2; is_secret_t t2; declassify_t t2 = t1\<rbrakk> \<Longrightarrow> \<C> \<turnstile> [Cvtop t1 Declassify t2 None] : ([t2] _> [t1])"
--"\<open>unreachable, nop, drop, select\<close>"
| unreachable:"\<C> \<turnstile> [Unreachable] : (ts _> ts')"
| nop:"\<C> \<turnstile> [Nop] : ([] _> [])"
| drop:"\<C> \<turnstile> [Drop] : ([t] _> [])"
| select:"\<lbrakk>sec = Secret \<longrightarrow> is_secret_t t\<rbrakk> \<Longrightarrow> \<C> \<turnstile> [Select sec] : ([t,t,(T_i32 sec)] _> [t])"
--"\<open>block\<close>"
| block:"\<lbrakk>tf = (tn _> tm); \<C>\<lparr>label := ([tm] @ (label \<C>))\<rparr> \<turnstile> es : (tn _> tm)\<rbrakk> \<Longrightarrow> \<C> \<turnstile> [Block tf es] : (tn _> tm)"
--"\<open>loop\<close>"
| loop:"\<lbrakk>tf = (tn _> tm); \<C>\<lparr>label := ([tn] @ (label \<C>))\<rparr> \<turnstile> es : (tn _> tm)\<rbrakk> \<Longrightarrow> \<C> \<turnstile> [Loop tf es] : (tn _> tm)"
--"\<open>if then else\<close>"
| if_wasm:"\<lbrakk>tf = (tn _> tm); \<C>\<lparr>label := ([tm] @ (label \<C>))\<rparr> \<turnstile> es1 : (tn _> tm); \<C>\<lparr>label := ([tm] @ (label \<C>))\<rparr> \<turnstile> es2 : (tn _> tm)\<rbrakk> \<Longrightarrow> \<C> \<turnstile> [If tf es1 es2] : (tn @ [(T_i32 Public)] _> tm)"
--"\<open>br\<close>"
| br:"\<lbrakk>i < length(label \<C>); (label \<C>)!i = ts\<rbrakk> \<Longrightarrow> \<C> \<turnstile> [Br i] : (t1s @ ts _> t2s)"
--"\<open>br_if\<close>"
| br_if:"\<lbrakk>i < length(label \<C>); (label \<C>)!i = ts\<rbrakk> \<Longrightarrow> \<C> \<turnstile> [Br_if i] : (ts @ [(T_i32 Public)] _> ts)"
--"\<open>br_table\<close>"
| br_table:"\<lbrakk>list_all (\<lambda>i. i < length(label \<C>) \<and> (label \<C>)!i = ts) (is@[i])\<rbrakk> \<Longrightarrow> \<C> \<turnstile> [Br_table is i] : (t1s @ ts @ [(T_i32 Public)] _> t2s)"
--"\<open>return\<close>"
| return:"\<lbrakk>(return \<C>) = Some ts\<rbrakk> \<Longrightarrow> \<C> \<turnstile> [Return] : (t1s @ ts _> t2s)"
--"\<open>call\<close>"
| call:"\<lbrakk>trust_compat (trust_t \<C>) tr; i < length(func_t \<C>); (func_t \<C>)!i = (tr,tf)\<rbrakk> \<Longrightarrow> \<C> \<turnstile> [Call i] : tf"
--"\<open>call_indirect\<close>"
| call_indirect:"\<lbrakk>trust_compat (trust_t \<C>) tr; i < length(types_t \<C>); (types_t \<C>)!i = (tr,(t1s _> t2s)); (table \<C>) \<noteq> None\<rbrakk> \<Longrightarrow> \<C> \<turnstile> [Call_indirect i] : (t1s @ [(T_i32 Public)] _> t2s)"
--"\<open>get_local\<close>"
| get_local:"\<lbrakk>i < length(local \<C>); (local \<C>)!i = t\<rbrakk> \<Longrightarrow> \<C> \<turnstile> [Get_local i] : ([] _> [t])"
--"\<open>set_local\<close>"
| set_local:"\<lbrakk>i < length(local \<C>); (local \<C>)!i = t\<rbrakk> \<Longrightarrow> \<C> \<turnstile> [Set_local i] : ([t] _> [])"
--"\<open>tee_local\<close>"
| tee_local:"\<lbrakk>i < length(local \<C>); (local \<C>)!i = t\<rbrakk> \<Longrightarrow> \<C> \<turnstile> [Tee_local i] : ([t] _> [t])"
--"\<open>get_global\<close>"
| get_global:"\<lbrakk>i < length(global \<C>); tg_t ((global \<C>)!i) = t\<rbrakk> \<Longrightarrow> \<C> \<turnstile> [Get_global i] : ([] _> [t])"
--"\<open>set_global\<close>"
| set_global:"\<lbrakk>i < length(global \<C>); tg_t ((global \<C>)!i) = t; is_mut ((global \<C>)!i)\<rbrakk> \<Longrightarrow> \<C> \<turnstile> [Set_global i] : ([t] _> [])"
--"\<open>load\<close>"
| load:"\<lbrakk>(memory \<C>) = Some (n, sec); t_sec t = sec; load_store_t_bounds a (option_projl tp_sx) t\<rbrakk> \<Longrightarrow> \<C> \<turnstile> [Load t tp_sx a off] : ([(T_i32 Public)] _> [t])"
--"\<open>store\<close>"
| store:"\<lbrakk>(memory \<C>) = Some (n, sec); t_sec t = sec; load_store_t_bounds a tp t\<rbrakk> \<Longrightarrow> \<C> \<turnstile> [Store t tp a off] : ([(T_i32 Public),t] _> [])"
--"\<open>current_memory\<close>"
| current_memory:"(memory \<C>) = Some (n, sec) \<Longrightarrow> \<C> \<turnstile> [Current_memory] : ([] _> [(T_i32 Public)])"
--"\<open>Grow_memory\<close>"
| grow_memory:"(memory \<C>) = Some (n, sec) \<Longrightarrow> \<C> \<turnstile> [Grow_memory] : ([(T_i32 Public)] _> [(T_i32 Public)])"
--"\<open>empty program\<close>"
| empty:"\<C> \<turnstile> [] : ([] _> [])"
--"\<open>composition\<close>"
| composition:"\<lbrakk>\<C> \<turnstile> es : (t1s _> t2s); \<C> \<turnstile> [e] : (t2s _> t3s)\<rbrakk> \<Longrightarrow> \<C> \<turnstile> es @ [e] : (t1s _> t3s)"
--"\<open>weakening\<close>"
| weakening:"\<C> \<turnstile> es : (t1s _> t2s) \<Longrightarrow> \<C> \<turnstile> es : (ts @ t1s _> ts @ t2s)"
inductive cl_typing :: "[s_context, cl, tf_t] \<Rightarrow> bool" where
"\<lbrakk>i < length (s_inst \<S>); ((s_inst \<S>)!i) = \<C>; tf = (t1s _> t2s); \<C>\<lparr>trust_t := tr, local := (local \<C>) @ t1s @ ts, label := ([t2s] @ (label \<C>)), return := Some t2s\<rparr> \<turnstile> es : ([] _> t2s)\<rbrakk> \<Longrightarrow> cl_typing \<S> (Func_native i (tr,tf) ts es) (tr,(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] \<Rightarrow> bool" ("_\<bullet>_ \<turnstile> _ : _" 60)
and s_typing :: "[s_context, trust, (t list) option, nat, v list, e list, t list] \<Rightarrow> bool" ("_\<bullet>_\<bullet>_ \<tturnstile>'_ _ _;_ : _" 60) where
(* section: e_typing *)
(* lifting *)
"\<C> \<turnstile> b_es : tf \<Longrightarrow> \<S>\<bullet>\<C> \<turnstile> $*b_es : tf"
(* composition *)
| "\<lbrakk>\<S>\<bullet>\<C> \<turnstile> es : (t1s _> t2s); \<S>\<bullet>\<C> \<turnstile> [e] : (t2s _> t3s)\<rbrakk> \<Longrightarrow> \<S>\<bullet>\<C> \<turnstile> es @ [e] : (t1s _> t3s)"
(* weakening *)
| "\<S>\<bullet>\<C> \<turnstile> es : (t1s _> t2s) \<Longrightarrow>\<S>\<bullet>\<C> \<turnstile> es : (ts @ t1s _> ts @ t2s)"
(* trap *)
| "\<S>\<bullet>\<C> \<turnstile> [Trap] : tf"
(* local *)
| "\<lbrakk>\<S>\<bullet>(trust_t \<C>)\<bullet>Some ts \<tturnstile>_i vs;es : ts; length ts = n\<rbrakk> \<Longrightarrow> \<S>\<bullet>\<C> \<turnstile> [Local n i vs es] : ([] _> ts)"
(* callcl *)
| "\<lbrakk>trust_compat (trust_t \<C>) tr; cl_typing \<S> cl (tr,tf)\<rbrakk> \<Longrightarrow> \<S>\<bullet>\<C> \<turnstile> [Callcl cl] : tf"
(* label *)
| "\<lbrakk>\<S>\<bullet>\<C> \<turnstile> e0s : (ts _> t2s); \<S>\<bullet>\<C>\<lparr>label := ([ts] @ (label \<C>))\<rparr> \<turnstile> es : ([] _> t2s); length ts = n\<rbrakk> \<Longrightarrow> \<S>\<bullet>\<C> \<turnstile> [Label n e0s es] : ([] _> t2s)"
(* section: s_typing *)
| "\<lbrakk>i < (length (s_inst \<S>)); tvs = map typeof vs; \<C> =((s_inst \<S>)!i)\<lparr>trust_t := tr, local := (local ((s_inst \<S>)!i) @ tvs), return := rs\<rparr>; \<S>\<bullet>\<C> \<turnstile> es : ([] _> ts); (rs = Some ts) \<or> rs = None\<rbrakk> \<Longrightarrow> \<S>\<bullet>tr\<bullet>rs \<tturnstile>_i vs;es : ts"
definition "globi_agree gs n g = (n < length gs \<and> gs!n = g)"
definition "memi_agree sm j m = ((\<exists>j' m'. j = Some j' \<and> j' < length sm \<and> m = Some m' \<and> sm!j' = m') \<or> j = None \<and> m = None)"
definition "funci_agree fs n f = (n < length fs \<and> fs!n = f)"
inductive inst_typing :: "[s_context, inst, t_context] \<Rightarrow> bool" where
"\<lbrakk>list_all2 (funci_agree (s_funcs \<S>)) fs tfs; list_all2 (globi_agree (s_globs \<S>)) gs tgs; (i = Some i' \<and> i' < length (s_tab \<S>) \<and> (s_tab \<S>)!i' = (the n)) \<or> (i = None \<and> n = None); memi_agree (s_mem \<S>) j m\<rbrakk> \<Longrightarrow> inst_typing \<S> \<lparr>types = ts, funcs = fs, tab = i, mem = j, globs = gs\<rparr> \<lparr>trust_t = tr, types_t = ts, func_t = tfs, global = tgs, table = n, memory = m, local = [], label = [], return = None\<rparr>"
definition "glob_agree g tg = (tg_mut tg = g_mut g \<and> tg_t tg = typeof (g_val g))"
definition "tab_agree \<S> tcl = (case tcl of None \<Rightarrow> True | Some cl \<Rightarrow> \<exists>tf. cl_typing \<S> cl tf)"
definition "mem_agree bs m = (\<lambda> (bs,sec) (m,sec'). m \<le> mem_size bs \<and> sec = sec') bs m"
inductive store_typing :: "[s, s_context] \<Rightarrow> bool" where
"\<lbrakk>\<S> = \<lparr>s_inst = \<C>s, s_funcs = tfs, s_tab = ns, s_mem = ms, s_globs = tgs\<rparr>; list_all2 (inst_typing \<S>) insts \<C>s; list_all2 (cl_typing \<S>) fs tfs; list_all (tab_agree \<S>) (concat tclss); list_all2 (\<lambda> tcls n. n \<le> length tcls) tclss ns; list_all2 mem_agree bss ms; list_all2 glob_agree gs tgs\<rbrakk> \<Longrightarrow> store_typing \<lparr>s.inst = insts, s.funcs = fs, s.tab = tclss, s.mem = bss, s.globs = gs\<rparr> \<S>"
inductive config_typing :: "[nat, s, v list, e list, (trust \<times> t list)] \<Rightarrow> bool" ("\<turnstile>'_ _ _;_;_ : _" 60) where
"\<lbrakk>store_typing s \<S>; \<S>\<bullet>tr\<bullet>None \<tturnstile>_i vs;es : ts\<rbrakk> \<Longrightarrow> \<turnstile>_i s;vs;es : (tr,ts)"
(* REDUCTION RELATION *)
inductive reduce_simple :: "[e list, action, e list] \<Rightarrow> bool" ("\<lparr>_\<rparr> _\<leadsto> \<lparr>_\<rparr>" 60) where
--"\<open>integer unary ops\<close>"
unop_i32:"\<lparr>[$C (ConstInt32 sec' c), $(Unop_i (T_i32 sec) iop)]\<rparr> (Unop_i32_action iop)\<leadsto> \<lparr>[$C (ConstInt32 sec (app_unop_i iop c))]\<rparr>"
| unop_i64:"\<lparr>[$C (ConstInt64 sec' c), $(Unop_i (T_i64 sec) iop)]\<rparr> (Unop_i64_action iop)\<leadsto> \<lparr>[$C (ConstInt64 sec (app_unop_i iop c))]\<rparr>"
--"\<open>float unary ops\<close>"
| unop_f32:"\<lparr>[$C (ConstFloat32 c), $(Unop_f T_f32 fop)]\<rparr> (Unop_f32_action fop c)\<leadsto> \<lparr>[$C (ConstFloat32 (app_unop_f fop c))]\<rparr>"
| unop_f64:"\<lparr>[$C (ConstFloat64 c), $(Unop_f T_f64 fop)]\<rparr> (Unop_f64_action fop c)\<leadsto> \<lparr>[$C (ConstFloat64 (app_unop_f fop c))]\<rparr>"
--"\<open>int32 binary ops\<close>"
| binop_i32_Some:"\<lbrakk>app_binop_i iop c1 c2 = (Some c)\<rbrakk> \<Longrightarrow> \<lparr>[$C (ConstInt32 sec' c1), $C (ConstInt32 sec'' c2), $(Binop_i (T_i32 sec) iop)]\<rparr> (Binop_i32_Some_action iop c1 c2)\<leadsto> \<lparr>[$C (ConstInt32 sec c)]\<rparr>"
| binop_i32_None:"\<lbrakk>app_binop_i iop c1 c2 = None\<rbrakk> \<Longrightarrow> \<lparr>[$C (ConstInt32 sec' c1), $C (ConstInt32 sec'' c2), $(Binop_i (T_i32 sec) iop)]\<rparr> (Binop_i32_None_action iop c1 c2)\<leadsto> \<lparr>[Trap]\<rparr>"
--"\<open>int64 binary ops\<close>"
| binop_i64_Some:"\<lbrakk>app_binop_i iop c1 c2 = (Some c)\<rbrakk> \<Longrightarrow> \<lparr>[$C (ConstInt64 sec' c1), $C (ConstInt64 sec'' c2), $(Binop_i (T_i64 sec) iop)]\<rparr> (Binop_i64_Some_action iop c1 c2)\<leadsto> \<lparr>[$C (ConstInt64 sec c)]\<rparr>"
| binop_i64_None:"\<lbrakk>app_binop_i iop c1 c2 = None\<rbrakk> \<Longrightarrow> \<lparr>[$C (ConstInt64 sec' c1), $C (ConstInt64 sec'' c2), $(Binop_i (T_i64 sec) iop)]\<rparr> (Binop_i64_None_action iop c1 c2)\<leadsto> \<lparr>[Trap]\<rparr>"
--"\<open>float32 binary ops\<close>"
| binop_f32_Some:"\<lbrakk>app_binop_f fop c1 c2 = (Some c)\<rbrakk> \<Longrightarrow> \<lparr>[$C (ConstFloat32 c1), $C (ConstFloat32 c2), $(Binop_f T_f32 fop)]\<rparr> (Binop_f32_Some_action fop c1 c2)\<leadsto> \<lparr>[$C (ConstFloat32 c)]\<rparr>"
| binop_f32_None:"\<lbrakk>app_binop_f fop c1 c2 = None\<rbrakk> \<Longrightarrow> \<lparr>[$C (ConstFloat32 c1), $C (ConstFloat32 c2), $(Binop_f T_f32 fop)]\<rparr> (Binop_f32_None_action fop c1 c2)\<leadsto> \<lparr>[Trap]\<rparr>"
--"\<open>float64 binary ops\<close>"
| binop_f64_Some:"\<lbrakk>app_binop_f fop c1 c2 = (Some c)\<rbrakk> \<Longrightarrow> \<lparr>[$C (ConstFloat64 c1), $C (ConstFloat64 c2), $(Binop_f T_f64 fop)]\<rparr> (Binop_f64_Some_action fop c1 c2)\<leadsto> \<lparr>[$C (ConstFloat64 c)]\<rparr>"
| binop_f64_None:"\<lbrakk>app_binop_f fop c1 c2 = None\<rbrakk> \<Longrightarrow> \<lparr>[$C (ConstFloat64 c1), $C (ConstFloat64 c2), $(Binop_f T_f64 fop)]\<rparr> (Binop_f64_None_action fop c1 c2)\<leadsto> \<lparr>[Trap]\<rparr>"
--"\<open>testops\<close>"
| testop_i32:"\<lparr>[$C (ConstInt32 sec' c), $(Testop (T_i32 sec) testop)]\<rparr> (Testop_i32_action testop)\<leadsto> \<lparr>[$C ConstInt32 sec (wasm_bool (app_testop_i testop c))]\<rparr>"
| testop_i64:"\<lparr>[$C (ConstInt64 sec' c), $(Testop (T_i64 sec) testop)]\<rparr> (Testop_i64_action testop)\<leadsto> \<lparr>[$C ConstInt32 sec (wasm_bool (app_testop_i testop c))]\<rparr>"
--"\<open>int relops\<close>"
| relop_i32:"\<lparr>[$C (ConstInt32 sec' c1), $C (ConstInt32 sec'' c2), $(Relop_i (T_i32 sec) iop)]\<rparr> (Relop_i32_action iop)\<leadsto> \<lparr>[$C (ConstInt32 sec (wasm_bool (app_relop_i iop c1 c2)))]\<rparr>"
| relop_i64:"\<lparr>[$C (ConstInt64 sec' c1), $C (ConstInt64 sec'' c2), $(Relop_i (T_i64 sec) iop)]\<rparr> (Relop_i64_action iop)\<leadsto> \<lparr>[$C (ConstInt32 sec (wasm_bool (app_relop_i iop c1 c2)))]\<rparr>"
--"\<open>float relops\<close>"
| relop_f32:"\<lparr>[$C (ConstFloat32 c1), $C (ConstFloat32 c2), $(Relop_f T_f32 fop)]\<rparr> (Relop_f32_action fop c1 c2)\<leadsto> \<lparr>[$C (ConstInt32 Public (wasm_bool (app_relop_f fop c1 c2)))]\<rparr>"
| relop_f64:"\<lparr>[$C (ConstFloat64 c1), $C (ConstFloat64 c2), $(Relop_f T_f64 fop)]\<rparr> (Relop_f64_action fop c1 c2)\<leadsto> \<lparr>[$C (ConstInt32 Public (wasm_bool (app_relop_f fop c1 c2)))]\<rparr>"
--"\<open>convert\<close>"
| convert_Some:"\<lbrakk>types_agree_insecure t1 v; cvt t2 sx v = (Some v')\<rbrakk> \<Longrightarrow> \<lparr>[$(C v), $(Cvtop t2 Convert t1 sx)]\<rparr> (Convert_Some_action t1 t2 v)\<leadsto> \<lparr>[$(C v')]\<rparr>"
| convert_None:"\<lbrakk>types_agree_insecure t1 v; cvt t2 sx v = None\<rbrakk> \<Longrightarrow> \<lparr>[$(C v), $(Cvtop t2 Convert t1 sx)]\<rparr> (Convert_None_action t1 t2 v)\<leadsto> \<lparr>[Trap]\<rparr>"
--"\<open>reinterpret\<close>"
| reinterpret:"types_agree_insecure t1 v \<Longrightarrow> \<lparr>[$(C v), $(Cvtop t2 Reinterpret t1 None)]\<rparr> (Reinterpret_action)\<leadsto> \<lparr>[$(C (wasm_deserialise (bits v) t2))]\<rparr>"
--"\<open>classify\<close>"
| classify:"types_agree_insecure t1 v \<Longrightarrow> \<lparr>[$(C v), $(Cvtop t2 Classify t1 None)]\<rparr> (Classify_action)\<leadsto> \<lparr>[$(C (classify v))]\<rparr>"
--"\<open>declassify\<close>"
| declassify:"types_agree_insecure t1 v \<Longrightarrow> \<lparr>[$(C v), $(Cvtop t2 Declassify t1 None)]\<rparr> (Declassify_action)\<leadsto> \<lparr>[$(C (declassify v))]\<rparr>"
--"\<open>unreachable\<close>"
| unreachable:"\<lparr>[$ Unreachable]\<rparr> (Unreachable_action)\<leadsto> \<lparr>[Trap]\<rparr>"
--"\<open>nop\<close>"
| nop:"\<lparr>[$ Nop]\<rparr> (Nop_action)\<leadsto> \<lparr>[]\<rparr>"
--"\<open>drop\<close>"
| drop:"\<lparr>[$(C v), ($ Drop)]\<rparr> (Drop_action)\<leadsto> \<lparr>[]\<rparr>"
--"\<open>select\<close>"
| select_false:"int_eq n 0 \<Longrightarrow> \<lparr>[$(C v1), $(C v2), $C (ConstInt32 sec n), ($ Select sec')]\<rparr> (Select_action sec' n)\<leadsto> \<lparr>[$(C v2)]\<rparr>"
| select_true:"int_ne n 0 \<Longrightarrow> \<lparr>[$(C v1), $(C v2), $C (ConstInt32 sec n), ($ Select sec')]\<rparr> (Select_action sec' n)\<leadsto> \<lparr>[$(C v1)]\<rparr>"
--"\<open>block\<close>"
| block:"\<lbrakk>const_list vs; length vs = n; length t1s = n; length t2s = m\<rbrakk> \<Longrightarrow> \<lparr>vs @ [$(Block (t1s _> t2s) es)]\<rparr> (Block_action)\<leadsto> \<lparr>[Label m [] (vs @ ($* es))]\<rparr>"
--"\<open>loop\<close>"
| loop:"\<lbrakk>const_list vs; length vs = n; length t1s = n; length t2s = m\<rbrakk> \<Longrightarrow> \<lparr>vs @ [$(Loop (t1s _> t2s) es)]\<rparr> (Loop_action)\<leadsto> \<lparr>[Label n [$(Loop (t1s _> t2s) es)] (vs @ ($* es))]\<rparr>"
--"\<open>if\<close>"
| if_false:"int_eq n 0 \<Longrightarrow> \<lparr>[$C (ConstInt32 sec n), $(If tf e1s e2s)]\<rparr> (If_false_action n)\<leadsto> \<lparr>[$(Block tf e2s)]\<rparr>"
| if_true:"int_ne n 0 \<Longrightarrow> \<lparr>[$C (ConstInt32 sec n), $(If tf e1s e2s)]\<rparr> (If_true_action n)\<leadsto> \<lparr>[$(Block tf e1s)]\<rparr>"
--"\<open>label\<close>"
| label_const:"const_list vs \<Longrightarrow> \<lparr>[Label n es vs]\<rparr> (Label_const_action)\<leadsto> \<lparr>vs\<rparr>"
| label_trap:"\<lparr>[Label n es [Trap]]\<rparr> (Label_trap_action)\<leadsto> \<lparr>[Trap]\<rparr>"
--"\<open>br\<close>"
| br:"\<lbrakk>const_list vs; length vs = n; Lfilled i lholed (vs @ [$(Br i)]) LI\<rbrakk> \<Longrightarrow> \<lparr>[Label n es LI]\<rparr> (Br_action)\<leadsto> \<lparr>vs @ es\<rparr>"
--"\<open>br_if\<close>"
| br_if_false:"int_eq n 0 \<Longrightarrow> \<lparr>[$C (ConstInt32 sec n), $(Br_if i)]\<rparr> (Br_if_false_action n)\<leadsto> \<lparr>[]\<rparr>"
| br_if_true:"int_ne n 0 \<Longrightarrow> \<lparr>[$C (ConstInt32 sec n), $(Br_if i)]\<rparr> (Br_if_true_action n)\<leadsto> \<lparr>[$(Br i)]\<rparr>"
--"\<open>br_table\<close>"
| br_table:"\<lbrakk>length is > (nat_of_int c)\<rbrakk> \<Longrightarrow> \<lparr>[$C (ConstInt32 sec c), $(Br_table is i)]\<rparr> (Br_table_action c)\<leadsto> \<lparr>[$(Br (is!(nat_of_int c)))]\<rparr>"
| br_table_length:"\<lbrakk>length is \<le> (nat_of_int c)\<rbrakk> \<Longrightarrow> \<lparr>[$C (ConstInt32 sec c), $(Br_table is i)]\<rparr> (Br_table_length_action c)\<leadsto> \<lparr>[$(Br i)]\<rparr>"
--"\<open>local\<close>"
| local_const:"\<lbrakk>const_list es; length es = n\<rbrakk> \<Longrightarrow> \<lparr>[Local n i vs es]\<rparr> (Local_const_action)\<leadsto> \<lparr>es\<rparr>"
| local_trap:"\<lparr>[Local n i vs [Trap]]\<rparr> (Local_trap_action)\<leadsto> \<lparr>[Trap]\<rparr>"
--"\<open>return\<close>"
| return:"\<lbrakk>const_list vs; length vs = n; Lfilled j lholed (vs @ [$Return]) es\<rbrakk> \<Longrightarrow> \<lparr>[Local n i vls es]\<rparr> (Return_action)\<leadsto> \<lparr>vs\<rparr>"
--"\<open>tee_local\<close>"
| tee_local:"is_const v \<Longrightarrow> \<lparr>[v, $(Tee_local i)]\<rparr> (Tee_local_action)\<leadsto> \<lparr>[v, v, $(Set_local i)]\<rparr>"
| trap:"\<lbrakk>es \<noteq> [Trap]; Lfilled 0 lholed [Trap] es\<rbrakk> \<Longrightarrow> \<lparr>es\<rparr> (Trap_action)\<leadsto> \<lparr>[Trap]\<rparr>"
(* full reduction rule *)
inductive reduce :: "[s, v list, e list, action, nat, s, v list, e list] \<Rightarrow> bool" ("\<lparr>_;_;_\<rparr> _\<leadsto>'_ _ \<lparr>_;_;_\<rparr>" 60) where
--"\<open>lifting basic reduction\<close>"
basic:"\<lparr>e\<rparr> a\<leadsto> \<lparr>e'\<rparr> \<Longrightarrow> \<lparr>s;vs;e\<rparr> a\<leadsto>_i \<lparr>s;vs;e'\<rparr>"
--"\<open>call\<close>"
| call:"\<lparr>s;vs;[$(Call j)]\<rparr> (Call_action)\<leadsto>_i \<lparr>s;vs;[Callcl (sfunc s i j)]\<rparr>"
--"\<open>call_indirect\<close>"
| call_indirect_Some:"\<lbrakk>stab s i (nat_of_int c) = Some cl; stypes s i j = tf; cl_type cl = tf\<rbrakk> \<Longrightarrow> \<lparr>s;vs;[$C (ConstInt32 sec c), $(Call_indirect j)]\<rparr> (Call_indirect_Some_action c)\<leadsto>_i \<lparr>s;vs;[Callcl cl]\<rparr>"
| call_indirect_None:"\<lbrakk>(stab s i (nat_of_int c) = Some cl \<and> stypes s i j \<noteq> cl_type cl) \<or> stab s i (nat_of_int c) = None\<rbrakk> \<Longrightarrow> \<lparr>s;vs;[$C (ConstInt32 sec c), $(Call_indirect j)]\<rparr> (Call_indirect_None_action c)\<leadsto>_i \<lparr>s;vs;[Trap]\<rparr>"
--"\<open>call\<close>"
| callcl_native:"\<lbrakk>cl = Func_native j (tr,(t1s _> t2s)) ts es; ves = ($$* vcs); length vcs = n; length ts = k; length t1s = n; length t2s = m; (n_zeros ts = zs) \<rbrakk> \<Longrightarrow> \<lparr>s;vs;ves @ [Callcl cl]\<rparr> (Callcl_native_action n)\<leadsto>_i \<lparr>s;vs;[Local m j (vcs@zs) [$(Block ([] _> t2s) es)]]\<rparr>"
| callcl_host_Some:"\<lbrakk>cl = Func_host (tr,(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')\<rbrakk> \<Longrightarrow> \<lparr>s;vs;ves @ [Callcl cl]\<rparr> (Callcl_host_Some_action s vcs s' vcs' tr (t1s _> t2s) f hs)\<leadsto>_i \<lparr>s';vs;($$* vcs')\<rparr>"
| callcl_host_None:"\<lbrakk>cl = Func_host (tr,(t1s _> t2s)) f; ves = ($$* vcs); length vcs = n; length t1s = n; length t2s = m\<rbrakk> \<Longrightarrow> \<lparr>s;vs;ves @ [Callcl cl]\<rparr> (Callcl_host_None_action s vcs tr (t1s _> t2s) f hs)\<leadsto>_i \<lparr>s;vs;[Trap]\<rparr>"
--"\<open>get_local\<close>"
| get_local:"\<lbrakk>length vi = j\<rbrakk> \<Longrightarrow> \<lparr>s;(vi @ [v] @ vs);[$(Get_local j)]\<rparr> (Get_local_action)\<leadsto>_i \<lparr>s;(vi @ [v] @ vs);[$(C v)]\<rparr>"
--"\<open>set_local\<close>"
| set_local:"\<lbrakk>length vi = j\<rbrakk> \<Longrightarrow> \<lparr>s;(vi @ [v] @ vs);[$(C v'), $(Set_local j)]\<rparr> (Set_local_action)\<leadsto>_i \<lparr>s;(vi @ [v'] @ vs);[]\<rparr>"
--"\<open>get_global\<close>"
| get_global:"\<lparr>s;vs;[$(Get_global j)]\<rparr> (Get_global_action)\<leadsto>_i \<lparr>s;vs;[$ C(sglob_val s i j)]\<rparr>"
--"\<open>set_global\<close>"
| set_global:"supdate_glob s i j v = s' \<Longrightarrow> \<lparr>s;vs;[$(C v), $(Set_global j)]\<rparr> (Set_global_action)\<leadsto>_i \<lparr>s';vs;[]\<rparr>"
--"\<open>load\<close>"
| load_Some:"\<lbrakk>smem_ind s i = Some j; ((mem s)!j) = (m,sec); load m (nat_of_int k) off (t_length t) = Some bs\<rbrakk> \<Longrightarrow> \<lparr>s;vs;[$C (ConstInt32 sec' k), $(Load t None a off)]\<rparr> (Load_Some_action t (nat_of_int k) a off)\<leadsto>_i \<lparr>s;vs;[$C (wasm_deserialise bs t)]\<rparr>"
| load_None:"\<lbrakk>smem_ind s i = Some j; ((mem s)!j) = (m,sec); load m (nat_of_int k) off (t_length t) = None\<rbrakk> \<Longrightarrow> \<lparr>s;vs;[$C (ConstInt32 sec' k), $(Load t None a off)]\<rparr> (Load_None_action t (nat_of_int k) a off)\<leadsto>_i \<lparr>s;vs;[Trap]\<rparr>"
--"\<open>load packed\<close>"
| load_packed_Some:"\<lbrakk>smem_ind s i = Some j; ((mem s)!j) = (m,sec); load_packed sx m (nat_of_int k) off (tp_length tp) (t_length t) = Some bs\<rbrakk> \<Longrightarrow> \<lparr>s;vs;[$C (ConstInt32 sec' k), $(Load t (Some (tp, sx)) a off)]\<rparr> (Load_packed_Some_action tp sx (nat_of_int k) a off)\<leadsto>_i \<lparr>s;vs;[$C (wasm_deserialise bs t)]\<rparr>"
| load_packed_None:"\<lbrakk>smem_ind s i = Some j; ((mem s)!j) = (m,sec); load_packed sx m (nat_of_int k) off (tp_length tp) (t_length t) = None\<rbrakk> \<Longrightarrow> \<lparr>s;vs;[$C (ConstInt32 sec' k), $(Load t (Some (tp, sx)) a off)]\<rparr> (Load_packed_None_action tp sx (nat_of_int k) a off)\<leadsto>_i \<lparr>s;vs;[Trap]\<rparr>"
--"\<open>store\<close>"
| store_Some:"\<lbrakk>types_agree_insecure t v; smem_ind s i = Some j; ((mem s)!j) = (m,sec); store m (nat_of_int k) off (bits v) (t_length t) = Some mem'\<rbrakk> \<Longrightarrow> \<lparr>s;vs;[$C (ConstInt32 sec' k), $C v, $(Store t None a off)]\<rparr> (Store_Some_action t (nat_of_int k) a off)\<leadsto>_i \<lparr>s\<lparr>mem:= ((mem s)[j := (mem',sec)])\<rparr>;vs;[]\<rparr>"
| store_None:"\<lbrakk>types_agree_insecure t v; smem_ind s i = Some j; ((mem s)!j) = (m,sec); store m (nat_of_int k) off (bits v) (t_length t) = None\<rbrakk> \<Longrightarrow> \<lparr>s;vs;[$C (ConstInt32 sec' k), $C v, $(Store t None a off)]\<rparr> (Store_None_action t (nat_of_int k) a off)\<leadsto>_i \<lparr>s;vs;[Trap]\<rparr>"
--"\<open>store packed\<close>" (* take only (tp_length tp) lower order bytes *)
| store_packed_Some:"\<lbrakk>types_agree_insecure t v; smem_ind s i = Some j; ((mem s)!j) = (m,sec); store_packed m (nat_of_int k) off (bits v) (tp_length tp) = Some mem'\<rbrakk> \<Longrightarrow> \<lparr>s;vs;[$C (ConstInt32 sec' k), $C v, $(Store t (Some tp) a off)]\<rparr> (Store_packed_Some_action t tp (nat_of_int k) a off)\<leadsto>_i \<lparr>s\<lparr>mem:= ((mem s)[j := (mem',sec)])\<rparr>;vs;[]\<rparr>"
| store_packed_None:"\<lbrakk>types_agree_insecure t v; smem_ind s i = Some j; ((mem s)!j) = (m,sec); store_packed m (nat_of_int k) off (bits v) (tp_length tp) = None\<rbrakk> \<Longrightarrow> \<lparr>s;vs;[$C (ConstInt32 sec' k), $C v, $(Store t (Some tp) a off)]\<rparr> (Store_packed_None_action t tp (nat_of_int k) a off)\<leadsto>_i \<lparr>s;vs;[Trap]\<rparr>"
--"\<open>current_memory\<close>"
| current_memory:"\<lbrakk>smem_ind s i = Some j; ((mem s)!j) = (m,sec); mem_size m = n\<rbrakk> \<Longrightarrow> \<lparr>s;vs;[ $(Current_memory)]\<rparr> (Current_memory_action n)\<leadsto>_i \<lparr>s;vs;[$C (ConstInt32 Public (int_of_nat n))]\<rparr>"
--"\<open>grow_memory\<close>"
| grow_memory:"\<lbrakk>smem_ind s i = Some j; ((mem s)!j) = (m,sec); mem_size m = n; mem_grow m (nat_of_int c) = mem'\<rbrakk> \<Longrightarrow> \<lparr>s;vs;[$C (ConstInt32 sec' c), $(Grow_memory)]\<rparr> (Grow_memory_Some_action n (nat_of_int c))\<leadsto>_i \<lparr>s\<lparr>mem:= ((mem s)[j := (mem',sec)])\<rparr>;vs;[$C (ConstInt32 Public (int_of_nat n))]\<rparr>"
--"\<open>grow_memory fail\<close>"
| grow_memory_fail:"\<lbrakk>smem_ind s i = Some j; ((mem s)!j) = (m,sec); mem_size m = n\<rbrakk> \<Longrightarrow> \<lparr>s;vs;[$C (ConstInt32 sec' c),$(Grow_memory)]\<rparr> (Grow_memory_None_action n (nat_of_int c))\<leadsto>_i \<lparr>s;vs;[$C (ConstInt32 Public int32_minus_one)]\<rparr>"
(* The bad ones. *)
--"\<open>inductive label reduction\<close>"
| label:"\<lbrakk>\<lparr>s;vs;es\<rparr> a\<leadsto>_i \<lparr>s';vs';es'\<rparr>; Lfilled k lholed es les; Lfilled k lholed es' les'\<rbrakk> \<Longrightarrow> \<lparr>s;vs;les\<rparr> a\<leadsto>_i \<lparr>s';vs';les'\<rparr>"
--"\<open>inductive local reduction\<close>"
| local:"\<lbrakk>\<lparr>s;vs;es\<rparr> a\<leadsto>_i \<lparr>s';vs';es'\<rparr>\<rbrakk> \<Longrightarrow> \<lparr>s;v0s;[Local n i vs es]\<rparr> a\<leadsto>_j \<lparr>s';v0s;[Local n i vs' es']\<rparr>"
end