1(*
2 * Copyright 2014, General Dynamics C4 Systems
3 *
4 * This software may be distributed and modified according to the terms of
5 * the GNU General Public License version 2. Note that NO WARRANTY is provided.
6 * See "LICENSE_GPLv2.txt" for details.
7 *
8 * @TAG(GD_GPL)
9 *)
10
11theory ArchKHeap_AI
12imports "../KHeapPre_AI"
13begin
14
15context Arch begin global_naming ARM
16
17fun
18  non_vspace_obj :: "kernel_object \<Rightarrow> bool"
19where
20  "non_vspace_obj (ArchObj _)           = False"
21| "non_vspace_obj _                     = True"
22
23lemma obj_at_split: "(obj_at (P xo) p s \<and> (Q xo)) = obj_at (\<lambda>ko. P xo ko \<and> Q xo) p s"
24  by (auto simp: obj_at_def)
25
26lemma valid_vspace_objs_lift:
27  assumes x: "\<And>P. \<lbrace>\<lambda>s. P (vs_lookup s)\<rbrace> f \<lbrace>\<lambda>_ s. P (vs_lookup s)\<rbrace>"
28  assumes y: "\<And>ako p. \<lbrace>\<lambda>s. \<not> ko_at (ArchObj ako) p s\<rbrace> f \<lbrace>\<lambda>rv s. \<not> ko_at (ArchObj ako) p s\<rbrace>"
29  assumes z: "\<And>p T. \<lbrace>typ_at (AArch T) p\<rbrace> f \<lbrace>\<lambda>rv. typ_at (AArch T) p\<rbrace>"
30  shows      "\<lbrace>valid_vspace_objs\<rbrace> f \<lbrace>\<lambda>rv. valid_vspace_objs\<rbrace>"
31  apply (simp add: valid_vspace_objs_def)
32  apply (rule hoare_vcg_all_lift, wp hoare_convert_imp[OF x]; (rule hoare_vcg_all_lift | assumption))
33  apply (rule hoare_convert_imp[OF y])
34  apply (rule valid_vspace_obj_typ[OF z])
35  done
36
37lemma vspace_obj_imp: "non_arch_obj ko \<Longrightarrow> non_vspace_obj ko"
38  apply (cases ko; clarsimp)
39  apply (rename_tac ako)
40  apply (case_tac ako, auto simp: non_arch_obj_def)
41  done
42
43lemma non_vspace_objs[intro]:
44  "non_vspace_obj (Endpoint ep)"
45  "non_vspace_obj (CNode sz cnode_contents)"
46  "non_vspace_obj (TCB tcb)"
47  "non_vspace_obj (Notification notification)"
48  by (auto)
49
50definition vspace_obj_pred :: "(kernel_object \<Rightarrow> bool) \<Rightarrow> bool" where
51  "vspace_obj_pred P \<equiv>
52    \<forall>ko ko'. non_vspace_obj ko \<longrightarrow> non_vspace_obj ko' \<longrightarrow>
53      P ko = P ko'"
54
55lemma vspace_obj_predE:
56  "\<lbrakk>vspace_obj_pred P; non_vspace_obj ko; non_vspace_obj ko'\<rbrakk> \<Longrightarrow> P ko = P ko'"
57  apply (unfold vspace_obj_pred_def)
58  apply (erule allE[where ?x="ko"])
59  apply (erule allE[where ?x="ko'"])
60  by blast
61
62lemmas vspace_obj_pred_defs = non_vspace_objs vspace_obj_pred_def
63
64lemma vspace_pred_imp: "vspace_obj_pred P \<Longrightarrow> arch_obj_pred P"
65  apply (clarsimp simp: arch_obj_pred_def)
66  apply (rule vspace_obj_predE)
67    apply simp
68   apply (rule vspace_obj_imp, assumption)+
69  done
70
71lemma vspace_obj_pred_a_type[intro, simp]: "vspace_obj_pred (\<lambda>ko. a_type ko = AArch T)"
72  by (auto simp add: vspace_obj_pred_defs a_type_def
73           split: kernel_object.splits arch_kernel_obj.splits)
74
75lemma
76  vspace_obj_pred_arch_obj_l[intro, simp]:
77     "vspace_obj_pred (\<lambda>ko. ArchObj ako = ko)" and
78  vspace_obj_pred_arch_obj_r[intro, simp]:
79     "vspace_obj_pred (\<lambda>ko. ko = ArchObj ako)"
80  apply (simp add: vspace_obj_pred_defs)
81  apply (rule allI[OF impI[OF allI[OF impI]]])
82  apply (auto simp add: vspace_obj_pred_defs
83              split: kernel_object.splits arch_kernel_obj.splits)
84done
85
86lemma vspace_obj_pred_fun_lift: "vspace_obj_pred (\<lambda>ko. F (vspace_obj_fun_lift P N ko))"
87  by (auto simp: vspace_obj_pred_defs vspace_obj_fun_lift_def
88           split: kernel_object.splits arch_kernel_obj.splits)
89
90lemmas vspace_obj_pred_fun_lift_id[simp]
91  = vspace_obj_pred_fun_lift[where F=id, simplified]
92
93lemmas vspace_obj_pred_fun_lift_k[intro]
94  = vspace_obj_pred_fun_lift[where F="K R" for R, simplified]
95
96lemmas vspace_obj_pred_fun_lift_el[simp]
97  = vspace_obj_pred_fun_lift[where F="\<lambda> S. x \<in> S" for x, simplified]
98
99lemma vspace_obj_pred_const_conjI[intro]:
100  "vspace_obj_pred P \<Longrightarrow>
101    vspace_obj_pred P' \<Longrightarrow>
102    vspace_obj_pred (\<lambda>ko. P ko \<and> P' ko)"
103  apply (simp only: vspace_obj_pred_def)
104  apply blast
105  done
106
107lemma vspace_obj_pred_fI:
108  "(\<And>x. vspace_obj_pred (P x)) \<Longrightarrow> vspace_obj_pred (\<lambda>ko. f (\<lambda>x :: 'a :: type. P x ko))"
109  apply (simp only: vspace_obj_pred_def)
110  apply (intro allI impI)
111  apply (rule arg_cong[where f=f])
112  by blast
113
114declare
115  vspace_obj_pred_fI[where f=All, intro]
116  vspace_obj_pred_fI[where f=Ex, intro]
117
118end
119
120locale vspace_only_obj_pred = Arch +
121  fixes P :: "kernel_object \<Rightarrow> bool"
122  assumes vspace_only: "vspace_obj_pred P"
123
124sublocale vspace_only_obj_pred < arch_only_obj_pred
125  using vspace_pred_imp[OF vspace_only] by unfold_locales
126
127context Arch begin global_naming ARM
128
129sublocale empty_table: vspace_only_obj_pred "empty_table S" for S
130  by unfold_locales (clarsimp simp: vspace_obj_pred_def empty_table_def
131                             split: arch_kernel_obj.splits kernel_object.splits)
132
133sublocale vs_refs: vspace_only_obj_pred "\<lambda>ko. x \<in> vs_refs ko"
134  by unfold_locales (clarsimp simp: vspace_obj_pred_def vs_refs_def
135                             split: arch_kernel_obj.splits kernel_object.splits)
136
137sublocale vs_refs_pages: vspace_only_obj_pred "\<lambda>ko. x \<in> vs_refs_pages ko"
138  by unfold_locales (clarsimp simp: vspace_obj_pred_def vs_refs_pages_def
139                             split: arch_kernel_obj.split kernel_object.splits)
140
141lemma pspace_in_kernel_window_atyp_lift_strong:
142  assumes atyp_inv: "\<And>P p T. \<lbrace> \<lambda>s. P (typ_at T p s) \<rbrace> f \<lbrace> \<lambda>rv s. P (typ_at T p s) \<rbrace>"
143  assumes arch_inv: "\<And>P. \<lbrace>\<lambda>s. P (arm_kernel_vspace (arch_state s))\<rbrace> f \<lbrace>\<lambda>r s. P (arm_kernel_vspace (arch_state s))\<rbrace>"
144  shows      "\<lbrace>\<lambda>s. pspace_in_kernel_window s\<rbrace> f \<lbrace>\<lambda>rv s. pspace_in_kernel_window s\<rbrace>"
145  apply (simp add: pspace_in_kernel_window_def)
146  apply (rule hoare_lift_Pf[where f="\<lambda>s. arm_kernel_vspace (arch_state s)", OF _ arch_inv])
147   apply (rule hoare_vcg_all_lift)
148   apply (simp add: obj_bits_T)
149   apply (simp add: valid_def)
150  apply clarsimp
151  subgoal for _ x s _ _ ko
152  apply (cases "kheap s x")
153  apply (frule use_valid[OF _ atyp_inv, where P1= "\<lambda>x. \<not> x" and T1="a_type ko" and p1=x];
154          simp add: obj_at_def a_type_def)
155
156   subgoal for ko'
157   apply (drule spec[of _ ko'])
158   apply (simp add: obj_bits_T)
159   apply (frule use_valid[OF _ atyp_inv, where P1= "\<lambda>x. x" and T1="a_type ko'" and p1=x])
160   by (simp add: obj_at_def a_type_def)+
161 done
162 done
163
164lemma pspace_in_kernel_window_atyp_lift:
165  assumes atyp_inv: "\<And>P p T. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>"
166  assumes arch_inv: "\<And>P. \<lbrace>\<lambda>s. P (arch_state s)\<rbrace> f \<lbrace>\<lambda>r s. P (arch_state s)\<rbrace>"
167  shows      "\<lbrace>\<lambda>s. pspace_in_kernel_window s\<rbrace> f \<lbrace>\<lambda>rv s. pspace_in_kernel_window s\<rbrace>"
168  by (rule pspace_in_kernel_window_atyp_lift_strong[OF atyp_inv arch_inv])
169
170lemma cap_refs_in_kernel_window_arch_update[simp]:
171  "arm_kernel_vspace (f (arch_state s)) = arm_kernel_vspace (arch_state s)
172     \<Longrightarrow> cap_refs_in_kernel_window (arch_state_update f s) = cap_refs_in_kernel_window s"
173  by (simp add: cap_refs_in_kernel_window_def)
174
175lemma
176  ex_ko_at_def2:
177  "(\<exists>ko. ko_at ko p s \<and> P ko) = (obj_at P p s)"
178  by (simp add: obj_at_def)
179
180lemma in_user_frame_obj_pred_lift:
181 assumes obj_at: "\<And>P P' p. vspace_obj_pred P' \<Longrightarrow>
182                             \<lbrace>\<lambda>s. P (obj_at P' p s)\<rbrace> f \<lbrace>\<lambda>r s. P (obj_at P' p s)\<rbrace>"
183 shows "\<lbrace>in_user_frame p\<rbrace> f \<lbrace>\<lambda>_. in_user_frame p\<rbrace>"
184 unfolding in_user_frame_def
185 apply (wp hoare_vcg_ex_lift obj_at)
186 apply (clarsimp simp: vspace_obj_pred_def)
187 apply (auto simp: a_type_def aa_type_def split: kernel_object.splits arch_kernel_obj.splits)
188 done
189
190lemma vs_lookup_arch_obj_at_lift:
191  assumes obj_at: "\<And>P P' p. arch_obj_pred P' \<Longrightarrow>
192                             \<lbrace>\<lambda>s. P (obj_at P' p s)\<rbrace> f \<lbrace>\<lambda>r s. P (obj_at P' p s)\<rbrace>"
193  assumes arch_state: "\<And>P. \<lbrace>\<lambda>s. P (arch_state s)\<rbrace> f \<lbrace>\<lambda>r s. P (arch_state s)\<rbrace>"
194  shows "\<lbrace>\<lambda>s. P (vs_lookup s)\<rbrace> f \<lbrace>\<lambda>rv s. P (vs_lookup s)\<rbrace>"
195  apply (simp add: vs_lookup_def vs_lookup1_def)
196  apply (simp add: ex_ko_at_def2)
197  apply (rule hoare_lift_Pf[where f="arch_state", OF _ arch_state])
198  apply (rule hoare_lift_Pf[where f="\<lambda>s rs p rs' p'. obj_at (P' p rs rs' p') p s" for P'])
199   apply (rule hoare_vcg_prop)
200  apply (clarsimp simp add: valid_def)
201  apply (erule_tac P=P in rsubst)
202  apply (rule ext)+
203  apply (erule use_valid, rule obj_at, simp)
204  by (auto simp: vs_refs.arch_only
205           intro!: arch_obj_pred_fI[where f=Ex])
206
207lemma vs_lookup_vspace_obj_at_lift:
208  assumes obj_at: "\<And>P P' p. vspace_obj_pred P' \<Longrightarrow>
209                             \<lbrace>\<lambda>s. P (obj_at P' p s)\<rbrace> f \<lbrace>\<lambda>r s. P (obj_at P' p s)\<rbrace>"
210  assumes arch_state: "\<And>P. \<lbrace>\<lambda>s. P (arch_state s)\<rbrace> f \<lbrace>\<lambda>r s. P (arch_state s)\<rbrace>"
211  shows "\<lbrace>\<lambda>s. P (vs_lookup s)\<rbrace> f \<lbrace>\<lambda>rv s. P (vs_lookup s)\<rbrace>"
212  apply (simp add: vs_lookup_def vs_lookup1_def)
213  apply (simp add: ex_ko_at_def2)
214  apply (rule hoare_lift_Pf[where f="arch_state", OF _ arch_state])
215  apply (rule hoare_lift_Pf[where f="\<lambda>s rs p rs' p'. obj_at (P' p rs rs' p') p s" for P'])
216   apply (rule hoare_vcg_prop)
217  apply (clarsimp simp add: valid_def)
218  apply (erule_tac P=P in rsubst)
219  apply (rule ext)+
220  apply (erule use_valid, rule obj_at, simp)
221  by (auto simp: vs_refs.vspace_only
222           intro!: vspace_obj_pred_fI[where f=Ex])
223
224lemma vs_lookup_pages_arch_obj_at_lift:
225  assumes obj_at: "\<And>P P' p. arch_obj_pred P' \<Longrightarrow>
226                            \<lbrace>\<lambda>s. P (obj_at P' p s)\<rbrace> f \<lbrace>\<lambda>r s. P (obj_at P' p s)\<rbrace>"
227  assumes arch_state: "\<And>P. \<lbrace>\<lambda>s. P (arch_state s)\<rbrace> f \<lbrace>\<lambda>r s. P (arch_state s)\<rbrace>"
228  shows "\<lbrace>\<lambda>s. P (vs_lookup_pages s)\<rbrace> f \<lbrace>\<lambda>rv s. P (vs_lookup_pages s)\<rbrace>"
229  apply (simp add: vs_lookup_pages_def vs_lookup_pages1_def)
230  apply (simp add: ex_ko_at_def2)
231  apply (rule hoare_lift_Pf[where f="arch_state", OF _ arch_state])
232  apply (rule hoare_lift_Pf[where f="\<lambda>s rs p rs' p'. obj_at (P' p rs rs' p') p s" for P'])
233   apply (rule hoare_vcg_prop)
234  apply (clarsimp simp add: valid_def)
235  apply (erule_tac P=P in rsubst)
236  apply (rule ext)+
237  apply (erule use_valid, rule obj_at, simp)
238  by (auto simp: vs_refs_pages.arch_only
239           intro!: arch_obj_pred_fI[where f=Ex])
240
241lemma vs_lookup_pages_vspace_obj_at_lift:
242  assumes obj_at: "\<And>P P' p. vspace_obj_pred P' \<Longrightarrow>
243                            \<lbrace>\<lambda>s. P (obj_at P' p s)\<rbrace> f \<lbrace>\<lambda>r s. P (obj_at P' p s)\<rbrace>"
244  assumes arch_state: "\<And>P. \<lbrace>\<lambda>s. P (arch_state s)\<rbrace> f \<lbrace>\<lambda>r s. P (arch_state s)\<rbrace>"
245  shows "\<lbrace>\<lambda>s. P (vs_lookup_pages s)\<rbrace> f \<lbrace>\<lambda>rv s. P (vs_lookup_pages s)\<rbrace>"
246  apply (simp add: vs_lookup_pages_def vs_lookup_pages1_def)
247  apply (simp add: ex_ko_at_def2)
248  apply (rule hoare_lift_Pf[where f="arch_state", OF _ arch_state])
249  apply (rule hoare_lift_Pf[where f="\<lambda>s rs p rs' p'. obj_at (P' p rs rs' p') p s" for P'])
250   apply (rule hoare_vcg_prop)
251  apply (clarsimp simp add: valid_def)
252  apply (erule_tac P=P in rsubst)
253  apply (rule ext)+
254  apply (erule use_valid, rule obj_at, simp)
255  by (auto simp: vs_refs_pages.vspace_only
256           intro!: vspace_obj_pred_fI[where f=Ex])
257
258lemma valid_vspace_objs_lift_weak:
259  assumes obj_at: "\<And>P P' p. vspace_obj_pred P' \<Longrightarrow>
260                             \<lbrace>\<lambda>s. P (obj_at P' p s)\<rbrace> f \<lbrace>\<lambda>r s. P (obj_at P' p s)\<rbrace>"
261  assumes arch_state: "\<And>P. \<lbrace>\<lambda>s. P (arch_state s)\<rbrace> f \<lbrace>\<lambda>r s. P (arch_state s)\<rbrace>"
262  shows "\<lbrace>valid_vspace_objs\<rbrace> f \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace>"
263  apply (rule valid_vspace_objs_lift)
264    apply (rule vs_lookup_vspace_obj_at_lift)
265    apply (rule obj_at arch_state vspace_pred_imp; simp)+
266  done
267
268lemma set_object_neg_lookup:
269  "\<lbrace>\<lambda>s. \<not> (\<exists>rs. (rs \<rhd> p') s) \<and> obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') p s \<rbrace>
270  set_object p ko
271  \<lbrace>\<lambda>_ s. \<not> (\<exists>rs. (rs \<rhd> p') s)\<rbrace>"
272  apply (simp add: set_object_def)
273  apply wp
274  apply clarsimp
275  apply (erule_tac x=rs in allE)
276  apply (erule notE)
277  apply (erule vs_lookup_stateI)
278   apply (clarsimp simp: obj_at_def split: if_split_asm)
279  apply simp
280  done
281
282lemma set_object_vs_lookup:
283  "\<lbrace>\<lambda>s. obj_at (\<lambda>ko'. vs_refs ko = vs_refs ko') p s \<and> P (vs_lookup s) \<rbrace>
284  set_object p ko
285  \<lbrace>\<lambda>_ s. P (vs_lookup s)\<rbrace>"
286  apply (simp add: set_object_def)
287  apply wp
288  apply clarsimp
289  apply (erule rsubst [where P=P])
290  apply (rule order_antisym)
291   apply (rule vs_lookup_sub)
292    apply (clarsimp simp: obj_at_def)
293   apply simp
294  apply (rule vs_lookup_sub)
295   apply (clarsimp simp: obj_at_def split: if_split_asm)
296  apply simp
297  done
298
299lemma set_object_pt_not_vs_lookup_pages:
300  "\<lbrace>\<lambda>s. \<not>(ref \<unrhd> p') s
301    \<and> ((\<exists>\<unrhd>p) s \<longrightarrow> (\<forall>x. case pte_ref_pages (pt x) of
302              Some ptr \<Rightarrow>
303                obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and>
304                ptr \<noteq> p'
305            | None \<Rightarrow> True))\<rbrace>
306   set_object p (ArchObj (PageTable pt))
307   \<lbrace>\<lambda>_ s. \<not>(ref \<unrhd> p') s\<rbrace>"
308  apply (simp add: set_object_def)
309  apply wp
310  apply (clarsimp simp: obj_at_def)
311   apply (case_tac "(\<exists>\<unrhd>p) s")
312   apply (erule notE)
313   apply clarsimp
314   apply (subst (asm) vs_lookup_pages_def)
315   apply clarsimp
316   apply (erule vs_lookup_pagesI)
317   apply (erule converse_rtrancl_induct)
318    apply simp
319   apply (drule vs_lookup_pages1D)
320   apply (clarsimp simp: obj_at_def split:if_split_asm)
321   apply (case_tac "pa=p")
322    apply (clarsimp simp: vs_refs_pages_def graph_of_def)
323    apply (erule_tac x=ab in allE)
324    apply (drule_tac R="vs_lookup_pages1 s" in rtranclD)
325    apply clarsimp
326    apply (drule tranclD)
327    apply clarsimp
328    apply (drule vs_lookup_pages1D)
329    apply (clarsimp simp: obj_at_def vs_refs_pages_def)
330   apply clarsimp
331   apply (erule rtrancl_trans[OF r_into_rtrancl, rotated])
332   apply (clarsimp simp: vs_lookup_pages1_def obj_at_def)
333  apply clarsimp
334  apply (erule notE)
335  apply (subst (asm) vs_lookup_pages_def)
336  apply clarsimp
337  apply (rule vs_lookup_pagesI, assumption)
338  apply (erule rtrancl_induct)
339   apply simp
340  apply (drule vs_lookup_pages1D)
341  apply (clarsimp simp: obj_at_def split:if_split_asm)
342  apply (case_tac "pa=p")
343   apply (clarsimp simp: vs_refs_pages_def graph_of_def)
344   apply (erule_tac x=rs in allE)
345   apply (clarsimp simp: vs_lookup_pages_def)
346   apply (drule(1) ImageI, erule (1) notE)
347  apply clarsimp
348  apply (erule rtrancl_trans[OF _ r_into_rtrancl])
349  apply (clarsimp simp: vs_lookup_pages1_def obj_at_def)
350  done
351
352
353lemma set_object_vs_lookup_pages:
354  "\<lbrace>\<lambda>s. obj_at (\<lambda>ko'. vs_refs_pages ko = vs_refs_pages ko') p s \<and> P (vs_lookup_pages s) \<rbrace>
355  set_object p ko
356  \<lbrace>\<lambda>_ s. P (vs_lookup_pages s)\<rbrace>"
357  apply (simp add: set_object_def)
358  apply wp
359  apply clarsimp
360  apply (erule rsubst [where P=P])
361  apply (rule order_antisym)
362   apply (rule vs_lookup_pages_sub)
363    apply (clarsimp simp: obj_at_def)
364   apply simp
365  apply (rule vs_lookup_pages_sub)
366   apply (clarsimp simp: obj_at_def split: if_split_asm)
367  apply simp
368  done
369
370
371lemma set_object_atyp_at:
372  "\<lbrace>\<lambda>s. typ_at (AArch (aa_type ako)) p s \<and> P (typ_at (AArch T) p' s)\<rbrace>
373    set_object p (ArchObj ako)
374   \<lbrace>\<lambda>rv s. P (typ_at (AArch T) p' s)\<rbrace>"
375  apply (simp add: set_object_def)
376  apply wp
377  apply clarsimp
378  apply (erule rsubst [where P=P])
379  apply (clarsimp simp: obj_at_def a_type_aa_type)
380  done
381
382lemma set_object_vspace_objs:
383  "\<lbrace>valid_vspace_objs and typ_at (a_type ko) p and
384    obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') p  and
385    (\<lambda>s. case ko of ArchObj ao \<Rightarrow>
386             (\<exists>\<rhd>p)s \<longrightarrow> valid_vspace_obj ao s
387            | _ \<Rightarrow> True)\<rbrace>
388  set_object p ko
389  \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace>"
390  apply (simp add: valid_vspace_objs_def)
391  apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift)
392  apply (subst imp_conv_disj)
393  apply (subst imp_conv_disj)
394  apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift set_object_neg_lookup set_object_neg_ko)
395  apply (wp valid_vspace_obj_typ2 [where Q="typ_at (a_type ko) p"] set_object_typ_at
396         | simp)+
397  apply (clarsimp simp: pred_neg_def obj_at_def)
398  apply (case_tac ko; auto)
399  done
400
401lemma set_object_valid_kernel_mappings:
402  "\<lbrace>\<lambda>s. valid_kernel_mappings s
403           \<and> valid_kernel_mappings_if_pd
404                (set (arm_global_pts (arch_state s)))
405                    ko\<rbrace>
406     set_object ptr ko
407   \<lbrace>\<lambda>rv. valid_kernel_mappings\<rbrace>"
408  apply (simp add: set_object_def)
409  apply wp
410  apply (clarsimp simp: valid_kernel_mappings_def
411                 elim!: ranE split: if_split_asm)
412  apply fastforce
413  done
414
415lemma valid_vs_lookup_lift:
416  assumes lookup: "\<And>P. \<lbrace>\<lambda>s. P (vs_lookup_pages s)\<rbrace> f \<lbrace>\<lambda>_ s. P (vs_lookup_pages s)\<rbrace>"
417  assumes cap: "\<And>P. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>"
418  shows "\<lbrace>valid_vs_lookup\<rbrace> f \<lbrace>\<lambda>_. valid_vs_lookup\<rbrace>"
419  unfolding valid_vs_lookup_def
420  apply (rule hoare_lift_Pf [where f=vs_lookup_pages])
421   apply (rule hoare_lift_Pf [where f="\<lambda>s. (caps_of_state s)"])
422     apply (wp lookup cap)+
423  done
424
425
426lemma valid_table_caps_lift:
427  assumes cap: "\<And>P. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>"
428  assumes pts: "\<And>P. \<lbrace>\<lambda>s. P (second_level_tables (arch_state s))\<rbrace> f \<lbrace>\<lambda>_ s. P (second_level_tables (arch_state s))\<rbrace>"
429  assumes obj: "\<And>S p. \<lbrace>obj_at (empty_table S) p\<rbrace> f \<lbrace>\<lambda>rv. obj_at (empty_table S) p\<rbrace>"
430  shows "\<lbrace>valid_table_caps\<rbrace> f \<lbrace>\<lambda>_. valid_table_caps\<rbrace>"
431  unfolding valid_table_caps_def
432   apply (rule hoare_lift_Pf [where f="\<lambda>s. (caps_of_state s)"])
433    apply (rule hoare_lift_Pf [where f="\<lambda>s. second_level_tables (arch_state s)"])
434     apply (wp cap pts hoare_vcg_all_lift hoare_vcg_const_imp_lift obj)+
435  done
436
437lemma valid_arch_caps_lift:
438  assumes lookup: "\<And>P. \<lbrace>\<lambda>s. P (vs_lookup_pages s)\<rbrace> f \<lbrace>\<lambda>_ s. P (vs_lookup_pages s)\<rbrace>"
439  assumes cap: "\<And>P. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>"
440  assumes pts: "\<And>P. \<lbrace>\<lambda>s. P (second_level_tables (arch_state s))\<rbrace> f \<lbrace>\<lambda>_ s. P (second_level_tables (arch_state s))\<rbrace>"
441  assumes obj: "\<And>S p. \<lbrace>obj_at (empty_table S) p\<rbrace> f \<lbrace>\<lambda>rv. obj_at (empty_table S) p\<rbrace>"
442  shows "\<lbrace>valid_arch_caps\<rbrace> f \<lbrace>\<lambda>_. valid_arch_caps\<rbrace>"
443  unfolding valid_arch_caps_def
444  apply (rule hoare_pre)
445   apply (wp valid_vs_lookup_lift valid_table_caps_lift lookup cap pts obj)
446  apply simp
447  done
448
449lemma valid_global_objs_lift':
450  assumes pts: "\<And>P. \<lbrace>\<lambda>s. P (arm_global_pts (arch_state s))\<rbrace> f \<lbrace>\<lambda>_ s. P (arm_global_pts (arch_state s))\<rbrace>"
451  assumes pd: "\<And>P. \<lbrace>\<lambda>s. P (arm_global_pd (arch_state s))\<rbrace> f \<lbrace>\<lambda>_ s. P (arm_global_pd (arch_state s))\<rbrace>"
452  assumes obj: "\<And>p. \<lbrace>valid_vso_at p\<rbrace> f \<lbrace>\<lambda>rv. valid_vso_at p\<rbrace>"
453  assumes ko: "\<And>ako p. \<lbrace>ko_at (ArchObj ako) p\<rbrace> f \<lbrace>\<lambda>_. ko_at (ArchObj ako) p\<rbrace>"
454  assumes emp: "\<And>pd S.
455       \<lbrace>\<lambda>s. (v \<longrightarrow> pd = arm_global_pd (arch_state s) \<and> S = set (second_level_tables (arch_state s)) \<and> P s)
456            \<and> obj_at (empty_table S) pd s\<rbrace>
457                 f \<lbrace>\<lambda>rv. obj_at (empty_table S) pd\<rbrace>"
458  shows "\<lbrace>\<lambda>s. valid_global_objs s \<and> (v \<longrightarrow> P s)\<rbrace> f \<lbrace>\<lambda>rv. valid_global_objs\<rbrace>"
459  unfolding valid_global_objs_def second_level_tables_def
460  apply (rule hoare_pre)
461   apply (rule hoare_use_eq [where f="\<lambda>s. arm_global_pts (arch_state s)", OF pts])
462   apply (rule hoare_use_eq [where f="\<lambda>s. arm_global_pd (arch_state s)", OF pd])
463   apply (wp obj ko emp hoare_vcg_const_Ball_lift hoare_ex_wp)
464  apply (clarsimp simp: second_level_tables_def)
465  done
466
467lemmas valid_global_objs_lift
468    = valid_global_objs_lift' [where v=False, simplified]
469
470context
471  fixes f :: "'a::state_ext state \<Rightarrow> ('b \<times> 'a state) set \<times> bool"
472  assumes arch: "\<And>P. \<lbrace>\<lambda>s. P (arch_state s)\<rbrace> f \<lbrace>\<lambda>_ s. P (arch_state s)\<rbrace>"
473begin
474
475context
476  assumes aobj_at:
477    "\<And>P P' pd. vspace_obj_pred P' \<Longrightarrow> \<lbrace>\<lambda>s. P (obj_at P' pd s)\<rbrace> f \<lbrace>\<lambda>r s. P (obj_at P' pd s)\<rbrace>"
478  notes vspace_obj_fun_lift_expand[simp del]
479begin
480
481lemma valid_global_vspace_mappings_lift:
482  "\<lbrace>valid_global_vspace_mappings\<rbrace> f \<lbrace>\<lambda>rv. valid_global_vspace_mappings\<rbrace>"
483  apply (simp add: valid_global_vspace_mappings_def valid_pd_kernel_mappings_def
484              del: valid_pd_kernel_mappings_arch_def)
485  apply (rule hoare_lift_Pf[where f="arch_state", OF _ arch])
486  apply (rule_tac f="valid_pd_kernel_mappings_arch (arm_kernel_vspace x)" in hoare_lift_Pf)
487   apply (rule aobj_at; simp)
488  apply (subst valid_pd_kernel_mappings_arch_def valid_pde_kernel_mappings_def)+
489  apply (clarsimp simp add: valid_def)
490  apply (erule_tac P=P in rsubst)
491  apply (rule ext)
492  apply (clarsimp intro!: iff_allI split: arch_kernel_obj.splits pde.splits)
493  apply (safe; clarsimp simp add: valid_pt_kernel_mappings_def
494                        simp del: valid_pt_kernel_mappings_arch_def)
495     apply (erule use_valid[OF _ aobj_at[where P="\<lambda>x. x"]]; simp add:)+
496   by (rule classical,
497          drule use_valid[OF _ aobj_at[where P="\<lambda>x. \<not>x", OF vspace_obj_pred_fun_lift_id]],
498          simp+)+
499
500lemma valid_arch_caps_lift_weak:
501  "(\<And>P. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>) \<Longrightarrow>
502      \<lbrace>valid_arch_caps\<rbrace> f \<lbrace>\<lambda>_. valid_arch_caps\<rbrace>"
503  apply (rule valid_arch_caps_lift[OF _ _ arch aobj_at])
504    apply (rule vs_lookup_pages_vspace_obj_at_lift[OF aobj_at arch], assumption+)
505  apply (rule empty_table.vspace_only)
506  done
507
508lemma valid_global_objs_lift_weak:
509  "\<lbrace>valid_global_objs\<rbrace> f \<lbrace>\<lambda>rv. valid_global_objs\<rbrace>"
510  apply (rule valid_global_objs_lift)
511      apply (wp arch)+
512    apply (simp add: valid_vso_at_def)
513    apply (rule hoare_vcg_ex_lift)
514    apply (rule hoare_vcg_conj_lift)
515     apply (wp aobj_at valid_vspace_obj_typ | simp | rule empty_table.vspace_only)+
516  done
517
518lemma valid_asid_map_lift:
519  "\<lbrace>valid_asid_map\<rbrace> f \<lbrace>\<lambda>rv. valid_asid_map\<rbrace>"
520  apply (simp add: valid_asid_map_def)
521  apply (rule hoare_lift_Pf[where f="arch_state", OF _ arch])
522  apply (simp add: vspace_at_asid_def)
523  by (rule vs_lookup_vspace_obj_at_lift[OF aobj_at arch])
524
525lemma valid_kernel_mappings_lift:
526  "\<lbrace>valid_kernel_mappings\<rbrace> f \<lbrace>\<lambda>rv. valid_kernel_mappings\<rbrace>"
527  apply (simp add: valid_kernel_mappings_def)
528  apply (rule hoare_lift_Pf[where f="arch_state", OF _ arch])
529  apply (simp add: valid_kernel_mappings_if_pd_def ran_def
530              del: valid_kernel_mappings_if_pd_arch_def)
531  apply (rule hoare_vcg_all_lift)
532  apply (case_tac "\<exists>ao. xa = ArchObj ao")
533   apply (rule hoare_convert_imp)
534    apply clarsimp
535    apply (rule hoare_vcg_all_lift)
536    subgoal for ao a
537    by (rule aobj_at[where P=Not and P'="\<lambda>x. x = ArchObj ao", simplified obj_at_def, simplified])
538   apply clarsimp
539   apply (case_tac ao; simp add: hoare_vcg_prop)
540  apply (clarsimp simp del: valid_kernel_mappings_if_pd_arch_def)
541  apply (case_tac xa; simp add: hoare_vcg_prop)
542  done
543
544end
545
546context
547  assumes aobj_at:
548    "\<And>P P' pd. arch_obj_pred P' \<Longrightarrow> \<lbrace>\<lambda>s. P (obj_at P' pd s)\<rbrace> f \<lbrace>\<lambda>r s. P (obj_at P' pd s)\<rbrace>"
549begin
550
551lemma valid_global_pts_lift:
552  "\<lbrace>valid_global_pts\<rbrace> f \<lbrace>\<lambda>rv. valid_global_pts\<rbrace>"
553  apply (simp add: valid_global_pts_def)
554  apply (rule hoare_lift_Pf[where f="arch_state", OF _ arch])
555  apply (rule hoare_vcg_ball_lift)
556  apply (rule aobj_at)
557  apply clarsimp
558  done
559
560lemma valid_arch_state_lift_aobj_at:
561  "\<lbrace>valid_arch_state\<rbrace> f \<lbrace>\<lambda>rv. valid_arch_state\<rbrace>"
562  apply (simp add: valid_arch_state_def valid_asid_table_def)
563  apply (rule hoare_lift_Pf[where f="arch_state", OF _ arch])
564  apply (wp hoare_vcg_conj_lift hoare_vcg_ball_lift valid_global_pts_lift | (rule aobj_at, clarsimp))+
565  apply simp
566  done
567
568end
569end
570
571lemma equal_kernel_mappings_lift:
572  assumes aobj_at:
573    "\<And>P P' pd. vspace_obj_pred P' \<Longrightarrow> \<lbrace>\<lambda>s. P (obj_at P' pd s)\<rbrace> f \<lbrace>\<lambda>r s. P (obj_at P' pd s)\<rbrace>"
574  shows "\<lbrace>equal_kernel_mappings\<rbrace> f \<lbrace>\<lambda>rv. equal_kernel_mappings\<rbrace>"
575  apply (simp add: equal_kernel_mappings_def)
576  apply (rule hoare_vcg_all_lift)+
577  apply (rule hoare_convert_imp)
578   apply simp
579   apply (rule hoare_convert_imp)
580    apply (wp aobj_at[OF vspace_obj_pred_arch_obj_l])+
581  done
582
583lemma valid_machine_state_lift:
584  assumes memory: "\<And>P. \<lbrace>\<lambda>s. P (underlying_memory (machine_state s))\<rbrace> f \<lbrace>\<lambda>_ s. P (underlying_memory (machine_state s))\<rbrace>"
585  assumes aobj_at: "\<And>P' pd. arch_obj_pred P' \<Longrightarrow> \<lbrace>obj_at P' pd\<rbrace> f \<lbrace>\<lambda>r s. obj_at P' pd s\<rbrace>"
586  shows "\<lbrace>valid_machine_state\<rbrace> f \<lbrace>\<lambda>_. valid_machine_state\<rbrace>"
587  unfolding valid_machine_state_def
588  apply (rule hoare_lift_Pf[where f="\<lambda>s. underlying_memory (machine_state s)", OF _ memory])
589  apply (rule hoare_vcg_all_lift)
590  apply (rule hoare_vcg_disj_lift[OF _ hoare_vcg_prop])
591  apply (rule in_user_frame_lift)
592  apply (wp aobj_at; simp)
593  done
594
595lemma valid_ao_at_lift:
596  assumes z: "\<And>P p T. \<lbrace>\<lambda>s. P (typ_at (AArch T) p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at (AArch T) p s)\<rbrace>"
597      and y: "\<And>ao. \<lbrace>\<lambda>s. ko_at (ArchObj ao) p s\<rbrace> f \<lbrace>\<lambda>rv s. ko_at (ArchObj ao) p s\<rbrace>"
598  shows      "\<lbrace>valid_ao_at p\<rbrace> f \<lbrace>\<lambda>rv. valid_ao_at p\<rbrace>"
599  unfolding valid_ao_at_def
600  by (wp hoare_vcg_ex_lift y valid_vspace_obj_typ z)
601
602lemma valid_ao_at_lift_aobj_at:
603  assumes aobj_at: "\<And>P' pd. arch_obj_pred P' \<Longrightarrow> \<lbrace>obj_at P' pd\<rbrace> f \<lbrace>\<lambda>r s. obj_at P' pd s\<rbrace>"
604  shows      "\<lbrace>valid_ao_at p\<rbrace> f \<lbrace>\<lambda>rv. valid_ao_at p\<rbrace>"
605  unfolding valid_ao_at_def
606  by (wp hoare_vcg_ex_lift valid_vspace_obj_typ aobj_at | clarsimp)+
607
608lemma valid_vso_at_lift:
609  assumes z: "\<And>P p T. \<lbrace>\<lambda>s. P (typ_at (AArch T) p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at (AArch T) p s)\<rbrace>"
610      and y: "\<And>ao. \<lbrace>\<lambda>s. ko_at (ArchObj ao) p s\<rbrace> f \<lbrace>\<lambda>rv s. ko_at (ArchObj ao) p s\<rbrace>"
611  shows      "\<lbrace>valid_vso_at p\<rbrace> f \<lbrace>\<lambda>rv. valid_vso_at p\<rbrace>"
612  unfolding valid_vso_at_def
613  by (wpsimp wp: hoare_vcg_ex_lift y valid_vspace_obj_typ z)+
614
615lemma valid_vso_at_lift_aobj_at:
616  assumes aobj_at: "\<And>P' pd. vspace_obj_pred P' \<Longrightarrow> \<lbrace>obj_at P' pd\<rbrace> f \<lbrace>\<lambda>r s. obj_at P' pd s\<rbrace>"
617  shows      "\<lbrace>valid_vso_at p\<rbrace> f \<lbrace>\<lambda>rv. valid_vso_at p\<rbrace>"
618  unfolding valid_vso_at_def
619  apply (rule hoare_vcg_ex_lift)
620  apply (rule hoare_vcg_conj_lift aobj_at)+
621   apply (clarsimp simp: vspace_obj_pred_def)
622   apply (rule iffI)
623    apply ((case_tac ao; clarsimp)+)[2]
624  apply (wpsimp wp: valid_vspace_obj_typ)
625   apply (wpsimp wp: aobj_at)
626  apply assumption
627  done
628
629lemmas set_object_v_ker_map
630    = set_object_valid_kernel_mappings
631            [unfolded valid_kernel_mappings_if_pd_def]
632
633lemma set_object_asid_map:
634  "\<lbrace>valid_asid_map and
635    obj_at (\<lambda>ko'. vs_refs ko' \<subseteq> vs_refs ko) p\<rbrace>
636  set_object p ko
637  \<lbrace>\<lambda>_. valid_asid_map\<rbrace>"
638  apply (simp add: valid_asid_map_def set_object_def)
639  apply wp
640  apply (clarsimp simp: vspace_at_asid_def simp del: fun_upd_apply)
641  apply (drule bspec, blast)
642  apply clarsimp
643  apply (rule vs_lookup_stateI, assumption)
644   apply (clarsimp simp: obj_at_def)
645   apply blast
646  apply simp
647  done
648
649lemma set_object_equal_mappings:
650  "\<lbrace>\<lambda>s. equal_kernel_mappings s
651          \<and> (\<forall>pd. ko = ArchObj (PageDirectory pd)
652                \<longrightarrow> (\<forall>x pd'. ko_at (ArchObj (PageDirectory pd')) x s
653                         \<longrightarrow> (\<forall>w \<in> kernel_mapping_slots. pd w = pd' w)))\<rbrace>
654     set_object p ko
655   \<lbrace>\<lambda>rv. equal_kernel_mappings\<rbrace>"
656  apply (simp add: set_object_def, wp)
657  apply (clarsimp simp: equal_kernel_mappings_def obj_at_def
658             split del: if_split)
659  apply (simp split: if_split_asm)
660  done
661
662lemma valid_global_vspace_mappings_pres:
663  "\<lbrakk> valid_global_vspace_mappings s;
664     \<And>pd. ko_at (ArchObj (PageDirectory pd)) (arm_global_pd (arch_state s)) s
665            \<Longrightarrow> ko_at (ArchObj (PageDirectory pd)) (arm_global_pd (arch_state s)) s';
666     \<And>pt p. \<lbrakk> ko_at (ArchObj (PageTable pt)) p s;
667               valid_global_objs s \<Longrightarrow> p \<in> set (arm_global_pts (arch_state s)) \<rbrakk>
668            \<Longrightarrow> ko_at (ArchObj (PageTable pt)) p s';
669     arm_global_pd (arch_state s') = arm_global_pd (arch_state s);
670     arm_kernel_vspace (arch_state s') = arm_kernel_vspace (arch_state s) \<rbrakk>
671        \<Longrightarrow> valid_global_vspace_mappings s'"
672  apply atomize
673  apply (clarsimp simp: valid_global_vspace_mappings_def obj_at_def)
674  apply (clarsimp simp: valid_pd_kernel_mappings_def
675                 split: kernel_object.split_asm arch_kernel_obj.split_asm)
676  apply (drule_tac x=x in spec)
677  apply (clarsimp simp: valid_pde_kernel_mappings_def obj_at_def
678                        valid_pt_kernel_mappings_def pde_ref_def
679                 split: pde.split_asm)
680  apply (simp split: kernel_object.split_asm
681                     arch_kernel_obj.split_asm)
682  apply (drule spec, drule spec, drule(1) mp)
683  apply (drule mp)
684   apply (clarsimp simp: valid_global_objs_def obj_at_def empty_table_def)
685   apply (drule_tac x=x in spec)
686   apply (simp add: pde_ref_def second_level_tables_def)[1]
687  apply clarsimp
688  done
689
690lemma valid_global_vspace_mappings_arch_update[simp]:
691  "arm_global_pd (f (arch_state s)) = arm_global_pd (arch_state s)
692   \<and> arm_kernel_vspace (f (arch_state s)) = arm_kernel_vspace (arch_state s)
693     \<Longrightarrow> valid_global_vspace_mappings (arch_state_update f s) = valid_global_vspace_mappings s"
694  by (simp add: valid_global_vspace_mappings_def)
695
696lemma set_object_global_vspace_mappings:
697  "\<lbrace>valid_global_vspace_mappings
698            and (\<lambda>s. (page_directory_at p s \<or> page_table_at p s)
699                       \<longrightarrow> valid_global_objs s \<and> p \<notin> global_refs s)\<rbrace>
700     set_object p ko
701   \<lbrace>\<lambda>rv. valid_global_vspace_mappings\<rbrace>"
702  apply (simp add: set_object_def, wp)
703  apply clarsimp
704  apply (erule valid_global_vspace_mappings_pres)
705     apply (clarsimp simp: obj_at_def a_type_def global_refs_def second_level_tables_def)+
706  done
707
708
709lemma valid_table_caps_ptD:
710  "\<lbrakk> (caps_of_state s) p = Some (ArchObjectCap (arch_cap.PageTableCap p' None));
711     page_table_at p' s; valid_table_caps s \<rbrakk> \<Longrightarrow>
712    \<exists>pt. ko_at (ArchObj (PageTable pt)) p' s \<and> valid_vspace_obj (PageTable pt) s"
713  apply (clarsimp simp: valid_table_caps_def simp del: split_paired_All)
714  apply (erule allE)+
715  apply (erule (1) impE)
716  apply (clarsimp simp add: is_pt_cap_def cap_asid_def)
717  apply (erule impE, rule refl)
718  apply (clarsimp simp: obj_at_def empty_table_def)
719  done
720
721lemma store_pde_pred_tcb_at:
722  "\<lbrace>pred_tcb_at proj P t\<rbrace> store_pde ptr val \<lbrace>\<lambda>rv. pred_tcb_at proj P t\<rbrace>"
723  apply (simp add: store_pde_def set_pd_def set_object_def
724                   get_pd_def bind_assoc)
725  apply (rule hoare_seq_ext [OF _ get_object_sp])
726  apply (case_tac x, simp_all)
727  apply (rename_tac arch_kernel_obj)
728  apply (case_tac arch_kernel_obj, simp_all)
729  apply (rule hoare_seq_ext [OF _ get_object_sp])
730  apply wp
731  apply (clarsimp simp: pred_tcb_at_def obj_at_def)
732  done
733
734lemma empty_table_lift:
735  assumes S: "\<And>P. \<lbrace>\<lambda>s. P (S s)\<rbrace> f \<lbrace>\<lambda>_ s. P (S s)\<rbrace>"
736  assumes o: "\<And>P. \<lbrace>obj_at P p and Q\<rbrace> f \<lbrace>\<lambda>_. obj_at P p\<rbrace>"
737  shows "\<lbrace>\<lambda>s. obj_at (empty_table (S s)) p s \<and> Q s\<rbrace>
738         f \<lbrace>\<lambda>_ s. obj_at (empty_table (S s)) p s\<rbrace>"
739  apply (rule hoare_lift_Pf2 [where f="S"])
740   apply (wp o S|simp)+
741  done
742
743lemma in_user_frame_obj_upd:
744  "\<lbrakk>kheap s p = Some ko; a_type k = a_type ko\<rbrakk> \<Longrightarrow>
745   in_user_frame x (s\<lparr>kheap := \<lambda>a. if a = p then Some k else kheap s a\<rparr>)
746   = in_user_frame x s"
747  apply (rule iffI)
748  apply (clarsimp simp: in_user_frame_def obj_at_def split: if_split_asm)
749   apply (elim disjE)
750    apply clarsimp
751    apply (intro exI)
752    apply (rule conjI,assumption)
753    apply (simp add: a_type_def)
754   apply (fastforce simp: a_type_def)
755  apply (clarsimp simp: in_user_frame_def obj_at_def split: if_split_asm)
756  apply (rule_tac x = sz in exI)
757  apply (intro conjI impI)
758    apply (fastforce simp: a_type_def)+
759  done
760
761lemma user_mem_obj_upd_dom:
762  "\<lbrakk>kheap s p = Some ko; a_type k = a_type ko\<rbrakk> \<Longrightarrow>
763   dom (user_mem (s\<lparr>kheap := \<lambda>a. if a = p then Some k else kheap s a\<rparr>))
764   = dom (user_mem s)"
765  by (clarsimp simp: user_mem_def in_user_frame_obj_upd dom_def)
766
767lemma in_device_frame_obj_upd:
768  "\<lbrakk>kheap s p = Some ko; a_type k = a_type ko\<rbrakk> \<Longrightarrow>
769   in_device_frame x (s\<lparr>kheap := \<lambda>a. if a = p then Some k else kheap s a\<rparr>)
770   = in_device_frame x s"
771  apply (rule iffI)
772  apply (clarsimp simp: in_device_frame_def obj_at_def split: if_split_asm)
773   apply (elim disjE)
774    apply clarsimp
775    apply (intro exI)
776    apply (rule conjI,assumption)
777    apply (simp add: a_type_def)
778   apply (fastforce simp: a_type_def)
779  apply (clarsimp simp: in_device_frame_def obj_at_def split: if_split_asm)
780  apply (rule_tac x = sz in exI)
781  apply (intro conjI impI)
782    apply (fastforce simp: a_type_def)+
783  done
784
785lemma device_mem_obj_upd_dom:
786  "\<lbrakk>kheap s p = Some ko; a_type k = a_type ko\<rbrakk> \<Longrightarrow>
787   dom (device_mem (s\<lparr>kheap := \<lambda>a. if a = p then Some k else kheap s a\<rparr>))
788   = dom (device_mem s)"
789  by (clarsimp simp: device_mem_def in_device_frame_obj_upd dom_def)
790
791lemma pspace_respects_region_cong[cong]:
792  "\<lbrakk>kheap a  = kheap b; device_state (machine_state a) = device_state (machine_state b)\<rbrakk>
793  \<Longrightarrow> pspace_respects_device_region a = pspace_respects_device_region b"
794  by (simp add: pspace_respects_device_region_def device_mem_def user_mem_def in_device_frame_def
795    in_user_frame_def obj_at_def dom_def)
796
797definition "obj_is_device tp dev \<equiv>
798  case tp of Untyped \<Rightarrow> dev
799    | _ \<Rightarrow>(case (default_object tp dev 0) of (ArchObj (DataPage dev _)) \<Rightarrow> dev
800          | _ \<Rightarrow> False)"
801
802lemma cap_is_device_obj_is_device[simp]:
803  "cap_is_device (default_cap tp a sz dev) = obj_is_device tp dev"
804  by (simp add: default_cap_def arch_default_cap_def obj_is_device_def
805                default_object_def  default_arch_object_def
806         split: apiobject_type.splits aobject_type.splits)
807
808crunch device_state_inv: storeWord "\<lambda>ms. P (device_state ms)"
809
810(* some hyp_ref invariants *)
811
812lemma state_hyp_refs_of_ep_update: "\<And>s ep val. typ_at AEndpoint ep s \<Longrightarrow>
813       state_hyp_refs_of (s\<lparr>kheap := kheap s(ep \<mapsto> Endpoint val)\<rparr>) = state_hyp_refs_of s"
814  apply (rule all_ext)
815  apply (clarsimp simp add: ARM.state_hyp_refs_of_def obj_at_def ARM.hyp_refs_of_def)
816  done
817
818lemma state_hyp_refs_of_ntfn_update: "\<And>s ep val. typ_at ANTFN ep s \<Longrightarrow>
819       state_hyp_refs_of (s\<lparr>kheap := kheap s(ep \<mapsto> Notification val)\<rparr>) = state_hyp_refs_of s"
820  apply (rule all_ext)
821  apply (clarsimp simp add: ARM.state_hyp_refs_of_def obj_at_def ARM.hyp_refs_of_def)
822  done
823
824lemma state_hyp_refs_of_tcb_bound_ntfn_update:
825       "kheap s t = Some (TCB tcb) \<Longrightarrow>
826          state_hyp_refs_of (s\<lparr>kheap := kheap s(t \<mapsto> TCB (tcb\<lparr>tcb_bound_notification := ntfn\<rparr>))\<rparr>)
827            = state_hyp_refs_of s"
828  apply (rule all_ext)
829  apply (clarsimp simp add: ARM.state_hyp_refs_of_def obj_at_def split: option.splits)
830  done
831
832lemma state_hyp_refs_of_tcb_state_update:
833       "kheap s t = Some (TCB tcb) \<Longrightarrow>
834          state_hyp_refs_of (s\<lparr>kheap := kheap s(t \<mapsto> TCB (tcb\<lparr>tcb_state := ts\<rparr>))\<rparr>)
835            = state_hyp_refs_of s"
836  apply (rule all_ext)
837  apply (clarsimp simp add: ARM.state_hyp_refs_of_def obj_at_def split: option.splits)
838  done
839
840lemma arch_valid_obj_same_type:
841  "\<lbrakk> arch_valid_obj ao s; kheap s p = Some ko; a_type k = a_type ko \<rbrakk>
842   \<Longrightarrow> arch_valid_obj ao (s\<lparr>kheap := kheap s(p \<mapsto> k)\<rparr>)"
843  by (induction ao rule: arch_kernel_obj.induct;
844         clarsimp simp: typ_at_same_type)
845
846
847lemma default_arch_object_not_live: "\<not> live (ArchObj (default_arch_object aty dev us))"
848  by (clarsimp simp: default_arch_object_def live_def hyp_live_def arch_live_def
849               split: aobject_type.splits)
850
851lemma default_tcb_not_live: "\<not> live (TCB default_tcb)"
852  by (clarsimp simp: default_tcb_def default_arch_tcb_def live_def hyp_live_def)
853
854lemma valid_arch_tcb_same_type:
855  "\<lbrakk> valid_arch_tcb t s; valid_obj p k s; kheap s p = Some ko; a_type k = a_type ko \<rbrakk>
856   \<Longrightarrow> valid_arch_tcb t (s\<lparr>kheap := kheap s(p \<mapsto> k)\<rparr>)"
857  by (auto simp: valid_arch_tcb_def obj_at_def)
858
859lemma valid_ioports_lift:
860  assumes x: "\<And>P. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace>"
861  assumes y: "\<And>P. \<lbrace>\<lambda>s. P (arch_state s)\<rbrace> f \<lbrace>\<lambda>rv s. P (arch_state s)\<rbrace>"
862  shows      "\<lbrace>valid_ioports\<rbrace> f \<lbrace>\<lambda>rv. valid_ioports\<rbrace>"
863  apply (simp add: valid_ioports_def)
864  apply (rule hoare_use_eq [where f=caps_of_state, OF x y])
865  done
866
867lemma valid_arch_mdb_lift:
868  assumes c: "\<And>P. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>r s. P (caps_of_state s)\<rbrace>"
869  assumes r: "\<And>P. \<lbrace>\<lambda>s. P (is_original_cap s)\<rbrace> f \<lbrace>\<lambda>r s. P (is_original_cap s)\<rbrace>"
870  shows "\<lbrace>\<lambda>s. valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>r s. valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrace>"
871  apply (clarsimp simp: valid_arch_mdb_def valid_def)
872  done
873
874
875end
876end
877