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 ArchArch_AI
12imports "../Arch_AI"
13begin
14
15context Arch begin global_naming ARM
16
17definition
18  "valid_aci aci \<equiv> case aci of MakePool frame slot parent base \<Rightarrow>
19  \<lambda>s. cte_wp_at (\<lambda>c. c = cap.NullCap) slot s \<and> real_cte_at slot s \<and>
20  ex_cte_cap_wp_to is_cnode_cap slot s \<and>
21  slot \<noteq> parent \<and>
22  cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False frame pageBits idx ) parent s \<and>
23  descendants_of parent (cdt s) = {} \<and>
24  is_aligned base asid_low_bits \<and> base \<le> 2^asid_bits - 1 \<and>
25  arm_asid_table (arch_state s) (asid_high_bits_of base) = None"
26
27definition
28  "valid_vcpu_invocation vi \<equiv> case vi of
29       VCPUSetTCB vcpu_ptr tcb_ptr \<Rightarrow> vcpu_at vcpu_ptr and tcb_at tcb_ptr and
30                                      ex_nonz_cap_to vcpu_ptr and ex_nonz_cap_to tcb_ptr
31                                      and (\<lambda>s. tcb_ptr \<noteq> idle_thread s)
32     | VCPUInjectIRQ vcpu_ptr index virq \<Rightarrow> vcpu_at vcpu_ptr
33     | VCPUReadRegister vcpu_ptr reg \<Rightarrow> vcpu_at vcpu_ptr
34     | VCPUWriteRegister vcpu_ptr reg val \<Rightarrow> vcpu_at vcpu_ptr"
35
36lemma safe_parent_strg:
37  "cte_wp_at (\<lambda>cap. cap = UntypedCap False frame pageBits idx) p s \<and>
38   descendants_of p (cdt s) = {} \<and>
39   valid_objs s
40  \<longrightarrow>
41  cte_wp_at (safe_parent_for (cdt s) p
42             (ArchObjectCap (ASIDPoolCap frame base)))
43             p s"
44  apply (clarsimp simp: cte_wp_at_caps_of_state safe_parent_for_def is_physical_def arch_is_physical_def)
45  apply (rule is_aligned_no_overflow)
46  apply (drule (1) caps_of_state_valid_cap)
47  apply (clarsimp simp: valid_cap_def cap_aligned_def)
48  done
49
50
51lemma asid_low_bits_pageBits:
52  "Suc (Suc asid_low_bits) = pageBits"
53  by (simp add: pageBits_def asid_low_bits_def)
54
55
56(* 32-bit instance of Detype_AI.range_cover_full *)
57lemma range_cover_full:
58  "\<lbrakk>is_aligned ptr sz;sz<word_bits\<rbrakk> \<Longrightarrow> range_cover (ptr::word32) sz sz (Suc 0)"
59   by (clarsimp simp:range_cover_def unat_eq_0 le_mask_iff[symmetric] word_and_le1 word_bits_def)
60
61
62definition
63  valid_arch_inv :: "arch_invocation \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
64where
65  "valid_arch_inv \<equiv> \<lambda>ai. case ai of
66     InvokePageTable pti \<Rightarrow>
67       valid_pti pti
68   | InvokePageDirectory pdi \<Rightarrow>
69       valid_pdi pdi
70   | InvokePage pinv \<Rightarrow>
71       valid_page_inv pinv
72   | InvokeASIDControl aci \<Rightarrow>
73       valid_aci aci
74   | InvokeASIDPool ap \<Rightarrow>
75       valid_apinv ap
76   | InvokeVCPU vi \<Rightarrow>
77       valid_vcpu_invocation vi"
78
79
80lemma check_vp_wpR [wp]:
81  "\<lbrace>\<lambda>s. vmsz_aligned w sz \<longrightarrow> P () s\<rbrace>
82  check_vp_alignment sz w \<lbrace>P\<rbrace>, -"
83  apply (simp add: check_vp_alignment_def unlessE_whenE cong: vmpage_size.case_cong)
84  apply (rule hoare_pre)
85   apply (wp hoare_whenE_wp|wpc)+
86  apply (simp add: vmsz_aligned_def)
87  done
88
89
90lemma check_vp_inv: "\<lbrace>P\<rbrace> check_vp_alignment sz w \<lbrace>\<lambda>_. P\<rbrace>"
91  apply (simp add: check_vp_alignment_def unlessE_whenE cong: vmpage_size.case_cong)
92  apply (rule hoare_pre)
93   apply (wp hoare_whenE_wp|wpc)+
94  apply simp
95  done
96
97
98lemma p2_low_bits_max:
99  "(2 ^ asid_low_bits - 1) = (max_word :: 10 word)"
100  by (simp add: asid_low_bits_def max_word_def)
101
102
103lemma dom_ucast_eq:
104  "(- dom (\<lambda>a::asid_low_index. p (ucast a::machine_word)) \<inter> {x. ucast x + y \<noteq> 0} = {}) =
105   (- dom p \<inter> {x. x \<le> 2 ^ asid_low_bits - 1 \<and> x + y \<noteq> 0} = {})"
106  apply safe
107   apply clarsimp
108   apply (rule ccontr)
109   apply (erule_tac x="ucast x" in in_emptyE)
110   apply (clarsimp simp: p2_low_bits_max)
111   apply (rule conjI)
112    apply (clarsimp simp: ucast_ucast_mask)
113    apply (subst (asm) less_mask_eq)
114    apply (rule word_less_sub_le [THEN iffD1])
115      apply (simp add: word_bits_def)
116     apply (simp add: asid_low_bits_def)
117    apply simp
118   apply (clarsimp simp: ucast_ucast_mask)
119   apply (subst (asm) less_mask_eq)
120   apply (rule word_less_sub_le [THEN iffD1])
121     apply (simp add: word_bits_def)
122    apply (simp add: asid_low_bits_def)
123   apply simp
124  apply (clarsimp simp: p2_low_bits_max)
125  apply (rule ccontr)
126  apply simp
127  apply (erule_tac x="ucast x" in in_emptyE)
128  apply clarsimp
129  apply (rule conjI, blast)
130  apply (rule word_less_sub_1)
131  apply (rule order_less_le_trans)
132  apply (rule ucast_less, simp)
133  apply (simp add: asid_low_bits_def)
134  done
135
136
137lemma asid_high_bits_max_word:
138  "(2 ^ asid_high_bits - 1 :: 7 word) = max_word"
139  by (simp add: asid_high_bits_def max_word_def)
140
141
142lemma dom_ucast_eq_7:
143  "(- dom (\<lambda>a::7 word. p (ucast a::word32)) \<inter> {x. x \<le> 2 ^ asid_high_bits - 1} = {}) =
144   (- dom p \<inter> {x. x \<le> 2 ^ asid_high_bits - 1} = {})"
145  apply safe
146   apply clarsimp
147   apply (rule ccontr)
148   apply (erule_tac x="ucast x" in in_emptyE)
149   apply (clarsimp simp: asid_high_bits_max_word)
150   apply (clarsimp simp: ucast_ucast_mask)
151   apply (subst (asm) less_mask_eq)
152   apply (rule word_less_sub_le [THEN iffD1])
153     apply (simp add: word_bits_def)
154    apply (simp add: asid_high_bits_def)
155   apply simp
156  apply (clarsimp simp: asid_high_bits_max_word)
157  apply (rule ccontr)
158  apply simp
159  apply (erule_tac x="ucast x" in in_emptyE)
160  apply clarsimp
161  apply (rule conjI, blast)
162  apply (rule word_less_sub_1)
163  apply (rule order_less_le_trans)
164  apply (rule ucast_less, simp)
165  apply (simp add: asid_high_bits_def)
166  done
167
168
169lemma ucast_fst_hd_assocs:
170  "- dom (\<lambda>x. pool (ucast (x::asid_low_index)::machine_word)) \<inter> {x. ucast x + (w::machine_word) \<noteq> 0} \<noteq> {}
171  \<Longrightarrow>
172  fst (hd [(x, y)\<leftarrow>assocs pool . x \<le> 2 ^ asid_low_bits - 1 \<and> x + w \<noteq> 0 \<and> y = None]) =
173  ucast (fst (hd [(x, y)\<leftarrow>assocs (\<lambda>a::asid_low_index. pool (ucast a)) .
174                          x \<le> 2 ^ asid_low_bits - 1 \<and>
175                          ucast x + w \<noteq> 0 \<and> y = None]))"
176  apply (simp add: ucast_assocs[unfolded o_def])
177  apply (simp add: filter_map split_def)
178  apply (simp cong: conj_cong add: ucast_ucast_len)
179  apply (simp add: asid_low_bits_def minus_one_norm)
180  apply (simp add: ord_le_eq_trans [OF word_n1_ge])
181  apply (simp add: word_le_make_less)
182  apply (subgoal_tac "P" for P)  (* cut_tac but more awesome *)
183   apply (subst hd_map, assumption)
184   apply simp
185   apply (rule sym, rule ucast_ucast_len)
186   apply (drule hd_in_set)
187   apply simp
188  apply (simp add: assocs_empty_dom_comp null_def split_def)
189  apply (simp add: ucast_assocs[unfolded o_def] filter_map split_def)
190  apply (simp cong: conj_cong add: ucast_ucast_len)
191  done
192
193
194crunch typ_at [wp]: perform_page_table_invocation, perform_page_invocation,
195         perform_asid_pool_invocation, perform_page_directory_invocation "\<lambda>s. P (typ_at T p s)"
196  (wp: crunch_wps)
197
198crunch typ_at [wp]: perform_vcpu_invocation "\<lambda>s. P (typ_at T p s)"
199  (wp: crunch_wps)
200
201lemmas perform_page_table_invocation_typ_ats [wp] =
202  abs_typ_at_lifts [OF perform_page_table_invocation_typ_at]
203
204lemmas perform_page_directory_invocation_typ_ats [wp] =
205  abs_typ_at_lifts [OF perform_page_directory_invocation_typ_at]
206
207lemmas perform_page_invocation_typ_ats [wp] =
208  abs_typ_at_lifts [OF perform_page_invocation_typ_at]
209
210lemmas perform_asid_pool_invocation_typ_ats [wp] =
211  abs_typ_at_lifts [OF perform_asid_pool_invocation_typ_at]
212
213lemmas perform_vcpu_invocation_typ_ats [wp] =
214  abs_typ_at_lifts [OF perform_vcpu_invocation_typ_at]
215(* ARMHYP FIXME this is not enough, add appropriate lifting rule to abs_typ_at_lifts *)
216
217lemma perform_asid_control_invocation_tcb_at:
218  "\<lbrace>invs and valid_aci aci and st_tcb_at active p and
219    K (\<forall>w a b c. aci = asid_control_invocation.MakePool w a b c \<longrightarrow> w \<noteq> p)\<rbrace>
220  perform_asid_control_invocation aci
221  \<lbrace>\<lambda>rv. tcb_at p\<rbrace>"
222  apply (simp add: perform_asid_control_invocation_def)
223  apply (cases aci)
224  apply clarsimp
225  apply (wp |simp)+
226    apply (wp obj_at_delete_objects retype_region_obj_at_other2  hoare_vcg_const_imp_lift|assumption)+
227  apply (intro impI conjI)
228    apply (clarsimp simp: retype_addrs_def obj_bits_api_def default_arch_object_def image_def ptr_add_def)
229   apply (clarsimp simp: st_tcb_at_tcb_at)+
230  apply (frule st_tcb_ex_cap)
231    apply fastforce
232   apply (clarsimp split: Structures_A.thread_state.splits)
233   apply auto[1]
234  apply (clarsimp simp: ex_nonz_cap_to_def valid_aci_def)
235  apply (frule invs_untyped_children)
236  apply (clarsimp simp:cte_wp_at_caps_of_state)
237  apply (erule_tac ptr="(aa,ba)" in untyped_children_in_mdbE[where P="\<lambda>c. t \<in> zobj_refs c" for t])
238      apply (simp add: cte_wp_at_caps_of_state)
239     apply simp
240    apply (simp add:cte_wp_at_caps_of_state)
241    apply fastforce
242   apply (clarsimp simp: zobj_refs_to_obj_refs)
243   apply (erule(1) in_empty_interE)
244    apply (clarsimp simp:page_bits_def)
245  apply simp
246  done
247
248
249lemma ucast_asid_high_btis_of_le [simp]:
250  "ucast (asid_high_bits_of w) \<le> (2 ^ asid_high_bits - 1 :: word32)"
251  apply (simp add: asid_high_bits_of_def)
252  apply (rule word_less_sub_1)
253  apply (rule order_less_le_trans)
254  apply (rule ucast_less)
255   apply simp
256  apply (simp add: asid_high_bits_def)
257  done
258
259crunch tcb_at[wp]: perform_vcpu_invocation "tcb_at p"
260
261lemma invoke_arch_tcb:
262  "\<lbrace>invs and valid_arch_inv ai and st_tcb_at active tptr\<rbrace>
263  arch_perform_invocation ai
264  \<lbrace>\<lambda>rv. tcb_at tptr\<rbrace>"
265  apply (simp add: arch_perform_invocation_def)
266  apply (cases ai, simp_all)
267      apply (wp, clarsimp simp: st_tcb_at_tcb_at)+
268    defer
269    apply (wp, clarsimp simp: st_tcb_at_tcb_at)
270   defer
271   apply (wp perform_asid_control_invocation_tcb_at)
272   apply (clarsimp simp add: valid_arch_inv_def)
273   apply (clarsimp simp: valid_aci_def)
274   apply (frule st_tcb_ex_cap)
275     apply fastforce
276    apply (clarsimp split: Structures_A.thread_state.splits)
277    apply auto[1]
278   apply (clarsimp simp: ex_nonz_cap_to_def)
279   apply (frule invs_untyped_children)
280   apply (clarsimp simp:cte_wp_at_caps_of_state)
281   apply (erule_tac ptr="(aa,ba)" in untyped_children_in_mdbE[where P="\<lambda>c. t \<in> zobj_refs c" for t])
282       apply (simp add: cte_wp_at_caps_of_state)+
283      apply fastforce
284    apply (clarsimp simp: zobj_refs_to_obj_refs cte_wp_at_caps_of_state)
285    apply (drule_tac p="(aa,ba)" in caps_of_state_valid_cap, fastforce)
286    apply (clarsimp simp: valid_cap_def cap_aligned_def)
287    apply (drule_tac x=tptr in base_member_set, simp)
288     apply (simp add: vspace_bits_defs field_simps del: atLeastAtMost_iff)
289    apply (metis (no_types) orthD1 x_power_minus_1)
290   apply simp
291  apply wp
292  apply (clarsimp simp: st_tcb_at_def tcb_at_def obj_at_def is_tcb_def)
293  done
294
295end
296
297
298locale asid_update = Arch +
299  fixes ap asid s s'
300  assumes ko: "ko_at (ArchObj (ASIDPool Map.empty)) ap s"
301  assumes empty: "arm_asid_table (arch_state s) asid = None"
302  defines "s' \<equiv> s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := arm_asid_table (arch_state s)(asid \<mapsto> ap)\<rparr>\<rparr>"
303
304
305context asid_update begin
306
307lemma vs_lookup1' [simp]:
308  "vs_lookup1 s' = vs_lookup1 s"
309  by (simp add: vs_lookup1_def s'_def)
310
311
312lemma vs_lookup_pages1' [simp]:
313  "vs_lookup_pages1 s' = vs_lookup_pages1 s"
314  by (simp add: vs_lookup_pages1_def s'_def)
315
316
317lemma vs_asid_refs' [simp]:
318  "vs_asid_refs (arm_asid_table (arch_state s')) =
319  vs_asid_refs (arm_asid_table (arch_state s)) \<union> {([VSRef (ucast asid) None], ap)}"
320  apply (simp add: s'_def)
321  apply (rule set_eqI)
322  apply (rule iffI)
323   apply (auto simp: vs_asid_refs_def split: if_split_asm)[1]
324  apply clarsimp
325  apply (erule disjE)
326   apply (auto simp: vs_asid_refs_def)[1]
327  apply (subst (asm) vs_asid_refs_def)
328  apply (clarsimp dest!: graph_ofD)
329  apply (rule vs_asid_refsI)
330  apply (clarsimp simp: empty)
331  done
332
333
334lemma vs_lookup':
335  "vs_lookup s' = vs_lookup s \<union> {([VSRef (ucast asid) None], ap)}"
336  using ko
337  apply (simp add: vs_lookup_def)
338  apply (rule rtrancl_insert)
339  apply (clarsimp simp: vs_lookup1_def obj_at_def vs_refs_def)
340  done
341
342
343lemma vs_lookup_pages':
344  "vs_lookup_pages s' = vs_lookup_pages s \<union> {([VSRef (ucast asid) None], ap)}"
345  using ko
346  apply (simp add: vs_lookup_pages_def)
347  apply (rule rtrancl_insert)
348  apply (clarsimp simp: vs_lookup_pages1_def obj_at_def vs_refs_pages_def)
349  done
350
351lemma obj_at [simp]:
352  "obj_at P p s' = obj_at P p s"
353  by (simp add: s'_def)
354
355lemma vs_lookup_neq: "\<lbrakk>(rs \<rhd> p) s' ; p \<noteq> ap\<rbrakk> \<Longrightarrow>  (rs \<rhd> p) s"
356   by (clarsimp simp: vs_lookup')
357
358lemma vspace_objs':
359  "valid_vspace_objs s \<Longrightarrow> valid_vspace_objs s'"
360  using ko
361  apply (clarsimp simp: valid_vspace_objs_def)
362  apply (erule_tac x=p in allE)
363  apply (case_tac "p = ap";
364         case_tac ao;
365         fastforce simp: obj_at_def s'_def
366                   intro: vs_lookup_neq)
367  done
368
369lemma caps_of_state_s':
370  "caps_of_state s' = caps_of_state s"
371  by (rule caps_of_state_pspace, simp add: s'_def)
372
373
374lemma valid_vs_lookup':
375  "\<lbrakk> valid_vs_lookup s;
376     \<exists>ptr cap. caps_of_state s ptr = Some cap
377     \<and> ap \<in> obj_refs cap \<and> vs_cap_ref cap = Some [VSRef (ucast asid) None] \<rbrakk>
378  \<Longrightarrow> valid_vs_lookup s'"
379  by (clarsimp simp: valid_vs_lookup_def caps_of_state_s' vs_lookup_pages')
380
381
382lemma valid_table_caps':
383  "\<lbrakk> valid_table_caps s \<rbrakk>
384        \<Longrightarrow> valid_table_caps s'"
385  apply (simp add: valid_table_caps_def caps_of_state_s')
386  done
387
388
389lemma valid_arch_caps:
390  "\<lbrakk> valid_arch_caps s;
391     \<exists>ptr cap. caps_of_state s ptr = Some cap
392     \<and> ap \<in> obj_refs cap \<and> vs_cap_ref cap = Some [VSRef (ucast asid) None] \<rbrakk>
393  \<Longrightarrow> valid_arch_caps s'"
394  by (simp add: valid_arch_caps_def caps_of_state_s'
395                valid_table_caps' valid_vs_lookup')
396
397
398lemma valid_asid_map':
399  "valid_asid_map s \<Longrightarrow> valid_asid_map s'"
400  using empty
401  apply (clarsimp simp: valid_asid_map_def s'_def)
402  apply (drule bspec, blast)
403  apply (clarsimp simp: vspace_at_asid_def)
404  apply (drule vs_lookup_2ConsD)
405  apply clarsimp
406  apply (erule vs_lookup_atE)
407  apply (drule vs_lookup1D)
408  apply clarsimp
409  apply (rule vs_lookupI[rotated])
410   apply (rule r_into_rtrancl)
411   apply (rule vs_lookup1I)
412     apply (fastforce simp: obj_at_def)
413    apply assumption
414   apply simp
415  apply (clarsimp simp: vs_asid_refs_def graph_of_def)
416  apply fastforce
417  done
418
419end
420
421
422context Arch begin global_naming ARM
423
424lemma valid_arch_state_strg:
425  "valid_arch_state s \<and> ap \<notin> ran (arm_asid_table (arch_state s)) \<and> asid_pool_at ap s \<longrightarrow>
426   valid_arch_state (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := arm_asid_table (arch_state s)(asid \<mapsto> ap)\<rparr>\<rparr>)"
427  apply (clarsimp simp: valid_arch_state_def split: option.split)
428  apply (clarsimp simp: valid_asid_table_def ran_def)
429  apply (fastforce intro!: inj_on_fun_updI)
430  done
431
432
433lemma valid_vs_lookup_at_upd_strg:
434  "valid_vs_lookup s \<and>
435   ko_at (ArchObj (ASIDPool Map.empty)) ap s \<and>
436   arm_asid_table (arch_state s) asid = None \<and>
437   (\<exists>ptr cap. caps_of_state s ptr = Some cap \<and> ap \<in> obj_refs cap \<and>
438              vs_cap_ref cap = Some [VSRef (ucast asid) None])
439   \<longrightarrow>
440   valid_vs_lookup (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := arm_asid_table (arch_state s)(asid \<mapsto> ap)\<rparr>\<rparr>)"
441  apply clarsimp
442  apply (subgoal_tac "asid_update ap asid s")
443   prefer 2
444   apply unfold_locales[1]
445    apply assumption+
446  apply (erule (1) asid_update.valid_vs_lookup')
447  apply fastforce
448  done
449
450
451lemma retype_region_ap:
452  "\<lbrace>\<top>\<rbrace>
453  retype_region ap 1 0 (ArchObject ASIDPoolObj) dev
454  \<lbrace>\<lambda>_. ko_at (ArchObj (arch_kernel_obj.ASIDPool Map.empty)) ap\<rbrace>"
455  apply (rule hoare_post_imp)
456   prefer 2
457   apply (rule retype_region_obj_at)
458    apply simp
459   apply simp
460  apply (clarsimp simp: retype_addrs_def obj_bits_api_def default_arch_object_def)
461  apply (clarsimp simp: obj_at_def default_object_def default_arch_object_def)
462  done
463
464
465lemma retype_region_ap':
466  "\<lbrace>\<top>\<rbrace> retype_region ap 1 0 (ArchObject ASIDPoolObj) dev \<lbrace>\<lambda>rv. asid_pool_at ap\<rbrace>"
467  apply (rule hoare_strengthen_post, rule retype_region_ap)
468  apply (clarsimp simp: a_type_def elim!: obj_at_weakenE)
469  done
470
471
472lemma no_cap_to_obj_with_diff_ref_null_filter:
473  "no_cap_to_obj_with_diff_ref cap S
474     = (\<lambda>s. \<forall>c \<in> ran (null_filter (caps_of_state s) |` (- S)).
475             obj_refs c = obj_refs cap
476                 \<longrightarrow> table_cap_ref c = table_cap_ref cap)"
477  apply (simp add: no_cap_to_obj_with_diff_ref_def
478                   ball_ran_eq cte_wp_at_caps_of_state)
479  apply (simp add: Ball_def)
480  apply (intro iff_allI ext)
481  apply (simp add: restrict_map_def null_filter_def)
482  apply (auto dest!: obj_ref_none_no_asid[rule_format]
483               simp: table_cap_ref_def)
484  done
485
486
487lemma retype_region_no_cap_to_obj:
488  "\<lbrace>valid_pspace and valid_mdb
489             and caps_overlap_reserved {ptr..ptr + 2 ^ obj_bits_api ty us - 1}
490             and caps_no_overlap ptr sz
491             and pspace_no_overlap_range_cover ptr sz
492             and no_cap_to_obj_with_diff_ref cap S
493             and (\<lambda>s. \<exists>slot. cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) slot s)
494             and K (ty = Structures_A.CapTableObject \<longrightarrow> 0 < us)
495             and K (range_cover ptr sz (obj_bits_api ty us) 1) \<rbrace>
496     retype_region ptr 1 us ty dev
497   \<lbrace>\<lambda>rv. no_cap_to_obj_with_diff_ref cap S\<rbrace>"
498  apply (rule hoare_gen_asm)+
499  apply (simp add: no_cap_to_obj_with_diff_ref_null_filter)
500  apply (wp retype_region_caps_of | simp)+
501  apply fastforce
502  done
503
504
505lemma valid_table_caps_asid_upd [iff]:
506  "valid_table_caps (s\<lparr>arch_state := (arm_asid_table_update f (arch_state s))\<rparr>) =
507   valid_table_caps s"
508  by (simp add: valid_table_caps_def)
509
510
511lemma vs_asid_ref_upd:
512  "([VSRef (ucast (asid_high_bits_of asid')) None] \<rhd> ap')
513    (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := arm_asid_table (arch_state s)(asid_high_bits_of asid \<mapsto> ap)\<rparr>\<rparr>)
514  = (if asid_high_bits_of asid' = asid_high_bits_of asid
515    then ap' = ap
516    else ([VSRef (ucast (asid_high_bits_of asid')) None] \<rhd> ap') s)"
517  by (fastforce intro: vs_lookup_atI elim: vs_lookup_atE)
518
519
520lemma vs_asid_ref_eq:
521  "([VSRef (ucast asid) None] \<rhd> ap) s
522  = (arm_asid_table (arch_state s) asid = Some ap)"
523  by (fastforce elim: vs_lookup_atE intro: vs_lookup_atI)
524
525
526lemma set_cap_reachable_pg_cap:
527  "\<lbrace>\<lambda>s. P (reachable_pg_cap cap s)\<rbrace> set_cap x y \<lbrace>\<lambda>_ s. P (reachable_pg_cap cap s)\<rbrace>"
528  by (unfold reachable_pg_cap_def, wp hoare_vcg_ex_lift set_cap.vs_lookup_pages)
529
530
531lemma cap_insert_simple_arch_caps_ap:
532  "\<lbrace>valid_arch_caps and (\<lambda>s. cte_wp_at (safe_parent_for (cdt s) src cap) src s)
533     and no_cap_to_obj_with_diff_ref cap {dest}
534     and (\<lambda>s. arm_asid_table (arch_state s) (asid_high_bits_of asid) = None)
535     and ko_at (ArchObj (ASIDPool Map.empty)) ap
536     and K (cap = ArchObjectCap (ASIDPoolCap ap asid)) \<rbrace>
537     cap_insert cap src dest
538   \<lbrace>\<lambda>rv s. valid_arch_caps (s\<lparr>arch_state := arch_state s
539                       \<lparr>arm_asid_table := arm_asid_table (arch_state s)(asid_high_bits_of asid \<mapsto> ap)\<rparr>\<rparr>)\<rbrace>"
540  apply (simp add: cap_insert_def update_cdt_def set_cdt_def valid_arch_caps_def
541    set_untyped_cap_as_full_def bind_assoc)
542  apply (strengthen valid_vs_lookup_at_upd_strg)
543  apply (wp get_cap_wp set_cap_valid_vs_lookup set_cap_arch_obj
544            set_cap_valid_table_caps hoare_vcg_all_lift
545          | simp split del: if_split)+
546       apply (rule_tac P = "cte_wp_at ((=) src_cap) src" in set_cap_orth)
547       apply (wp hoare_vcg_imp_lift hoare_vcg_ball_lift set_free_index_final_cap
548                 hoare_vcg_disj_lift set_cap_reachable_pg_cap set_cap.vs_lookup_pages
549              | clarsimp)+
550      apply (wp set_cap_arch_obj set_cap_valid_table_caps hoare_vcg_ball_lift
551                get_cap_wp static_imp_wp set_cap_empty_tables[simplified second_level_tables_def, simplified])+
552  apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps)
553  apply (rule conjI)
554   apply (clarsimp simp: vs_cap_ref_def)
555   apply (rule_tac x="fst dest" in exI)
556   apply (rule_tac x="snd dest" in exI)
557   apply simp
558  apply (rule conjI)
559   apply (simp add: unique_table_caps_def is_cap_simps)
560  apply (subst unique_table_refs_def)
561  apply (intro allI impI)
562  apply (simp split: if_split_asm)
563    apply (simp add: no_cap_to_obj_with_diff_ref_def cte_wp_at_caps_of_state)
564   apply (simp add: no_cap_to_obj_with_diff_ref_def cte_wp_at_caps_of_state)
565  apply (erule (3) unique_table_refsD)
566  done
567
568lemma valid_asid_map_asid_upd_strg:
569  "valid_asid_map s \<and>
570   ko_at (ArchObj (ASIDPool Map.empty)) ap s \<and>
571   arm_asid_table (arch_state s) asid = None \<longrightarrow>
572   valid_asid_map (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := arm_asid_table (arch_state s)(asid \<mapsto> ap)\<rparr>\<rparr>)"
573  apply clarsimp
574  apply (subgoal_tac "asid_update ap asid s")
575   prefer 2
576   apply unfold_locales[1]
577    apply assumption+
578  apply (erule (1) asid_update.valid_asid_map')
579  done
580
581lemma valid_vspace_objs_asid_upd_strg:
582  "valid_vspace_objs s \<and>
583   ko_at (ArchObj (ASIDPool Map.empty)) ap s \<and>
584   arm_asid_table (arch_state s) asid = None \<longrightarrow>
585   valid_vspace_objs (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := arm_asid_table (arch_state s)(asid \<mapsto> ap)\<rparr>\<rparr>)"
586  apply clarsimp
587  apply (subgoal_tac "asid_update ap asid s")
588   prefer 2
589   apply unfold_locales[1]
590    apply assumption+
591  apply (erule (1) asid_update.vspace_objs')
592  done
593
594lemma safe_parent_cap_is_device:
595  "safe_parent_for m p cap pcap \<Longrightarrow> cap_is_device cap = cap_is_device pcap"
596  by (simp add: safe_parent_for_def)
597
598lemma cap_insert_ap_invs:
599  "\<lbrace>invs and valid_cap cap and tcb_cap_valid cap dest and
600    ex_cte_cap_wp_to (appropriate_cte_cap cap) dest and
601    cte_wp_at (\<lambda>c. c = NullCap) dest and
602    no_cap_to_obj_with_diff_ref cap {dest} and
603    (\<lambda>s. cte_wp_at (safe_parent_for (cdt s) src cap) src s) and
604    K (cap = ArchObjectCap (ASIDPoolCap ap asid)) and
605   (\<lambda>s. \<forall>irq \<in> cap_irqs cap. irq_issued irq s) and
606   ko_at (ArchObj (ASIDPool Map.empty)) ap and
607   (\<lambda>s. ap \<notin> ran (arm_asid_table (arch_state s)) \<and>
608        arm_asid_table (arch_state s) (asid_high_bits_of asid) = None)\<rbrace>
609  cap_insert cap src dest
610  \<lbrace>\<lambda>rv s. invs (s\<lparr>arch_state := arch_state s
611                       \<lparr>arm_asid_table := (arm_asid_table \<circ> arch_state) s(asid_high_bits_of asid \<mapsto> ap)\<rparr>\<rparr>)\<rbrace>"
612
613  apply (simp add: invs_def valid_state_def valid_pspace_def)
614  apply (strengthen valid_arch_state_strg valid_vspace_objs_asid_upd_strg
615                    valid_asid_map_asid_upd_strg )
616  apply (simp cong: conj_cong)
617  apply (rule hoare_pre)
618   apply (wpsimp wp: cap_insert_simple_mdb cap_insert_iflive
619             cap_insert_zombies cap_insert_ifunsafe
620             cap_insert_valid_global_refs cap_insert_idle
621             valid_irq_node_typ cap_insert_simple_arch_caps_ap
622             simp: valid_global_objs_def valid_global_vspace_mappings_def)
623  apply (clarsimp simp: is_simple_cap_def cte_wp_at_caps_of_state is_cap_simps)
624  apply (frule safe_parent_cap_is_device)
625  apply (drule safe_parent_cap_range)
626  apply (simp add: cap_range_def)
627  apply (rule conjI)
628  apply clarsimp
629   apply (drule_tac p="(a,b)" in caps_of_state_valid_cap, fastforce)
630   apply (auto simp: obj_at_def is_tcb_def is_cap_table_def a_type_def
631                     valid_cap_def [where c="cap.Zombie a b x" for a b x]
632               dest: obj_ref_is_tcb obj_ref_is_cap_table split: option.splits)
633  done
634
635lemma max_index_upd_no_cap_to:
636  "\<lbrace>\<lambda>s. no_cap_to_obj_with_diff_ref cap {slot} s \<and>
637        cte_wp_at ((=) ucap) cref s \<and> is_untyped_cap ucap\<rbrace>
638   set_cap (max_free_index_update ucap) cref
639   \<lbrace>\<lambda>rv s. no_cap_to_obj_with_diff_ref cap {slot} s \<rbrace>"
640  apply (clarsimp simp:no_cap_to_obj_with_diff_ref_def)
641  apply (wp hoare_vcg_ball_lift set_cap_cte_wp_at_neg)
642  apply (clarsimp simp:cte_wp_at_caps_of_state free_index_update_def is_cap_simps)
643  apply (drule_tac x = cref in bspec)
644   apply clarsimp
645  apply (clarsimp simp:table_cap_ref_def)
646  done
647
648
649lemma perform_asid_control_invocation_st_tcb_at:
650  "\<lbrace>st_tcb_at (P and (Not \<circ> inactive) and (Not \<circ> idle)) t
651    and ct_active and invs and valid_aci aci\<rbrace>
652    perform_asid_control_invocation aci
653  \<lbrace>\<lambda>y. st_tcb_at P t\<rbrace>"
654  supply
655    is_aligned_neg_mask_eq[simp del]
656    is_aligned_neg_mask_weaken[simp del]
657  apply (clarsimp simp: perform_asid_control_invocation_def split: asid_control_invocation.splits)
658  apply (rename_tac word1 a b aa ba word2)
659  apply (rule hoare_name_pre_state)
660  apply (subgoal_tac "is_aligned word1 page_bits")
661   prefer 2
662   apply (clarsimp simp: valid_aci_def cte_wp_at_caps_of_state)
663   apply (drule(1) caps_of_state_valid[rotated])+
664   apply (simp add:valid_cap_simps cap_aligned_def page_bits_def)
665  apply (subst delete_objects_rewrite)
666     apply (simp add:page_bits_def word_bits_def word_size_bits_def pageBits_def)+
667   apply (simp add:is_aligned_neg_mask_eq)
668  apply (wp hoare_vcg_const_imp_lift retype_region_st_tcb_at set_cap_no_overlap|simp)+
669    apply (strengthen invs_valid_objs invs_psp_aligned)
670    apply (clarsimp simp:conj_comms)
671    apply (wp max_index_upd_invs_simple get_cap_wp)+
672  apply (clarsimp simp: valid_aci_def)
673  apply (frule intvl_range_conv)
674   apply (simp add:word_bits_def page_bits_def pageBits_def)
675  apply (clarsimp simp:detype_clear_um_independent page_bits_def is_aligned_neg_mask_eq)
676  apply (rule conjI)
677  apply (clarsimp simp:cte_wp_at_caps_of_state)
678   apply (rule pspace_no_overlap_detype)
679     apply (rule caps_of_state_valid_cap)
680      apply (simp add:page_bits_def)+
681    apply (simp add:invs_valid_objs invs_psp_aligned)+
682  apply (rule conjI)
683   apply (erule pred_tcb_weakenE, simp)
684  apply (rule conjI)
685   apply (frule st_tcb_ex_cap)
686     apply clarsimp
687    apply (clarsimp split: Structures_A.thread_state.splits)
688   apply (clarsimp simp: ex_nonz_cap_to_def)
689   apply (frule invs_untyped_children)
690   apply (clarsimp simp:cte_wp_at_caps_of_state)
691   apply (erule_tac ptr="(aa,ba)" in untyped_children_in_mdbE[where P="\<lambda>c. t \<in> zobj_refs c" for t])
692       apply (simp add: cte_wp_at_caps_of_state)+
693      apply fastforce
694    apply (clarsimp simp: zobj_refs_to_obj_refs)
695    apply (fastforce simp:page_bits_def)
696   apply simp
697  apply (clarsimp simp:obj_bits_api_def arch_kobj_size_def cte_wp_at_caps_of_state
698    default_arch_object_def empty_descendants_range_in)
699  apply (frule_tac cap = "(cap.UntypedCap False word1 pageBits idx)"
700    in detype_invariants[rotated 3],clarsimp+)
701    apply (simp add:cte_wp_at_caps_of_state
702      empty_descendants_range_in descendants_range_def2)+
703  apply (thin_tac "x = Some cap.NullCap" for x)+
704  apply (drule(1) caps_of_state_valid_cap[OF _ invs_valid_objs])
705  apply (intro conjI)
706    apply (clarsimp simp:valid_cap_def cap_aligned_def range_cover_full
707     invs_psp_aligned invs_valid_objs page_bits_def)
708   apply (erule pspace_no_overlap_detype)
709  apply (auto simp:page_bits_def detype_clear_um_independent)
710  done
711
712
713lemma set_cap_idx_up_aligned_area:
714  "\<lbrace>K (\<exists>idx. pcap = UntypedCap dev ptr pageBits idx) and cte_wp_at ((=) pcap) slot
715      and valid_objs\<rbrace> set_cap (max_free_index_update pcap) slot
716  \<lbrace>\<lambda>rv s. (\<exists>slot. cte_wp_at (\<lambda>c. up_aligned_area ptr pageBits \<subseteq> cap_range c \<and> cap_is_device c = dev) slot s)\<rbrace>"
717  apply (rule hoare_pre)
718  apply (wp hoare_vcg_ex_lift set_cap_cte_wp_at)
719  apply (rule_tac x = slot in exI)
720  apply clarsimp
721  apply (frule(1) cte_wp_valid_cap)
722  apply (clarsimp simp: cte_wp_at_caps_of_state is_aligned_neg_mask_eq
723                        p_assoc_help valid_cap_def valid_untyped_def cap_aligned_def)
724  done
725
726primrec(nonexhaustive)  get_untyped_cap_idx :: "cap \<Rightarrow> nat"
727where "get_untyped_cap_idx (UntypedCap dev ref sz idx) = idx"
728
729
730lemma aci_invs':
731  assumes Q_ignores_arch[simp]: "\<And>f s. Q (arch_state_update f s) = Q s"
732  assumes Q_ignore_machine_state[simp]: "\<And>f s. Q (machine_state_update f s) = Q s"
733  assumes Q_detype[simp]: "\<And>f s. Q (detype f s) = Q s"
734  assumes cap_insert_Q: "\<And>cap src dest. \<lbrace>Q and invs and K (src \<noteq> dest)\<rbrace>
735                            cap_insert cap src dest
736                           \<lbrace>\<lambda>_.Q\<rbrace>"
737  assumes retype_region_Q[wp]:"\<And>a b c d e. \<lbrace>Q\<rbrace> retype_region a b c d e \<lbrace>\<lambda>_.Q\<rbrace>"
738  assumes set_cap_Q[wp]: "\<And>a b. \<lbrace>Q\<rbrace> set_cap a b \<lbrace>\<lambda>_.Q\<rbrace>"
739  shows
740  "\<lbrace>invs and Q and ct_active and valid_aci aci\<rbrace> perform_asid_control_invocation aci \<lbrace>\<lambda>y s. invs s \<and> Q s\<rbrace>"
741  proof -
742  have cap_insert_invsQ:
743       "\<And>cap src dest ap asid.
744        \<lbrace>Q and (invs and valid_cap cap and tcb_cap_valid cap dest and
745         ex_cte_cap_wp_to (appropriate_cte_cap cap) dest and
746         cte_wp_at (\<lambda>c. c = NullCap) dest and
747         no_cap_to_obj_with_diff_ref cap {dest} and
748         (\<lambda>s. cte_wp_at (safe_parent_for (cdt s) src cap) src s) and
749         K (cap = ArchObjectCap (ASIDPoolCap ap asid)) and
750         (\<lambda>s. \<forall>irq\<in>cap_irqs cap. irq_issued irq s) and
751         ko_at (ArchObj (ASIDPool Map.empty)) ap and
752         (\<lambda>s. ap \<notin> ran (arm_asid_table (arch_state s)) \<and>
753         arm_asid_table (arch_state s) (asid_high_bits_of asid) = None))\<rbrace>
754         cap_insert cap src dest
755        \<lbrace>\<lambda>rv s.
756           invs
757             (s\<lparr>arch_state := arch_state s
758                 \<lparr>arm_asid_table := (arm_asid_table \<circ> arch_state) s
759                    (asid_high_bits_of asid \<mapsto> ap)\<rparr>\<rparr>) \<and>
760           Q
761             (s\<lparr>arch_state := arch_state s
762                 \<lparr>arm_asid_table := (arm_asid_table \<circ> arch_state) s
763                    (asid_high_bits_of asid \<mapsto> ap)\<rparr>\<rparr>)\<rbrace>"
764        apply (wp cap_insert_ap_invs)
765        apply simp
766        apply (rule hoare_pre)
767        apply (rule cap_insert_Q)
768        apply (auto simp: cte_wp_at_caps_of_state)
769        done
770  show ?thesis
771  apply (clarsimp simp: perform_asid_control_invocation_def valid_aci_def
772    split: asid_control_invocation.splits)
773  apply (rename_tac word1 a b aa ba word2)
774  apply (rule hoare_pre)
775   apply (wp hoare_vcg_const_imp_lift)
776     apply (wp cap_insert_invsQ hoare_vcg_ex_lift
777             | simp)+
778    apply (simp add: valid_cap_def |
779           strengthen real_cte_tcb_valid safe_parent_strg
780                      invs_vobjs_strgs
781                      ex_cte_cap_to_cnode_always_appropriate_strg)+
782    apply (wp hoare_vcg_const_imp_lift set_free_index_invs
783              retype_region_plain_invs[where sz = pageBits]
784              retype_cte_wp_at[where sz = pageBits] hoare_vcg_ex_lift
785              retype_region_obj_at_other3[where P="is_cap_table n" and sz = pageBits for n]
786              retype_region_ex_cte_cap_to[where sz = pageBits]
787              retype_region_ap[simplified]
788              retype_region_ap'[simplified]
789              retype_region_no_cap_to_obj[where sz = pageBits,simplified]
790               | simp del: split_paired_Ex)+
791   apply (strengthen invs_valid_objs invs_psp_aligned invs_mdb invs_valid_pspace
792                     exI[where x="case aci of MakePool frame slot parent base \<Rightarrow> parent"]
793                     exI[where x="case aci of MakePool frame slot parent base \<Rightarrow> parent", simplified]
794                     caps_region_kernel_window_imp[where
795                       p = "case aci of MakePool frame slot parent base \<Rightarrow> parent"]
796                     invs_cap_refs_in_kernel_window)+
797    apply (wp set_cap_caps_no_overlap set_cap_no_overlap get_cap_wp
798      max_index_upd_caps_overlap_reserved max_index_upd_invs_simple
799      set_cap_cte_cap_wp_to set_cap_cte_wp_at max_index_upd_no_cap_to
800      | simp split del: if_split | wp_once hoare_vcg_ex_lift)+
801    apply (rule_tac P = "is_aligned word1 page_bits" in hoare_gen_asm)
802    apply (subst delete_objects_rewrite)
803       apply (simp add:page_bits_def pageBits_def word_size_bits_def)
804      apply (simp add:page_bits_def pageBits_def word_bits_def)
805     apply (simp add:is_aligned_neg_mask_eq)
806    apply wp
807  apply (clarsimp simp: cte_wp_at_caps_of_state if_option_Some
808                        Word_Miscellaneous.if_bool_simps
809             split del: if_split)
810  apply (strengthen refl)
811  apply (frule_tac cap = "(cap.UntypedCap False word1 pageBits idx)"
812    in detype_invariants[rotated 3],clarsimp+)
813    apply (simp add:cte_wp_at_caps_of_state)+
814   apply (simp add:descendants_range_def2 empty_descendants_range_in)
815  apply (simp add:invs_mdb invs_valid_pspace invs_psp_aligned invs_valid_objs)
816  apply (clarsimp dest!:caps_of_state_cteD)
817  apply (frule(1) unsafe_protected[where p=t and p'=t for t])
818     apply (simp add:empty_descendants_range_in)+
819    apply fastforce
820   apply clarsimp
821  apply (frule_tac p = "(aa,ba)" in cte_wp_valid_cap)
822   apply fastforce
823  apply (clarsimp simp: detype_clear_um_independent obj_bits_api_def arch_kobj_size_def
824   default_arch_object_def conj_comms)
825  apply (rule conjI)
826   apply (clarsimp simp:valid_cap_simps cap_aligned_def page_bits_def not_le)
827  apply clarsimp
828  apply (simp add:empty_descendants_range_in)
829  apply (frule valid_cap_aligned)
830  apply (clarsimp simp: cap_aligned_def is_aligned_neg_mask_eq)
831  apply (subst caps_no_overlap_detype[OF descendants_range_caps_no_overlapI],
832    assumption, simp add: is_aligned_neg_mask_eq,
833    simp add: empty_descendants_range_in)
834  apply (frule pspace_no_overlap_detype, clarify+)
835  apply (frule intvl_range_conv[where bits = pageBits])
836   apply (simp add:pageBits_def word_bits_def)
837  apply (simp add:is_aligned_neg_mask_eq)
838  apply (clarsimp simp:is_aligned_neg_mask_eq page_bits_def)
839  apply (frule(1) ex_cte_cap_protects)
840      apply (simp add:empty_descendants_range_in)
841     apply fastforce
842    apply (rule subset_refl)
843   apply fastforce
844  apply (clarsimp simp: field_simps)
845  apply (intro conjI impI,
846     simp_all add:free_index_of_def valid_cap_simps valid_untyped_def
847     empty_descendants_range_in range_cover_full clear_um_def max_free_index_def,
848     (clarsimp simp:valid_untyped_def valid_cap_simps)+)[1]
849
850    apply (erule(1) cap_to_protected)
851    apply (simp add:empty_descendants_range_in descendants_range_def2)+
852
853   apply clarsimp
854   apply (drule invs_arch_state)+
855   apply (clarsimp simp: valid_arch_state_def valid_asid_table_def)
856   apply (drule (1) bspec)+
857   apply clarsimp
858   apply (erule notE, erule is_aligned_no_overflow)
859
860  apply (clarsimp simp: no_cap_to_obj_with_diff_ref_def)
861  apply (thin_tac "cte_wp_at ((=) cap.NullCap) p s" for p s)
862  apply (subst(asm) eq_commute,
863         erule(1) untyped_children_in_mdbE[where cap="cap.UntypedCap dev p bits idx" for dev p bits idx,
864                                         simplified, rotated])
865    apply (simp add: is_aligned_no_overflow)
866   apply simp
867  apply clarsimp
868  done
869
870qed
871
872lemmas aci_invs[wp] = aci_invs'[where Q=\<top>,simplified hoare_post_taut, OF refl refl refl TrueI TrueI TrueI,simplified]
873
874lemma obj_at_upd2:
875  "obj_at P t' (s\<lparr>kheap := kheap s(t \<mapsto> v, x \<mapsto> v')\<rparr>) = (if t' = x then P v' else obj_at P t' (s\<lparr>kheap := kheap s(t \<mapsto> v)\<rparr>))"
876  by (simp add: obj_at_update obj_at_def)
877
878lemma vcpu_invalidate_active_hyp_refs_empty[wp]:
879  "\<lbrace>obj_at (\<lambda>ko. hyp_refs_of ko = {}) p\<rbrace> vcpu_invalidate_active \<lbrace>\<lambda>r. obj_at (\<lambda>ko. hyp_refs_of ko = {}) p\<rbrace>"
880  unfolding vcpu_invalidate_active_def vcpu_disable_def by wpsimp
881
882lemma as_user_hyp_refs_empty[wp]:
883  "\<lbrace>obj_at (\<lambda>ko. hyp_refs_of ko = {}) p\<rbrace> as_user t f \<lbrace>\<lambda>r. obj_at (\<lambda>ko. hyp_refs_of ko = {}) p\<rbrace>"
884  unfolding as_user_def
885  apply (wpsimp wp: set_object_wp)
886  by (clarsimp simp: get_tcb_Some_ko_at obj_at_def arch_tcb_context_set_def)
887
888lemma dissociate_vcpu_tcb_obj_at_hyp_refs[wp]:
889  "\<lbrace>\<lambda>s. p \<notin> {t, vr} \<longrightarrow> obj_at (\<lambda>ko. hyp_refs_of ko = {}) p s \<rbrace>
890     dissociate_vcpu_tcb t vr
891   \<lbrace>\<lambda>rv s. obj_at (\<lambda>ko. hyp_refs_of ko = {}) p s\<rbrace>"
892  unfolding dissociate_vcpu_tcb_def
893  apply (cases "p \<notin> {t, vr}"; clarsimp)
894   apply (wp arch_thread_set_wp set_vcpu_wp)
895        apply (clarsimp simp: obj_at_upd2 obj_at_update)
896        apply (wp hoare_drop_imp get_vcpu_wp)+
897   apply (clarsimp simp: obj_at_upd2 obj_at_update)
898  apply (erule disjE;
899          (wp arch_thread_set_wp set_vcpu_wp
900          | clarsimp simp: obj_at_upd2 obj_at_update)+)
901  done
902
903lemma associate_vcpu_tcb_sym_refs_hyp[wp]:
904  "\<lbrace>\<lambda>s. sym_refs (state_hyp_refs_of s)\<rbrace> associate_vcpu_tcb vr t \<lbrace>\<lambda>rv s. sym_refs (state_hyp_refs_of s)\<rbrace>"
905  apply (simp add: associate_vcpu_tcb_def)
906  apply (wp arch_thread_set_wp set_vcpu_wp | clarsimp)+
907      apply (rule_tac P="\<lambda>s. ko_at (ArchObj (VCPU v)) vr s \<and>
908                             obj_at (\<lambda>ko. hyp_refs_of ko = {} ) t s  \<and>
909                             sym_refs (state_hyp_refs_of s)"
910                          in hoare_triv)
911      apply (rule_tac Q="\<lambda>rv s. obj_at (\<lambda>ko. hyp_refs_of ko = {} ) vr s \<and>
912                                obj_at (\<lambda>ko. hyp_refs_of ko = {} ) t s  \<and>
913                                sym_refs (state_hyp_refs_of s)"
914                             in hoare_post_imp)
915       apply (clarsimp dest!: get_tcb_SomeD simp: obj_at_def)
916       apply (clarsimp simp add: sym_refs_def)
917       apply (case_tac "x = t"; case_tac "x = vr"; clarsimp simp add: state_hyp_refs_of_def obj_at_def
918                                                                 dest!: get_tcb_SomeD)
919       apply fastforce
920      apply (rule hoare_pre)
921       apply (wp | wpc | clarsimp)+
922      apply (simp add: obj_at_def)
923     apply (wp  get_vcpu_ko | wpc | clarsimp)+
924   apply (rule_tac Q="\<lambda>rv s. (\<exists>t'. obj_at (\<lambda>tcb. tcb = TCB t' \<and> rv = tcb_vcpu (tcb_arch t')) t s) \<and>
925                             sym_refs (state_hyp_refs_of s)"
926                          in hoare_post_imp)
927    apply (clarsimp simp: obj_at_def)
928   apply (wp arch_thread_get_tcb)
929  apply simp
930  done
931
932lemma arch_thread_set_inv_neq:
933  "\<lbrace>obj_at P p and K (t \<noteq> p)\<rbrace> arch_thread_set f t \<lbrace>\<lambda>rv. obj_at P p\<rbrace>"
934  unfolding arch_thread_set_def by (wpsimp wp: set_object_wp) (simp add: obj_at_def)
935
936lemma live_vcpu [simp]:
937  "live (ArchObj (VCPU (v\<lparr>vcpu_tcb := Some tcb\<rparr>)))"
938  by (simp add: live_def hyp_live_def arch_live_def)
939
940lemma ex_nonz_cap_to_vcpu_udpate[simp]:
941  "ex_nonz_cap_to t (s\<lparr>arch_state := arm_current_vcpu_update f (arch_state s)\<rparr>) = ex_nonz_cap_to t s"
942  by (simp add: ex_nonz_cap_to_def)
943
944lemma caps_of_state_VCPU_update:
945  "vcpu_at a s \<Longrightarrow> caps_of_state (s\<lparr>kheap := kheap s(a \<mapsto> ArchObj (VCPU b))\<rparr>) = caps_of_state s"
946  by (rule ext) (auto simp: caps_of_state_cte_wp_at cte_wp_at_cases obj_at_def)
947
948lemma set_vcpu_ex_nonz_cap_to[wp]:
949  "\<lbrace>ex_nonz_cap_to t\<rbrace> set_vcpu a b \<lbrace>\<lambda>_. ex_nonz_cap_to t\<rbrace>"
950  apply (wp set_vcpu_wp)
951  apply (clarsimp simp: ex_nonz_cap_to_def cte_wp_at_caps_of_state caps_of_state_VCPU_update)
952  done
953
954lemma caps_of_state_tcb_arch_update:
955  "ko_at (TCB y) t' s \<Longrightarrow> caps_of_state (s\<lparr>kheap := kheap s(t' \<mapsto> TCB (y\<lparr>tcb_arch := f (tcb_arch y)\<rparr>))\<rparr>) = caps_of_state s"
956  by (rule ext) (auto simp: caps_of_state_cte_wp_at cte_wp_at_cases obj_at_def tcb_cap_cases_def)
957
958lemma arch_thread_set_ex_nonz_cap_to[wp]:
959  "\<lbrace>ex_nonz_cap_to t\<rbrace> arch_thread_set f t' \<lbrace>\<lambda>_. ex_nonz_cap_to t\<rbrace>"
960  apply (wp arch_thread_set_wp)
961  apply clarsimp
962  apply (clarsimp simp: ex_nonz_cap_to_def get_tcb_Some_ko_at cte_wp_at_caps_of_state
963                        caps_of_state_tcb_arch_update)
964  done
965
966crunch ex_nonz_cap_to[wp]: dissociate_vcpu_tcb "ex_nonz_cap_to t"
967  (wp: crunch_wps)
968
969lemma associate_vcpu_tcb_if_live_then_nonz_cap[wp]:
970  "\<lbrace>if_live_then_nonz_cap and ex_nonz_cap_to vcpu and ex_nonz_cap_to tcb\<rbrace>
971    associate_vcpu_tcb vcpu tcb \<lbrace>\<lambda>_. if_live_then_nonz_cap\<rbrace>"
972  unfolding associate_vcpu_tcb_def
973  by (wpsimp wp: arch_thread_set_inv_neq hoare_disjI1 get_vcpu_wp hoare_vcg_all_lift hoare_drop_imps)
974
975lemma set_vcpu_valid_arch_Some[wp]:
976  "\<lbrace>valid_arch_state\<rbrace> set_vcpu vcpu (v\<lparr>vcpu_tcb := Some tcb\<rparr>) \<lbrace>\<lambda>_. valid_arch_state\<rbrace>"
977  apply (wp set_vcpu_wp)
978  apply (clarsimp simp: valid_arch_state_def)
979  apply (rule conjI)
980   apply (fastforce simp: valid_asid_table_def obj_at_def)
981  apply (clarsimp simp: obj_at_def is_vcpu_def hyp_live_def arch_live_def split: option.splits)
982  done
983
984lemma valid_global_objs_vcpu_update_str:
985  "valid_global_objs s \<Longrightarrow> valid_global_objs (s\<lparr>arch_state := arm_current_vcpu_update f (arch_state s)\<rparr>)"
986  by (simp add: valid_global_objs_def)
987
988lemma valid_global_vspace_mappings_vcpu_update_str:
989  "valid_global_vspace_mappings s \<Longrightarrow> valid_global_vspace_mappings (s\<lparr>arch_state := arm_current_vcpu_update f (arch_state s)\<rparr>)"
990  by (simp add: valid_global_vspace_mappings_def)
991
992lemma associate_vcpu_tcb_invs[wp]:
993  "\<lbrace>invs and ex_nonz_cap_to vcpu and ex_nonz_cap_to tcb and vcpu_at vcpu and  (\<lambda>s. tcb \<noteq> idle_thread s)\<rbrace>
994   associate_vcpu_tcb vcpu tcb
995   \<lbrace>\<lambda>_. invs\<rbrace>"
996  using valid_global_vspace_mappings_def
997  apply (simp add: invs_def valid_state_def valid_pspace_def)
998  apply (simp add: pred_conj_def)
999  apply (rule hoare_pre)
1000   apply (rule hoare_vcg_conj_lift[rotated])+
1001   by (wp get_vcpu_wp arch_thread_get_wp weak_if_wp as_user_only_idle hoare_vcg_all_lift
1002        | wp_once hoare_drop_imps
1003        | wpc
1004        | clarsimp
1005        | strengthen valid_arch_state_vcpu_update_str valid_global_refs_vcpu_update_str
1006                     valid_global_vspace_mappings_vcpu_update_str valid_global_objs_vcpu_update_str
1007        | simp add: associate_vcpu_tcb_def valid_obj_def[abs_def] valid_vcpu_def
1008                    dissociate_vcpu_tcb_def vcpu_invalidate_active_def vcpu_disable_def
1009        | simp add: obj_at_def)+
1010
1011lemma set_vcpu_regs_update[wp]:
1012  "\<lbrace>invs and valid_obj p (ArchObj (VCPU vcpu)) and
1013    obj_at (\<lambda>ko'. hyp_refs_of ko' = vcpu_tcb_refs (vcpu_tcb vcpu)) p\<rbrace>
1014  set_vcpu p (vcpu_regs_update f vcpu) \<lbrace>\<lambda>_. invs\<rbrace>"
1015  unfolding invs_def valid_state_def
1016  by (wpsimp wp: set_vcpu_valid_pspace set_vcpu_valid_arch_eq_hyp)
1017
1018lemma vcpu_write_reg_invs[wp]:
1019  "\<lbrace>invs\<rbrace> vcpu_write_reg vcpuptr r v \<lbrace>\<lambda>_. invs\<rbrace>"
1020  unfolding vcpu_write_reg_def vcpu_update_def
1021  apply (wpsimp wp: get_vcpu_wp)
1022  apply (fastforce simp: obj_at_def dest!: invs_valid_objs)
1023  done
1024
1025lemma write_vcpu_register_invs[wp]:
1026  "\<lbrace>invs\<rbrace> write_vcpu_register vcpu reg val \<lbrace>\<lambda>_. invs\<rbrace>"
1027  unfolding write_vcpu_register_def
1028  by wpsimp
1029
1030lemma vgic_update_valid_pspace[wp]:
1031  "\<lbrace>valid_pspace\<rbrace> vgic_update vcpuptr f \<lbrace>\<lambda>_. valid_pspace\<rbrace>"
1032  unfolding vgic_update_def vcpu_update_def
1033  apply (wpsimp wp: set_vcpu_valid_pspace get_vcpu_wp simp: valid_vcpu_def)
1034  apply (fastforce simp: obj_at_def dest!: valid_pspace_vo)
1035  done
1036
1037crunches invoke_vcpu_inject_irq, vcpu_read_reg
1038  for invs[wp]: invs (ignore: do_machine_op)
1039
1040lemma perform_vcpu_invs[wp]:
1041  "\<lbrace>invs and valid_vcpu_invocation vi\<rbrace> perform_vcpu_invocation vi \<lbrace>\<lambda>_. invs\<rbrace>"
1042  apply (simp add: perform_vcpu_invocation_def valid_vcpu_invocation_def)
1043  apply (wpsimp simp: invoke_vcpu_read_register_def read_vcpu_register_def
1044                      invoke_vcpu_write_register_def)
1045  done
1046
1047lemma invoke_arch_invs[wp]:
1048  "\<lbrace>invs and ct_active and valid_arch_inv ai\<rbrace>
1049   arch_perform_invocation ai
1050   \<lbrace>\<lambda>rv. invs\<rbrace>"
1051  apply (cases ai, simp_all add: valid_arch_inv_def arch_perform_invocation_def)
1052  apply (wp perform_vcpu_invs |simp)+
1053  done
1054
1055
1056lemma sts_empty_pde [wp]:
1057  "\<lbrace>empty_pde_at p\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. empty_pde_at p\<rbrace>"
1058  apply (simp add: empty_pde_at_def)
1059  apply (rule hoare_pre)
1060   apply (wp hoare_vcg_ex_lift set_thread_state_ko)
1061  apply (clarsimp simp: is_tcb_def)
1062  done
1063
1064
1065lemma sts_pd_at_asid [wp]:
1066  "\<lbrace>vspace_at_asid asid pd\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. vspace_at_asid asid pd\<rbrace>"
1067  apply (simp add: vspace_at_asid_def)
1068  apply wp
1069  done
1070
1071
1072lemma sts_same_refs_inv[wp]:
1073  "\<lbrace>\<lambda>s. same_refs m cap s\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv s. same_refs m cap s\<rbrace>"
1074  by (cases m, (clarsimp simp: same_refs_def, wp)+)
1075
1076
1077lemma sts_valid_slots_inv[wp]:
1078  "\<lbrace>valid_slots m\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_slots m\<rbrace>"
1079  by (cases m, (clarsimp simp: valid_slots_def, wp hoare_vcg_ball_lift sts.vs_lookup sts_typ_ats)+)
1080
1081
1082lemma sts_valid_page_inv[wp]:
1083"\<lbrace>valid_page_inv page_invocation\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_page_inv page_invocation\<rbrace>"
1084  by (cases page_invocation,
1085       (wp hoare_vcg_const_Ball_lift hoare_vcg_ex_lift hoare_vcg_imp_lift sts_typ_ats
1086        | clarsimp simp: valid_page_inv_def same_refs_def
1087        | wps)+)
1088
1089
1090lemma sts_valid_pdi_inv[wp]:
1091  "\<lbrace>valid_pdi page_directory_invocation\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_pdi page_directory_invocation\<rbrace>"
1092  apply (cases page_directory_invocation)
1093   apply (wp | simp add: valid_pdi_def)+
1094  done
1095
1096
1097lemma sts_valid_vcpu_invocation_inv:
1098  "\<lbrace>valid_vcpu_invocation vcpu_invocation\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_vcpu_invocation vcpu_invocation\<rbrace>"
1099  unfolding valid_vcpu_invocation_def by (cases vcpu_invocation; wpsimp)
1100
1101lemma sts_valid_arch_inv:
1102  "\<lbrace>valid_arch_inv ai\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_arch_inv ai\<rbrace>"
1103  apply (cases ai, simp_all add: valid_arch_inv_def)
1104     apply (rename_tac page_table_invocation)
1105     apply (case_tac page_table_invocation, simp_all add: valid_pti_def)[1]
1106      apply ((wp valid_pde_lift set_thread_state_valid_cap
1107                 hoare_vcg_all_lift hoare_vcg_const_imp_lift
1108                 hoare_vcg_ex_lift set_thread_state_ko
1109                 sts_typ_ats set_thread_state_cte_wp_at
1110               | clarsimp simp: is_tcb_def)+)[4]
1111   apply (rename_tac asid_control_invocation)
1112   apply (case_tac asid_control_invocation)
1113   apply (clarsimp simp: valid_aci_def cte_wp_at_caps_of_state)
1114   apply (rule hoare_pre, wp hoare_vcg_ex_lift cap_table_at_typ_at)
1115   apply clarsimp
1116  apply (clarsimp simp: valid_apinv_def split: asid_pool_invocation.splits)
1117  apply (rule hoare_pre)
1118   apply (wp hoare_vcg_ex_lift set_thread_state_ko)
1119  apply (clarsimp simp: is_tcb_def, wp sts_valid_vcpu_invocation_inv)
1120  done
1121
1122crunch inv[wp]: ensure_safe_mapping, create_mapping_entries "P"
1123  (wp: crunch_wps mapME_x_inv_wp)
1124
1125crunch_ignore (add: select_ext)
1126
1127crunch inv [wp]: arch_decode_invocation "P"
1128  (wp: crunch_wps select_wp select_ext_weak_wp simp: crunch_simps)
1129
1130
1131lemma create_mappings_empty [wp]:
1132  "\<lbrace>\<top>\<rbrace> create_mapping_entries base vptr vmsz R A pd \<lbrace>\<lambda>m s. empty_refs m\<rbrace>, -"
1133  apply (cases vmsz, simp_all add: empty_refs_def)
1134    apply (wpsimp simp: pde_ref_def)+
1135  done
1136
1137
1138lemma empty_pde_atI:
1139  "\<lbrakk> ko_at (ArchObj (PageDirectory pd)) (p && ~~ mask pd_bits) s;
1140     pd (ucast (p && mask pd_bits >> 3)) = InvalidPDE \<rbrakk> \<Longrightarrow>
1141   empty_pde_at p s"
1142  by (fastforce simp add: vspace_bits_defs empty_pde_at_def)
1143
1144
1145declare lookup_slot_for_cnode_op_cap_to [wp]
1146
1147
1148lemma shiftr_irrelevant:
1149  "x < 2 ^ asid_low_bits \<Longrightarrow> is_aligned (y :: word32) asid_low_bits \<Longrightarrow>
1150    x + y >> asid_low_bits = y >> asid_low_bits"
1151  apply (subst word_plus_and_or_coroll)
1152   apply (rule word_eqI)
1153   apply (clarsimp simp: is_aligned_nth)
1154   apply (drule(1) nth_bounded)
1155    apply (simp add: asid_low_bits_def word_bits_def)
1156   apply simp
1157  apply (rule word_eqI)
1158  apply (simp add: nth_shiftr)
1159  apply safe
1160  apply (drule(1) nth_bounded)
1161   apply (simp add: asid_low_bits_def word_bits_def)
1162  apply simp
1163  done
1164
1165lemma map_up_enum_0x78:
1166  "is_aligned (r::32 word) 7 \<Longrightarrow> map (\<lambda>x. x + r) [0 , 8 .e. 0x78] = [r, r + 8 .e. r + 0x78]"
1167  apply (simp add: upto_enum_step_def upto_enum_def not_less)
1168  apply (drule is_aligned_no_overflow')
1169  apply simp
1170  apply (erule word_plus_mono_right2)
1171  apply simp
1172  done
1173
1174lemma create_mapping_entries_parent_for_refs:
1175  "\<lbrace>invs and \<exists>\<rhd> pd and page_directory_at pd
1176           and K (is_aligned pd pd_bits) and K (vmsz_aligned vptr pgsz)
1177           and K (vptr < kernel_base)\<rbrace>
1178    create_mapping_entries ptr vptr pgsz
1179                 rights attribs pd
1180   \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, -"
1181  apply (rule hoare_gen_asmE)+
1182  apply (cases pgsz,
1183         simp_all add: vmsz_aligned_def largePagePTE_offsets_def superSectionPDE_offsets_def
1184                       pte_bits_def pde_bits_def)
1185     apply (rule hoare_pre)
1186      apply wp
1187      apply (rule hoare_post_imp_R, rule lookup_pt_slot_cap_to)
1188      apply (elim exEI)
1189      apply (clarsimp simp: cte_wp_at_caps_of_state parent_for_refs_def)
1190     apply simp
1191    apply (rule hoare_pre)
1192     apply wp
1193     apply (rule hoare_post_imp_R)
1194      apply (rule lookup_pt_slot_cap_to_multiple1)
1195     apply (elim conjE exEI cte_wp_at_weakenE)
1196     apply (clarsimp simp: cte_wp_at_caps_of_state parent_for_refs_def
1197                           subset_iff p_0x3C_shift map_up_enum_0x78)
1198    apply simp
1199   apply (rule hoare_pre, wp)
1200   apply (clarsimp dest!:vs_lookup_pages_vs_lookupI)
1201   apply (drule valid_vs_lookupD, clarsimp)
1202   apply (simp, elim exEI)
1203   apply (clarsimp simp: cte_wp_at_caps_of_state parent_for_refs_def
1204                         lookup_pd_slot_def Let_def)
1205   apply (subst pd_shifting, simp add: pd_bits_def pageBits_def pde_bits_def)
1206   apply (clarsimp simp: vs_cap_ref_def
1207                  split: cap.split_asm arch_cap.split_asm option.split_asm)
1208     apply (auto simp: valid_cap_def obj_at_def is_cap_simps cap_asid_def
1209                dest!: caps_of_state_valid_cap split:if_splits)[3]
1210     apply (frule(1) caps_of_state_valid)
1211     apply (clarsimp simp:valid_cap_def obj_at_def)
1212   apply (simp add:is_cap_simps)
1213  apply (rule hoare_pre, wp)
1214  apply (clarsimp dest!:vs_lookup_pages_vs_lookupI)
1215  apply (drule valid_vs_lookupD, clarsimp)
1216  apply (simp, elim exEI)
1217  apply (clarsimp simp: cte_wp_at_caps_of_state parent_for_refs_def)
1218  apply (rule conjI)
1219   apply (simp add: subset_eq)
1220   apply (clarsimp simp: lookup_pd_slot_add_eq)
1221  apply (clarsimp simp: vs_cap_ref_def
1222                 split: cap.split_asm arch_cap.split_asm option.split_asm)
1223       apply (auto simp: valid_cap_def obj_at_def is_cap_simps cap_asid_def
1224             dest!: caps_of_state_valid_cap split:if_splits)[3]
1225   apply (frule(1) caps_of_state_valid)
1226   apply (clarsimp simp:valid_cap_def obj_at_def)
1227  apply (simp add:is_cap_simps)
1228  done
1229
1230
1231lemma find_pd_for_asid_shifting_voodoo:
1232  "\<lbrace>pspace_aligned and valid_vspace_objs\<rbrace>
1233     find_pd_for_asid asid
1234   \<lbrace>\<lambda>rv s. v >> 21 = rv + (v >> 21 << 3) && mask pd_bits >> 3\<rbrace>,-"
1235  apply (rule hoare_post_imp_R,
1236         rule find_pd_for_asid_aligned_pd, simp add: vspace_bits_defs)
1237  apply (subst pd_shifting_dual[simplified vspace_bits_defs, simplified], simp)
1238  apply (rule word_eqI)
1239  apply (simp add: nth_shiftr nth_shiftl word_size)
1240  apply safe
1241  apply (drule test_bit_size)
1242  apply (simp add: word_size)
1243  done
1244
1245
1246lemma find_pd_for_asid_ref_offset_voodoo:
1247  "\<lbrace>pspace_aligned and valid_vspace_objs and
1248         K (ref = [VSRef (asid && mask asid_low_bits) (Some AASIDPool),
1249                  VSRef (ucast (asid_high_bits_of asid)) None])\<rbrace>
1250      find_pd_for_asid asid
1251   \<lbrace>\<lambda>rv. (ref \<rhd> (rv + (v >> 21 << 3) && ~~ mask pd_bits))\<rbrace>,-"
1252  apply (rule hoare_gen_asmE)
1253  apply (rule_tac Q'="\<lambda>rv s. is_aligned rv 14 \<and> (ref \<rhd> rv) s"
1254               in hoare_post_imp_R)
1255   apply (simp add: ucast_ucast_mask
1256                    mask_asid_low_bits_ucast_ucast)
1257   apply (fold asid_low_bits_def)
1258   apply (rule hoare_pre, wp find_pd_for_asid_lookup_ref)
1259   apply (simp add: vspace_bits_defs)
1260  apply (simp add: pd_shifting[simplified vspace_bits_defs, simplified] vspace_bits_defs)
1261  done
1262
1263
1264declare asid_high_bits_of_shift [simp]
1265declare mask_shift [simp]
1266declare word_less_sub_le [simp del]
1267declare ptrFormPAddr_addFromPPtr [simp]
1268
1269
1270(* FIXME: move *)
1271lemma valid_mask_vm_rights[simp]:
1272  "mask_vm_rights V R \<in> valid_vm_rights"
1273  by (simp add: mask_vm_rights_def)
1274
1275
1276lemma vs_lookup_and_unique_refs:
1277  "\<lbrakk>(ref \<rhd> p) s; caps_of_state s cptr = Some cap; table_cap_ref cap = Some ref';
1278    p \<in> obj_refs cap; valid_vs_lookup s; unique_table_refs (caps_of_state s)\<rbrakk>
1279   \<Longrightarrow> ref = ref'"
1280  apply (frule_tac ref=ref in valid_vs_lookupD[OF vs_lookup_pages_vs_lookupI], assumption)
1281  apply clarsimp
1282  apply (frule_tac cap'=capa in unique_table_refsD)
1283     apply simp+
1284   apply (case_tac capa, simp_all)
1285        apply ((case_tac cap, simp_all)+)[6]
1286     apply (clarsimp simp add: table_cap_ref_def vs_cap_ref_def split: cap.splits arch_cap.splits option.splits)
1287  done
1288
1289
1290lemma create_mapping_entries_same_refs:
1291  "\<lbrace>valid_arch_state and valid_vspace_objs and valid_vs_lookup and (\<lambda>s. unique_table_refs (caps_of_state s))
1292    and pspace_aligned and valid_objs and valid_kernel_mappings and \<exists>\<rhd> pd and
1293    (\<lambda>s. \<exists>dev pd_cap pd_cptr. cte_wp_at (diminished pd_cap) pd_cptr s
1294          \<and> pd_cap = ArchObjectCap (PageDirectoryCap pd (Some asid))) and
1295    page_directory_at pd and K (vaddr < kernel_base \<and> (cap = (ArchObjectCap (PageCap dev p rights' pgsz (Some (asid, vaddr))))))\<rbrace>
1296   create_mapping_entries (addrFromPPtr p) vaddr pgsz rights attribs pd
1297   \<lbrace>\<lambda>rv s. same_refs rv cap s\<rbrace>,-"
1298  apply (rule hoare_gen_asmE)
1299  apply (cases pgsz, simp_all add: lookup_pt_slot_def)
1300     apply (wp get_pde_wp | wpc)+
1301     apply (clarsimp simp: lookup_pd_slot_def)
1302     apply (frule (1) pd_aligned)
1303     apply (simp add: pd_shifting)
1304     apply (simp add: vaddr_segment_nonsense2 pageBits_def pt_bits_def pte_bits_def pde_bits_def)
1305     apply (frule (2) valid_vspace_objsD[rotated], simp)
1306     apply (erule_tac x="ucast (vaddr >> 21)" in allE)
1307     apply (simp, drule (1) pt_aligned)
1308     apply (clarsimp simp: same_refs_def vs_cap_ref_def split: option.splits)
1309     apply (simp add: vaddr_segment_nonsense4 shiftl_shiftr_id mask_def[of 9]
1310                      less_trans[OF and_mask_less'[where n=9, unfolded mask_def, simplified]]
1311                      word_bits_def pageBits_def
1312                      vaddr_segment_nonsense3)
1313     apply (rule conjI, simp add: mask_def pt_bits_def pte_bits_def)
1314     apply (clarsimp simp: cte_wp_at_caps_of_state diminished_def
1315                           mask_cap_def cap_rights_update_def)
1316     apply (clarsimp split: Structures_A.cap.splits)
1317     apply (clarsimp simp: acap_rights_update_def split: arch_cap.splits)
1318     apply (frule (1) vs_lookup_and_unique_refs)
1319         apply (simp_all add: table_cap_ref_def obj_refs_def)[4]
1320     apply (frule_tac p=pd and p'="ptrFromPAddr x" in vs_lookup_step)
1321      apply (clarsimp simp: vs_lookup1_def)
1322      apply (rule exI, erule conjI)
1323      apply (rule exI[where x="VSRef (vaddr >> 21) (Some APageDirectory)"])
1324      apply (rule conjI, rule refl)
1325      apply (simp add: vs_refs_def)
1326      apply (rule_tac x="(ucast (vaddr >> 21), ptrFromPAddr x)" in image_eqI)
1327       apply (simp add: ucast_ucast_len[OF shiftr_less_t2n'] mask_32_max_word graph_of_def)
1328      apply (clarsimp simp:graph_of_def)
1329      apply (simp add: pde_ref_def)
1330     apply simp
1331     apply (drule (1) ref_is_unique)
1332           apply (simp add: ptrFromPAddr_def)
1333          apply (simp_all add: pde_ref_def valid_arch_state_def valid_objs_caps pt_bits_def)[8]
1334    apply (wp get_pde_wp | wpc)+
1335    apply (clarsimp simp: lookup_pd_slot_def)
1336    apply (frule (1) pd_aligned)
1337    apply (simp add: pd_shifting)
1338    apply (simp add: vaddr_segment_nonsense2 pageBits_def pt_bits_def pte_bits_def pde_bits_def)
1339    apply (frule (2) valid_vspace_objsD[rotated], simp)
1340    apply (erule_tac x="ucast (vaddr >> 21)" in allE)
1341    apply (simp, drule (1) pt_aligned)
1342    apply (simp add: largePagePTE_offsets_def pte_bits_def)
1343    apply (clarsimp simp: same_refs_def vs_cap_ref_def upto_enum_step_def upto_enum_word upt_conv_Cons)
1344    apply (simp add: vaddr_segment_nonsense4 shiftl_shiftr_id
1345                     less_trans[OF and_mask_less'[where n=9, unfolded mask_def, simplified]]
1346                     word_bits_def pageBits_def  mask_def [of 9]
1347                     vaddr_segment_nonsense3)
1348    apply (simp add: pt_bits_def pte_bits_def)
1349    apply (rule conjI, simp add: mask_def)
1350    apply (clarsimp simp: cte_wp_at_caps_of_state diminished_def
1351                          mask_cap_def cap_rights_update_def)
1352    apply (clarsimp split: Structures_A.cap.splits )
1353    apply (clarsimp simp: acap_rights_update_def split: arch_cap.splits)
1354    apply (frule (1) vs_lookup_and_unique_refs)
1355        apply (simp_all add: table_cap_ref_def obj_refs_def)[4]
1356    apply (frule_tac p=pd and p'="ptrFromPAddr x" in vs_lookup_step)
1357     apply (clarsimp simp: vs_lookup1_def)
1358     apply (rule exI, erule conjI)
1359     apply (rule exI[where x="VSRef (vaddr >> 21) (Some APageDirectory)"])
1360     apply (rule conjI, rule refl)
1361     apply (simp add: vs_refs_def)
1362     apply (rule_tac x="(ucast (vaddr >> 21), ptrFromPAddr x)" in image_eqI)
1363      apply (simp add: ucast_ucast_len[OF shiftr_less_t2n'] mask_32_max_word graph_of_def)
1364     apply (clarsimp simp:graph_of_def)
1365     apply (simp add: pde_ref_def)
1366    apply simp
1367    apply (drule (1) ref_is_unique)
1368          apply (simp add: ptrFromPAddr_def)
1369         apply (simp_all add: pde_ref_def valid_arch_state_def valid_objs_caps)[8]
1370   apply (wp get_pde_wp returnOKE_R_wp | wpc)+
1371   apply (clarsimp simp: lookup_pd_slot_def)
1372   apply (frule (1) pd_aligned)
1373   apply (clarsimp simp: same_refs_def vs_cap_ref_def pde_ref_pages_def)
1374   apply (simp add: vaddr_segment_nonsense vaddr_segment_nonsense2
1375                    pageBits_def pt_bits_def pte_bits_def pde_bits_def)
1376   apply (clarsimp simp: cte_wp_at_caps_of_state diminished_def
1377                         mask_cap_def cap_rights_update_def)
1378   apply (clarsimp split: Structures_A.cap.splits )
1379   apply (clarsimp simp: acap_rights_update_def split: arch_cap.splits)
1380   apply (frule (1) vs_lookup_and_unique_refs)
1381       apply (simp_all add: table_cap_ref_def obj_refs_def)[4]
1382   apply (drule (1) ref_is_unique)
1383        apply (simp_all add: valid_arch_state_def valid_objs_caps)[7]
1384  apply (wp returnOKE_R_wp | wpc)+
1385  apply (clarsimp simp: lookup_pd_slot_def)
1386  apply (frule (1) pd_aligned)
1387  apply (simp add: superSectionPDE_offsets_def pde_bits_def pageBits_def pt_bits_def)
1388  apply (clarsimp simp: same_refs_def vs_cap_ref_def pde_ref_pages_def upto_enum_step_def upto_enum_word upt_conv_Cons)
1389  apply (simp add: vaddr_segment_nonsense vaddr_segment_nonsense2 pageBits_def pt_bits_def)
1390  apply (clarsimp simp: cte_wp_at_caps_of_state diminished_def
1391                        mask_cap_def cap_rights_update_def)
1392  apply (clarsimp split: Structures_A.cap.splits )
1393  apply (clarsimp simp: acap_rights_update_def split: arch_cap.splits)
1394  apply (frule (1) vs_lookup_and_unique_refs)
1395      apply (simp_all add: table_cap_ref_def obj_refs_def)[4]
1396  apply (drule (1) ref_is_unique)
1397        apply (clarsimp simp: obj_at_def a_type_def valid_arch_state_def)
1398       apply (simp_all add: valid_arch_state_def valid_objs_caps)
1399  done
1400
1401
1402lemma create_mapping_entries_same_refs_ex:
1403  "\<lbrace>valid_arch_state and valid_vspace_objs and valid_vs_lookup and (\<lambda>s. unique_table_refs (caps_of_state s))
1404    and pspace_aligned and valid_objs and valid_kernel_mappings and \<exists>\<rhd> pd and
1405    (\<lambda>s. \<exists>dev pd_cap pd_cptr asid rights'. cte_wp_at (diminished pd_cap) pd_cptr s
1406          \<and> pd_cap = cap.ArchObjectCap (arch_cap.PageDirectoryCap pd (Some asid))
1407          \<and> page_directory_at pd s \<and> vaddr < kernel_base \<and> (cap = (cap.ArchObjectCap (arch_cap.PageCap dev p rights' pgsz (Some (asid, vaddr))))))\<rbrace>
1408   create_mapping_entries (Platform.ARM_HYP.addrFromPPtr p) vaddr pgsz rights attribs pd
1409   \<lbrace>\<lambda>rv s. same_refs rv cap s\<rbrace>,-"
1410  apply (clarsimp simp: validE_R_def validE_def valid_def split: sum.split)
1411  apply (erule use_validE_R[OF _ create_mapping_entries_same_refs])
1412  apply fastforce
1413  done
1414
1415
1416lemma diminished_pd_capD:
1417  "diminished (ArchObjectCap (PageDirectoryCap a b)) cap
1418   \<Longrightarrow> cap = (ArchObjectCap (PageDirectoryCap a b))"
1419  apply (clarsimp simp: diminished_def mask_cap_def cap_rights_update_def)
1420  apply (clarsimp simp: acap_rights_update_def split: cap.splits arch_cap.splits)
1421  done
1422
1423
1424lemma diminished_pd_self:
1425  "diminished (ArchObjectCap (PageDirectoryCap a b)) (ArchObjectCap (PageDirectoryCap a b))"
1426  apply (clarsimp simp: diminished_def mask_cap_def cap_rights_update_def)
1427  apply (clarsimp simp: acap_rights_update_def split: cap.splits arch_cap.splits)
1428  done
1429
1430
1431lemma cte_wp_at_page_cap_weaken:
1432  "cte_wp_at (diminished (ArchObjectCap (PageCap dev word seta vmpage_size None))) slot s \<Longrightarrow>
1433   cte_wp_at (\<lambda>a. \<exists>dev p R sz m. a = ArchObjectCap (PageCap dev p R sz m)) slot s"
1434  apply (clarsimp simp: cte_wp_at_def diminished_def mask_cap_def cap_rights_update_def)
1435  apply (clarsimp simp: acap_rights_update_def split: cap.splits arch_cap.splits)
1436  done
1437
1438
1439lemma find_pd_for_asid_lookup_pd_wp:
1440  "\<lbrace> \<lambda>s. valid_vspace_objs s \<and> (\<forall>pd. vspace_at_asid asid pd s \<and> page_directory_at pd s
1441    \<and> (\<exists>\<rhd> pd) s \<longrightarrow> Q pd s) \<rbrace> find_pd_for_asid asid \<lbrace> Q \<rbrace>, -"
1442  apply (rule hoare_post_imp_R)
1443   apply (rule hoare_vcg_conj_lift_R[OF find_pd_for_asid_page_directory])
1444   apply (rule hoare_vcg_conj_lift_R[OF find_pd_for_asid_lookup, simplified])
1445   apply (rule hoare_vcg_conj_lift_R[OF find_pd_for_asid_pd_at_asid, simplified])
1446   apply (wp_once find_pd_for_asid_inv)
1447  apply auto
1448  done
1449
1450
1451lemma aligned_sum_less_kernel_base:
1452  "vmsz_aligned p sz
1453    \<Longrightarrow> (p + 2 ^ pageBitsForSize sz - 1 < kernel_base) = (p < kernel_base)"
1454  apply (rule iffI)
1455   apply (rule le_less_trans)
1456    apply (rule is_aligned_no_overflow)
1457    apply (simp add: vmsz_aligned_def)
1458   apply simp
1459  apply (simp add:field_simps[symmetric])
1460  apply (erule gap_between_aligned)
1461    apply (simp add: vmsz_aligned_def)+
1462   apply (case_tac sz,simp_all add:kernel_base_def is_aligned_def)+
1463  done
1464
1465lemma diminished_VCPUCap[simp]:
1466  "diminished (ArchObjectCap (VCPUCap vcpu_ptr)) c = (c = ArchObjectCap (VCPUCap vcpu_ptr))"
1467  apply (cases c; simp add: diminished_def mask_cap_def cap_rights_update_def)
1468  apply (rename_tac acap)
1469  apply (case_tac acap; simp add: acap_rights_update_def)
1470  apply auto
1471  done
1472
1473lemma diminshed_ThreadCap[simp]:
1474  "diminished (ThreadCap t) c = (c = ThreadCap t)"
1475  by (cases c) (auto simp: diminished_def mask_cap_def cap_rights_update_def)
1476
1477lemma find_pd_for_asid_pde_unfolded[wp]:
1478  "\<lbrace>valid_vspace_objs and pspace_aligned\<rbrace>
1479  find_pd_for_asid asid
1480  \<lbrace>\<lambda>pd. pde_at (pd + (vptr >> 21 << 3))\<rbrace>, -"
1481  apply (rule hoare_post_imp_R, rule find_pd_for_asid_pde)
1482  apply (simp add: pageBits_def pt_bits_def pde_bits_def)
1483  done
1484
1485lemma arch_decode_inv_wf[wp]:
1486  "\<lbrace>invs and valid_cap (ArchObjectCap arch_cap) and
1487    cte_wp_at (diminished (ArchObjectCap arch_cap)) slot and
1488    (\<lambda>s. \<forall>x \<in> set excaps. cte_wp_at (diminished (fst x)) (snd x) s)\<rbrace>
1489     arch_decode_invocation label args cap_index slot arch_cap excaps
1490   \<lbrace>valid_arch_inv\<rbrace>,-"
1491  apply (cases arch_cap)
1492       apply (rename_tac word1 word2)
1493       apply (simp add: arch_decode_invocation_def Let_def decode_mmu_invocation_def split_def cong: if_cong split del: if_split)
1494       apply (rule hoare_pre)
1495        apply ((wp whenE_throwError_wp check_vp_wpR ensure_empty_stronger select_wp select_ext_weak_wp|
1496                wpc|
1497                simp add: valid_arch_inv_def valid_apinv_def)+)[1]
1498       apply (simp add: if_apply_def2 valid_apinv_def)
1499       apply (intro allI impI ballI)
1500       apply (elim conjE exE)
1501       apply simp
1502       apply (clarsimp simp: dom_def neq_Nil_conv)
1503       apply (thin_tac "Ball S P" for S P)+
1504       apply (clarsimp simp: valid_cap_def)
1505       apply (rule conjI)
1506        apply (clarsimp simp: obj_at_def)
1507        apply (subgoal_tac "ucast (ucast xa + word2) = xa")
1508         apply simp
1509        apply (simp add: is_aligned_nth)
1510        apply (subst word_plus_and_or_coroll)
1511         apply (rule word_eqI)
1512         apply (clarsimp simp: word_size word_bits_def nth_ucast)
1513         apply (drule test_bit_size)
1514         apply (simp add: word_size asid_low_bits_def)
1515        apply (rule word_eqI)
1516        apply (clarsimp simp: word_size word_bits_def nth_ucast)
1517        apply (auto simp: asid_low_bits_def)[1]
1518       apply (rule conjI)
1519        apply (clarsimp simp add: cte_wp_at_caps_of_state)
1520        apply (rename_tac c c')
1521        apply (frule_tac cap=c' in caps_of_state_valid, assumption)
1522        apply (drule (1) diminished_is_update)
1523        apply (clarsimp simp: is_pd_cap_def cap_rights_update_def acap_rights_update_def)
1524       apply (clarsimp simp: word_neq_0_conv)
1525       apply (rule conjI)
1526        apply (subst field_simps, erule is_aligned_add_less_t2n)
1527          apply (simp add: asid_low_bits_def)
1528          apply (rule ucast_less[where 'b=10, simplified], simp)
1529         apply (simp add: asid_low_bits_def asid_bits_def)
1530        apply (simp add: asid_bits_def)
1531       apply (drule vs_lookup_atI)
1532       apply (subst asid_high_bits_of_add_ucast, assumption)
1533       apply assumption
1534      apply (simp add: arch_decode_invocation_def Let_def split_def decode_mmu_invocation_def
1535                 cong: if_cong split del: if_split)
1536      apply (rule hoare_pre)
1537       apply ((wp whenE_throwError_wp check_vp_wpR ensure_empty_stronger|
1538               wpc|
1539               simp add: valid_arch_inv_def valid_aci_def is_aligned_shiftl_self)+)[1]
1540              apply (rule_tac Q'=
1541                         "\<lambda>rv. real_cte_at rv and
1542                               ex_cte_cap_wp_to is_cnode_cap rv and
1543                               (\<lambda>s. descendants_of (snd (excaps!0)) (cdt s) = {}) and
1544                               cte_wp_at (\<lambda>c. \<exists>idx. c = (cap.UntypedCap False frame pageBits idx)) (snd (excaps!0)) and
1545                               (\<lambda>s. arm_asid_table (arch_state s) free = None)"
1546                         in hoare_post_imp_R)
1547               apply (simp add: lookup_target_slot_def)
1548               apply wp
1549              apply (clarsimp simp: cte_wp_at_def)
1550              apply (rule conjI, clarsimp)
1551              apply (rule shiftl_less_t2n)
1552               apply (rule order_less_le_trans, rule ucast_less, simp)
1553               apply (simp add: asid_bits_def asid_low_bits_def)
1554              apply (simp add: asid_bits_def)
1555             apply (simp split del: if_split)
1556             apply (wp ensure_no_children_sp select_ext_weak_wp select_wp whenE_throwError_wp|wpc | simp)+
1557      apply clarsimp
1558      apply (rule conjI, fastforce)
1559      apply (cases excaps, simp)
1560      apply (case_tac list, simp)
1561      apply clarsimp
1562      apply (rule conjI)
1563       apply (drule cte_wp_at_norm, clarsimp, drule cte_wp_valid_cap, fastforce)+
1564       apply (clarsimp simp add: diminished_def)
1565      apply (rule conjI)
1566       apply clarsimp
1567       apply (simp add: ex_cte_cap_wp_to_def)
1568       apply (rule_tac x=ac in exI)
1569       apply (rule_tac x=ba in exI)
1570       apply (clarsimp simp add: cte_wp_at_caps_of_state)
1571       apply (drule (1) caps_of_state_valid[rotated])+
1572       apply (drule (1) diminished_is_update)+
1573
1574       apply (clarsimp simp: is_cap_simps cap_rights_update_def)
1575      apply (clarsimp simp add: cte_wp_at_caps_of_state)
1576      apply (drule (1) caps_of_state_valid[rotated])+
1577      apply (drule (1) diminished_is_update)+
1578      apply (clarsimp simp: cap_rights_update_def)
1579     apply (clarsimp simp:diminished_def)
1580     apply (simp add: arch_decode_invocation_def Let_def split_def decode_mmu_invocation_def
1581                cong: if_cong split del: if_split)
1582     apply (cases "invocation_type label = ArchInvocationLabel ARMPageMap")
1583      apply (rename_tac word rights vmpage_size option)
1584      apply (simp split del: if_split)
1585      apply (rule hoare_pre)
1586       apply ((wp whenE_throwError_wp check_vp_wpR hoare_vcg_const_imp_lift_R
1587                  create_mapping_entries_parent_for_refs find_pd_for_asid_pd_at_asid
1588                  create_mapping_entries_valid_slots create_mapping_entries_same_refs_ex
1589                  find_pd_for_asid_lookup_pd_wp
1590              | wpc
1591              | simp add: valid_arch_inv_def valid_page_inv_def is_pg_cap_def)+)
1592      apply (clarsimp simp: neq_Nil_conv)
1593      apply (frule diminished_cte_wp_at_valid_cap[where p="(a, b)" for a b], clarsimp)
1594      apply (frule diminished_cte_wp_at_valid_cap[where p=slot], clarsimp)
1595      apply (clarsimp simp: cte_wp_at_caps_of_state mask_cap_def conj_ac
1596                            diminished_def[where cap="ArchObjectCap (PageCap x y z v w)" for x y z v w]
1597                            linorder_not_le aligned_sum_less_kernel_base
1598                     dest!: diminished_pd_capD)
1599      apply (clarsimp simp: cap_rights_update_def acap_rights_update_def
1600                     split: cap.splits arch_cap.splits)
1601      apply (rule conjI, fastforce)
1602      apply (cases slot)
1603      apply (clarsimp simp: valid_cap_simps cap_aligned_def valid_kernel_mappings_def
1604                            aligned_sum_less_kernel_base asid_bits_def mask_def
1605                            is_arch_update_def cap_master_cap_simps is_arch_cap_def)
1606      apply (rule conjI, fastforce)
1607      apply (rule conjI, fastforce)
1608      apply (rule conjI, fastforce)
1609      apply (rule conjI, fastforce)
1610      apply (rule conjI, fastforce)
1611      apply (rule conjI, fastforce)
1612      apply (rule conjI, fastforce)
1613      apply (rule conjI, fastforce)
1614      apply (rule conjI)
1615       apply (fastforce elim!: is_aligned_weaken intro!: pbfs_atleast_pageBits is_aligned_addrFromPPtr)
1616      apply (rule conjI)
1617       apply (fastforce simp: data_at_def split: if_splits)
1618      apply (rule conjI, fastforce)
1619      apply (rule conjI)
1620       apply (clarsimp simp: vs_cap_ref_def split: vmpage_size.split)
1621      apply (rule conjI, fastforce)
1622      apply (fastforce intro: diminished_pd_self)
1623     apply (cases "invocation_type label = ArchInvocationLabel ARMPageRemap")
1624      apply (rename_tac word rights vmpage_size option)
1625      apply (simp split del: if_split)
1626      apply (rule hoare_pre)
1627       apply ((wp whenE_throwError_wp check_vp_wpR hoare_vcg_const_imp_lift_R
1628                  create_mapping_entries_parent_for_refs
1629                  find_pd_for_asid_lookup_pd_wp
1630              | wpc
1631              | simp add: valid_arch_inv_def valid_page_inv_def
1632              | (simp add: cte_wp_at_caps_of_state,
1633                 wp create_mapping_entries_same_refs_ex hoare_vcg_ex_lift_R))+)[1]
1634      apply (clarsimp simp: valid_cap_def cap_aligned_def neq_Nil_conv)
1635      apply (frule diminished_cte_wp_at_valid_cap[where p="(a, b)" for a b], clarsimp)
1636      apply (clarsimp simp: cte_wp_at_caps_of_state mask_cap_def
1637                            diminished_def[where cap="ArchObjectCap (PageCap x y z v w)" for x y z v w])
1638      apply (clarsimp simp: cap_rights_update_def acap_rights_update_def
1639                     split: cap.splits arch_cap.splits)
1640      apply (cases slot)
1641      apply (clarsimp simp: valid_cap_simps cap_aligned_def valid_kernel_mappings_def
1642                            aligned_sum_less_kernel_base asid_bits_def mask_def
1643                            is_arch_update_def cap_master_cap_simps is_arch_cap_def)
1644      apply (fastforce elim!: is_aligned_weaken
1645                       intro!: pbfs_atleast_pageBits is_aligned_addrFromPPtr diminished_pd_self
1646                       simp: data_at_def split: if_splits)
1647     apply (cases "invocation_type label = ArchInvocationLabel ARMPageUnmap")
1648      apply (simp split del: if_split)
1649      apply (rule hoare_pre, wp)
1650      apply (clarsimp simp: valid_arch_inv_def valid_page_inv_def)
1651      apply (thin_tac "Ball S P" for S P)
1652      apply (rule conjI)
1653       apply (clarsimp split: option.split)
1654       apply (clarsimp simp: valid_cap_def cap_aligned_def)
1655       apply (simp add: valid_unmap_def)
1656       apply (fastforce simp: vmsz_aligned_def elim: is_aligned_weaken intro!: pbfs_atleast_pageBits)
1657      apply (erule cte_wp_at_weakenE)
1658      apply (clarsimp simp: is_arch_diminished_def is_cap_simps)
1659     apply (cases "isPageFlushLabel (invocation_type label)")
1660      apply (simp split del: if_split)
1661      apply (rule hoare_pre)
1662       apply (wp whenE_throwError_wp static_imp_wp hoare_drop_imps)
1663         apply (simp add: valid_arch_inv_def valid_page_inv_def)
1664         apply (wp find_pd_for_asid_pd_at_asid | wpc)+
1665      apply (clarsimp simp: valid_cap_def mask_def)
1666     apply (simp split del: if_split)
1667     apply (cases "invocation_type label = ArchInvocationLabel ARMPageGetAddress")
1668      apply (simp split del: if_split)
1669      apply (rule hoare_pre, wp)
1670      apply (clarsimp simp: valid_arch_inv_def valid_page_inv_def)
1671     apply (rule hoare_pre, wp)
1672     apply (simp)
1673    apply (simp add: arch_decode_invocation_def Let_def split_def
1674                     is_final_cap_def decode_mmu_invocation_def
1675               cong: if_cong split del: if_split)
1676    apply (rename_tac word option)
1677    apply (rule hoare_pre)
1678     apply ((wp whenE_throwError_wp check_vp_wpR get_master_pde_wp hoare_vcg_all_lift_R|
1679             wpc|
1680             simp add: valid_arch_inv_def valid_pti_def unlessE_whenE vs_cap_ref_def|
1681             rule_tac x="fst p" in hoare_imp_eq_substR|
1682             wp_once hoare_vcg_ex_lift_R)+)[1]
1683
1684          apply (rule_tac Q'="\<lambda>a b. ko_at (ArchObj (PageDirectory pd))
1685                                    (a + (args ! 0 >> 21 << 3) && ~~ mask pd_bits) b \<longrightarrow>
1686                                    pd (ucast (a + (args ! 0 >> 21 << 3) && mask pd_bits >> 3)) =
1687                                    InvalidPDE \<longrightarrow> L word option p pd a b" for L in hoare_post_imp_R[rotated])
1688           apply (intro impI)
1689           apply (erule impE)
1690            apply (clarsimp simp: pageBits_def pde_bits_def pt_bits_def)
1691           apply (erule impE)
1692            apply (clarsimp simp: pageBits_def pde_bits_def pt_bits_def split:pde.splits)
1693           apply assumption
1694          apply ((wp whenE_throwError_wp hoare_vcg_all_lift_R
1695                     find_pd_for_asid_lookup_slot [unfolded lookup_pd_slot_def Let_def]
1696                     find_pd_for_asid_ref_offset_voodoo find_pd_for_asid_shifting_voodoo
1697                     find_pd_for_asid_inv
1698                  | wpc
1699                  | simp add: valid_arch_inv_def valid_pti_def unlessE_whenE empty_pde_atI
1700                              vs_cap_ref_def pageBits_def pt_bits_def pde_bits_def
1701                  | wp_once hoare_drop_imps hoare_vcg_ex_lift_R)+)[6]
1702    apply (clarsimp simp: is_cap_simps if_apply_def2)
1703    apply (rule conjI)
1704     apply clarsimp
1705     apply (rule conjI, fastforce)
1706     apply (rule conjI, fastforce)
1707     apply (clarsimp simp: neq_Nil_conv)
1708     apply (thin_tac "Ball S P" for S P)
1709     apply (rule conjI)
1710      apply (clarsimp simp: valid_cap_def cap_aligned_def)
1711     apply (rule conjI)
1712      apply (drule cte_wp_at_norm, clarsimp, drule cte_wp_valid_cap, fastforce)+
1713      apply (drule (1) diminished_is_update[rotated])+
1714      apply (clarsimp simp add: cap_rights_update_def acap_rights_update_def)
1715      apply (clarsimp simp: valid_cap_def cap_aligned_def
1716                            pt_bits_def pageBits_def
1717                            linorder_not_le
1718                            order_le_less_trans[OF word_and_le2])
1719     apply (rule conjI)
1720      apply (clarsimp simp add: cte_wp_at_caps_of_state)
1721      apply (drule (1) caps_of_state_valid[rotated])
1722      apply (drule (1) diminished_is_update)
1723      apply clarsimp
1724      apply (clarsimp simp: cap_master_cap_def is_arch_update_def)
1725      apply (clarsimp simp: cap_asid_def cap_rights_update_def acap_rights_update_def is_cap_simps
1726                     split: option.split)
1727     apply (rule conjI, fastforce)
1728     apply (rule conjI, fastforce)
1729     apply (clarsimp simp: pde_ref_def)
1730     apply (frule invs_pd_caps)
1731     apply (clarsimp simp: cte_wp_at_caps_of_state)
1732     apply (frule (1) caps_of_state_valid[rotated])
1733     apply (drule (1) diminished_is_update)
1734     apply (clarsimp simp: cap_rights_update_def acap_rights_update_def valid_cap_def)
1735     apply (drule (2) valid_table_caps_ptD)
1736     apply (rule conjI, fastforce)+
1737     apply (clarsimp simp: kernel_vsrefs_def)
1738     apply fastforce
1739    apply (clarsimp simp: cte_wp_at_def is_arch_diminished_def is_cap_simps
1740                          valid_arch_inv_def valid_pti_def)
1741   apply (simp add: arch_decode_invocation_def Let_def decode_mmu_invocation_def split del: if_split)
1742   apply (cases "isPDFlushLabel (invocation_type label)")
1743    apply (simp split del: if_split)
1744    apply (rule hoare_pre)
1745     apply (wp whenE_throwError_wp static_imp_wp hoare_drop_imp | wpc | simp)+
1746           apply (simp add: resolve_vaddr_def)
1747           apply (wp get_master_pte_wp get_master_pde_wp whenE_throwError_wp | wpc | simp)+
1748         apply (clarsimp simp: valid_arch_inv_def valid_pdi_def)+
1749         apply (rule_tac Q'="\<lambda>pd' s. vspace_at_asid x2 pd' s \<and> x2 \<le> mask asid_bits \<and> x2 \<noteq> 0" in hoare_post_imp_R)
1750          apply wp
1751         apply clarsimp
1752        apply (wp | wpc)+
1753    apply (clarsimp simp: valid_cap_def mask_def)
1754   apply (clarsimp, wp throwError_validE_R)
1755
1756  (* VCPU *)
1757  apply (rename_tac vcpu_ptr)
1758  apply (clarsimp simp: arch_decode_invocation_def decode_vcpu_invocation_def)
1759  apply (cases "invocation_type label"; (simp, wp?))
1760  apply (rename_tac arch_iv)
1761  apply (case_tac "arch_iv"; (simp, wp?))
1762     apply (simp add: decode_vcpu_set_tcb_def)
1763     apply (rule hoare_pre, wpsimp)
1764     apply (clarsimp simp: valid_arch_inv_def valid_vcpu_invocation_def)
1765     apply (rename_tac tcb_ptr)
1766     apply (frule_tac c="ThreadCap tcb_ptr" in diminished_cte_wp_at_valid_cap, fastforce)
1767     apply (simp add: valid_cap_def)
1768     apply (cases slot)
1769     apply (clarsimp simp: ex_nonz_cap_to_def)
1770     apply (rule conjI, fastforce elim: cte_wp_at_weakenE)
1771     apply (rule conjI, fastforce elim: cte_wp_at_weakenE)
1772     apply (clarsimp dest!: invs_valid_global_refs simp:  cte_wp_at_caps_of_state)
1773     apply (drule_tac ?cap="ThreadCap (idle_thread s)" in valid_global_refsD2, assumption)
1774     apply (simp add:global_refs_def cap_range_def)
1775    apply (simp add: decode_vcpu_inject_irq_def)
1776    apply (rule hoare_pre, wpsimp simp: whenE_def wp: get_vcpu_wp)
1777    apply (clarsimp simp: valid_arch_inv_def valid_vcpu_invocation_def obj_at_def)
1778   apply (simp add: decode_vcpu_read_register_def)
1779   apply (rule hoare_pre, wpsimp)
1780   apply (clarsimp simp: valid_arch_inv_def valid_cap_def valid_vcpu_invocation_def)
1781  apply (simp add: decode_vcpu_write_register_def)
1782  apply (rule hoare_pre, wpsimp)
1783  apply (clarsimp simp: valid_arch_inv_def valid_cap_def valid_vcpu_invocation_def)
1784  done
1785
1786
1787declare word_less_sub_le [simp]
1788
1789crunches associate_vcpu_tcb
1790  for pred_tcb_at[wp_unsafe]: "pred_tcb_at proj P t"
1791  (wp: crunch_wps simp: crunch_simps)
1792
1793crunches vcpu_read_reg, vcpu_write_reg, invoke_vcpu_inject_irq
1794  for pred_tcb_at[wp]: "pred_tcb_at proj P t"
1795
1796lemma perform_vcpu_invocation_pred_tcb_at[wp_unsafe]:
1797  "\<lbrace>pred_tcb_at proj P t and K (proj_not_field proj tcb_arch_update)\<rbrace>
1798     perform_vcpu_invocation iv
1799   \<lbrace>\<lambda>_. pred_tcb_at proj P t\<rbrace>"
1800  apply (simp add: perform_vcpu_invocation_def)
1801  apply (rule hoare_pre)
1802  apply (wp associate_vcpu_tcb_pred_tcb_at | wpc
1803        | clarsimp simp: invoke_vcpu_read_register_def
1804                         read_vcpu_register_def
1805                         invoke_vcpu_write_register_def
1806                         write_vcpu_register_def)+
1807  done
1808
1809crunch pred_tcb_at: perform_page_table_invocation, perform_page_invocation,
1810           perform_asid_pool_invocation,
1811           perform_page_directory_invocation "pred_tcb_at proj P t"
1812  (wp: crunch_wps simp: crunch_simps)
1813
1814
1815lemma arch_pinv_st_tcb_at:
1816  "\<lbrace>invs and valid_arch_inv ai and ct_active and
1817    st_tcb_at (P and (Not \<circ> inactive) and (Not \<circ> idle)) t\<rbrace>
1818     arch_perform_invocation ai
1819   \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace>"
1820  apply (cases ai, simp_all add: arch_perform_invocation_def valid_arch_inv_def)
1821      apply (wp perform_page_table_invocation_pred_tcb_at,
1822             fastforce elim!: pred_tcb_weakenE)
1823      apply (wp perform_page_directory_invocation_pred_tcb_at, fastforce elim: pred_tcb_weakenE)
1824     apply (wp perform_page_invocation_pred_tcb_at, fastforce elim!: pred_tcb_weakenE)
1825    apply (wp perform_asid_control_invocation_st_tcb_at,
1826           fastforce elim!: pred_tcb_weakenE)
1827   apply (wp perform_asid_pool_invocation_pred_tcb_at,
1828          fastforce elim!: pred_tcb_weakenE)
1829  apply (wp perform_vcpu_invocation_pred_tcb_at,
1830         fastforce elim!: pred_tcb_weakenE)
1831  done
1832
1833
1834lemma get_cap_diminished:
1835  "\<lbrace>valid_objs\<rbrace> get_cap slot \<lbrace>\<lambda>cap. cte_wp_at (diminished cap) slot\<rbrace>"
1836  apply (wp get_cap_wp)
1837  apply (intro allI impI)
1838  apply (simp add: cte_wp_at_caps_of_state diminished_def)
1839  apply (frule (1) caps_of_state_valid_cap)
1840  apply (clarsimp simp add: valid_cap_def2 wellformed_cap_def mask_cap_def
1841             cap_rights_update_def acap_rights_update_def
1842           split: cap.splits arch_cap.splits)
1843    apply fastforce+
1844  apply (clarsimp simp add: wellformed_acap_def
1845           split: cap.splits arch_cap.splits)
1846  apply (rename_tac rights vmpage_size option)
1847  apply (rule_tac x=rights in exI)
1848  apply auto
1849  done
1850
1851end
1852
1853
1854context begin interpretation Arch .
1855
1856requalify_consts
1857  valid_arch_inv
1858
1859requalify_facts
1860  invoke_arch_tcb
1861  invoke_arch_invs
1862  sts_valid_arch_inv
1863  arch_decode_inv_wf
1864  arch_pinv_st_tcb_at
1865  get_cap_diminished
1866
1867end
1868
1869declare invoke_arch_invs[wp]
1870declare arch_decode_inv_wf[wp]
1871
1872
1873end
1874