1(*
2 * Copyright 2014, NICTA
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(NICTA_GPL)
9 *)
10
11theory Ipc_IF
12imports Finalise_IF
13begin
14
15context begin interpretation Arch . (*FIXME: arch_split*)
16
17section "reads_respects"
18subsection "Notifications"
19
20lemma equiv_valid_2_get_assert:
21  "equiv_valid_2 I A A R P P' f f' \<Longrightarrow>
22   equiv_valid_2 I A A R P P' (get >>= (\<lambda> s. assert (g s) >>= (\<lambda> y. f))) (get >>= (\<lambda> s. assert (g' s) >>= (\<lambda> y. f')))"
23  apply(rule equiv_valid_2_guard_imp)
24   apply(rule_tac R'="\<top>\<top>" in equiv_valid_2_bind)
25       apply(rule_tac R'="\<top>\<top>" in equiv_valid_2_bind)
26          apply assumption
27         apply(simp add: assert_ev2)
28        apply(wp equiv_valid_rv_trivial | simp)+
29  done
30
31lemma dummy_machine_state_update:
32  "st = st\<lparr>machine_state := machine_state st\<rparr>"
33  apply simp
34  done
35
36lemma dmo_storeWord_modifies_at_most:
37  "modifies_at_most aag (pasObjectAbs aag ` ptr_range p 2) \<top>
38        (do_machine_op (storeWord p w))"
39  apply(rule modifies_at_mostI)
40  apply(simp add: do_machine_op_def storeWord_def)
41  apply(wp modify_wp | simp add: split_def)+
42  apply clarsimp
43  apply(erule use_valid)
44  apply(wp modify_wp)
45  apply(clarsimp simp: equiv_but_for_labels_def)
46  apply(subst (asm) is_aligned_mask[symmetric])
47  apply(subst dummy_machine_state_update)
48  apply(rule states_equiv_for_machine_state_update)
49   apply assumption
50  apply (erule states_equiv_forE_mem)
51  apply (intro conjI equiv_forI)
52   apply(fastforce simp: image_def dest: distinct_lemma[where f="pasObjectAbs aag"] intro: ptr_range_memI ptr_range_add_memI)+
53  done
54
55
56
57lemma get_object_reads_respects:
58  "reads_respects aag l (K (aag_can_read aag oref \<or> aag_can_affect aag l oref)) (get_object oref)"
59  unfolding get_object_def
60  apply(subst gets_apply)
61  apply(wp gets_apply_ev | wpc | simp)+
62  apply(blast intro: reads_affects_equiv_kheap_eq)
63  done
64
65lemma get_cap_reads_respects:
66  "reads_respects aag l (K (aag_can_read aag (fst slot) \<or> aag_can_affect aag l (fst slot))) (get_cap slot)"
67  apply(simp add: get_cap_def split_def)
68  apply(wp get_object_reads_respects | wpc | simp)+
69  done
70
71lemma lookup_ipc_buffer_reads_respects:
72  "reads_respects aag l (K (aag_can_read aag thread \<or> aag_can_affect aag l thread)) (lookup_ipc_buffer is_receiver thread)"
73  unfolding lookup_ipc_buffer_def
74  apply(wp thread_get_reads_respects get_cap_reads_respects | wpc | simp)+
75  done
76
77
78lemmas lookup_ipc_buffer_reads_respects_g = reads_respects_g_from_inv[OF lookup_ipc_buffer_reads_respects lookup_ipc_buffer_inv]
79
80lemma as_user_equiv_but_for_labels:
81  "\<lbrace>equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L)\<rbrace>
82    as_user thread f
83    \<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace>"
84  unfolding as_user_def
85  apply (wp set_object_equiv_but_for_labels | simp add: split_def)+
86  apply(blast dest: get_tcb_not_asid_pool_at)
87  done
88
89crunch equiv_but_for_labels: set_message_info "equiv_but_for_labels aag L st"
90
91
92lemma storeWord_equiv_but_for_labels:
93  "\<lbrace>\<lambda>ms. equiv_but_for_labels aag L st (s\<lparr>machine_state := ms\<rparr>) \<and>
94        for_each_byte_of_word (\<lambda> x. pasObjectAbs aag x \<in> L) p\<rbrace>
95    storeWord p v \<lbrace>\<lambda>a b. equiv_but_for_labels aag L st (s\<lparr>machine_state := b\<rparr>)\<rbrace>"
96  unfolding storeWord_def
97  apply (wp modify_wp)
98  apply (clarsimp simp: equiv_but_for_labels_def)
99  apply (rule states_equiv_forI)
100            apply(fastforce intro!: equiv_forI elim!: states_equiv_forE dest: equiv_forD[where f=kheap])
101           apply (simp add: states_equiv_for_def)
102          apply (rule conjI)
103           apply(rule equiv_forI)
104           apply clarsimp
105           apply(drule_tac f=underlying_memory in equiv_forD,fastforce)
106           apply(fastforce intro: is_aligned_no_wrap' word_plus_mono_right simp: is_aligned_mask for_each_byte_of_word_def)
107           apply(rule equiv_forI)
108          apply clarsimp
109          apply(drule_tac f=device_state in equiv_forD,fastforce)
110          apply clarsimp
111         apply(fastforce elim: states_equiv_forE intro: equiv_forI dest: equiv_forD[where f=cdt])
112        apply(fastforce elim: states_equiv_forE intro: equiv_forI dest: equiv_forD[where f=ekheap])
113       apply(fastforce elim: states_equiv_forE intro: equiv_forI dest: equiv_forD[where f=cdt_list])
114      apply(fastforce elim: states_equiv_forE intro: equiv_forI dest: equiv_forD[where f=is_original_cap])
115     apply(fastforce elim: states_equiv_forE intro: equiv_forI dest: equiv_forD[where f=interrupt_states])
116    apply(fastforce elim: states_equiv_forE intro: equiv_forI dest: equiv_forD[where f=interrupt_irq_node])
117   apply(fastforce simp: equiv_asids_def equiv_asid_def elim: states_equiv_forE)
118  apply(fastforce elim: states_equiv_forE intro: equiv_forI dest: equiv_forD[where f=ready_queues])
119  done
120
121lemma store_word_offs_equiv_but_for_labels:
122  "\<lbrace> equiv_but_for_labels aag L st and K (for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) (ptr + of_nat offs * of_nat word_size)) \<rbrace>
123   store_word_offs ptr offs v
124   \<lbrace> \<lambda>_. equiv_but_for_labels aag L st \<rbrace>"
125  unfolding store_word_offs_def
126  apply(wp modify_wp | simp add: do_machine_op_def split_def)+
127  apply clarsimp
128  apply(erule use_valid[OF _ storeWord_equiv_but_for_labels])
129  apply simp
130  done
131
132definition
133  ipc_buffer_has_read_auth :: "'a PAS \<Rightarrow> 'a \<Rightarrow> word32 option \<Rightarrow> bool"
134where
135"ipc_buffer_has_read_auth aag l \<equiv>
136    case_option True (\<lambda>buf'. is_aligned buf' msg_align_bits \<and> (\<forall>x \<in> ptr_range buf' msg_align_bits. (l,Read,pasObjectAbs aag x) \<in> (pasPolicy aag)))"
137
138
139lemma set_mrs_equiv_but_for_labels:
140  "\<lbrace> equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and>
141       (case buf of (Some buf') \<Rightarrow>
142        is_aligned buf' msg_align_bits \<and>
143        (\<forall>x \<in> ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)
144                 | _ \<Rightarrow> True)) \<rbrace>
145   set_mrs thread buf msgs
146   \<lbrace> \<lambda>_. equiv_but_for_labels aag L st \<rbrace>"
147  unfolding set_mrs_def
148  apply (wp | wpc)+
149       apply(subst zipWithM_x_mapM_x)
150       apply(rule_tac Q="\<lambda>_. equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L  \<and>
151       (case buf of (Some buf') \<Rightarrow>
152        is_aligned buf' msg_align_bits \<and>
153        (\<forall>x \<in> ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)
154                 | _ \<Rightarrow> True))" in hoare_strengthen_post)
155       apply(wp mapM_x_wp' store_word_offs_equiv_but_for_labels | simp add: split_def)+
156        apply(case_tac xa, clarsimp split: if_split_asm elim!: in_set_zipE)
157        apply(clarsimp simp: for_each_byte_of_word_def)
158        apply(erule bspec)
159        apply(clarsimp simp: ptr_range_def)
160        apply(rule conjI)
161         apply(erule order_trans[rotated])
162         apply(erule is_aligned_no_wrap')
163         apply(rule mul_word_size_lt_msg_align_bits_ofnat)
164         apply(fastforce simp: msg_max_length_def msg_align_bits)
165        apply(erule order_trans)
166        apply(subst p_assoc_help)
167        apply(simp add: add.assoc)
168        apply(rule word_plus_mono_right)
169         apply(rule word_less_sub_1)
170         apply(rule_tac y="of_nat msg_max_length * of_nat word_size + 3" in le_less_trans)
171          apply(rule word_plus_mono_left)
172           apply(rule word_mult_le_mono1)
173             apply(erule disjE)
174              apply(rule word_of_nat_le)
175              apply(simp add: msg_max_length_def)
176             apply clarsimp
177             apply(rule word_of_nat_le)
178             apply(simp add: msg_max_length_def)
179            apply(simp add: word_size_def)
180           apply(simp add: msg_max_length_def word_size_def)
181          apply(simp add: msg_max_length_def word_size_def)
182         apply(rule mul_add_word_size_lt_msg_align_bits_ofnat)
183          apply(simp add: msg_max_length_def msg_align_bits)
184         apply simp
185        apply(erule is_aligned_no_overflow')
186       apply simp
187      apply(wp set_object_equiv_but_for_labels hoare_vcg_all_lift static_imp_wp | simp)+
188   apply (fastforce dest: get_tcb_not_asid_pool_at)+
189  done
190
191
192definition all_to_which_has_auth where
193  "all_to_which_has_auth aag auth source \<equiv> {t. (source,auth,t) \<in> pasPolicy aag}"
194
195definition all_with_auth_to where
196  "all_with_auth_to aag auth target \<equiv> {x. (x, auth, target) \<in> pasPolicy aag}"
197
198lemma valid_ntfn_WaitingNtfn_tl:
199  "\<lbrakk>ntfn_obj ntfn = (WaitingNtfn list); valid_ntfn ntfn s; tl list \<noteq> []; ntfn' = ntfn\<lparr>ntfn_obj := (WaitingNtfn (tl list))\<rparr> \<rbrakk> \<Longrightarrow>
200   valid_ntfn ntfn' s"
201  apply(case_tac list, simp_all)
202  apply(rename_tac a lista)
203  apply(case_tac lista, simp_all)
204  apply(clarsimp simp: valid_ntfn_def split: option.splits)
205  done
206
207lemma update_waiting_ntfn_reads_respects:
208  assumes domains_distinct[wp]: "pas_domains_distinct aag"
209  notes tl_drop_1[simp del]
210  shows
211  "reads_respects aag l (valid_objs and sym_refs \<circ> state_refs_of and pas_refined aag and pas_cur_domain aag and ko_at (Notification ntfn) ntfnptr and (\<lambda>s. is_subject aag (cur_thread s)) and K (ntfn_obj ntfn = WaitingNtfn queue)) (update_waiting_ntfn ntfnptr queue bound_tcb badge)"
212  unfolding update_waiting_ntfn_def fun_app_def
213  apply (wp assert_sp possible_switch_to_reads_respects gets_cur_thread_ev | simp add: split_def)+
214  apply (wp as_user_set_register_reads_respects' set_thread_state_reads_respects
215            set_simple_ko_reads_respects set_thread_state_pas_refined
216            set_simple_ko_valid_objs hoare_vcg_disj_lift set_simple_ko_pas_refined
217        | simp add: split_def reads_lrefl)+
218  done
219
220lemma set_thread_state_ext_runnable_equiv_but_for_labels:
221  "\<lbrace>equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L) and st_tcb_at runnable thread\<rbrace>
222    set_thread_state_ext thread
223    \<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace>"
224  apply (simp add: set_thread_state_ext_def)
225  apply wp
226     apply (rule hoare_pre_cont)
227    apply (wp gts_wp)+
228  apply (force simp: st_tcb_at_def obj_at_def)
229  done
230
231lemma set_thread_state_runnable_equiv_but_for_labels:
232  "runnable tst \<Longrightarrow> \<lbrace>equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L)\<rbrace>
233    set_thread_state thread tst
234    \<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace>"
235  unfolding set_thread_state_def
236  apply (wp set_object_equiv_but_for_labels set_thread_state_ext_runnable_equiv_but_for_labels | simp add: split_def)+
237   apply (simp add: set_object_def, wp+)
238  apply (fastforce dest: get_tcb_not_asid_pool_at simp: st_tcb_at_def obj_at_def)
239  done
240
241lemma tcb_sched_action_equiv_but_for_labels:
242  "\<lbrace>equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L) and pas_refined aag\<rbrace>
243    tcb_sched_action action thread
244    \<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace>"
245  apply (simp add: tcb_sched_action_def, wp)
246  apply (clarsimp simp: etcb_at_def equiv_but_for_labels_def split: option.splits)
247  apply (rule states_equiv_forI)
248           apply(fastforce intro!: equiv_forI elim!: states_equiv_forE dest: equiv_forD[where f=kheap])
249          apply (simp add: states_equiv_for_def)
250         apply(fastforce elim: states_equiv_forE intro: equiv_forI dest: equiv_forD[where f=cdt])
251        apply(fastforce elim: states_equiv_forE intro: equiv_forI dest: equiv_forD[where f=ekheap])
252       apply(fastforce elim: states_equiv_forE intro: equiv_forI dest: equiv_forD[where f=cdt_list])
253      apply(fastforce elim: states_equiv_forE intro: equiv_forI dest: equiv_forD[where f=is_original_cap])
254     apply(fastforce elim: states_equiv_forE intro: equiv_forI dest: equiv_forD[where f=interrupt_states])
255    apply(fastforce elim: states_equiv_forE intro: equiv_forI dest: equiv_forD[where f=interrupt_irq_node])
256   apply(fastforce simp: equiv_asids_def equiv_asid_def elim: states_equiv_forE)
257  apply (clarsimp simp: pas_refined_def tcb_domain_map_wellformed_aux_def split: option.splits)
258  apply (rule equiv_forI)
259  apply (erule_tac x="(thread, tcb_domain (the (ekheap s thread)))" in ballE)
260   apply(fastforce elim: states_equiv_forE intro: equiv_forI dest: equiv_forD[where f=ready_queues])
261  apply (force intro: domtcbs)
262  done
263
264lemma possible_switch_to_equiv_but_for_labels:
265  "\<lbrace>equiv_but_for_labels aag L st and (\<lambda>s. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) target s) and K (pasObjectAbs aag target \<in> L) and pas_refined aag\<rbrace>
266    possible_switch_to target
267    \<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace>"
268  apply (simp add: possible_switch_to_def)
269  apply (wp tcb_sched_action_equiv_but_for_labels)
270       (* possible_switch_to does not modify scheduler action if target is in different domain *)
271       apply (rule hoare_pre_cont)
272      apply (wp tcb_sched_action_equiv_but_for_labels)
273      apply (rule hoare_pre_cont)
274     apply (wp tcb_sched_action_equiv_but_for_labels)+
275  apply (clarsimp simp: etcb_at_def split: option.splits)
276  done
277
278crunch etcb_at_cdom[wp]: set_thread_state_ext, set_thread_state, set_simple_ko
279   "\<lambda>s. etcb_at (P (cur_domain s)) t s"
280  (wp: crunch_wps)
281
282lemma update_waiting_ntfn_equiv_but_for_labels:
283  notes tl_drop_1[simp del]
284  shows
285  "\<lbrace> equiv_but_for_labels aag L st and pas_refined aag and valid_objs and
286     ko_at (Notification ntfn) ntfnptr and
287     sym_refs \<circ> state_refs_of and
288     (\<lambda>s. \<forall>t\<in> set list. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) t s) and
289     K (ntfn_obj ntfn = WaitingNtfn list \<and> pasObjectAbs aag ntfnptr \<in> L \<and>
290        all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<subseteq> L \<and>
291       \<Union> ((all_to_which_has_auth aag Write) ` (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr))) \<subseteq> L)\<rbrace>
292   update_waiting_ntfn ntfnptr list boundtcb badge
293   \<lbrace> \<lambda>_. equiv_but_for_labels aag L st \<rbrace>"
294  unfolding update_waiting_ntfn_def
295  apply (wp static_imp_wp as_user_equiv_but_for_labels set_thread_state_runnable_equiv_but_for_labels
296            set_thread_state_pas_refined set_notification_equiv_but_for_labels
297            set_simple_ko_pred_tcb_at set_simple_ko_pas_refined
298            hoare_vcg_disj_lift possible_switch_to_equiv_but_for_labels
299        | wpc | simp add: split_def)+
300  apply (clarsimp simp: conj_ac)
301  apply(frule_tac P="receive_blocked_on ntfnptr" and t="hd list" in ntfn_queued_st_tcb_at')
302      apply(fastforce)
303     apply assumption
304    apply assumption
305   apply simp
306  apply (subgoal_tac "pasObjectAbs aag (hd list) \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)")
307   apply(fastforce)
308  apply(clarsimp simp: all_with_auth_to_def)
309  apply (erule pas_refined_mem[rotated])
310  apply (rule sta_ts)
311  apply(clarsimp simp: thread_states_def split: option.split simp: tcb_states_of_state_def st_tcb_def2)
312  apply(case_tac "tcb_state tcb", simp_all)
313  done
314
315
316lemma update_waiting_ntfn_modifies_at_most:
317  "modifies_at_most aag
318          ({pasObjectAbs aag ntfnptr} \<union>
319           all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union>
320           \<Union> ((all_to_which_has_auth aag Write) ` (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr))))
321          (pas_refined aag and valid_objs and
322           ko_at (Notification ntfn) ntfnptr and
323           (\<lambda>s. \<forall>t\<in> set list. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) t s) and
324           sym_refs \<circ> state_refs_of and K (ntfn_obj ntfn = WaitingNtfn list))
325          (update_waiting_ntfn ntfnptr list boundtcb badge)"
326  apply(rule modifies_at_mostI)
327  apply(wp update_waiting_ntfn_equiv_but_for_labels | fastforce)+
328  done
329
330
331lemma invisible_ntfn_invisible_receivers_and_ipcbuffers:
332  "\<lbrakk>labels_are_invisible aag l {pasObjectAbs aag ntfnptr};
333    (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag\<rbrakk>
334    \<Longrightarrow> labels_are_invisible aag l
335        ({pasObjectAbs aag ntfnptr} \<union>
336         all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union>
337         \<Union>(all_to_which_has_auth aag Write `
338          all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))"
339  apply(auto simp: labels_are_invisible_def aag_can_affect_label_def dest: reads_read_page_read_thread reads_read_queued_thread_read_ep simp: all_to_which_has_auth_def all_with_auth_to_def)
340  done
341
342lemma invisible_ntfn_invisible_receivers_and_receivers:
343  "\<lbrakk>labels_are_invisible aag l {pasObjectAbs aag ntfnptr};
344    (pasSubject aag, auth, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag;
345    auth \<in> {Notify,Receive,SyncSend}\<rbrakk>
346    \<Longrightarrow> labels_are_invisible aag l
347        ({pasObjectAbs aag ntfnptr} \<union>
348         all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union>
349         (\<Union>(all_to_which_has_auth aag Receive `
350          all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr))) \<union>
351         (\<Union>(all_to_which_has_auth aag Write `
352          all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr))))"
353  by (auto simp: labels_are_invisible_def aag_can_affect_label_def
354        dest: read_sync_ep_read_senders_strong read_sync_ep_read_receivers_strong
355              reads_read_queued_thread_read_ep
356              reads_read_page_read_thread
357              reads_ep
358        simp: all_to_which_has_auth_def all_with_auth_to_def)
359
360lemma read_queued_thread_reads_ntfn:
361  "\<lbrakk>ko_at (Notification ntfn) ntfnptr s; t \<in> set queue; aag_can_read aag t;
362    valid_objs s; sym_refs (state_refs_of s); pas_refined aag s; ntfn_obj ntfn = WaitingNtfn queue;
363    (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag\<rbrakk>
364  \<Longrightarrow> aag_can_read aag ntfnptr"
365  apply(frule_tac P="receive_blocked_on ntfnptr" and t=t in ntfn_queued_st_tcb_at')
366      apply(fastforce)
367     apply assumption
368    apply assumption
369   apply simp
370  apply (rule_tac t="pasObjectAbs aag t" and auth="Receive" and auth'="Notify" in reads_read_queued_thread_read_ep)
371      apply assumption
372     apply simp
373    apply (erule pas_refined_mem[rotated])
374    apply (rule sta_ts)
375    apply(clarsimp simp: thread_states_def split: option.split simp: tcb_states_of_state_def st_tcb_def2)
376    apply (case_tac "tcb_state tcb", simp_all)[1]
377   apply simp
378  apply simp
379  done
380
381lemma not_etcb_at_not_cdom_can_read:
382  assumes domains_distinct[wp]: "pas_domains_distinct aag"
383  shows
384  "\<lbrakk>\<not> etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) t s;
385   tcb_at t s; valid_etcbs s; pas_refined aag s; pas_cur_domain aag s\<rbrakk>
386  \<Longrightarrow> aag_can_read aag t"
387  apply (clarsimp simp: valid_etcbs_def tcb_at_st_tcb_at etcb_at_def is_etcb_at_def
388                        pas_refined_def tcb_domain_map_wellformed_aux_def)
389  apply (erule_tac x="(t, cur_domain s)" in ballE)
390   apply (force dest: domains_distinct[THEN pas_domains_distinct_inj])
391  apply (force intro: domtcbs)
392  done
393
394lemma tcb_at_ntfn_queue:
395  "\<lbrakk>valid_objs s; t \<in> set queue; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = WaitingNtfn queue\<rbrakk>
396  \<Longrightarrow> tcb_at t s"
397  apply (erule valid_objsE, force simp: obj_at_def)
398  apply (simp add: valid_obj_def valid_ntfn_def)
399  done
400
401
402lemma invisible_ep_invisible_receiver:
403  "\<lbrakk>labels_are_invisible aag l {pasObjectAbs aag epptr};
404    (pasObjectAbs aag tcb, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag;
405    (pasObjectAbs aag tcb, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk>
406   \<Longrightarrow> labels_are_invisible aag l
407          ({pasObjectAbs aag epptr} \<union> {pasObjectAbs aag tcb})"
408  apply (auto simp: labels_are_invisible_def aag_can_affect_label_def
409                    all_with_auth_to_def
410                  dest: reads_ep reads_read_queued_thread_read_ep)
411  done
412
413
414lemma no_fail_gts:"no_fail (tcb_at tcb) (get_thread_state tcb)"
415  apply (clarsimp simp: get_thread_state_def thread_get_def)
416  apply (rule no_fail_pre)
417   apply wp
418  by (clarsimp simp: get_tcb_def tcb_at_def)
419
420lemma monadic_rewrite_impossible: "monadic_rewrite F E (\<lambda>_. False) f g"
421  by (clarsimp simp: monadic_rewrite_def)
422
423lemma monadic_rewrite_add_get:
424  "monadic_rewrite F E P (do x <- get; f od) (do x <- get; g od) \<Longrightarrow>
425       monadic_rewrite F E P f g"
426       by (clarsimp simp: bind_def get_def)
427
428lemma sts_noop:
429   "monadic_rewrite True True (tcb_at tcb and (\<lambda>s. tcb \<noteq> cur_thread s))
430   (set_thread_state_ext tcb)
431   (return ())"
432  apply (rule monadic_rewrite_imp)
433   apply (rule monadic_rewrite_add_get)
434   apply (rule monadic_rewrite_bind_tail)
435    apply (clarsimp simp: set_thread_state_ext_def)
436    apply (rule_tac x="tcb_state (the (get_tcb tcb x))" in monadic_rewrite_symb_exec)
437       apply (wp gts_wp | simp)+
438    apply (rule monadic_rewrite_symb_exec)
439       apply wp+
440    apply (rule monadic_rewrite_symb_exec)
441       apply wp+
442    apply (simp only: when_def)
443    apply (rule monadic_rewrite_trans)
444     apply (rule monadic_rewrite_if)
445      apply (rule monadic_rewrite_impossible[where g="return ()"])
446     apply (rule monadic_rewrite_refl)
447    apply simp
448    apply (rule monadic_rewrite_refl)
449   apply wp
450  by (auto simp: pred_tcb_at_def obj_at_def is_tcb_def get_tcb_def)
451
452lemma sts_to_modify':
453  "monadic_rewrite True True (tcb_at tcb and (\<lambda>s :: det_ext state. tcb \<noteq> cur_thread s))
454       (set_thread_state tcb st)  (modify (\<lambda>s. s\<lparr>kheap := kheap s(tcb \<mapsto> TCB (the (get_tcb tcb s)\<lparr>tcb_state := st\<rparr>))\<rparr>))"
455  apply (clarsimp simp: set_thread_state_def set_object_def)
456  apply (rule monadic_rewrite_add_get)
457  apply (rule monadic_rewrite_bind_tail)
458   apply (rule monadic_rewrite_imp)
459    apply (rule monadic_rewrite_trans)
460     apply (simp only: bind_assoc[symmetric])
461     apply (rule monadic_rewrite_bind_tail)
462      apply (rule sts_noop)
463     apply wp
464    apply simp
465    apply (rule_tac x="the (get_tcb tcb x)" in monadic_rewrite_symb_exec,(wp | simp)+)
466    apply (rule_tac x="x" in  monadic_rewrite_symb_exec,(wp | simp)+)
467    apply (rule_tac P="(=) x" in monadic_rewrite_refl3)
468    apply (clarsimp simp add: put_def modify_def get_def bind_def)
469   apply assumption
470  apply wp
471  by (clarsimp simp: get_tcb_def tcb_at_def)
472
473
474lemma
475  monadic_rewrite_weaken_failure:
476  "monadic_rewrite True True P f f' \<Longrightarrow>
477  no_fail P' f \<Longrightarrow> no_fail Q' f' \<Longrightarrow>
478   monadic_rewrite F E (P and P' and Q') f f'"
479  by (clarsimp simp: monadic_rewrite_def no_fail_def)
480
481lemma
482  sts_no_fail:
483  "no_fail (\<lambda>s :: det_ext state. tcb_at tcb s) (set_thread_state tcb st)"
484  apply (simp add: set_thread_state_def set_object_def)
485  apply (simp add: set_thread_state_ext_def get_thread_state_def thread_get_def set_scheduler_action_def)
486  apply (rule no_fail_pre)
487   apply wp
488  by (clarsimp simp: get_tcb_def tcb_at_def)
489
490lemmas sts_to_modify = monadic_rewrite_weaken_failure[OF sts_to_modify' sts_no_fail no_fail_modify,simplified]
491
492definition "blocked_cancel_ipc_nosts tcb \<equiv>
493  do state <- get_thread_state tcb;
494     epptr \<leftarrow> get_blocking_object state;
495     ep \<leftarrow> get_endpoint epptr;
496     queue \<leftarrow> get_ep_queue ep;
497     queue' \<leftarrow> return $ remove1 tcb queue;
498     ep' \<leftarrow> return (case queue' of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep queue');
499     set_endpoint epptr ep';
500     set_thread_state tcb Running
501  od"
502
503lemma cancel_ipc_to_blocked_nosts:
504      "monadic_rewrite False False
505       (\<lambda>s. st_tcb_at receive_blocked tcb (s :: det_ext state) \<and>
506       cur_thread s \<noteq> tcb)
507       (blocked_cancel_ipc_nosts tcb)
508       (cancel_ipc tcb >>= (\<lambda>_. set_thread_state tcb Running))"
509  apply (simp add: cancel_ipc_def bind_assoc blocked_cancel_ipc_nosts_def)
510  apply (rule monadic_rewrite_bind_tail)
511   apply (rule monadic_rewrite_transverse)
512    apply (rename_tac state)
513    apply (rule_tac P="\<lambda>_. \<exists>xa. state = BlockedOnReceive xa" in monadic_rewrite_bind_head)
514    apply (rule monadic_rewrite_gen_asm[where Q=\<top>,simplified])
515    apply clarsimp
516    apply (rule monadic_rewrite_refl)
517   apply (simp add: blocked_cancel_ipc_def blocked_cancel_ipc_nosts_def bind_assoc)
518   apply (rule monadic_rewrite_bind_tail)
519    apply (rule monadic_rewrite_bind_tail)
520     apply (rule monadic_rewrite_bind_tail)
521      apply (rule monadic_rewrite_bind_tail)
522       apply (rule monadic_rewrite_trans)
523        apply (rule sts_to_modify)
524       apply (rule monadic_rewrite_transverse)
525        apply (rule monadic_rewrite_bind)
526          apply (rule sts_to_modify)
527         apply (rule sts_to_modify)
528        apply (rule hoare_modifyE_var[where P="tcb_at tcb and (\<lambda>s. tcb \<noteq> cur_thread s)"])
529        apply (clarsimp simp: tcb_at_def get_tcb_def)
530       apply (simp add: modify_modify)
531       apply (rule monadic_rewrite_refl2)
532       apply (fastforce simp add: simpler_modify_def o_def get_tcb_def)
533      apply (wp gts_wp)+
534  apply (simp add: set_thread_state_def bind_assoc gets_the_def)
535  apply (clarsimp simp add: pred_tcb_at_def receive_blocked_def obj_at_def is_tcb_def split: thread_state.splits)
536  by (case_tac "tcb_state tcba";fastforce)
537
538
539lemma gts_reads_respects:
540  "reads_respects aag l (K (aag_can_read aag thread \<or> aag_can_affect aag l thread)) (get_thread_state thread)"
541  unfolding get_thread_state_def
542  by (wp thread_get_reads_respects)
543
544
545lemma ev2_invisible_simple:
546  assumes domains_distinct: "pas_domains_distinct aag"
547  shows
548  "labels_are_invisible aag l L \<Longrightarrow>
549       modifies_at_most aag L Q f \<Longrightarrow>
550       reads_respects aag l Q (f :: det_ext state \<Rightarrow> (unit \<times> det_ext state) set \<times> bool)"
551  apply (simp add: equiv_valid_def2)
552  apply (rule equiv_valid_2_guard_imp)
553    apply (rule ev2_invisible[OF domains_distinct])
554        by fastforce+
555
556lemma blocked_cancel_ipc_nosts_equiv_but_for_labels:
557  "\<lbrace>pas_refined aag and
558    st_tcb_at (\<lambda>st. st = BlockedOnReceive x) t and
559    bound_tcb_at ((=) (Some ntfnptr)) t and
560    equiv_but_for_labels aag L st and
561    K(pasObjectAbs aag x \<in> L) and
562    K(pasObjectAbs aag t \<in> L) \<rbrace>
563   blocked_cancel_ipc_nosts t
564   \<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace>"
565  unfolding blocked_cancel_ipc_nosts_def get_blocking_object_def
566  apply (wp set_endpoint_equiv_but_for_labels get_object_wp gts_wp
567            set_thread_state_runnable_equiv_but_for_labels
568       | wpc
569       | simp)+
570  by (clarsimp simp: pred_tcb_at_def obj_at_def)
571
572lemma blocked_cancel_ipc_nosts_reads_respects:
573  assumes domains_distinct[wp]: "pas_domains_distinct aag"
574  shows
575  "reads_respects aag l (pas_refined aag
576                          and st_tcb_at (\<lambda>st. \<exists>xa. st = (BlockedOnReceive x)) t
577
578                          and bound_tcb_at ((=) (Some ntfnptr)) t
579                          and (\<lambda>s. is_subject aag (cur_thread s))
580                          and K (
581                              (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag
582                            \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag
583                            \<and> (pasObjectAbs aag t, Receive, pasObjectAbs aag x) \<in> pasPolicy aag))
584           (blocked_cancel_ipc_nosts t)"
585  unfolding blocked_cancel_ipc_nosts_def
586  apply (simp only:bind_assoc[symmetric])
587  apply (rule bind_ev[where P''=\<top>,simplified])
588    apply (wp set_thread_state_runnable_reads_respects,simp)
589
590    subgoal
591    proof (cases "aag_can_read_label aag (pasObjectAbs aag x) \<or> aag_can_affect aag l x")
592      case True thus ?thesis \<comment> \<open>boring case, can read or affect ep\<close>
593      unfolding blocked_cancel_ipc_nosts_def get_blocking_object_def
594      apply clarsimp
595      apply (rule pre_ev)
596       apply ((wp set_thread_state_reads_respects get_ep_queue_reads_respects
597                  get_simple_ko_reads_respects get_blocking_object_reads_respects
598                  gts_reads_respects set_simple_ko_reads_respects
599                  gts_wp
600                  | wpc
601                  | simp add: get_blocking_object_def get_thread_state_rev)+)[2]
602      apply (clarsimp simp: pred_tcb_at_def obj_at_def)
603      by (fastforce dest:read_sync_ep_read_receivers_strong )
604
605    next
606      case False thus ?thesis apply -  \<comment> \<open>can't read or affect ep\<close>
607      apply (rule gen_asm_ev)
608      apply (drule label_is_invisible[THEN iffD2])
609      apply clarsimp
610      apply (rule ev2_invisible_simple[OF domains_distinct],assumption)
611      apply (simp add: get_blocking_object_def)
612      apply (rule modifies_at_mostI)
613      apply (rule hoare_pre)
614       apply (wp set_thread_state_runnable_equiv_but_for_labels
615                 set_endpoint_equiv_but_for_labels get_object_wp gts_wp
616                 set_thread_state_runnable_equiv_but_for_labels
617            | wpc
618            | simp)+
619      by (fastforce simp: pred_tcb_at_def obj_at_def)
620    qed
621  by wp
622
623crunch silc_inv[wp]: "blocked_cancel_ipc_nosts" "silc_inv aag st"
624
625lemmas blocked_cancel_ipc_nosts_reads_respects_f =
626  reads_respects_f[where Q=\<top>,simplified,
627                   OF blocked_cancel_ipc_nosts_reads_respects
628                      blocked_cancel_ipc_nosts_silc_inv,
629                      simplified]
630
631lemma monadic_rewrite_is_valid:
632  "monadic_rewrite False False P' f f' \<Longrightarrow>
633  \<lbrace>P\<rbrace> do x <- f; g x od \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P and P'\<rbrace> do x <- f'; g x od  \<lbrace>Q\<rbrace>"
634  by (fastforce simp: monadic_rewrite_def valid_def bind_def)
635
636lemma monadic_rewrite_reads_respects:
637  "monadic_rewrite False False P f f' \<Longrightarrow>
638   reads_respects l aag P' (do x <- f; g x od) \<Longrightarrow>
639   reads_respects l aag (P and P') (do x <- f'; g x od)"
640  apply (clarsimp simp: monadic_rewrite_def equiv_valid_def
641                        spec_equiv_valid_def equiv_valid_2_def
642                        bind_def)
643  apply (frule_tac x=st in spec)
644  apply (drule_tac x=t in spec)
645  by fastforce
646
647
648lemmas cancel_ipc_reads_respects_rewrite =
649  monadic_rewrite_reads_respects[OF cancel_ipc_to_blocked_nosts, simplified bind_assoc]
650
651lemmas cancel_ipc_valid_rewrite =
652  monadic_rewrite_is_valid[OF cancel_ipc_to_blocked_nosts, simplified bind_assoc]
653
654crunch etcb_at[wp]: blocked_cancel_ipc_nosts "etcb_at P t"
655crunch cur_domain[wp]: blocked_cancel_ipc_nosts "\<lambda>s. P (cur_domain s)"
656crunch pas_refined[wp]: blocked_cancel_ipc_nosts "pas_refined aag"
657crunch cur_thread[wp]: blocked_cancel_ipc_nosts "\<lambda>s. P (cur_thread s)"
658
659lemma BlockedOnReceive_inj:
660  "x = (case (BlockedOnReceive x) of BlockedOnReceive x \<Rightarrow> x)"
661  by (cases "BlockedOnReceive x";simp)
662
663
664lemma send_signal_reads_respects:
665  assumes domains_distinct[wp]: "pas_domains_distinct aag"
666  notes set_thread_state_owned_reads_respects[wp del]
667        cancel_ipc_pas_refined[wp del]
668  shows
669  "reads_respects aag l (pas_refined aag and pas_cur_domain aag and
670    (\<lambda>s. is_subject aag (cur_thread s)) and valid_etcbs and ct_active and
671    (\<lambda>s. sym_refs (state_refs_of s)) and valid_objs and
672    K ((pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag))
673    (send_signal ntfnptr badge)"
674  unfolding send_signal_def fun_app_def
675  subgoal
676  proof (cases "aag_can_read aag ntfnptr \<or> aag_can_affect aag l ntfnptr")
677    case True
678    note visible = this
679    show ?thesis
680    apply (rule pre_ev)
681     apply (simp split del: if_split
682          | rule_tac ntfnptr=ntfnptr in blocked_cancel_ipc_nosts_reads_respects
683          | rule cancel_ipc_reads_respects_rewrite
684          | wp_once
685              set_simple_ko_reads_respects
686              possible_switch_to_reads_respects
687              as_user_set_register_reads_respects'
688              set_thread_state_pas_refined
689              set_thread_state_pas_refined
690              set_simple_ko_reads_respects
691              gts_reads_respects
692              cancel_ipc_receive_blocked_pas_refined
693              gts_wp
694              hoare_vcg_imp_lift
695              update_waiting_ntfn_reads_respects
696              get_simple_ko_wp
697              get_simple_ko_reads_respects
698          | wpc
699          | simp )+
700    apply (insert visible)
701    apply clarsimp
702    apply (rule conjI[rotated])
703     apply fastforce
704    apply (rule disjI2)
705    apply (intro impI allI)
706    apply (simp add: obj_at_def)
707    apply (rule conjI)
708     apply (frule (3) ntfn_bound_tcb_at[where P="(=) (Some ntfnptr)",OF _ _ _ _ refl])
709     apply (frule (1) bound_tcb_at_implies_receive)
710     apply (elim disjE)
711      apply (rule disjI1)
712      apply (fastforce dest:read_sync_ep_read_receivers_strong)
713     apply (rule disjI2)
714     apply (fastforce dest:read_sync_ep_read_receivers_strong)
715    apply (clarsimp)
716    apply (frule (1) ntfn_bound_tcb_at[where P="(=) (Some ntfnptr)",OF _ _ _ _ refl])
717      apply (fastforce simp: obj_at_def)
718     apply assumption
719    apply (rule conjI)
720     apply (fastforce simp: pred_tcb_at_def receive_blocked_def obj_at_def)
721    apply (rule conjI[rotated])
722     apply (frule (1) bound_tcb_at_implies_receive)
723     apply (frule (1) bound_tcb_at_implies_reset)
724     apply (clarsimp simp: pred_tcb_at_def get_tcb_def obj_at_def)
725     apply (rule context_conjI)
726      apply (fastforce simp: receive_blocked_def intro!: BlockedOnReceive_inj split:thread_state.splits)
727     apply (frule_tac t=x and tcb=tcb and ep = "case (tcb_state tcb) of BlockedOnReceive a \<Rightarrow> a"
728              in get_tcb_recv_blocked_implies_receive)
729       apply (fastforce simp: pred_tcb_at_def get_tcb_def obj_at_def)
730      apply (fastforce simp: receive_blocked_def split:thread_state.splits)
731     apply (fastforce simp: receive_blocked_def intro!: BlockedOnReceive_inj split:thread_state.splits)
732    by (fastforce simp: pred_tcb_at_def get_tcb_def obj_at_def receive_blocked_def
733                        ct_in_state_def
734                  split:thread_state.splits)
735
736  next
737    case False note invisible = this show ?thesis
738    apply (insert label_is_invisible[THEN iffD2, OF invisible])
739    apply (rule gen_asm_ev)
740    apply (drule (1) invisible_ntfn_invisible_receivers_and_receivers)
741     apply simp
742     apply (rule ev2_invisible_simple[OF domains_distinct],assumption)
743     apply (rule modifies_at_mostI)
744
745     apply ( simp split del: if_split
746           | rule cancel_ipc_valid_rewrite
747           | wp_once
748               set_notification_equiv_but_for_labels
749               possible_switch_to_equiv_but_for_labels
750               as_user_equiv_but_for_labels
751               set_thread_state_runnable_equiv_but_for_labels
752               set_thread_state_pas_refined
753               blocked_cancel_ipc_nosts_equiv_but_for_labels
754               gts_wp
755               update_waiting_ntfn_equiv_but_for_labels
756               get_simple_ko_wp
757           | wpc
758           | wps
759           )+
760
761    apply (elim conjE)
762    apply (match premises in "ntfn_bound_tcb _ = _" \<Rightarrow> \<open>fail\<close>
763                                               \<bar> _ \<Rightarrow> \<open>rule allI impI conjI\<close>)+
764     prefer 2
765     apply (intro conjI allI impI; fastforce?)
766     subgoal waiting_ntfn
767       apply clarsimp
768       apply (rule ccontr)
769       apply (frule (3) not_etcb_at_not_cdom_can_read[OF domains_distinct, rotated 2])
770        apply (rule tcb_at_ntfn_queue;assumption)
771       apply(frule (7) read_queued_thread_reads_ntfn)
772       using invisible
773       by (fastforce simp add: all_with_auth_to_def all_to_which_has_auth_def)
774
775     apply (frule (1)
776       ntfn_bound_tcb_at[where P="(=) (Some ntfnptr)",OF _ _ _ _ refl])
777       apply (fastforce simp: obj_at_def)
778      apply assumption
779     apply (intro allI conjI impI)
780            apply (fastforce simp: pred_tcb_at_def receive_blocked_def obj_at_def split:thread_state.splits
781                           intro!: BlockedOnReceive_inj)
782           apply assumption
783          apply distinct_subgoals
784         apply (fold_subgoals (prefix))
785     apply (frule st_tcb_at_tcb_at)
786     subgoal bound_ntfn premises prems for st s ntfn x sta
787       prefer 2
788           apply (rule disjI2)
789           apply (rule disjI1)
790           subgoal bound_tcb_can_receive
791             using prems
792             apply (clarsimp simp: all_with_auth_to_def obj_at_def)
793             by (rule bound_tcb_at_implies_receive;assumption)
794          apply (rule disjI2)
795          apply (rule disjI2)
796          apply (rule disjI1)
797          subgoal bound_ep_can_receive
798            apply (rule bexI[OF _ bound_tcb_can_receive])
799            apply (simp add: all_with_auth_to_def all_to_which_has_auth_def)
800            using prems
801            apply (case_tac sta;(clarsimp simp: pred_tcb_at_def obj_at_def receive_blocked_def split:thread_state.splits))
802            apply (rule get_tcb_recv_blocked_implies_receive, assumption)
803             apply (fastforce simp: get_tcb_def)
804            by (fastforce  split:thread_state.splits)
805         apply (rule ccontr)
806         apply (insert prems)
807         apply (frule (4) not_etcb_at_not_cdom_can_read[OF domains_distinct])
808         using bound_tcb_can_receive
809         apply (fastforce simp: labels_are_invisible_def all_with_auth_to_def all_to_which_has_auth_def)
810        apply (fastforce simp: pred_tcb_at_def receive_blocked_def obj_at_def)
811       apply (rule ccontr)
812       apply clarsimp
813       using invisible bound_tcb_can_receive reads_ep
814       by (fastforce simp add: all_with_auth_to_def all_to_which_has_auth_def)
815    done
816  qed
817  done
818
819lemma receive_signal_reads_respects:
820  assumes domains_distinct[wp]: "pas_domains_distinct aag"
821  shows
822  "reads_respects aag l (valid_objs and pas_refined aag and
823        (\<lambda>s. is_subject aag (cur_thread s)) and
824        K ((\<forall>ntfnptr\<in>Access.obj_refs cap.
825            (pasSubject aag, Receive, pasObjectAbs aag ntfnptr)
826             \<in> pasPolicy aag \<and> is_subject aag thread)))
827         (receive_signal thread cap is_blocking)"
828  unfolding receive_signal_def fun_app_def do_nbrecv_failed_transfer_def
829  apply(wp set_simple_ko_reads_respects set_thread_state_reads_respects
830           as_user_set_register_reads_respects' get_simple_ko_reads_respects hoare_vcg_all_lift
831       | wpc
832       | wp_once hoare_drop_imps)+
833  apply(force dest: reads_ep)
834  done
835
836subsection "Sync IPC"
837
838(* FIXME move *)
839lemma conj_imp:
840  "\<lbrakk>Q \<longrightarrow> R; P \<longrightarrow> Q; P' \<longrightarrow> Q\<rbrakk> \<Longrightarrow>
841    (P \<longrightarrow> R) \<and> (P' \<longrightarrow> R)"
842  by(fastforce)
843
844(* basically clagged directly from lookup_ipc_buffer_has_auth *)
845lemma lookup_ipc_buffer_has_read_auth:
846  "\<lbrace>pas_refined aag and valid_objs\<rbrace>
847   lookup_ipc_buffer is_receiver thread
848   \<lbrace>\<lambda>rv s. ipc_buffer_has_read_auth aag (pasObjectAbs aag thread) rv\<rbrace>"
849  apply (rule hoare_pre)
850   apply (simp add: lookup_ipc_buffer_def)
851   apply (wp get_cap_wp thread_get_wp'
852        | wpc)+
853  apply (clarsimp simp: cte_wp_at_caps_of_state ipc_buffer_has_read_auth_def get_tcb_ko_at [symmetric])
854  apply (frule caps_of_state_tcb_cap_cases [where idx = "tcb_cnode_index 4"])
855   apply (simp add: dom_tcb_cap_cases)
856  apply (frule (1) caps_of_state_valid_cap)
857  apply (clarsimp simp: vm_read_only_def vm_read_write_def)
858  apply (rule_tac Q="AllowRead \<in> xc" in conj_imp)
859    apply (clarsimp simp: valid_cap_simps cap_aligned_def)
860    apply (rule conjI)
861     apply (erule aligned_add_aligned)
862      apply (rule is_aligned_andI1)
863      apply (drule (1) valid_tcb_objs)
864      apply (clarsimp simp: valid_obj_def valid_tcb_def valid_ipc_buffer_cap_def
865                     split: if_splits)
866     apply (rule order_trans [OF _ pbfs_atleast_pageBits])
867     apply (simp add: msg_align_bits pageBits_def)
868    apply (drule (1) cap_auth_caps_of_state)
869    apply (clarsimp simp: aag_cap_auth_def cap_auth_conferred_def vspace_cap_rights_to_auth_def vm_read_only_def)
870    apply (drule bspec)
871     apply (erule (3) ipcframe_subset_page)
872    apply (clarsimp split: if_split_asm simp: vspace_cap_rights_to_auth_def is_page_cap_def)
873   apply(simp_all)
874  done
875
876
877definition
878  aag_can_read_or_affect_ipc_buffer :: "'a PAS \<Rightarrow> 'a \<Rightarrow> word32 option \<Rightarrow> bool"
879where
880"aag_can_read_or_affect_ipc_buffer aag l \<equiv>
881    case_option True (\<lambda>buf'. is_aligned buf' msg_align_bits \<and> (\<forall>x \<in> ptr_range buf' msg_align_bits. aag_can_read aag x \<or> aag_can_affect aag l x))"
882
883
884lemma lookup_ipc_buffer_aag_can_read_or_affect:
885  "\<lbrace>pas_refined aag and valid_objs and K (aag_can_read aag thread \<or> aag_can_affect aag l thread)\<rbrace>
886    lookup_ipc_buffer is_receiver thread
887   \<lbrace>\<lambda>rv s. aag_can_read_or_affect_ipc_buffer aag l rv\<rbrace>"
888  apply(rule hoare_gen_asm)
889  apply(rule hoare_strengthen_post[OF lookup_ipc_buffer_has_read_auth])
890  apply(auto simp: ipc_buffer_has_read_auth_def aag_can_read_or_affect_ipc_buffer_def intro: reads_read_thread_read_pages simp: aag_can_affect_label_def split: option.splits)
891  done
892
893lemma cptrs_in_ipc_buffer:
894  "\<lbrakk>x \<in> set [buffer_cptr_index..<
895             buffer_cptr_index + unat (mi_extra_caps mi)];
896    is_aligned a msg_align_bits;
897    buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - 2)\<rbrakk>
898   \<Longrightarrow>
899     ptr_range (a + of_nat x * of_nat word_size) 2 \<subseteq>
900     ptr_range (a :: word32) msg_align_bits"
901  apply(rule ptr_range_subset)
902     apply assumption
903    apply(simp add: msg_align_bits)
904   apply(simp add: msg_align_bits word_bits_def)
905  apply(simp add: word_size_def)
906  apply(subst upto_enum_step_shift_red[where us=2, simplified])
907     apply (simp add: msg_align_bits word_bits_def)+
908  done
909
910lemma for_each_byte_of_word_def2:
911  "for_each_byte_of_word P ptr \<equiv> (\<forall> x\<in>ptr_range ptr 2. P x)"
912  apply(simp add: for_each_byte_of_word_def ptr_range_def add.commute)
913  done
914
915lemma aag_has_auth_to_read_cptrs:
916  "\<lbrakk>x \<in> set [buffer_cptr_index..<
917             buffer_cptr_index + unat (mi_extra_caps mi)];
918    ipc_buffer_has_read_auth aag (pasSubject aag) (Some a);
919    buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - 2)\<rbrakk>
920   \<Longrightarrow>
921   for_each_byte_of_word (\<lambda> y. aag_can_read aag y)
922     (a + of_nat x * of_nat word_size)"
923  apply(simp add: for_each_byte_of_word_def2 ipc_buffer_has_read_auth_def)
924  apply(rule ballI)
925  apply(rule reads_read)
926  apply(clarify)
927  apply(erule bspec)
928  apply(rule subsetD[OF cptrs_in_ipc_buffer])
929     apply fastforce
930    apply assumption
931   apply assumption
932  apply assumption
933  done
934
935lemma get_extra_cptrs_rev:
936  "reads_equiv_valid_inv A aag (K (ipc_buffer_has_read_auth aag (pasSubject aag) buffer \<and> (buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - 2))))
937      (get_extra_cptrs buffer mi)"
938  unfolding get_extra_cptrs_def
939  apply (rule gen_asm_ev)
940  apply clarsimp
941  apply(case_tac buffer, simp_all add: return_ev_pre)
942  apply (wp mapM_ev equiv_valid_guard_imp[OF load_word_offs_rev]
943       | erule (2) aag_has_auth_to_read_cptrs)+
944  done
945
946lemma lookup_extra_caps_rev:
947  shows "reads_equiv_valid_inv A aag (pas_refined aag and (K (is_subject aag thread))  and (\<lambda> s. ipc_buffer_has_read_auth aag (pasSubject aag) buffer \<and> buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - 2)))
948     (lookup_extra_caps thread buffer mi)"
949  apply(rule gen_asm_ev)
950  unfolding lookup_extra_caps_def fun_app_def
951  apply (wp mapME_ev cap_fault_on_failure_rev lookup_cap_and_slot_rev
952            get_extra_cptrs_rev)
953  apply simp
954  done
955
956lemmas lookup_extra_caps_reads_respects_g =  reads_respects_g_from_inv[OF lookup_extra_caps_rev lookup_extra_caps_inv]
957
958lemma msg_in_ipc_buffer:
959  "\<lbrakk>x = msg_max_length \<or> x < msg_max_length;
960    unat (mi_length mi) < 2 ^ (msg_align_bits - 2);
961    is_aligned a msg_align_bits\<rbrakk>
962   \<Longrightarrow>
963     ptr_range (a + of_nat x * of_nat word_size) 2 \<subseteq>
964     ptr_range (a::word32) msg_align_bits"
965  apply(rule ptr_range_subset)
966     apply assumption
967    apply(simp add: msg_align_bits)
968   apply(simp add: msg_align_bits word_bits_def)
969  apply(simp add: word_size_def)
970  apply(subst upto_enum_step_shift_red[where us=2, simplified])
971     apply (simp add: msg_align_bits word_bits_def)+
972  apply(simp add: image_def)
973  apply(rule_tac x=x in bexI)
974   apply(rule refl)
975  apply(auto simp: msg_max_length_def)
976  done
977
978
979lemma aag_has_auth_to_read_msg:
980  "\<lbrakk>x = msg_max_length \<or> x < msg_max_length;
981    ipc_buffer_has_read_auth aag (pasSubject aag) (Some a);
982    unat (mi_length mi) < 2 ^ (msg_align_bits - 2)\<rbrakk>
983   \<Longrightarrow>
984   for_each_byte_of_word (aag_can_read aag)
985     (a + of_nat x * of_nat word_size)"
986  apply(simp add: for_each_byte_of_word_def2 ipc_buffer_has_read_auth_def)
987  apply(rule ballI)
988  apply(rule reads_read)
989  apply(clarify)
990  apply(erule bspec)
991  apply(rule subsetD[OF msg_in_ipc_buffer[where x=x]])
992     apply assumption
993    apply assumption
994   apply assumption
995  apply assumption
996  done
997
998(* only called within do_reply_transfer for which access assumes sender
999   and receiver in same domain *)
1000lemma get_mrs_rev:
1001  shows "reads_equiv_valid_inv A aag ((K (is_subject aag thread \<and> ipc_buffer_has_read_auth aag (pasSubject aag) buf \<and> unat (mi_length mi) < 2 ^ (msg_align_bits - 2)))) (get_mrs thread buf mi)"
1002  apply (rule gen_asm_ev)
1003  unfolding get_mrs_def
1004  apply (wp mapM_ev'' load_word_offs_rev thread_get_rev
1005       | wpc
1006       | rule aag_has_auth_to_read_msg[where mi=mi]
1007       | clarsimp split: if_split_asm)+
1008  done
1009
1010lemmas get_mrs_reads_respects_g = reads_respects_g_from_inv[OF get_mrs_rev get_mrs_inv]
1011
1012
1013
1014lemma setup_caller_cap_reads_respects:
1015  "reads_respects aag l (K (is_subject aag sender \<and> is_subject aag receiver))
1016    (setup_caller_cap sender receiver)"
1017  unfolding setup_caller_cap_def
1018  apply(wp cap_insert_reads_respects set_thread_state_owned_reads_respects | simp)+
1019  done
1020
1021
1022lemma const_on_failure_ev:
1023  "equiv_valid_inv I A P m \<Longrightarrow>
1024   equiv_valid_inv I A P (const_on_failure c m)"
1025  unfolding const_on_failure_def catch_def
1026  apply(wp | wpc | simp)+
1027  done
1028
1029
1030lemma set_extra_badge_reads_respects:
1031  "reads_respects aag l \<top> (set_extra_badge buffer badge n)"
1032  unfolding set_extra_badge_def
1033  by (rule store_word_offs_reads_respects)
1034
1035lemma reads_equiv_cdt_has_children:
1036  "\<lbrakk>pas_refined aag s; pas_refined aag s'; is_subject aag (fst slot);
1037    equiv_for (aag_can_read aag \<circ> fst) cdt s s'\<rbrakk> \<Longrightarrow>
1038    (\<exists> c. (cdt s) c = Some slot) = (\<exists> c. (cdt s') c = Some slot)"
1039  apply(rule iffI)
1040   apply(erule exE)
1041   apply(frule (2) aag_owned_cdt_link)
1042   apply(fastforce elim: equiv_forE dest: aag_can_read_self)
1043  apply(erule exE)
1044  apply(drule (2) aag_owned_cdt_link[rotated])
1045  apply(erule equiv_forE)
1046  apply(drule_tac x=c in meta_spec)
1047  apply(fastforce dest: aag_can_read_self)
1048  done
1049
1050lemma ensure_no_children_rev:
1051  "reads_equiv_valid_inv A aag (pas_refined aag and K (is_subject aag (fst slot)))
1052  (ensure_no_children slot)"
1053  unfolding ensure_no_children_def fun_app_def equiv_valid_def2
1054  apply(rule equiv_valid_rv_guard_imp)
1055   apply(rule_tac Q="\<lambda> rv s. pas_refined aag s \<and> is_subject aag (fst slot) \<and> rv = cdt s" in equiv_valid_rv_liftE_bindE[OF equiv_valid_rv_guard_imp[OF gets_cdt_revrv']])
1056     apply(rule TrueI)
1057    apply(clarsimp simp: equiv_valid_2_def)
1058    apply(drule reads_equiv_cdt_has_children)
1059       apply assumption
1060      apply assumption
1061     apply(fastforce elim: reads_equivE)
1062    apply(fastforce simp: in_whenE in_throwError)
1063   apply(wp ,simp)
1064  done
1065
1066lemma arch_derive_cap_reads_respects:
1067  "reads_respects aag l \<top> (arch_derive_cap cap)"
1068  unfolding arch_derive_cap_def
1069  apply(rule equiv_valid_guard_imp)
1070   apply(wp | wpc)+
1071  apply(simp)
1072  done
1073
1074lemma derive_cap_rev':
1075  "reads_equiv_valid_inv A aag (\<lambda> s. (\<exists>x xa xb d. cap = cap.UntypedCap d x xa xb) \<longrightarrow>
1076         pas_refined aag s \<and> is_subject aag (fst slot)) (derive_cap slot cap)"
1077  unfolding derive_cap_def arch_derive_cap_def
1078  apply(rule equiv_valid_guard_imp)
1079  apply(wp ensure_no_children_rev | wpc | simp)+
1080  done
1081
1082lemma derive_cap_rev:
1083  "reads_equiv_valid_inv A aag (\<lambda> s. pas_refined aag s \<and> is_subject aag (fst slot)) (derive_cap slot cap)"
1084  by(blast intro: equiv_valid_guard_imp[OF derive_cap_rev'])
1085
1086
1087lemma transfer_caps_loop_reads_respects:
1088  "reads_respects aag l
1089       (pas_refined aag and
1090        K ((\<forall>cap\<in>set caps. is_subject aag (fst (snd cap)) \<and>
1091                           pas_cap_cur_auth aag (fst cap)) \<and>
1092           (\<forall>slot\<in>set slots. is_subject aag (fst slot))))
1093    (transfer_caps_loop ep rcv_buffer n caps slots mi)"
1094  apply(induct caps arbitrary: slots n mi)
1095   apply simp
1096   apply(rule return_ev_pre)
1097  apply(case_tac a)
1098  apply(simp split del: if_split)
1099  apply(rule equiv_valid_guard_imp)
1100  apply(wp const_on_failure_ev
1101       | simp | intro conjI impI)+
1102       apply fast
1103      apply(wp set_extra_badge_reads_respects | simp)+
1104           apply fast
1105          apply(wp cap_insert_reads_respects cap_insert_pas_refined whenE_throwError_wp derive_cap_rev derive_cap_cap_cur_auth | simp split del: if_split | wp_once hoare_drop_imps)+
1106  apply(clarsimp simp: remove_rights_cur_auth)
1107  apply(fastforce dest: subsetD[OF set_tl_subset])
1108  done
1109
1110lemma empty_on_failure_ev:
1111  "equiv_valid_inv I A P m \<Longrightarrow>
1112  equiv_valid_inv I A P (empty_on_failure m)"
1113  unfolding empty_on_failure_def catch_def
1114  apply(wp | wpc | simp)+
1115  done
1116
1117lemma unify_failure_ev:
1118  "equiv_valid_inv I A P m \<Longrightarrow>
1119  equiv_valid_inv I A P (unify_failure m)"
1120  unfolding unify_failure_def handleE'_def
1121  apply(wp | wpc | simp)+
1122  done
1123
1124lemma lookup_slot_for_cnode_op_rev:
1125  "reads_equiv_valid_inv A aag (\<lambda>s. ((depth \<noteq> 0 \<and> depth \<le> word_bits) \<longrightarrow> (pas_refined aag s \<and> (is_cnode_cap croot \<longrightarrow> is_subject aag (obj_ref_of croot))))) (lookup_slot_for_cnode_op is_source croot ptr depth)"
1126  unfolding lookup_slot_for_cnode_op_def
1127  apply (clarsimp split del: if_split)
1128  apply (wp resolve_address_bits_rev lookup_error_on_failure_rev
1129            whenE_throwError_wp
1130       | wpc
1131       | rule hoare_post_imp_R[OF hoare_True_E_R[where P="\<top>"]]
1132       | simp add: split_def split del: if_split)+
1133  done
1134
1135lemma lookup_slot_for_cnode_op_reads_respects:
1136  "reads_respects aag l (pas_refined aag and K (is_subject aag (obj_ref_of croot))) (lookup_slot_for_cnode_op is_source croot ptr depth)"
1137  apply(rule equiv_valid_guard_imp[OF lookup_slot_for_cnode_op_rev])
1138  by simp
1139
1140lemma lookup_cap_rev:
1141  "reads_equiv_valid_inv A aag (pas_refined aag and K (is_subject aag thread)) (lookup_cap thread ref)"
1142  unfolding lookup_cap_def split_def fun_app_def
1143  apply(wp lookup_slot_for_thread_rev get_cap_rev | simp)+
1144   apply(rule lookup_slot_for_thread_authorised)
1145  apply(simp)
1146  done
1147
1148lemma captransfer_indices_in_range:
1149  "x \<in> {0..2} \<Longrightarrow>
1150  ((2::word32) + (of_nat msg_max_length + of_nat msg_max_extra_caps)) * word_size + (x * word_size) \<le> 2 ^ msg_align_bits - 1"
1151  apply(rule order_trans)
1152   prefer 2
1153   apply(rule word_less_sub_1)
1154   apply(rule_tac p=127 in mul_word_size_lt_msg_align_bits_ofnat)
1155   apply(simp add: msg_align_bits)
1156  apply(rule_tac y="0x7F * word_size" in order_trans)
1157   apply(clarsimp simp: msg_max_length_def msg_max_extra_caps_def word_size_def)
1158   apply(drule_tac k=4 in word_mult_le_mono1)
1159     apply simp
1160    apply simp
1161   apply(drule_tac x="0x1F4" in word_plus_mono_right)
1162    apply simp
1163   apply simp
1164  apply (simp add: word_size_def)
1165  done
1166
1167
1168lemma word_plus_power_2_offset_le:
1169  "\<lbrakk>is_aligned (p :: 'a :: len word) n; is_aligned q m; p < q; n \<le> m; n < len_of TYPE('a)\<rbrakk> \<Longrightarrow> p + (2^n) \<le> q"
1170  apply(drule is_aligned_weaken, assumption)
1171  apply(clarsimp simp: is_aligned_def)
1172  apply(elim dvdE)
1173  apply(rename_tac k ka)
1174  apply(rule_tac ua=0 and n="int k" and n'="int ka" in udvd_incr')
1175    apply assumption
1176  apply(clarsimp simp: uint_nat)+
1177  done
1178
1179
1180lemma is_aligned_mult_word_size:
1181  "is_aligned (p * word_size) 2"
1182  apply(rule_tac k=p in is_alignedI)
1183  apply(fastforce simp: word_size_def)
1184  done
1185
1186
1187lemma captransfer_in_ipc_buffer:
1188  "\<lbrakk>is_aligned (buffer :: word32) msg_align_bits;
1189    x \<in> {0..2}\<rbrakk> \<Longrightarrow>
1190  ptr_range (buffer + (2 + (of_nat msg_max_length + of_nat msg_max_extra_caps)) *
1191          word_size + x * word_size) 2 \<subseteq> ptr_range buffer msg_align_bits"
1192  apply(rule ptr_range_subset)
1193     apply assumption
1194    apply(simp add: msg_align_bits)
1195   apply(simp add: msg_align_bits word_bits_def)
1196  apply(simp add: word_size_def)
1197  apply(subst upto_enum_step_shift_red[where us=2, simplified])
1198     apply (simp add: msg_align_bits word_bits_def)+
1199  apply(simp add: image_def msg_max_length_def msg_max_extra_caps_def)
1200  apply(rule_tac x="(125::nat) + unat x"  in bexI)
1201   apply simp+
1202  apply(fastforce intro: unat_less_helper minus_one_helper5)
1203  done
1204
1205lemma aag_has_auth_to_read_captransfer:
1206  "\<lbrakk>ipc_buffer_has_read_auth aag (pasSubject aag) (Some buffer);
1207    x \<in> {0..2}\<rbrakk> \<Longrightarrow>
1208  for_each_byte_of_word (aag_can_read aag) (buffer + (2 + (of_nat msg_max_length + of_nat msg_max_extra_caps)) *
1209          word_size + x * word_size)"
1210  apply(simp add: for_each_byte_of_word_def2 ipc_buffer_has_read_auth_def)
1211  apply(rule ballI)
1212  apply(rule reads_read)
1213  apply(clarify)
1214  apply(erule bspec)
1215  apply(rule subsetD[OF captransfer_in_ipc_buffer])
1216     apply fastforce+
1217  done
1218
1219lemma load_cap_transfer_rev:
1220  "reads_equiv_valid_inv A aag (K (ipc_buffer_has_read_auth aag (pasSubject aag) (Some buffer)))
1221    (load_cap_transfer buffer)"
1222  unfolding load_cap_transfer_def fun_app_def captransfer_from_words_def
1223  apply(wp dmo_loadWord_rev | simp)+
1224  apply safe
1225      apply(erule aag_has_auth_to_read_captransfer[where x=0, simplified])
1226    apply(erule aag_has_auth_to_read_captransfer[where x=1, simplified])
1227  apply(erule aag_has_auth_to_read_captransfer[where x=2, simplified])
1228  done
1229
1230
1231lemma get_endpoint_rev:
1232  "reads_equiv_valid_inv A aag (K (is_subject aag ptr)) (get_endpoint ptr)"
1233  unfolding get_simple_ko_def
1234  apply(wp get_object_rev | wpc | simp)+
1235  done
1236
1237lemma send_endpoint_threads_blocked:
1238"\<lbrakk>valid_objs s; (sym_refs \<circ> state_refs_of) s;
1239  ko_at (Endpoint (SendEP list)) ep s; x\<in>set list\<rbrakk> \<Longrightarrow>
1240  st_tcb_at (send_blocked_on ep) x s"
1241  apply (rule ep_queued_st_tcb_at'')
1242  apply simp+
1243  done
1244
1245lemma send_blocked_threads_have_SyncSend_auth:
1246  "\<lbrakk>pas_refined aag s; valid_objs s; sym_refs (state_refs_of s);
1247    st_tcb_at (send_blocked_on ep) x s\<rbrakk> \<Longrightarrow>
1248  (pasObjectAbs aag x,SyncSend,pasObjectAbs aag ep) \<in> pasPolicy aag"
1249  apply(drule_tac auth="SyncSend" and x=x in pas_refined_mem[rotated])
1250   apply(rule sta_ts)
1251   apply(clarsimp simp: thread_states_def split: option.split simp: tcb_states_of_state_def st_tcb_def2)
1252   apply(case_tac "tcb_state tcb", simp_all)
1253  done
1254
1255
1256(*MOVE*)
1257lemma ev_invisible:
1258  assumes domains_distinct: "pas_domains_distinct aag"
1259  shows
1260  "\<lbrakk>labels_are_invisible aag l L; modifies_at_most aag L Q f; \<forall>s t. P s \<and> P t \<longrightarrow> (\<forall>(rva, s') \<in> fst (f s). \<forall>(rvb, t') \<in> fst(f t). W rva rvb)\<rbrakk> \<Longrightarrow>
1261  equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) W (P and Q) (P and Q) f f"
1262  apply (rule ev2_invisible[OF domains_distinct])
1263  apply simp+
1264  done
1265
1266
1267lemma get_thread_state_reads_respects:
1268  "reads_respects aag l (\<lambda> s. aag_can_read aag thread \<or> aag_can_affect aag l thread) (get_thread_state thread)"
1269  unfolding get_thread_state_def
1270  apply(rule equiv_valid_guard_imp)
1271   apply(wp thread_get_reads_respects | simp)+
1272  done
1273
1274lemma send_endpoint_reads_affects_queued:
1275  "\<lbrakk>(pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag;
1276        auth \<in> {Receive,Reset};
1277        aag_can_read_label aag (pasObjectAbs aag epptr) \<or>
1278        aag_can_affect aag l epptr;
1279        pas_refined aag s; valid_objs s; sym_refs (state_refs_of s);
1280        ko_at (Endpoint (SendEP list)) epptr s; ep = SendEP list;
1281        x \<in> set list\<rbrakk>
1282       \<Longrightarrow>
1283             aag_can_read_label aag (pasObjectAbs aag x) \<or>
1284             aag_can_affect aag l x"
1285  apply(frule send_endpoint_threads_blocked, (simp | assumption)+)
1286  apply(drule send_blocked_threads_have_SyncSend_auth, (simp | assumption)+)
1287  apply(auto dest: read_sync_ep_read_senders)
1288  done
1289
1290(*
1291lemma cancel_badged_sends_equiv_but_for_labels:
1292  "\<lbrace> pas_refined aag and valid_objs and sym_refs \<circ> state_refs_of and
1293     equiv_but_for_labels aag L st and
1294      K ({pasObjectAbs aag epptr} \<union> all_with_auth_to aag SyncSend (pasObjectAbs aag epptr) \<subseteq> L) \<rbrace>
1295     cancel_badged_sends epptr badge
1296   \<lbrace> \<lambda>_. equiv_but_for_labels aag L st \<rbrace>"
1297  unfolding cancel_badged_sends_def
1298  apply(wp set_endpoint_equiv_but_for_labels  | wpc | simp)+
1299     apply(rule_tac Q="\<lambda> r s. equiv_but_for_labels aag L st s \<and>
1300               {pasObjectAbs aag epptr} \<union> all_with_auth_to aag SyncSend (pasObjectAbs aag epptr) \<subseteq> L \<and> (\<forall>x\<in>set list. (pasObjectAbs aag x, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag)" in hoare_strengthen_post)
1301      apply(wp mapM_wp' set_thread_state_equiv_but_for_labels gts_wp  | simp add: filterM_mapM)+
1302      apply(fastforce simp: all_with_auth_to_def)
1303     apply simp
1304    apply(wp set_endpoint_equiv_but_for_labels get_simple_ko_wp | simp)+
1305  apply clarsimp
1306  apply(frule send_endpoint_threads_blocked, (simp | assumption)+)
1307  apply(drule send_blocked_threads_have_SyncSend_auth, (simp | assumption)+)
1308  done
1309*)
1310
1311(*
1312lemma cancel_badged_sends_reads_respects:
1313  shows
1314  "reads_respects aag l (pas_refined aag and valid_objs and (sym_refs \<circ> state_refs_of) and K ((pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag)) (cancel_badged_sends epptr badge)"
1315  apply (rule gen_asm_ev)+
1316  apply(case_tac "aag_can_read aag epptr \<or> aag_can_affect aag l epptr")
1317   apply(simp add: cancel_badged_sends_def fun_app_def)
1318   apply wp
1319      apply (rule_tac Q="\<lambda>s.
1320    (case rv of SendEP list \<Rightarrow> \<forall>x\<in>set list. aag_can_read aag x \<or> aag_can_affect aag l x | _ \<Rightarrow> True)" in equiv_valid_guard_imp)
1321       apply (case_tac rv)
1322         apply ((wp mapM_ev'' get_thread_state_reads_respects set_thread_state_reads_respects set_simple_ko_reads_respects get_simple_ko_reads_respects hoare_vcg_ball_lift  | wpc | simp add: filterM_mapM tcb_at_st_tcb_at[symmetric])+)
1323    apply (wp get_simple_ko_wp)
1324   apply (intro impI allI conjI)
1325    apply simp
1326   apply (case_tac ep,simp_all)
1327   apply (elim conjE, rule ballI)
1328   apply (rule send_endpoint_reads_affects_queued, (simp | assumption)+)
1329  apply(simp add: equiv_valid_def2)
1330  apply(rule equiv_valid_rv_guard_imp)
1331   apply(rule_tac Q="pas_refined aag and valid_objs and sym_refs \<circ> state_refs_of" and L="{pasObjectAbs aag epptr} \<union> all_with_auth_to aag SyncSend (pasObjectAbs aag epptr)" in ev_invisible)
1332     apply(auto dest: reads_read_queued_thread_read_ep simp: labels_are_invisible_def aag_can_affect_label_def all_with_auth_to_def)[1]
1333    apply(rule modifies_at_mostI)
1334    apply(wp cancel_badged_sends_equiv_but_for_labels | simp)+
1335  done
1336*)
1337
1338lemma mapM_ev''':
1339  assumes reads_res: "\<And> x. x \<in> set lst \<Longrightarrow> equiv_valid_inv D A (Q and P x) (m x)"
1340  assumes inv: "\<And> x. x \<in> set lst \<Longrightarrow> invariant (m x) (\<lambda> s. Q s \<and> (\<forall>x\<in>set lst. P x s))"
1341  shows "equiv_valid_inv D A (\<lambda> s. Q s \<and> (\<forall>x\<in>set lst. P x s)) (mapM m lst)"
1342  apply(rule mapM_ev)
1343  apply(rule equiv_valid_guard_imp[OF reads_res], simp+)
1344  apply(wpsimp wp: inv)
1345  done
1346
1347lemma cancel_badged_sends_reads_respects:
1348  assumes domains_distinct[wp]: "pas_domains_distinct aag"
1349  notes gts_st_tcb_at[wp del]
1350  shows
1351  "reads_respects aag l (pas_refined aag and valid_objs and (sym_refs \<circ> state_refs_of) and (\<lambda>s. is_subject aag (cur_thread s)) and K (is_subject aag epptr)) (cancel_badged_sends epptr badge)"
1352  apply (rule gen_asm_ev)+
1353  apply(simp add: cancel_badged_sends_def fun_app_def)
1354  apply wp
1355     apply ((wp mapM_ev'' mapM_wp get_thread_state_reads_respects set_thread_state_runnable_reads_respects
1356                set_simple_ko_reads_respects get_simple_ko_reads_respects hoare_vcg_ball_lift
1357                tcb_sched_action_reads_respects set_thread_state_pas_refined
1358            | wpc | simp add: filterM_mapM tcb_at_st_tcb_at[symmetric] | wp_once hoare_drop_imps | rule subset_refl | force)+)[1]
1359    apply (wp get_simple_ko_reads_respects)
1360   apply (wp get_simple_ko_wp)
1361  apply simp
1362  apply (intro conjI allI impI ballI, elim conjE)
1363  apply (rule send_endpoint_reads_affects_queued[where epptr = epptr])
1364         apply (force simp: pas_refined_def policy_wellformed_def | assumption)+
1365         done
1366
1367lemma get_cap_ret_is_subject':
1368  "\<lbrace>pas_refined aag and K (is_subject aag (fst ptr))\<rbrace> get_cap ptr
1369       \<lbrace>\<lambda>rv s. is_cnode_cap rv \<longrightarrow> (\<forall>x\<in>Access.obj_refs rv. is_subject aag x)\<rbrace>"
1370  apply(rule hoare_strengthen_post[OF get_cap_ret_is_subject])
1371  apply(clarsimp simp: is_cap_simps)
1372  done
1373
1374
1375lemma get_receive_slots_rev:
1376  "reads_equiv_valid_inv A aag (pas_refined aag and (K (is_subject aag thread \<and>
1377         ipc_buffer_has_read_auth aag (pasSubject aag) buf)))
1378   (get_receive_slots thread buf)"
1379  apply(case_tac buf)
1380   apply(fastforce intro: return_ev_pre)
1381  apply(simp add: lookup_cap_def split_def
1382       | wp empty_on_failure_ev unify_failure_ev lookup_slot_for_cnode_op_rev get_cap_rev
1383            lookup_slot_for_thread_rev lookup_slot_for_thread_authorised
1384            get_cap_ret_is_subject get_cap_ret_is_subject' load_cap_transfer_rev
1385       | wp_once hoare_drop_imps)+
1386  done
1387
1388lemma transfer_caps_reads_respects:
1389  "reads_respects aag l (pas_refined aag
1390     and K (is_subject aag receiver \<and>
1391        ipc_buffer_has_read_auth aag (pasSubject aag) receive_buffer \<and>
1392        (\<forall>cap\<in>set caps.
1393            is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap))))
1394     (transfer_caps mi caps endpoint receiver receive_buffer)"
1395  unfolding transfer_caps_def fun_app_def
1396  apply(wp transfer_caps_loop_reads_respects get_receive_slots_rev get_receive_slots_authorised
1397           hoare_vcg_all_lift static_imp_wp
1398        | wpc | simp)+
1399  done
1400
1401lemma mrs_in_ipc_buffer:
1402  "\<lbrakk>is_aligned (buf :: word32) msg_align_bits;
1403    x \<in> set [length msg_registers + 1..<Suc n];
1404    n < 2 ^ (msg_align_bits - 2)\<rbrakk>
1405       \<Longrightarrow> ptr_range
1406           (buf + of_nat x * of_nat word_size) 2 \<subseteq> ptr_range buf msg_align_bits"
1407  apply(rule ptr_range_subset)
1408     apply assumption
1409    apply(simp add: msg_align_bits)
1410   apply(simp add: msg_align_bits word_bits_def)
1411  apply(simp add: word_size_def)
1412  apply(subst upto_enum_step_shift_red[where us=2, simplified])
1413     apply (simp add: msg_align_bits word_bits_def)+
1414  apply(simp add: image_def)
1415  apply(rule_tac x=x in bexI)
1416   apply(rule refl)
1417  apply (fastforce split: if_split_asm)
1418  done
1419
1420lemma aag_has_auth_to_read_mrs:
1421  "\<lbrakk>aag_can_read_or_affect_ipc_buffer aag l (Some buf);
1422    x \<in> set [length msg_registers + 1..<Suc n];
1423    n < 2 ^ (msg_align_bits - 2)\<rbrakk>
1424       \<Longrightarrow> for_each_byte_of_word (\<lambda>x. aag_can_read_label aag (pasObjectAbs aag x) \<or> aag_can_affect aag l x)
1425           (buf + of_nat x * of_nat word_size)"
1426  apply(simp add: for_each_byte_of_word_def2 aag_can_read_or_affect_ipc_buffer_def)
1427  apply(rule ballI)
1428  apply(erule conjE)
1429  apply(erule bspec)
1430  apply(rule subsetD[OF mrs_in_ipc_buffer[where x=x and n=n]])
1431     apply assumption
1432    apply (clarsimp split: if_splits)
1433   apply assumption
1434  apply assumption
1435  done
1436
1437
1438abbreviation aag_can_read_or_affect where
1439  "aag_can_read_or_affect aag l x \<equiv>
1440    aag_can_read aag x \<or> aag_can_affect aag l x"
1441
1442lemma dmo_loadWord_reads_respects:
1443  "reads_respects aag l (K (for_each_byte_of_word (\<lambda> x. aag_can_read_or_affect aag l x) p))
1444     (do_machine_op (loadWord p))"
1445  apply(rule gen_asm_ev)
1446  apply(rule use_spec_ev)
1447  apply(rule spec_equiv_valid_hoist_guard)
1448
1449  apply(rule do_machine_op_spec_reads_respects)
1450  apply(simp add: loadWord_def equiv_valid_def2 spec_equiv_valid_def)
1451  apply(rule_tac R'="\<lambda> rv rv'. for_each_byte_of_word (\<lambda> y. rv y = rv' y) p" and Q="\<top>\<top>" and Q'="\<top>\<top>" and P="\<top>" and P'="\<top>" in equiv_valid_2_bind_pre)
1452       apply(rule_tac R'="(=)" and Q="\<lambda> r s. p && mask 2 = 0" and Q'="\<lambda> r s. p && mask 2 = 0" and P="\<top>" and P'="\<top>" in equiv_valid_2_bind_pre)
1453            apply(rule return_ev2)
1454            apply(rule_tac f="word_rcat" in arg_cong)
1455            apply(fastforce intro: is_aligned_no_wrap' word_plus_mono_right simp: is_aligned_mask for_each_byte_of_word_def) (* slow *)
1456           apply(rule assert_ev2[OF refl])
1457          apply(rule assert_wp)+
1458        apply simp+
1459       apply(clarsimp simp: equiv_valid_2_def in_monad for_each_byte_of_word_def)
1460       apply(fastforce elim: equiv_forD orthD1 simp: ptr_range_def add.commute)
1461      apply (wp wp_post_taut loadWord_inv | simp)+
1462  done
1463
1464lemma load_word_offs_reads_respects:
1465  "reads_respects aag l (\<lambda> s. for_each_byte_of_word (\<lambda> x. aag_can_read_or_affect aag l x) (a + of_nat x * of_nat word_size)) (load_word_offs a x)"
1466  unfolding load_word_offs_def fun_app_def
1467  apply(rule equiv_valid_guard_imp[OF dmo_loadWord_reads_respects])
1468  apply(clarsimp)
1469  done
1470
1471lemma as_user_reads_respects:
1472  "reads_respects aag l (K (det f \<and> aag_can_read_or_affect aag l thread)) (as_user thread f)"
1473  apply (simp add: as_user_def fun_app_def split_def)
1474  apply (rule gen_asm_ev)
1475  apply (wp set_object_reads_respects select_f_ev gets_the_ev)
1476  apply (auto intro: reads_affects_equiv_get_tcb_eq[where aag=aag])
1477  done
1478
1479lemma copy_mrs_reads_respects:
1480  assumes domains_distinct[wp]: "pas_domains_distinct aag"
1481  shows
1482  "reads_respects aag l (K (aag_can_read_or_affect aag l sender \<and> aag_can_read_or_affect_ipc_buffer aag l sbuf \<and> unat n < 2 ^ (msg_align_bits - 2))) (copy_mrs sender sbuf receiver rbuf n)"
1483  unfolding copy_mrs_def fun_app_def
1484  apply(rule gen_asm_ev)
1485  apply(wp mapM_ev'' store_word_offs_reads_respects
1486           load_word_offs_reads_respects as_user_set_register_reads_respects'
1487           as_user_reads_respects
1488       | wpc
1489       | simp add: det_setRegister det_getRegister split del: if_split)+
1490  apply clarsimp
1491  apply(rename_tac n')
1492  apply(subgoal_tac " ptr_range (x + of_nat n' * of_nat word_size) 2
1493          \<subseteq> ptr_range x msg_align_bits")
1494   apply(simp add: for_each_byte_of_word_def2)
1495   apply(simp add: aag_can_read_or_affect_ipc_buffer_def)
1496   apply(erule conjE)
1497   apply(rule ballI)
1498   apply(erule bspec)
1499   apply(erule (1) subsetD[rotated])
1500  apply(rule ptr_range_subset)
1501     apply(simp add: aag_can_read_or_affect_ipc_buffer_def)
1502    apply(simp add: msg_align_bits)
1503    apply(simp add: msg_align_bits word_bits_def)
1504   apply(simp add: word_size_def)
1505  apply(subst upto_enum_step_shift_red[where us=2, simplified])
1506     apply (simp add: msg_align_bits word_bits_def aag_can_read_or_affect_ipc_buffer_def )+
1507  apply(fastforce simp: image_def)
1508  done
1509
1510lemma get_mi_length':
1511   "\<lbrace>\<top>\<rbrace> get_message_info sender
1512    \<lbrace>\<lambda>rv s. buffer_cptr_index + unat (mi_extra_caps rv)
1513            < 2 ^ (msg_align_bits - 2)\<rbrace>"
1514  apply(rule hoare_post_imp[OF _ get_mi_valid'])
1515  apply(clarsimp simp: valid_message_info_def msg_align_bits msg_max_length_def word_le_nat_alt buffer_cptr_index_def msg_max_extra_caps_def)
1516  done
1517
1518lemma validE_E_wp_post_taut:
1519   "\<lbrace> P \<rbrace> f -, \<lbrace>\<lambda> r s. True \<rbrace>"
1520  by(auto simp: validE_E_def validE_def valid_def)
1521
1522lemma aag_has_read_auth_can_read_or_affect_ipc_buffer:
1523  "ipc_buffer_has_read_auth aag (pasSubject aag) buf \<Longrightarrow>
1524   aag_can_read_or_affect_ipc_buffer aag l buf"
1525  apply(clarsimp simp: ipc_buffer_has_read_auth_def
1526                       aag_can_read_or_affect_ipc_buffer_def
1527                 split: option.splits)
1528  apply(rule reads_read)
1529  apply blast
1530  done
1531
1532lemma ev_irrelevant_bind:
1533  assumes inv: "\<And> P. \<lbrace> P \<rbrace> f \<lbrace>\<lambda>_. P \<rbrace>"
1534  assumes ev: "equiv_valid I A A P g"
1535  shows "equiv_valid I A A P (do y \<leftarrow> f; g od)"
1536  apply(simp add: equiv_valid_def2)
1537  apply(rule equiv_valid_rv_guard_imp)
1538   apply(rule equiv_valid_2_bind)
1539      apply(rule ev[simplified equiv_valid_def2])
1540     apply(wp equiv_valid_rv_trivial[OF inv] inv | simp)+
1541  done
1542
1543lemma get_message_info_reads_respects:
1544  "reads_respects aag l (K (aag_can_read_or_affect aag l ptr)) (get_message_info ptr)"
1545  apply (simp add: get_message_info_def)
1546  apply (wp as_user_reads_respects | clarsimp simp: getRegister_def)+
1547  done
1548
1549lemma do_normal_transfer_reads_respects:
1550  assumes domains_distinct[wp]: "pas_domains_distinct aag"
1551  shows
1552  "reads_respects aag l (pas_refined aag and
1553          K (aag_can_read_or_affect aag l sender \<and>
1554             ipc_buffer_has_read_auth aag (pasObjectAbs aag sender) sbuf \<and>
1555             ipc_buffer_has_read_auth aag (pasObjectAbs aag receiver) rbuf \<and>
1556             (grant \<longrightarrow> (is_subject aag sender \<and> is_subject aag receiver))))
1557   (do_normal_transfer sender sbuf endpoint badge grant receiver rbuf)"
1558  apply(case_tac grant)
1559   apply(rule gen_asm_ev)
1560   apply(simp add: do_normal_transfer_def)
1561   apply(wp get_message_info_rev lookup_extra_caps_rev
1562            as_user_set_register_reads_respects' set_message_info_reads_respects
1563            transfer_caps_reads_respects copy_mrs_reads_respects
1564            lookup_extra_caps_rev lookup_extra_caps_authorised
1565            lookup_extra_caps_auth get_message_info_rev
1566            get_mi_length' get_mi_length validE_E_wp_post_taut
1567        | wpc
1568        | simp add: det_setRegister ball_conj_distrib)+
1569   apply (fastforce intro: aag_has_read_auth_can_read_or_affect_ipc_buffer)
1570  apply(rule gen_asm_ev)
1571  apply(simp add: do_normal_transfer_def transfer_caps_def)
1572  apply(subst transfer_caps_loop.simps)
1573  apply(wp ev_irrelevant_bind[where f="get_receive_slots receiver rbuf"]
1574           as_user_set_register_reads_respects'
1575           set_message_info_reads_respects copy_mrs_reads_respects
1576           get_message_info_reads_respects get_mi_length
1577       |wpc
1578       |simp)+
1579  apply(auto simp: ipc_buffer_has_read_auth_def aag_can_read_or_affect_ipc_buffer_def dest: reads_read_thread_read_pages split: option.splits)
1580  done
1581
1582lemma getRestartPC_det:
1583  "det getRestartPC"
1584  apply (clarsimp simp: getRestartPC_def getRegister_def)
1585  done
1586
1587lemma getRegister_det:
1588  "det (getRegister x)"
1589  by (clarsimp simp: getRegister_def)
1590
1591lemma make_fault_msg_reads_respects:
1592  "reads_respects aag l (K (aag_can_read_or_affect aag l sender)) (make_fault_msg rva sender)"
1593  apply(case_tac rva)
1594     apply (wp as_user_reads_respects
1595           | simp split del: if_split
1596                  add: getRestartPC_det getRegister_det
1597           | rule det_mapM
1598           | rule subset_refl)+
1599  apply (case_tac x4)
1600  apply (wp as_user_reads_respects
1601        | simp split del: if_split
1602               add: getRestartPC_det getRegister_det)+
1603  done
1604
1605lemma set_mrs_returns_a_constant:
1606  "\<exists> x. \<lbrace> \<top> \<rbrace> set_mrs thread buf msgs \<lbrace> \<lambda> rv s. rv = x \<rbrace>"
1607  apply(case_tac buf)
1608   apply(rule exI)
1609   apply((simp add: set_mrs_def | wp | rule impI)+)[1]
1610  apply(rule exI)
1611  apply((simp add: set_mrs_def split del: if_split | wp | rule impI)+)[1]
1612  done
1613
1614lemma set_mrs_ret_eq:
1615  "\<forall>(s::'a::state_ext state) (t::'a::state_ext state). \<forall>(rva, s')\<in>fst (set_mrs thread buf msgs s).
1616                \<forall>(rvb, t')\<in>fst (set_mrs thread  buf msgs t). rva = rvb"
1617  apply(clarsimp)
1618  apply(cut_tac thread=thread and buf=buf and msgs=msgs in set_mrs_returns_a_constant)
1619  apply(erule exE)
1620  apply(subgoal_tac "a = x \<and> aa = x")
1621   apply simp
1622  apply(rule conjI)
1623   apply(erule (1) use_valid | simp)+
1624  done
1625
1626
1627lemma set_mrs_reads_respects':
1628  assumes domains_distinct[wp]: "pas_domains_distinct aag"
1629  shows
1630  "reads_respects aag l (K (ipc_buffer_has_auth aag thread buf \<and>  (case buf of (Some buf') \<Rightarrow>
1631        is_aligned buf' msg_align_bits | _ \<Rightarrow> True))) (set_mrs thread buf msgs)"
1632  apply(case_tac "aag_can_read_or_affect aag l thread")
1633   apply((wp equiv_valid_guard_imp[OF set_mrs_reads_respects] | simp)+)[1]
1634  apply(rule gen_asm_ev)
1635  apply(simp add: equiv_valid_def2)
1636  apply(rule equiv_valid_rv_guard_imp)
1637  apply(case_tac buf)
1638   apply(rule_tac Q="\<top>" and P="\<top>" and L="{pasObjectAbs aag thread}" in ev_invisible[OF domains_distinct])
1639      apply(clarsimp simp: labels_are_invisible_def)
1640     apply(rule modifies_at_mostI)
1641     apply(simp add: set_mrs_def)
1642     apply((wp set_object_equiv_but_for_labels | simp | auto dest: get_tcb_not_asid_pool_at)+)[1]
1643    apply(simp)
1644    apply(rule set_mrs_ret_eq)
1645   apply(rename_tac buf')
1646   apply(rule_tac Q="\<top>" and L="{pasObjectAbs aag thread} \<union> (pasObjectAbs aag) ` (ptr_range buf' msg_align_bits)" in ev_invisible[OF domains_distinct])
1647     apply(auto simp: labels_are_invisible_def ipc_buffer_has_auth_def dest: reads_read_page_read_thread simp: aag_can_affect_label_def)[1]
1648    apply(rule modifies_at_mostI)
1649    apply(wp set_mrs_equiv_but_for_labels | simp)+
1650   apply(rule set_mrs_ret_eq)
1651  by simp
1652
1653lemma do_fault_transfer_reads_respects:
1654  assumes domains_distinct[wp]: "pas_domains_distinct aag"
1655  shows
1656  "reads_respects aag l (K (aag_can_read_or_affect aag l sender \<and> ipc_buffer_has_auth aag receiver buf \<and>
1657    (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits))) (do_fault_transfer badge sender receiver buf)"
1658  unfolding do_fault_transfer_def
1659  apply (wp as_user_set_register_reads_respects' as_user_reads_respects set_message_info_reads_respects
1660            set_mrs_reads_respects' make_fault_msg_reads_respects thread_get_reads_respects
1661         | wpc
1662         | simp add: split_def det_setRegister
1663         | wp_once hoare_drop_imps)+
1664  done
1665
1666
1667
1668lemma tl_tl_in_set:
1669  "tl xs = (x # xs') \<Longrightarrow> set xs' \<subseteq> set xs"
1670  apply(case_tac xs, auto)
1671  done
1672
1673(* GENERALIZE the following is possible *)
1674lemma ptr_in_obj_range:
1675  "\<lbrakk>valid_objs s; pspace_aligned s; kheap s ptr = Some obj\<rbrakk>
1676  \<Longrightarrow> ptr + (a && mask (obj_bits obj)) \<in> obj_range ptr obj"
1677  apply (simp add: obj_range_def)
1678  apply (rule context_conjI)
1679  apply (frule(1) pspace_alignedD)
1680  apply (erule is_aligned_no_wrap')
1681   apply (rule and_mask_less')
1682    apply (drule valid_obj_sizes)
1683    apply fastforce
1684   apply (simp add: word_bits_def)
1685  apply (simp add: p_assoc_help)
1686  apply (rule word_plus_mono_right)
1687   apply (rule word_less_sub_1)
1688    apply (drule valid_obj_sizes)
1689    apply fastforce
1690   apply (simp add: word_bits_def and_mask_less')
1691  apply (rule is_aligned_no_overflow')
1692  apply (erule(1) pspace_alignedD)
1693  done
1694
1695lemma do_ipc_transfer_reads_respects:
1696  assumes domains_distinct[wp]: "pas_domains_distinct aag"
1697  shows
1698  "reads_respects aag l (valid_objs and valid_global_refs and pspace_distinct and pspace_aligned
1699                         and valid_arch_state and pas_refined aag and
1700                         K ((grant \<longrightarrow> (is_subject aag sender \<and>
1701                                       is_subject aag receiver)) \<and>
1702                           aag_can_read_or_affect aag l sender \<and>
1703                           aag_can_read_or_affect aag l receiver
1704                           ))
1705     (do_ipc_transfer sender ep badge grant receiver)"
1706  unfolding do_ipc_transfer_def
1707  apply (wp do_normal_transfer_reads_respects lookup_ipc_buffer_reads_respects
1708            lookup_ipc_buffer_has_read_auth do_fault_transfer_reads_respects
1709            thread_get_reads_respects lookup_ipc_buffer_has_auth
1710            lookup_ipc_buffer_aligned
1711        | wpc
1712        | simp
1713        | wp_once hoare_drop_imps)+
1714  done
1715
1716crunch pas_cur_domain[wp]: set_extra_badge, do_ipc_transfer "pas_cur_domain aag"
1717  (wp: crunch_wps transfer_caps_loop_pres ignore: const_on_failure simp: crunch_simps)
1718
1719lemma complete_signal_reads_respects:
1720  assumes domains_distinct[wp]: "pas_domains_distinct aag"
1721  shows
1722  "reads_respects aag l ( K(aag_can_read aag ntfnptr \<or> aag_can_affect aag l ntfnptr))
1723     (complete_signal ntfnptr receiver)"
1724  unfolding complete_signal_def
1725  apply (wp set_simple_ko_reads_respects
1726            get_simple_ko_reads_respects
1727            as_user_set_register_reads_respects'
1728        | wpc
1729        | simp)+
1730  done
1731
1732lemma receive_ipc_base_reads_respects:
1733  assumes domains_distinct[wp]: "pas_domains_distinct aag"
1734  notes do_nbrecv_failed_transfer_def[simp]
1735  shows "reads_respects aag l
1736     (valid_objs
1737      and valid_global_refs
1738      and pspace_distinct and pspace_aligned
1739      and pas_refined aag
1740      and pas_cur_domain aag
1741      and valid_arch_state
1742      and ko_at (Endpoint ep) epptr
1743      and (\<lambda>s. is_subject aag (cur_thread s) \<and> sym_refs (state_refs_of s))
1744      and K (is_subject aag thread
1745             \<and> (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag))
1746     (receive_ipc_base aag thread ep epptr rights is_blocking)"
1747  apply (rule gen_asm_ev)
1748  apply (simp add: thread_get_def split: endpoint.split)
1749  apply (intro conjI impI)
1750    prefer 2 defer
1751    apply ((wp set_thread_state_reads_respects set_simple_ko_reads_respects
1752               as_user_set_register_reads_respects'
1753        | simp | intro allI impI | rule pre_ev, wpc)+)[2]
1754  apply (intro allI impI)
1755  apply (wp static_imp_wp set_simple_ko_reads_respects set_thread_state_reads_respects
1756           setup_caller_cap_reads_respects do_ipc_transfer_reads_respects
1757           possible_switch_to_reads_respects
1758           gets_cur_thread_ev set_thread_state_pas_refined
1759           | wpc
1760           | simp)+
1761           apply (rename_tac list rvc rvd)
1762           apply (rule_tac Q="\<lambda>rv s. pas_refined aag s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s) \<and>
1763                              (sender_can_grant rvd \<longrightarrow> is_subject aag (hd list))"
1764                  in hoare_strengthen_post)
1765            apply(wp set_simple_ko_reads_respects
1766                     hoare_vcg_imp_lift [OF set_simple_ko_get_tcb, unfolded disj_not1]
1767                     hoare_vcg_all_lift
1768                     set_thread_state_reads_respects get_simple_ko_reads_respects
1769                     get_simple_ko_wp do_ipc_transfer_pas_refined
1770                 | wpc | simp add: get_thread_state_def thread_get_def)+
1771  apply (clarsimp simp: conj_comms)
1772  apply (rename_tac x s)
1773  apply (rule context_conjI[rotated])
1774   apply clarsimp
1775   apply(rule conjI, rule impI)
1776    (* clagged from Ipc_AC *)
1777    apply (subgoal_tac "aag_has_auth_to aag Control (hd x)")
1778     apply (fastforce simp add: pas_refined_refl dest!: aag_Control_into_owns)
1779    apply (rule_tac ep = "pasObjectAbs aag epptr" in aag_wellformed_grant_Control_to_send [OF _ _ pas_refined_wellformed])
1780      apply (rule_tac s = s in pas_refined_mem [OF sta_ts])
1781       apply (clarsimp simp: tcb_at_def thread_states_def tcb_states_of_state_def dest!: pred_tcb_at_tcb_at)
1782       apply (frule (1) sym_refs_obj_atD)
1783       apply clarsimp
1784       apply (drule (1) bspec [OF _ hd_in_set])
1785       apply (clarsimp simp: obj_at_def tcb_bound_refs_def dest!: get_tcb_SomeD split: option.splits)
1786      apply assumption+
1787   apply(rule conjI)
1788    (* clagged from Ipc_AC *)
1789    apply (auto elim!: ep_queued_st_tcb_at
1790     simp: tcb_at_st_tcb_at valid_ep_def valid_obj_def neq_Nil_conv
1791     split: list.split)[1]
1792     apply (simp add: obj_at_def)
1793     apply (erule (1) valid_objsE)
1794     apply (fastforce simp: valid_obj_def valid_ep_def dest: distinct_drop[where i=1])
1795    apply (simp add: obj_at_def)
1796    apply (erule (1) valid_objsE)
1797    apply (fastforce simp: valid_obj_def valid_ep_def dest: distinct_drop[where i=1])
1798   apply(rule send_endpoint_reads_affects_queued, simp+)
1799         apply(fastforce dest: reads_ep)
1800        apply simp+
1801  apply(clarsimp)
1802  apply(rule_tac aag=aag and l=l in reads_affects_equiv_get_tcb_eq)
1803    apply(rule send_endpoint_reads_affects_queued)
1804            apply assumption
1805           apply blast
1806          apply(fastforce dest: reads_ep)
1807         apply assumption
1808        apply assumption
1809       apply assumption
1810      apply assumption
1811     apply(rule refl)
1812    apply simp
1813   apply simp
1814  apply simp
1815  done
1816
1817lemma receive_ipc_reads_respects:
1818  assumes domains_distinct[wp]: "pas_domains_distinct aag"
1819  shows
1820  "reads_respects aag l (valid_objs and pspace_distinct and pspace_aligned and
1821                         valid_global_refs and valid_arch_state and sym_refs \<circ> state_refs_of and
1822                         pas_refined aag and pas_cur_domain aag and valid_cap cap and (\<lambda>s. is_subject aag (cur_thread s)) and K (is_subject aag receiver \<and> (\<forall>epptr\<in>Access.obj_refs cap.
1823          (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag))) (receive_ipc receiver cap is_blocking)"
1824  apply (rule gen_asm_ev)
1825  apply (simp add: receive_ipc_def thread_get_def split: cap.split)
1826  apply (clarsimp simp: fail_ev_pre)
1827  apply (rename_tac word1 word2 rights)
1828  apply (wp receive_ipc_base_reads_respects[simplified AllowSend_def]
1829            complete_signal_reads_respects
1830        | simp)+
1831        apply (wp static_imp_wp set_simple_ko_reads_respects set_thread_state_reads_respects
1832                  setup_caller_cap_reads_respects do_ipc_transfer_reads_respects
1833                  complete_signal_reads_respects thread_get_reads_respects
1834                  get_thread_state_reads_respects
1835                  possible_switch_to_reads_respects
1836                  gets_cur_thread_ev set_thread_state_pas_refined
1837                  do_ipc_transfer_pas_refined
1838                  hoare_vcg_all_lift
1839                  get_simple_ko_reads_respects
1840                  get_bound_notification_reads_respects'
1841                  gbn_wp
1842                  get_simple_ko_reads_respects
1843                  get_simple_ko_wp
1844                  get_simple_ko_wp
1845              | wpc
1846              | simp)+
1847  apply (clarsimp)
1848  apply(rule conjI)
1849   apply(auto dest: reads_ep)[1]
1850  apply clarsimp
1851  apply(rule context_conjI, rule allI, rule impI)
1852   apply (rule disjI1)
1853   apply (frule bound_tcb_at_implies_receive)
1854    apply simp
1855   apply (frule bound_tcb_at_implies_read[where t = receiver])
1856     apply simp
1857    apply simp
1858   apply simp
1859  apply clarsimp
1860  done
1861
1862lemma receive_endpoint_threads_blocked:
1863"\<lbrakk>valid_objs s; (sym_refs \<circ> state_refs_of) s;
1864  ko_at (Endpoint (RecvEP list)) ep s; x\<in>set list\<rbrakk> \<Longrightarrow>
1865  st_tcb_at (receive_blocked_on ep) x s"
1866  apply (rule ep_queued_st_tcb_at'')
1867  apply simp+
1868  done
1869
1870lemma receive_blocked_threads_have_Receive_auth:
1871  "\<lbrakk>pas_refined aag s; valid_objs s; sym_refs (state_refs_of s);
1872    st_tcb_at (receive_blocked_on ep) x s\<rbrakk> \<Longrightarrow>
1873  (pasObjectAbs aag x,Receive,pasObjectAbs aag ep) \<in> pasPolicy aag"
1874  apply(drule_tac auth="Receive" and x=x in pas_refined_mem[rotated])
1875   apply(rule sta_ts)
1876   apply(clarsimp simp: thread_states_def split: option.split simp: tcb_states_of_state_def st_tcb_def2)
1877   apply(case_tac "tcb_state tcb", simp_all)
1878  done
1879
1880lemma receive_endpoint_reads_affects_queued:
1881  "\<lbrakk>(pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag;
1882        aag_can_read_label aag (pasObjectAbs aag epptr) \<or>
1883        aag_can_affect aag l epptr;
1884        pas_refined aag s; valid_objs s; sym_refs (state_refs_of s);
1885        ko_at (Endpoint (RecvEP list)) epptr s; ep = RecvEP list;
1886        x \<in> set list\<rbrakk>
1887       \<Longrightarrow>
1888             aag_can_read_label aag (pasObjectAbs aag x) \<or>
1889             aag_can_affect aag l x"
1890  apply(frule receive_endpoint_threads_blocked, (simp | assumption)+)
1891  apply(drule receive_blocked_threads_have_Receive_auth, (simp | assumption)+)
1892  apply(auto dest: read_sync_ep_read_receivers)
1893  done
1894
1895lemma send_ipc_reads_respects:
1896  assumes domains_distinct[wp]: "pas_domains_distinct aag"
1897  shows
1898  "reads_respects aag l (pas_refined aag and pas_cur_domain aag and valid_objs and pspace_distinct and
1899                         pspace_aligned and valid_arch_state and valid_global_refs and sym_refs \<circ> state_refs_of and
1900         (\<lambda>s. is_subject aag (cur_thread s)) and
1901         (\<lambda>s. \<exists>ep. ko_at (Endpoint ep) epptr s
1902                     \<and> (can_grant \<longrightarrow> ((\<forall>(t, rt) \<in> ep_q_refs_of ep. rt = EPRecv \<longrightarrow> is_subject aag t)
1903                                      \<and> aag_has_auth_to aag Grant epptr))) and K (is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag)) (send_ipc block call badge can_grant thread epptr)"
1904  apply(rule gen_asm_ev)
1905  apply(simp add: send_ipc_def)
1906  apply (wp set_simple_ko_reads_respects set_thread_state_reads_respects
1907            when_ev setup_caller_cap_reads_respects thread_get_reads_respects
1908        | wpc | simp split del: if_split)+
1909               apply(rename_tac list word list' rvb)
1910               apply(rule_tac Q="\<lambda>r s. is_subject aag (cur_thread s) \<and>
1911                                       (can_grant \<longrightarrow> is_subject aag (hd list))"
1912                              in hoare_strengthen_post)
1913                apply(wp set_thread_state_reads_respects
1914                         do_ipc_transfer_reads_respects
1915                         set_simple_ko_reads_respects
1916                         hoare_vcg_imp_lift [OF set_simple_ko_get_tcb, unfolded disj_not1] hoare_vcg_all_lift
1917                         get_simple_ko_reads_respects get_simple_ko_wp
1918                         possible_switch_to_reads_respects
1919                         gets_cur_thread_ev set_thread_state_pas_refined
1920                         do_ipc_transfer_pas_refined
1921                     | wpc
1922                     | simp add: get_thread_state_def thread_get_def)+
1923  apply (rule conjI)
1924   apply(fastforce dest: reads_ep)
1925  apply clarsimp
1926  apply(subgoal_tac "\<forall> s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow>
1927                      get_tcb xa s = get_tcb xa t")
1928  apply (clarsimp simp: conj_comms cong: conj_cong)
1929   apply(rule conjI)
1930    (* clagged from Ipc_AC *)
1931    apply (clarsimp simp: split_def obj_at_def)
1932   apply(rule conjI)
1933    apply (rule obj_at_valid_objsE, assumption+)
1934    apply (clarsimp cong: conj_cong imp_cong simp: tcb_at_st_tcb_at conj_comms)
1935    apply (auto dest: ep_queued_st_tcb_at [where P = \<top>] simp:  tcb_at_st_tcb_at valid_ep_def valid_obj_def obj_at_def split: list.split)[1]
1936   apply(rule receive_endpoint_reads_affects_queued)
1937           apply (assumption | simp)+
1938          apply(fastforce dest: reads_ep)
1939         apply (assumption | simp)+
1940  apply clarsimp
1941  apply(rule_tac aag=aag and l=l in reads_affects_equiv_get_tcb_eq)
1942    apply(rule receive_endpoint_reads_affects_queued)
1943           apply assumption
1944          apply(fastforce dest: reads_ep)
1945         apply assumption
1946        apply assumption
1947       apply assumption
1948      apply assumption
1949     apply(rule refl)
1950    apply simp
1951   apply simp
1952  apply simp
1953  done
1954
1955
1956subsection "Faults"
1957
1958lemma send_fault_ipc_reads_respects:
1959  assumes domains_distinct[wp]: "pas_domains_distinct aag"
1960  shows
1961  "reads_respects aag l (sym_refs \<circ> state_refs_of and pas_refined aag and pas_cur_domain aag
1962        and valid_objs and pspace_distinct and pspace_aligned
1963        and valid_global_refs and valid_arch_state and (\<lambda>s. is_subject aag (cur_thread s)) and K (is_subject aag thread \<and> valid_fault fault)) (send_fault_ipc thread fault)"
1964  apply (rule gen_asm_ev)
1965  apply (simp add: send_fault_ipc_def Let_def lookup_cap_def split_def)
1966  apply (wp send_ipc_reads_respects thread_set_reads_respects
1967            thread_set_refs_trivial thread_set_obj_at_impossible
1968            thread_set_valid_objs''
1969            hoare_vcg_conj_lift hoare_vcg_ex_lift hoare_vcg_all_lift
1970            thread_set_pas_refined cap_fault_on_failure_rev
1971            lookup_slot_for_thread_rev
1972            lookup_slot_for_thread_authorised hoare_vcg_all_lift_R
1973            thread_get_reads_respects get_cap_auth_wp[where aag=aag] get_cap_rev
1974       | wpc
1975       | simp add: split_def del: if_split add: tcb_cap_cases_def)+
1976  (* clagged from Ipc_AC *)
1977      apply (rule_tac Q'="\<lambda>rv s. pas_refined aag s
1978                          \<and> pas_cur_domain aag s
1979                          \<and> valid_objs s \<and> pspace_distinct s \<and> pspace_aligned s
1980                          \<and> valid_global_refs s \<and> valid_arch_state s
1981                          \<and> sym_refs (state_refs_of s)
1982                          \<and> valid_fault fault
1983                          \<and> is_subject aag (fst (fst rv))
1984                          \<and> is_subject aag (cur_thread s)"
1985               in hoare_post_imp_R[rotated])
1986       apply (clarsimp simp: invs_valid_objs invs_sym_refs cte_wp_at_caps_of_state
1987        | intro conjI)+
1988         apply (fastforce intro: valid_tcb_fault_update)
1989        apply (frule caps_of_state_valid_cap, assumption)
1990        apply (clarsimp simp: valid_cap_simps obj_at_def is_ep)
1991        apply rule
1992         apply clarsimp
1993         apply (subgoal_tac "\<forall>auth. aag_has_auth_to aag auth x")
1994          apply (erule (3) owns_ep_owns_receivers', simp add: obj_at_def, assumption)
1995         apply (auto dest!: pas_refined_mem[OF sta_caps]
1996                simp: cap_auth_conferred_def cap_rights_to_auth_def)[3]
1997
1998      apply (wp get_cap_auth_wp[where aag=aag] lookup_slot_for_thread_authorised
1999                thread_get_reads_respects
2000            | simp add: add: lookup_cap_def split_def)+
2001  done
2002
2003
2004lemma handle_fault_reads_respects:
2005  assumes domains_distinct[wp]: "pas_domains_distinct aag"
2006  shows
2007  "reads_respects aag l (sym_refs \<circ> state_refs_of and pas_refined aag and pas_cur_domain aag
2008  and valid_objs and pspace_distinct and pspace_aligned
2009  and valid_global_refs and valid_arch_state and (\<lambda>s. is_subject aag (cur_thread s))
2010  and K (is_subject aag thread \<and> valid_fault fault)) (handle_fault thread fault)"
2011  unfolding handle_fault_def catch_def fun_app_def handle_double_fault_def
2012  apply(wp_once hoare_drop_imps |
2013        wp set_thread_state_reads_respects send_fault_ipc_reads_respects | wpc | simp)+
2014  apply(fastforce intro: reads_affects_equiv_get_tcb_eq reads_lrefl)
2015  done
2016
2017
2018
2019subsection "Replies"
2020
2021lemma handle_arch_fault_reply_reads_respects:
2022  "reads_respects aag l (K (is_subject aag thread)) (handle_arch_fault_reply afault thread x y)"
2023  by (simp add: handle_arch_fault_reply_def, wp)
2024
2025lemma handle_fault_reply_reads_respects:
2026  "reads_respects aag l (K (is_subject aag thread)) (handle_fault_reply fault thread x y)"
2027  apply(case_tac fault)
2028     apply (wp as_user_reads_respects thread_get_reads_respects
2029               thread_get_wp' handle_arch_fault_reply_reads_respects[simplified K_def]
2030          | simp add: reads_lrefl det_zipWithM_x det_setRegister)+
2031  done
2032
2033lemma lookup_ipc_buffer_has_read_auth':
2034  "\<lbrace>pas_refined aag and valid_objs and K (is_subject aag thread)\<rbrace>
2035   lookup_ipc_buffer is_receiver thread
2036   \<lbrace>\<lambda>rv s. ipc_buffer_has_read_auth aag (pasSubject aag) rv\<rbrace>"
2037  apply(rule hoare_gen_asm)
2038  apply(rule hoare_strengthen_post[OF lookup_ipc_buffer_has_read_auth])
2039  apply(drule sym, simp)
2040  done
2041
2042
2043crunch valid_ko_at_arm[wp]: handle_fault_reply "valid_ko_at_arm"
2044
2045crunch pas_cur_domain[wp]: handle_fault_reply "pas_cur_domain aag"
2046
2047lemma do_reply_transfer_reads_respects_f:
2048  assumes domains_distinct[wp]: "pas_domains_distinct aag"
2049  shows
2050  "reads_respects_f aag l (silc_inv aag st and invs and pas_refined aag and pas_cur_domain aag and tcb_at receiver and tcb_at sender and emptyable slot and (\<lambda>s. is_subject aag (cur_thread s)) and K (is_subject aag sender \<and> is_subject aag receiver \<and> is_subject aag (fst slot))) (do_reply_transfer sender receiver slot)"
2051  unfolding do_reply_transfer_def
2052  apply (wp gets_cur_thread_ev[THEN reads_respects_f[where aag=aag and st=st and Q=\<top>]]
2053            set_thread_state_reads_respects cap_delete_one_reads_respects_f
2054            do_ipc_transfer_reads_respects do_ipc_transfer_pas_refined
2055            thread_set_reads_respects handle_fault_reply_reads_respects
2056            get_mrs_rev lookup_ipc_buffer_reads_respects
2057            lookup_ipc_buffer_has_read_auth' get_message_info_rev
2058            get_mi_length
2059            cap_delete_one_silc_inv do_ipc_transfer_silc_inv
2060            set_thread_state_pas_refined thread_set_fault_pas_refined'
2061            possible_switch_to_reads_respects[THEN reads_respects_f[where aag=aag and st=st and Q=\<top>]] when_ev
2062        | wpc | simp split del: if_split | wp_once reads_respects_f[where aag=aag and st=st] | elim conjE | assumption | simp split del: if_split cong: if_cong
2063 | wp_once hoare_drop_imps)+
2064         apply(rule_tac Q="\<lambda> rv s. pas_refined aag s \<and> pas_cur_domain aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> is_subject aag sender \<and> silc_inv aag st s \<and> is_subject aag receiver" in hoare_strengthen_post)
2065          apply((wp_once hoare_drop_imps
2066               | wp cap_delete_one_invs  hoare_vcg_all_lift
2067                    cap_delete_one_silc_inv reads_respects_f[OF thread_get_reads_respects]
2068                    reads_respects_f[OF get_thread_state_rev]
2069               | simp add: invs_valid_objs invs_psp_aligned invs_valid_global_refs invs_distinct invs_arch_state invs_valid_ko_at_arm | rule conjI | elim conjE | assumption)+)[8]
2070  apply(clarsimp simp: conj_comms)
2071  apply(rule conjI, fastforce intro: reads_lrefl)+
2072  apply(rule allI)
2073  apply(rule conjI, fastforce intro: reads_lrefl)+
2074  apply(fastforce intro: reads_lrefl)
2075  done
2076
2077lemma handle_reply_reads_respects_f:
2078  assumes domains_distinct[wp]: "pas_domains_distinct aag"
2079  shows
2080  "reads_respects_f aag l (silc_inv aag st and invs and pas_refined aag and pas_cur_domain aag and is_subject aag \<circ> cur_thread) (handle_reply)"
2081  unfolding handle_reply_def
2082  apply (wp do_reply_transfer_reads_respects_f get_cap_wp reads_respects_f[OF get_cap_reads_respects, where Q="\<top>" and st=st] hoare_vcg_all_lift | wpc | blast)+
2083  apply(rule conjI)
2084   apply(fastforce intro: requiv_cur_thread_eq simp: reads_equiv_f_def)
2085  apply clarsimp
2086  apply(rule conjI)
2087   apply assumption
2088  apply(rule conjI)
2089   apply(drule cte_wp_valid_cap)
2090    apply(erule invs_valid_objs)
2091   apply(simp add: valid_cap_simps)
2092  apply(rule conjI, fastforce simp: tcb_at_invs)
2093  apply(rule conjI)
2094   apply(erule emptyable_cte_wp_atD)
2095    apply(erule invs_valid_objs)
2096   apply(simp add: is_master_reply_cap_def)
2097  apply(frule_tac p="(cur_thread s, tcb_cnode_index 3)" in cap_cur_auth_caps_of_state[rotated])
2098    apply simp
2099   apply(simp add: cte_wp_at_caps_of_state)
2100  apply(simp add: aag_cap_auth_Reply)
2101  done
2102
2103lemma reply_from_kernel_reads_respects:
2104  assumes domains_distinct[wp]: "pas_domains_distinct aag"
2105  shows
2106  "reads_respects aag l (K (is_subject aag thread)) (reply_from_kernel thread x)"
2107  unfolding reply_from_kernel_def fun_app_def
2108  apply (wp set_message_info_reads_respects set_mrs_reads_respects
2109            as_user_reads_respects lookup_ipc_buffer_reads_respects
2110        | simp add: split_def reads_lrefl det_setRegister)+
2111  done
2112
2113
2114
2115section "globals_equiv"
2116
2117subsection "Sync IPC"
2118
2119lemma setup_caller_cap_globals_equiv:
2120  "\<lbrace>globals_equiv s and valid_ko_at_arm and valid_global_objs\<rbrace> setup_caller_cap sender receiver
2121    \<lbrace>\<lambda>_. globals_equiv s\<rbrace>"
2122  unfolding setup_caller_cap_def
2123  apply(wp cap_insert_globals_equiv'' set_thread_state_globals_equiv)
2124   apply(simp_all)
2125   done
2126
2127lemma set_extra_badge_globals_equiv:
2128  "\<lbrace>globals_equiv s \<rbrace>
2129    set_extra_badge buffer badge n
2130    \<lbrace>\<lambda>_. globals_equiv s\<rbrace>"
2131  unfolding set_extra_badge_def
2132  apply(wp store_word_offs_globals_equiv)
2133  done
2134
2135lemma transfer_caps_loop_globals_equiv:
2136  "\<lbrace>globals_equiv st and valid_ko_at_arm and valid_global_objs\<rbrace>
2137    transfer_caps_loop ep rcv_buffer n caps slots mi
2138    \<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
2139proof (induct caps arbitrary: slots n mi)
2140  case Nil
2141  thus ?case by (simp, wp, simp)
2142next
2143  case (Cons c caps')
2144  show ?case
2145    apply(cases c)
2146    apply(simp split del: if_split cong: if_cong)
2147    apply(rule hoare_pre)
2148     apply(wp)
2149       apply(erule conjE, erule subst, rule Cons.hyps)
2150      apply(clarsimp)
2151      apply(wp set_extra_badge_globals_equiv)+
2152         apply(rule Cons.hyps)
2153        apply(simp)
2154        apply(wp cap_insert_globals_equiv'')
2155       apply(rule_tac Q="\<lambda>_. globals_equiv st and valid_ko_at_arm and valid_global_objs"
2156 and
2157  E="\<lambda>_. globals_equiv st and valid_ko_at_arm and valid_global_objs" in hoare_post_impErr)
2158         apply(simp add: whenE_def, rule conjI)
2159          apply(rule impI, wp)+
2160         apply(simp)+
2161       apply wp+
2162    apply(fastforce)
2163    done
2164qed
2165
2166lemma transfer_caps_globals_equiv:
2167  "\<lbrace>globals_equiv st and valid_ko_at_arm and valid_global_objs\<rbrace>
2168    transfer_caps info caps endpoint receiver recv_buffer
2169    \<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
2170  unfolding transfer_caps_def
2171  apply(wp transfer_caps_loop_globals_equiv | wpc | simp)+
2172  done
2173
2174lemma copy_mrs_globals_equiv:
2175  "\<lbrace>globals_equiv s and valid_ko_at_arm and (\<lambda>s. receiver \<noteq> idle_thread s)\<rbrace>
2176    copy_mrs sender sbuf receiver rbuf n
2177    \<lbrace>\<lambda>_. globals_equiv s\<rbrace>"
2178  unfolding copy_mrs_def including no_pre
2179  apply(wp | wpc)+
2180    apply(rule_tac Q="\<lambda>_. globals_equiv s"
2181         in hoare_strengthen_post)
2182     apply(wp mapM_wp' | wpc)+
2183      apply(wp store_word_offs_globals_equiv)+
2184     apply fastforce
2185    apply simp
2186   apply(rule_tac Q="\<lambda>_. globals_equiv s and valid_ko_at_arm and (\<lambda>sa. receiver \<noteq> idle_thread sa)"
2187          in hoare_strengthen_post)
2188    apply(wp mapM_wp' as_user_globals_equiv)
2189    apply(simp)
2190   apply(fastforce)
2191  apply simp
2192  done
2193
2194(* FIXME: move *)
2195lemma validE_to_valid:
2196  "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>v. rv = Inr v \<longrightarrow> Q v s\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>v. Q v\<rbrace>, -"
2197  apply(rule validE_validE_R)
2198  apply(simp add: validE_def valid_def)
2199  done
2200
2201
2202lemma do_normal_transfer_globals_equiv:
2203  "\<lbrace>globals_equiv st and valid_ko_at_arm and valid_global_objs and
2204    (\<lambda>sa. receiver \<noteq> idle_thread sa)\<rbrace>
2205    do_normal_transfer sender sbuf endpoint badge grant receiver rbuf
2206    \<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
2207  unfolding do_normal_transfer_def
2208  apply(wp as_user_globals_equiv set_message_info_globals_equiv transfer_caps_globals_equiv)
2209    apply(wp copy_mrs_globals_equiv)
2210     apply(subst K_def)
2211     apply(wp | rule impI)+
2212  apply(clarsimp)
2213  done
2214
2215
2216
2217lemma do_fault_transfer_globals_equiv:
2218  "\<lbrace>globals_equiv s and valid_ko_at_arm and
2219    (\<lambda>sa. receiver \<noteq> idle_thread sa)\<rbrace>
2220      do_fault_transfer badge sender receiver buf
2221    \<lbrace>\<lambda>_. globals_equiv s\<rbrace>"
2222  unfolding do_fault_transfer_def
2223  apply(wp)
2224     apply(simp add: split_def)
2225     apply(wp as_user_globals_equiv set_message_info_globals_equiv
2226              set_mrs_globals_equiv | wpc)+
2227  apply(clarsimp)
2228  apply(rule hoare_drop_imps)
2229  apply(wp thread_get_inv, simp)
2230  done
2231
2232lemma lookup_ipc_buffer_ptr_range':
2233  "\<lbrace>valid_objs\<rbrace>
2234  lookup_ipc_buffer True thread
2235  \<lbrace>\<lambda>rv s. rv = Some buf' \<longrightarrow> auth_ipc_buffers s thread = ptr_range buf' msg_align_bits\<rbrace>"
2236  unfolding lookup_ipc_buffer_def
2237  apply (rule hoare_pre)
2238  apply (wp get_cap_wp thread_get_wp' | wpc)+
2239  apply (clarsimp simp: cte_wp_at_caps_of_state ipc_buffer_has_auth_def get_tcb_ko_at [symmetric])
2240  apply (frule caps_of_state_tcb_cap_cases [where idx = "tcb_cnode_index 4"])
2241   apply (simp add: dom_tcb_cap_cases)
2242  apply (clarsimp simp: auth_ipc_buffers_def get_tcb_ko_at [symmetric])
2243  apply (drule(1) valid_tcb_objs)
2244  apply (drule get_tcb_SomeD)+
2245  apply (simp add: vm_read_write_def valid_tcb_def valid_ipc_buffer_cap_def split: bool.splits)
2246  done
2247
2248lemma lookup_ipc_buffer_aligned':
2249  "\<lbrace>valid_objs\<rbrace> lookup_ipc_buffer True thread
2250\<lbrace>\<lambda>rv s. rv = Some buf' \<longrightarrow> is_aligned buf' msg_align_bits\<rbrace>"
2251  apply(insert lookup_ipc_buffer_aligned)
2252  apply(fastforce simp: valid_def)
2253  done
2254
2255lemma set_collection: "a = {x. x\<in>a}"
2256  by simp
2257
2258lemma do_ipc_transfer_globals_equiv:
2259  "\<lbrace>globals_equiv st and valid_ko_at_arm and valid_objs and valid_arch_state and valid_global_refs
2260    and pspace_distinct and pspace_aligned and valid_global_objs and (\<lambda>s. receiver \<noteq> idle_thread s)\<rbrace>
2261    do_ipc_transfer sender ep badge grant receiver
2262    \<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
2263  unfolding do_ipc_transfer_def
2264  apply(wp do_normal_transfer_globals_equiv do_fault_transfer_globals_equiv | wpc)+
2265    apply(rule_tac Q="\<lambda>_. globals_equiv st and valid_ko_at_arm and valid_global_objs and
2266           (\<lambda>sa. receiver \<noteq> idle_thread sa) and
2267           (\<lambda>sa. (\<forall>rb. recv_buffer = Some rb \<longrightarrow>
2268           auth_ipc_buffers sa receiver = ptr_range rb msg_align_bits) \<and>
2269           (\<forall>rb. recv_buffer = Some rb \<longrightarrow> is_aligned rb msg_align_bits))"
2270           in hoare_strengthen_post)
2271     apply(wp)
2272    apply(clarsimp | rule conjI)+
2273   apply(wp hoare_vcg_all_lift lookup_ipc_buffer_ptr_range' lookup_ipc_buffer_aligned' | fastforce)+
2274  done
2275
2276crunch valid_ko_at_arm[wp]: do_ipc_transfer "valid_ko_at_arm"
2277
2278lemma send_ipc_globals_equiv:
2279  "\<lbrace>globals_equiv st and valid_objs and valid_arch_state and valid_global_refs
2280    and pspace_distinct and pspace_aligned and valid_global_objs and valid_idle and (\<lambda>s. sym_refs (state_refs_of s))\<rbrace>
2281    send_ipc block call badge can_grant thread epptr
2282    \<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
2283  unfolding send_ipc_def
2284  apply(wp set_simple_ko_globals_equiv set_thread_state_globals_equiv
2285           setup_caller_cap_globals_equiv | wpc)+
2286         apply(rule_tac Q="\<lambda>_. globals_equiv st and valid_ko_at_arm and valid_global_objs"
2287               in hoare_strengthen_post)
2288          apply(rule thread_get_inv)
2289         apply(fastforce)
2290        apply(wp set_thread_state_globals_equiv dxo_wp_weak | simp)+
2291        apply wpc
2292      apply(wp do_ipc_transfer_globals_equiv)+
2293    apply(clarsimp)
2294    apply(rule hoare_drop_imps)
2295    apply(wp set_simple_ko_globals_equiv)+
2296  apply(rule_tac Q="\<lambda>ep. ko_at (Endpoint ep) epptr and globals_equiv st and valid_objs
2297        and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned
2298        and valid_global_objs and (\<lambda>s. sym_refs (state_refs_of s)) and valid_idle"
2299        in hoare_strengthen_post)
2300   apply(wp get_simple_ko_sp)
2301    apply(clarsimp simp: valid_arch_state_ko_at_arm)+
2302  apply (rule context_conjI)
2303   apply(rule valid_ep_recv_dequeue')
2304    apply(simp)+
2305  apply (frule_tac x=xa in receive_endpoint_threads_blocked,simp+)
2306  by (clarsimp simp add: valid_idle_def pred_tcb_at_def obj_at_def)+
2307
2308
2309lemma valid_ep_send_enqueue: "\<lbrakk>ko_at (Endpoint (SendEP (t # ts))) a s; valid_objs s\<rbrakk>
2310       \<Longrightarrow> valid_ep (case ts of [] \<Rightarrow> IdleEP | b # bs \<Rightarrow> SendEP (b # bs)) s"
2311  unfolding valid_objs_def valid_obj_def valid_ep_def obj_at_def
2312  apply (drule bspec)
2313  apply (auto split: list.splits)
2314  done
2315
2316crunch globals_equiv[wp]: complete_signal "globals_equiv st"
2317
2318
2319lemma receive_ipc_globals_equiv:
2320  notes do_nbrecv_failed_transfer_def[simp]
2321  shows "\<lbrace>globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct
2322     and pspace_aligned and valid_global_objs and (\<lambda>s. thread \<noteq> idle_thread s)\<rbrace>
2323     receive_ipc thread cap is_blocking
2324    \<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
2325  unfolding receive_ipc_def thread_get_def including no_pre
2326  apply(wp)
2327   apply(simp add: split_def)
2328   apply(wp set_simple_ko_globals_equiv set_thread_state_globals_equiv
2329             setup_caller_cap_globals_equiv dxo_wp_weak as_user_globals_equiv
2330       | wpc
2331       | simp split del: if_split)+
2332             apply (rule hoare_strengthen_post[where Q= "\<lambda>_. globals_equiv st and valid_ko_at_arm and valid_global_objs"])
2333              apply (wp do_ipc_transfer_globals_equiv as_user_globals_equiv)
2334             apply clarsimp
2335            apply (wp gts_wp get_simple_ko_sp | wpc)+
2336          apply (wp hoare_vcg_all_lift hoare_drop_imps)[1]
2337           apply(wp set_simple_ko_globals_equiv | wpc)+
2338       apply(wp set_thread_state_globals_equiv)
2339      apply (wp get_simple_ko_wp gbn_wp get_simple_ko_wp as_user_globals_equiv | wpc | simp)+
2340  apply (rule hoare_pre)
2341   apply(wpc)
2342              apply(rule fail_wp | rule return_wp)+
2343  by (auto intro: valid_arch_state_ko_at_arm valid_ep_send_enqueue
2344          simp: neq_Nil_conv cong: case_list_cons_cong)
2345
2346
2347subsection "Notifications"
2348
2349lemma valid_ntfn_dequeue:
2350  "\<lbrakk> ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = (WaitingNtfn (t # ts));
2351     valid_objs s; ts \<noteq> []\<rbrakk>
2352     \<Longrightarrow> valid_ntfn ntfn s"
2353  unfolding valid_objs_def valid_obj_def valid_ntfn_def obj_at_def
2354  apply (drule bspec)
2355  apply (auto split: list.splits)
2356  done
2357
2358
2359(* FIXME: NTFN OBJECT CHANGED *)
2360
2361lemma update_waiting_ntfn_globals_equiv:
2362  "\<lbrace>globals_equiv s and valid_objs and valid_arch_state and valid_global_refs and ko_at (Notification ntfn) ntfnptr and pspace_distinct and sym_refs \<circ> state_refs_of and (\<lambda>s. idle_thread s \<notin> set queue) and K (ntfn_obj ntfn = WaitingNtfn queue)\<rbrace>
2363    update_waiting_ntfn ntfnptr queue bound_tcb badge
2364    \<lbrace>\<lambda>_. globals_equiv s\<rbrace>"
2365  unfolding update_waiting_ntfn_def
2366  apply(wp)
2367    apply(simp add: split_def)
2368    apply(wp set_thread_state_globals_equiv as_user_globals_equiv
2369             set_notification_globals_equiv set_notification_valid_ko_at_arm
2370             dxo_wp_weak | simp)+
2371  by (auto intro: valid_arch_state_ko_at_arm simp: neq_Nil_conv)
2372
2373lemma
2374  blocked_cancel_ipc_globals_equiv[wp]:
2375  "\<lbrace>globals_equiv st and valid_ko_at_arm\<rbrace> blocked_cancel_ipc a b \<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
2376  unfolding blocked_cancel_ipc_def
2377  by (wp set_thread_state_globals_equiv set_simple_ko_globals_equiv | wpc | simp)+
2378
2379
2380
2381
2382lemma cancel_ipc_blocked_globals_equiv:
2383  "\<lbrace>globals_equiv st and valid_ko_at_arm and st_tcb_at receive_blocked a\<rbrace>
2384    cancel_ipc a \<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
2385  unfolding cancel_ipc_def
2386  apply (rule hoare_seq_ext[OF _ gts_sp])
2387  apply (rule hoare_pre)
2388  apply (wpc; (simp,rule blocked_cancel_ipc_globals_equiv)?)
2389  apply (rule hoare_pre_cont)+
2390  apply clarsimp
2391  apply (case_tac state;(clarsimp simp: pred_tcb_at_def obj_at_def receive_blocked_def))
2392  by (simp add: eq_commute)
2393
2394
2395crunch globals_equiv[wp]: possible_switch_to "globals_equiv (st :: det_ext state)"
2396  (wp: tcb_sched_action_extended.globals_equiv reschedule_required_ext_extended.globals_equiv
2397       crunch_wps)
2398
2399lemma send_signal_globals_equiv:
2400  "\<lbrace>globals_equiv (s :: det_ext state) and valid_objs and valid_arch_state
2401     and valid_global_refs and sym_refs \<circ> state_refs_of and
2402     pspace_distinct and valid_idle\<rbrace> send_signal ntfnptr badge
2403    \<lbrace>\<lambda>_. globals_equiv s\<rbrace>"
2404  unfolding send_signal_def
2405  apply (wp set_notification_globals_equiv
2406            possible_switch_to_globals_equiv
2407            set_thread_state_globals_equiv
2408            as_user_globals_equiv
2409            cancel_ipc_blocked_globals_equiv
2410            update_waiting_ntfn_globals_equiv
2411            get_simple_ko_wp
2412            gts_wp
2413       | wpc
2414       | simp)+
2415  apply clarsimp
2416  apply (frule (1) sym_refs_ko_atD)
2417  apply (intro allI impI conjI)
2418           prefer 8
2419           apply clarsimp
2420           apply (frule_tac t="idle_thread sa" and P="\<lambda>ref. \<not> idle ref" in ntfn_queued_st_tcb_at')
2421               by (auto intro: valid_arch_state_ko_at_arm
2422                         simp: pred_tcb_at_def obj_at_def valid_idle_def receive_blocked_def)
2423
2424(*FIXME: belongs in Arch_IF*)
2425
2426lemma receive_signal_globals_equiv:
2427  "\<lbrace>globals_equiv s and valid_objs and valid_arch_state and valid_global_refs
2428     and pspace_distinct and (\<lambda>s. thread \<noteq> idle_thread s)\<rbrace>
2429     receive_signal thread cap is_blocking
2430    \<lbrace>\<lambda>_. globals_equiv s\<rbrace>"
2431  unfolding receive_signal_def fun_app_def do_nbrecv_failed_transfer_def
2432  apply (rule hoare_pre)
2433  apply(wp set_notification_globals_equiv set_thread_state_globals_equiv
2434           as_user_globals_equiv get_simple_ko_wp
2435       | wpc)+
2436   apply(simp add: valid_arch_state_ko_at_arm)
2437  done
2438
2439lemma set_object_valid_global_refs:
2440  "\<lbrace>valid_global_refs and (\<lambda>s. \<forall>b. (\<forall>sz fun. obj=CNode sz fun \<longrightarrow> well_formed_cnode_n sz fun \<longrightarrow> (\<forall>cap. fun b = Some cap \<longrightarrow> global_refs s \<inter> cap_range cap = {})) \<and> (\<forall>tcb. obj = (TCB tcb) \<longrightarrow> (\<forall>get. (\<forall>set restr. tcb_cap_cases b \<noteq> Some (get, set, restr) \<or> global_refs s \<inter> cap_range(get tcb) = {}))))\<rbrace> set_object ptr obj
2441    \<lbrace>\<lambda>_. valid_global_refs\<rbrace>"
2442   unfolding set_object_def valid_global_refs_def valid_refs_def
2443   apply(clarsimp simp: cte_wp_at_cases)
2444   apply(wp)
2445   apply(clarify)
2446   apply(rule conjI)
2447    apply(clarsimp)
2448   apply(clarsimp)
2449   apply(erule_tac x=b in allE)
2450   apply(erule_tac x=get in allE)
2451   apply(simp)
2452   done
2453
2454
2455lemma send_fault_ipc_globals_equiv:
2456  "\<lbrace>globals_equiv st and valid_objs and valid_arch_state and valid_global_refs
2457    and pspace_distinct and pspace_aligned
2458    and valid_global_objs and valid_idle and (\<lambda>s. sym_refs (state_refs_of s)) and K (valid_fault fault)\<rbrace>
2459    send_fault_ipc tptr fault
2460    \<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
2461  unfolding send_fault_ipc_def
2462  apply(wp)
2463    apply(simp add: Let_def)
2464    apply(wp send_ipc_globals_equiv thread_set_globals_equiv thread_set_valid_objs'' thread_set_fault_valid_global_refs thread_set_valid_idle_trivial thread_set_refs_trivial | wpc | simp)+
2465   apply(rule_tac Q'="\<lambda>_. globals_equiv st and valid_objs and valid_arch_state and valid_global_refs
2466        and pspace_distinct and pspace_aligned and
2467        valid_global_objs and K (valid_fault fault) and valid_idle and (\<lambda>s. sym_refs (state_refs_of s))"
2468        in hoare_post_imp_R)
2469    apply(wp | simp)+
2470   apply(clarsimp simp: valid_arch_state_ko_at_arm)
2471   apply(rule valid_tcb_fault_update)
2472    apply(wp | simp)+
2473    done
2474
2475lemma handle_double_fault_globals_equiv:
2476  "\<lbrace>globals_equiv s and valid_ko_at_arm\<rbrace> handle_double_fault tptr ex1 ex2
2477    \<lbrace>\<lambda>_. globals_equiv s\<rbrace>"
2478  unfolding handle_double_fault_def
2479  by (wp set_thread_state_globals_equiv)
2480
2481lemma send_ipc_valid_global_objs:
2482  "\<lbrace>valid_global_objs \<rbrace> send_ipc block call badge can_grant thread epptr
2483    \<lbrace>\<lambda>_. valid_global_objs\<rbrace>"
2484  unfolding send_ipc_def
2485  apply(wp | wpc)+
2486         apply(rule_tac Q="\<lambda>_. valid_global_objs" in hoare_strengthen_post)
2487          apply(wp, simp, (wp dxo_wp_weak |simp)+)
2488      apply(wpc)
2489             apply(rule fail_wp | rule return_wp | wp)+
2490     apply(simp)
2491     apply(rule hoare_drop_imps)
2492     apply(wp)+
2493   apply(rule_tac Q="\<lambda>_. valid_global_objs" in hoare_strengthen_post)
2494    apply(wp, simp+)
2495  done
2496
2497lemma send_fault_ipc_valid_global_objs:
2498  "\<lbrace>valid_global_objs \<rbrace> send_fault_ipc tptr fault
2499    \<lbrace>\<lambda>_. valid_global_objs\<rbrace>"
2500  unfolding send_fault_ipc_def
2501  apply(wp)
2502     apply(simp add: Let_def)
2503     apply(wp send_ipc_valid_global_objs | wpc)+
2504    apply(rule_tac Q'="\<lambda>_. valid_global_objs" in hoare_post_imp_R)
2505     apply(wp | simp)+
2506  done
2507
2508crunch valid_ko_at_arm[wp]: send_ipc "valid_ko_at_arm"
2509  (wp: hoare_drop_imps hoare_vcg_if_lift2 dxo_wp_weak)
2510
2511lemma send_fault_ipc_valid_ko_at_arm[wp]:
2512  "invariant (send_fault_ipc a b) valid_ko_at_arm"
2513  unfolding send_fault_ipc_def
2514  apply wp
2515    apply(simp add: Let_def)
2516    apply (wp send_ipc_valid_ko_at_arm | wpc)+
2517   apply(rule_tac Q'="\<lambda>_. valid_ko_at_arm" in hoare_post_imp_R)
2518  apply (wp | simp)+
2519done
2520
2521lemma handle_fault_globals_equiv:
2522  "\<lbrace>globals_equiv st and valid_objs and valid_arch_state and valid_global_refs
2523    and pspace_distinct and pspace_aligned
2524    and valid_global_objs and valid_idle and (\<lambda>s. sym_refs (state_refs_of s))
2525    and K (valid_fault ex)\<rbrace> handle_fault thread ex
2526    \<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
2527  unfolding handle_fault_def
2528  apply(wp handle_double_fault_globals_equiv)
2529   apply(rule_tac Q="\<lambda>_. globals_equiv st and valid_ko_at_arm" and
2530             E="\<lambda>_. globals_equiv st and valid_ko_at_arm" in hoare_post_impErr)
2531     apply(wp send_fault_ipc_globals_equiv
2532          | simp add: valid_arch_state_ko_at_arm)+
2533     done
2534
2535
2536lemma handle_fault_reply_globals_equiv:
2537  "\<lbrace>globals_equiv st and valid_ko_at_arm and (\<lambda>s. thread \<noteq> idle_thread s)\<rbrace> handle_fault_reply fault thread x y
2538    \<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
2539  apply(case_tac fault)
2540     apply(wp as_user_globals_equiv | simp add: handle_arch_fault_reply_def)+
2541     done
2542
2543crunch valid_global_objs: handle_fault_reply "valid_global_objs"
2544
2545lemma do_reply_transfer_globals_equiv:
2546  "\<lbrace>globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct
2547    and pspace_aligned and valid_global_objs and valid_idle\<rbrace>
2548    do_reply_transfer sender receiver slot
2549    \<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
2550  unfolding do_reply_transfer_def
2551  apply(wp set_thread_state_globals_equiv cap_delete_one_globals_equiv  do_ipc_transfer_globals_equiv
2552    thread_set_globals_equiv handle_fault_reply_globals_equiv dxo_wp_weak | wpc | simp split del: if_split)+
2553    apply(rule_tac Q="\<lambda>_. globals_equiv st and valid_ko_at_arm and valid_objs and valid_arch_state
2554      and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and (\<lambda>s. receiver \<noteq> idle_thread s) and valid_idle" in hoare_strengthen_post)
2555    apply (wp gts_wp | fastforce simp: valid_arch_state_ko_at_arm pred_tcb_at_def obj_at_def valid_idle_def)+
2556    done
2557
2558lemma handle_reply_globals_equiv:
2559  "\<lbrace>globals_equiv st and valid_objs and valid_arch_state and valid_global_refs
2560    and pspace_distinct and pspace_aligned and valid_global_objs and valid_idle\<rbrace> handle_reply
2561    \<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
2562  unfolding handle_reply_def
2563  apply(wp do_reply_transfer_globals_equiv | wpc)+
2564   apply(rule_tac Q="\<lambda>_. globals_equiv st and valid_objs and valid_arch_state and valid_global_refs
2565        and pspace_distinct and pspace_aligned and valid_global_objs and valid_idle"
2566        in hoare_strengthen_post)
2567    apply(wp | simp)+
2568    done
2569
2570lemma reply_from_kernel_globals_equiv:
2571  "\<lbrace>globals_equiv s and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct
2572   and pspace_aligned and  (\<lambda>s. thread \<noteq> idle_thread s)\<rbrace> reply_from_kernel thread x
2573    \<lbrace>\<lambda>_. globals_equiv s\<rbrace>"
2574  unfolding reply_from_kernel_def
2575  apply(wp set_message_info_globals_equiv set_mrs_globals_equiv
2576           as_user_globals_equiv | simp add: split_def)+
2577  apply(insert length_msg_lt_msg_max)
2578  apply(simp add: valid_arch_state_ko_at_arm)
2579  done
2580
2581section "reads_respects_g"
2582
2583subsection "Notifications"
2584
2585lemma send_signal_reads_respects_g:
2586  assumes domains_distinct: "pas_domains_distinct aag"
2587  shows
2588  "reads_respects_g aag l (pas_refined aag and pas_cur_domain aag and valid_etcbs and
2589      valid_objs and valid_global_objs and valid_arch_state and valid_global_refs and
2590      pspace_distinct and valid_idle and sym_refs \<circ> state_refs_of and ct_active and
2591      is_subject aag \<circ> cur_thread and K ((pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag)) (send_signal ntfnptr badge)"
2592  apply(rule equiv_valid_guard_imp[OF reads_respects_g])
2593    apply(rule send_signal_reads_respects[OF domains_distinct])
2594   apply(rule doesnt_touch_globalsI)
2595   apply(wp send_signal_globals_equiv | simp)+
2596  done
2597
2598lemma receive_signal_reads_respects_g:
2599  assumes domains_distinct: "pas_domains_distinct aag"
2600  shows
2601  "reads_respects_g aag l (valid_global_objs and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pas_refined aag and (\<lambda>s. thread \<noteq> idle_thread s) and is_subject aag \<circ> cur_thread and K ((\<forall>ntfnptr\<in>Access.obj_refs cap.
2602          (pasSubject aag, Receive, pasObjectAbs aag ntfnptr)
2603          \<in> pasPolicy aag \<and>
2604      is_subject aag thread))) (receive_signal thread cap is_blocking)"
2605  apply(rule equiv_valid_guard_imp[OF reads_respects_g])
2606    apply(rule receive_signal_reads_respects[OF domains_distinct])
2607   apply(rule doesnt_touch_globalsI)
2608   apply(wp receive_signal_globals_equiv | simp)+
2609  done
2610
2611subsection "Sycn IPC"
2612
2613lemma send_ipc_reads_respects_g:
2614  assumes domains_distinct: "pas_domains_distinct aag"
2615  shows
2616  "reads_respects_g aag l (pas_refined aag and pas_cur_domain aag and valid_objs and valid_global_objs
2617     and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned
2618     and valid_idle and sym_refs \<circ> state_refs_of and is_subject aag \<circ> cur_thread and (\<lambda> s. \<exists>ep. ko_at (Endpoint ep) epptr s \<and>
2619             (can_grant \<longrightarrow>
2620              (\<forall>x\<in>ep_q_refs_of ep.
2621                  (\<lambda>(t, rt). rt = EPRecv \<longrightarrow> is_subject aag t) x) \<and>
2622              (pasSubject aag, Grant, pasObjectAbs aag epptr)
2623              \<in> pasPolicy aag)) and K (is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag)) (send_ipc block call badge can_grant thread epptr)"
2624  apply(rule equiv_valid_guard_imp[OF reads_respects_g])
2625    apply(rule send_ipc_reads_respects[OF domains_distinct])
2626   apply(rule doesnt_touch_globalsI)
2627   apply(wp send_ipc_globals_equiv | simp)+
2628  done
2629
2630lemma receive_ipc_reads_respects_g:
2631  assumes domains_distinct: "pas_domains_distinct aag"
2632  shows
2633  "reads_respects_g aag l (valid_objs and valid_global_objs and valid_arch_state and valid_global_refs
2634    and pspace_distinct and pspace_aligned and (\<lambda>s. receiver \<noteq> idle_thread s) and sym_refs \<circ> state_refs_of and pas_refined aag and pas_cur_domain aag and valid_cap cap and is_subject aag \<circ> cur_thread and K (is_subject aag receiver \<and> (\<forall>epptr\<in>Access.obj_refs cap.
2635          (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag))) (receive_ipc receiver cap is_blocking)"
2636  apply(rule equiv_valid_guard_imp[OF reads_respects_g])
2637    apply(rule receive_ipc_reads_respects[OF domains_distinct])
2638   apply(rule doesnt_touch_globalsI)
2639   apply(wp receive_ipc_globals_equiv | simp)+
2640  done
2641
2642
2643subsection "Faults"
2644
2645lemma send_fault_ipc_reads_respects_g:
2646  assumes domains_distinct: "pas_domains_distinct aag"
2647  shows
2648  "reads_respects_g aag l (sym_refs \<circ> state_refs_of and pas_refined aag and pas_cur_domain aag and valid_objs and valid_global_objs and valid_arch_state and valid_global_refs
2649    and pspace_distinct and pspace_aligned and valid_idle and is_subject aag \<circ> cur_thread and K (is_subject aag thread \<and> valid_fault fault)) (send_fault_ipc thread fault)"
2650  apply(rule equiv_valid_guard_imp[OF reads_respects_g])
2651    apply(rule send_fault_ipc_reads_respects[OF domains_distinct])
2652   apply(rule doesnt_touch_globalsI)
2653   apply(wp send_fault_ipc_globals_equiv | simp)+
2654  done
2655
2656
2657lemma handle_fault_reads_respects_g:
2658  assumes domains_distinct: "pas_domains_distinct aag"
2659  shows
2660  "reads_respects_g aag l (sym_refs \<circ> state_refs_of and pas_refined aag and pas_cur_domain aag
2661    and valid_objs and valid_global_objs and valid_arch_state and valid_global_refs
2662    and pspace_distinct and pspace_aligned and valid_idle and is_subject aag \<circ> cur_thread and K (is_subject aag thread \<and> valid_fault fault)) (handle_fault thread fault)"
2663  apply(rule equiv_valid_guard_imp[OF reads_respects_g])
2664    apply(rule handle_fault_reads_respects[OF domains_distinct])
2665   apply(rule doesnt_touch_globalsI)
2666   apply(wp handle_fault_globals_equiv | simp)+
2667  done
2668
2669subsection "Replies"
2670
2671lemma handle_fault_reply_reads_respects_g:
2672  "reads_respects_g aag l (valid_ko_at_arm and (\<lambda>s. thread \<noteq> idle_thread s) and K (is_subject aag thread)) (handle_fault_reply fault thread x y)"
2673  apply(rule equiv_valid_guard_imp[OF reads_respects_g])
2674    apply(rule handle_fault_reply_reads_respects)
2675   apply(rule doesnt_touch_globalsI)
2676   apply(wp handle_fault_reply_globals_equiv | simp)+
2677  done
2678
2679lemma do_reply_transfer_reads_respects_f_g:
2680  assumes domains_distinct: "pas_domains_distinct aag"
2681  shows
2682  "reads_respects_f_g aag l (silc_inv aag st and invs and pas_refined aag and pas_cur_domain aag and tcb_at receiver and tcb_at sender and emptyable slot and is_subject aag \<circ> cur_thread and K (is_subject aag sender \<and> is_subject aag receiver \<and> is_subject aag (fst slot))) (do_reply_transfer sender receiver slot)"
2683  apply(rule equiv_valid_guard_imp[OF reads_respects_f_g])
2684    apply(rule do_reply_transfer_reads_respects_f[OF domains_distinct])
2685   apply(rule doesnt_touch_globalsI)
2686   apply(wp do_reply_transfer_globals_equiv | simp)+
2687  apply(simp add: invs_def valid_state_def valid_pspace_def | blast)+
2688  done
2689
2690lemma handle_reply_reads_respects_g:
2691  assumes domains_distinct: "pas_domains_distinct aag"
2692  shows
2693  "reads_respects_f_g aag l (silc_inv aag st and invs and
2694        pas_refined aag and pas_cur_domain aag and
2695        is_subject aag \<circ> cur_thread) (handle_reply)"
2696  apply(rule equiv_valid_guard_imp[OF reads_respects_f_g])
2697    apply(rule handle_reply_reads_respects_f[OF domains_distinct])
2698   apply(rule doesnt_touch_globalsI)
2699   apply(wp handle_reply_globals_equiv | simp)+
2700  apply(simp add: invs_def valid_state_def valid_pspace_def | blast)+
2701  done
2702
2703lemma reply_from_kernel_reads_respects_g:
2704  assumes domains_distinct: "pas_domains_distinct aag"
2705  shows
2706  "reads_respects_g aag l (valid_global_objs and
2707        valid_objs and valid_arch_state and valid_global_refs and pspace_distinct
2708        and pspace_aligned and (\<lambda>s. thread \<noteq> idle_thread s) and K (is_subject aag thread)) (reply_from_kernel thread x)"
2709  apply(rule equiv_valid_guard_imp[OF reads_respects_g])
2710    apply(rule reply_from_kernel_reads_respects[OF domains_distinct])
2711   apply(rule doesnt_touch_globalsI)
2712   apply(wp reply_from_kernel_globals_equiv | simp)+
2713  done
2714
2715end
2716
2717end
2718