1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: GPL-2.0-only
5 *)
6
7theory Ipc_AC
8imports Finalise_AC "Lib.MonadicRewrite"
9begin
10
11context begin interpretation Arch . (*FIXME: arch_split*)
12
13section\<open>Notifications\<close>
14
15subsection\<open>@{term "pas_refined"}\<close>
16
17crunch thread_bound_ntfns[wp]: do_machine_op "\<lambda>s. P (thread_bound_ntfns s)"
18
19crunches deleted_irq_handler, send_signal
20  for state_vrefs[wp]: "\<lambda>s. P (state_vrefs (s :: det_ext state))"
21  (wp: crunch_wps hoare_unless_wp select_wp dxo_wp_weak simp: crunch_simps)
22
23lemma cancel_ipc_receive_blocked_caps_of_state:
24  "\<lbrace>\<lambda>s. P (caps_of_state (s :: det_ext state)) \<and> st_tcb_at receive_blocked t s\<rbrace> cancel_ipc t \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace>"
25  apply (clarsimp simp: cancel_ipc_def)
26  apply (rule hoare_seq_ext[OF _ gts_sp])
27  apply (rule hoare_pre)
28  apply (wp gts_wp | wpc | simp)+
29     apply (rule hoare_pre_cont)+
30  apply (clarsimp simp: st_tcb_def2 receive_blocked_def)
31  apply (clarsimp split: thread_state.splits)
32  done
33
34lemma send_signal_caps_of_state[wp]:
35  "\<lbrace>\<lambda>s :: det_ext state. P (caps_of_state s) \<rbrace> send_signal ntfnptr badge \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>"
36  apply (clarsimp simp: send_signal_def)
37  apply (rule hoare_seq_ext[OF _ get_simple_ko_sp])
38  apply (rule hoare_pre)
39   apply (wp dxo_wp_weak cancel_ipc_receive_blocked_caps_of_state gts_wp static_imp_wp | wpc | simp add: update_waiting_ntfn_def)+
40  apply (clarsimp simp: fun_upd_def[symmetric] st_tcb_def2)
41  done
42
43crunches deleted_irq_handler, send_signal
44  for arch_state[wp]: "\<lambda>s. P (arch_state (s :: det_ext state))"
45  (wp: crunch_wps hoare_unless_wp select_wp dxo_wp_weak simp: crunch_simps)
46
47crunch mdb[wp]: blocked_cancel_ipc, update_waiting_ntfn "\<lambda>s. P (cdt (s :: det_ext state))" (wp: crunch_wps hoare_unless_wp select_wp dxo_wp_weak simp: crunch_simps)
48
49lemma cancel_ipc_receive_blocked_mdb:
50  "\<lbrace>\<lambda>s. P (cdt (s :: det_ext state)) \<and> st_tcb_at receive_blocked t s\<rbrace> cancel_ipc t \<lbrace>\<lambda>rv s. P (cdt s)\<rbrace>"
51  apply (clarsimp simp: cancel_ipc_def)
52  apply (rule hoare_seq_ext[OF _ gts_sp])
53  apply (rule hoare_pre)
54  apply (wp gts_wp | wpc | simp)+
55     apply (rule hoare_pre_cont)+
56  apply (clarsimp simp: st_tcb_def2 receive_blocked_def)
57  apply (clarsimp split: thread_state.splits)
58  done
59
60lemma send_signal_mdb[wp]:
61  "\<lbrace>\<lambda>s. P (cdt (s :: det_ext state))\<rbrace> send_signal ntfnptr badge \<lbrace>\<lambda>rv s. P (cdt s)\<rbrace>"
62  apply (clarsimp simp: send_signal_def)
63  apply (rule hoare_seq_ext[OF _ get_simple_ko_sp])
64  apply (rule hoare_pre)
65   apply (wp dxo_wp_weak gts_wp cancel_ipc_receive_blocked_mdb | wpc | simp)+
66  apply (clarsimp simp: st_tcb_def2)
67  done
68
69crunches possible_switch_to
70  for tcb_domain_map_wellformed[wp]: "tcb_domain_map_wellformed aag"
71
72lemma update_waiting_ntfn_pas_refined:
73  "\<lbrace>pas_refined aag and ko_at (Notification ntfn) ntfnptr and K (ntfn_obj ntfn = WaitingNtfn queue)\<rbrace>
74     update_waiting_ntfn ntfnptr queue badge val
75   \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>"
76  apply (simp add: update_waiting_ntfn_def)
77  apply (wp set_thread_state_pas_refined set_simple_ko_pas_refined | simp)+
78  done
79
80lemma cancel_ipc_receive_blocked_pas_refined:
81  "\<lbrace>pas_refined aag and st_tcb_at receive_blocked t\<rbrace> cancel_ipc t \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>"
82  apply (clarsimp simp: cancel_ipc_def)
83  apply (rule hoare_seq_ext[OF _ gts_sp])
84  apply (rule hoare_pre)
85  apply (wp gts_wp | wpc | simp)+
86  apply (clarsimp simp: st_tcb_def2 receive_blocked_def)
87  done
88
89lemma send_signal_pas_refined:
90  "\<lbrace>\<lambda>s. pas_refined aag s\<rbrace> send_signal ntfnptr badge \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>"
91  apply (simp add: send_signal_def)
92  apply (rule hoare_seq_ext[OF _ get_simple_ko_sp])
93  apply (rule hoare_pre)
94  apply (wp set_simple_ko_pas_refined update_waiting_ntfn_pas_refined gts_wp set_thread_state_pas_refined
95            cancel_ipc_receive_blocked_pas_refined
96       | wpc
97       | simp)+
98  apply clarsimp
99  apply (fastforce simp: st_tcb_def2)
100  done
101
102lemma receive_signal_pas_refined:
103  "\<lbrace>pas_refined aag and K (\<forall>ntfnptr \<in> obj_refs cap. (pasObjectAbs aag thread, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag)\<rbrace>
104     receive_signal thread cap is_blocking
105   \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>"
106  apply (simp add: receive_signal_def)
107  apply (cases cap, simp_all)
108  apply (rule hoare_seq_ext [OF _ get_simple_ko_sp])
109  apply (rule hoare_pre)
110  by (wp set_simple_ko_pas_refined set_thread_state_pas_refined
111       | wpc | simp add: do_nbrecv_failed_transfer_def)+
112
113
114subsection\<open>integrity\<close>
115
116subsubsection\<open>autarchy\<close>
117
118text\<open>
119  For the case when the currently-running thread owns the receiver
120  (i.e. receiver last to the notification rendezvous or sender owns
121  receiver).
122\<close>
123
124lemma st_tcb_at_tcb_states_of_state:
125  "(st_tcb_at stf p s) = (\<exists>st. tcb_states_of_state s p = Some st \<and> stf st)"
126  unfolding tcb_states_of_state_def st_tcb_def2 by auto
127
128lemma st_tcb_at_tcb_states_of_state_eq:
129  "(st_tcb_at ((=) st) p s) = (tcb_states_of_state s p = Some st)"
130  unfolding tcb_states_of_state_def st_tcb_def2 by auto
131
132lemma kheap_auth_ipc_buffer_same:
133  "kheap st thread = kheap s thread \<Longrightarrow> auth_ipc_buffers st thread = auth_ipc_buffers s thread"
134  unfolding auth_ipc_buffers_def get_tcb_def by simp
135
136lemma tcb_ipc_buffer_not_device:
137  "\<lbrakk>kheap s thread = Some (TCB tcb);valid_objs s\<rbrakk>
138  \<Longrightarrow> \<not> cap_is_device (tcb_ipcframe tcb)"
139  apply (erule(1) valid_objsE)
140  apply (clarsimp simp: valid_obj_def valid_tcb_def valid_ipc_buffer_cap_def
141                 split: cap.split_asm arch_cap.split_asm)
142  done
143
144lemma tro_auth_ipc_buffer_idem:
145  "\<lbrakk> \<forall>x. integrity_obj aag activate subjects (pasObjectAbs aag x) (kheap st x) (kheap s x);
146        pasObjectAbs aag thread \<notin> subjects; valid_objs s \<rbrakk>
147   \<Longrightarrow> auth_ipc_buffers st thread = auth_ipc_buffers s thread"
148  apply (drule spec [where x = thread])
149  by (erule integrity_objE;
150      simp add: auth_ipc_buffers_def get_tcb_def;
151      fastforce cong: cap.case_cong arch_cap.case_cong if_cong
152                simp: case_bool_if
153               dest!: tcb_ipc_buffer_not_device split:arch_cap.splits cap.splits
154               split: if_splits)
155
156
157lemma dmo_storeWord_respects_ipc:
158  "\<lbrace>integrity aag X st and st_tcb_at ((=) Structures_A.Running) thread and
159    K ((\<not> is_subject aag thread \<longrightarrow> st_tcb_at (receive_blocked_on ep) thread st \<and> auth_ipc_buffers st thread = ptr_range buf msg_align_bits) \<and>
160      ipc_buffer_has_auth aag thread (Some buf) \<and> p < 2 ^ (msg_align_bits - 2)) \<rbrace>
161    do_machine_op (storeWord (buf + of_nat p * of_nat word_size) v)
162   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
163  apply (rule hoare_gen_asm)
164  apply (elim conjE)
165  apply (cases "is_subject aag thread")
166   apply (rule hoare_pre)
167   apply (rule dmo_storeWord_respects_Write)
168    apply clarsimp
169    apply (drule (1) ipc_buffer_has_auth_wordE)
170       apply simp
171      apply (simp add: msg_align_bits)
172     apply (erule mul_word_size_lt_msg_align_bits_ofnat)
173    apply simp
174   \<comment> \<open>non auth case\<close>
175  apply (rule hoare_pre)
176  apply (simp add: storeWord_def)
177  apply (wp dmo_wp)
178  apply clarsimp
179  apply (simp add: integrity_def split del: if_split)
180  apply (clarsimp split del: if_split)
181  apply (case_tac "x \<in> ptr_range (buf + of_nat p * of_nat word_size) 2")
182   apply (clarsimp simp add: st_tcb_at_tcb_states_of_state split del: if_split)
183   apply (rule trm_ipc [where p' = thread])
184      apply simp
185     apply assumption
186    apply (clarsimp simp: ipc_buffer_has_auth_def)
187    apply (erule (1) set_mp [OF ptr_range_subset, rotated -1])
188      apply simp
189     apply (simp add: msg_align_bits)
190    apply (erule mul_word_size_lt_msg_align_bits_ofnat)
191   apply simp
192  \<comment> \<open>otherwise\<close>
193  apply (auto simp: is_aligned_mask [symmetric] intro!: trm_lrefl ptr_range_memI ptr_range_add_memI)
194  done
195
196lemma store_word_offs_respects:
197  "\<lbrace>integrity aag X st and st_tcb_at ((=) Structures_A.Running) thread and
198    K ((\<not> is_subject aag thread \<longrightarrow> st_tcb_at (receive_blocked_on ep) thread st \<and> auth_ipc_buffers st thread = ptr_range buf msg_align_bits) \<and>
199      ipc_buffer_has_auth aag thread (Some buf) \<and> p < 2 ^ (msg_align_bits - 2)) \<rbrace>
200   store_word_offs buf p v
201   \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
202  apply (simp add: store_word_offs_def)
203  apply (rule hoare_pre)
204   apply (wp dmo_storeWord_respects_ipc [where thread = thread])
205  apply fastforce
206  done
207
208
209lemma ipc_buffer_has_auth_None [simp]:
210  "ipc_buffer_has_auth aag receiver None"
211  unfolding ipc_buffer_has_auth_def by simp
212
213(* FIXME: MOVE *)
214lemma cap_auth_caps_of_state:
215  "\<lbrakk> caps_of_state s p = Some cap; pas_refined aag s\<rbrakk>
216  \<Longrightarrow> aag_cap_auth aag (pasObjectAbs aag (fst p)) cap"
217  unfolding aag_cap_auth_def
218  apply (intro conjI)
219    apply clarsimp
220    apply (drule (2) sta_caps)
221    apply (drule auth_graph_map_memI [where x = "pasObjectAbs aag (fst p)", OF _ sym refl])
222    apply (rule refl)
223    apply (fastforce simp: pas_refined_def)
224   apply clarsimp
225   apply (drule (2) sta_untyped [THEN pas_refined_mem] )
226   apply simp
227  apply (drule (1) clas_caps_of_state)
228  apply simp
229  apply (drule (1) cli_caps_of_state)
230  apply simp
231  done
232
233lemma lookup_ipc_buffer_has_auth [wp]:
234  "\<lbrace>pas_refined aag and valid_objs\<rbrace>
235    lookup_ipc_buffer True receiver
236   \<lbrace>\<lambda>rv s. ipc_buffer_has_auth aag receiver rv\<rbrace>"
237  apply (rule hoare_pre)
238   apply (simp add: lookup_ipc_buffer_def)
239   apply (wp get_cap_wp thread_get_wp'
240        | wpc)+
241  apply (clarsimp simp: cte_wp_at_caps_of_state ipc_buffer_has_auth_def get_tcb_ko_at [symmetric])
242  apply (frule caps_of_state_tcb_cap_cases [where idx = "tcb_cnode_index 4"])
243   apply (simp add: dom_tcb_cap_cases)
244  apply (frule (1) caps_of_state_valid_cap)
245  apply (rule conjI)
246   apply (clarsimp simp: valid_cap_simps cap_aligned_def)
247   apply (erule aligned_add_aligned)
248    apply (rule is_aligned_andI1)
249    apply (drule (1) valid_tcb_objs)
250    apply (clarsimp simp: valid_obj_def valid_tcb_def valid_ipc_buffer_cap_def
251                   split: if_splits)
252   apply (rule order_trans [OF _ pbfs_atleast_pageBits])
253   apply (simp add: msg_align_bits pageBits_def)
254  apply simp
255  apply (drule (1) cap_auth_caps_of_state)
256  apply (clarsimp simp: aag_cap_auth_def cap_auth_conferred_def vspace_cap_rights_to_auth_def
257                        vm_read_write_def is_page_cap_def split: if_split_asm)
258  apply (drule bspec)
259   apply (erule (3) ipcframe_subset_page)
260  apply simp
261  done
262
263lemma set_notification_respects:
264  "\<lbrace>integrity aag X st and K (aag_has_auth_to aag auth epptr \<and> auth \<in> {Receive, Notify, Reset})\<rbrace>
265     set_notification epptr ntfn'
266   \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
267  apply (simp add: set_simple_ko_def set_object_def)
268  apply (wp get_object_wp)
269  apply (clarsimp simp: obj_at_def partial_inv_def a_type_def)
270  apply (erule integrity_trans)
271  apply (clarsimp simp: integrity_def tro_ntfn)
272  done
273
274lemma receive_signal_integrity_autarch:
275  "\<lbrace>integrity aag X st and pas_refined aag and valid_objs
276           and K ((\<forall>ntfnptr \<in> obj_refs cap. aag_has_auth_to aag Receive ntfnptr)
277                 \<and> is_subject aag thread)\<rbrace>
278     receive_signal thread cap is_blocking
279   \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
280  apply (simp add: receive_signal_def)
281  apply (cases cap, simp_all)
282  apply (rule hoare_seq_ext [OF _ get_simple_ko_sp])
283  apply (rule hoare_pre)
284  apply (wp set_notification_respects[where auth=Receive] set_thread_state_integrity_autarch as_user_integrity_autarch
285       | wpc
286       | simp add: do_nbrecv_failed_transfer_def)+
287  done
288
289subsubsection\<open>Non-autarchy: the sender is running\<close>
290
291
292lemma length_msg_registers:
293  "length msg_registers = 4"
294  unfolding msg_registers_def
295  by (simp add: msgRegisters_def upto_enum_def fromEnum_def enum_register)
296
297lemma send_upd_ctxintegrity:
298  "\<lbrakk> direct_send {pasSubject aag} aag ep tcb
299      \<or> indirect_send {pasSubject aag} aag (the (tcb_bound_notification tcb)) ep tcb;
300     integrity aag X st s; st_tcb_at ((=) Structures_A.thread_state.Running) thread s;
301     get_tcb thread st = Some tcb; get_tcb thread s = Some tcb'\<rbrakk>
302     \<Longrightarrow> integrity aag X st (s\<lparr>kheap :=
303                               kheap s(thread \<mapsto> TCB (tcb'\<lparr>tcb_arch :=
304                                                           arch_tcb_context_set c' (tcb_arch tcb')
305                                                          \<rparr>))
306                              \<rparr>)"
307 apply (clarsimp simp: integrity_def tcb_states_of_state_preserved st_tcb_def2)
308  apply (drule get_tcb_SomeD)+
309  apply (drule spec[where x=thread], simp)
310  apply (cases "is_subject aag thread")
311   apply (rule tro_lrefl, solves\<open>simp\<close>)
312
313  (* slow 5s *)
314  by (erule integrity_objE;
315      (* eliminate all TCB unrelated cases and simplifies the other *)
316      clarsimp;
317        (* deal with the orefl case *)
318      ( solves\<open>simp add:direct_send_def indirect_send_def\<close>
319        (* deal with the other case by applying either the reply, call or send rules and then
320           the generic rule *)
321      | rule tro_trans_spec,
322        (rule tro_tcb_reply'[OF refl refl refl] tro_tcb_call[OF refl refl refl]
323              tro_tcb_send[OF refl refl refl];
324          blast),
325        rule tro_trans_spec,
326        (rule tro_tcb_generic'[OF refl refl refl]; simp),
327        rule tro_orefl, simp, rule tcb.equality; solves\<open>simp add:arch_tcb_context_set_def\<close>))
328
329lemma set_mrs_respects_in_signalling':
330  "\<lbrace>integrity aag X st and st_tcb_at ((=) Structures_A.Running) thread and
331    K ((\<not> is_subject aag thread \<longrightarrow> st_tcb_at (receive_blocked_on ep) thread st
332        \<and> case_option True (\<lambda>buf'. auth_ipc_buffers st thread = ptr_range buf' msg_align_bits) buf)
333        \<and> aag_has_auth_to aag Notify ep \<and> ipc_buffer_has_auth aag thread buf) \<rbrace>
334     set_mrs thread buf msgs
335   \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
336  apply (rule hoare_gen_asm)
337  apply (simp add: set_mrs_def split_def set_object_def get_object_def split del: if_split)
338  apply (wp gets_the_wp get_wp put_wp
339       | wpc
340       | simp split del: if_split
341                    add: zipWithM_x_mapM_x split_def store_word_offs_def fun_upd_def[symmetric])+
342     apply (rule hoare_post_imp [where Q = "\<lambda>rv. st_tcb_at ((=) Structures_A.Running) thread and integrity aag X st"])
343      apply simp
344     apply (wp mapM_x_wp' dmo_storeWord_respects_ipc [where thread = thread and ep = ep])
345     apply (fastforce simp add: set_zip nth_append simp: msg_align_bits msg_max_length_def
346                         split: if_split_asm)
347    apply wp+
348  apply (rule impI)
349  apply (subgoal_tac "\<forall>c'. integrity aag X st
350          (s\<lparr>kheap := kheap s(thread \<mapsto>
351               TCB ((the (get_tcb thread s))\<lparr>tcb_arch :=  arch_tcb_set_registers c' (tcb_arch (the (get_tcb thread s))) \<rparr>))\<rparr>)")
352   apply (clarsimp simp: fun_upd_def st_tcb_at_nostate_upd [unfolded fun_upd_def])
353  apply (rule allI)
354  apply clarsimp
355  apply (cases "is_subject aag thread")
356   apply (erule (1) integrity_update_autarch)
357  apply (clarsimp simp: st_tcb_def2 arch_tcb_set_registers_def)
358  apply (rule send_upd_ctxintegrity[OF disjI1], auto simp: st_tcb_def2 direct_send_def)
359  done
360
361lemma as_user_set_register_respects:
362  "\<lbrace>integrity aag X st and st_tcb_at ((=) Structures_A.Running) thread and
363    K ((\<not> is_subject aag thread \<longrightarrow> st_tcb_at (receive_blocked_on ep) thread st) \<and> (aag_has_auth_to aag SyncSend ep \<or> aag_has_auth_to aag Notify ep)) \<rbrace>
364   as_user thread (set_register r v)
365   \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
366  apply (simp add: as_user_def split_def set_object_def get_object_def)
367  apply wp
368  apply (clarsimp simp: in_monad setRegister_def)
369  apply (cases "is_subject aag thread")
370   apply (erule (1) integrity_update_autarch [unfolded fun_upd_def])
371  apply (clarsimp simp: st_tcb_def2)
372  apply (rule send_upd_ctxintegrity [OF disjI1, unfolded fun_upd_def])
373      apply (auto simp: direct_send_def st_tcb_def2)
374  done
375
376lemma lookup_ipc_buffer_ptr_range:
377  "\<lbrace>valid_objs and integrity aag X st\<rbrace>
378  lookup_ipc_buffer True thread
379  \<lbrace>\<lambda>rv s. \<not> is_subject aag thread \<longrightarrow> (case rv of None \<Rightarrow> True | Some buf' \<Rightarrow> auth_ipc_buffers st thread = ptr_range buf' msg_align_bits) \<rbrace>"
380  unfolding lookup_ipc_buffer_def
381  apply (rule hoare_pre)
382  apply (wp get_cap_wp thread_get_wp' | wpc)+
383  apply (clarsimp simp: cte_wp_at_caps_of_state ipc_buffer_has_auth_def get_tcb_ko_at [symmetric])
384  apply (frule caps_of_state_tcb_cap_cases [where idx = "tcb_cnode_index 4"])
385   apply (simp add: dom_tcb_cap_cases)
386  apply (clarsimp simp: auth_ipc_buffers_def get_tcb_ko_at [symmetric] integrity_def)
387  apply (drule spec [where x = thread])+
388  apply (drule get_tcb_SomeD)+
389  apply (erule(1) valid_objsE)
390  apply (clarsimp simp: valid_obj_def valid_tcb_def valid_ipc_buffer_cap_def case_bool_if
391                 split: if_split_asm)
392  apply (erule integrity_objE, simp_all add: get_tcb_def vm_read_write_def)
393  apply auto
394  done
395
396lemma set_thread_state_respects_in_signalling:
397  "\<lbrace>integrity aag X st
398             and (\<lambda>s. \<not> is_subject aag thread \<longrightarrow> st_tcb_at (receive_blocked_on ntfnptr) thread s)
399             and K (aag_has_auth_to aag Notify ntfnptr)\<rbrace>
400     set_thread_state thread Structures_A.thread_state.Running
401   \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
402  apply (simp add: set_thread_state_def set_object_def get_object_def)
403  apply wp
404  apply (clarsimp)
405  apply (cases "is_subject aag thread")
406   apply (erule(1) integrity_update_autarch [unfolded fun_upd_def])
407  apply (erule integrity_trans)
408  apply (drule get_tcb_SomeD)
409  apply (clarsimp simp: integrity_def st_tcb_def2)
410  apply (clarsimp dest!: get_tcb_SomeD)
411  apply (rule tro_tcb_send [OF refl refl])
412  apply (rule tcb.equality;simp; rule arch_tcb_context_set_eq[symmetric])
413  apply (auto simp: indirect_send_def direct_send_def)
414  done
415
416lemma set_notification_obj_at:
417  "\<lbrace>obj_at P ptr and K (ptr \<noteq> ntfnptr)\<rbrace>
418     set_notification ntfnptr queue
419   \<lbrace>\<lambda>rv. obj_at P ptr\<rbrace>"
420  apply (simp add: set_simple_ko_def set_object_def)
421  apply (wp get_object_wp)
422  apply (auto simp: obj_at_def)
423  done
424
425lemma set_ntfn_valid_objs_at:
426  "\<lbrace>valid_objs and (\<lambda>s. ntfn_at p s \<longrightarrow> valid_ntfn ntfn s)\<rbrace> set_notification p ntfn \<lbrace>\<lambda>rv. valid_objs\<rbrace>"
427  unfolding set_simple_ko_def
428  apply (rule hoare_pre)
429  apply (wp set_object_valid_objs get_object_wp)
430  apply (clarsimp simp: valid_obj_def obj_at_def is_ntfn partial_inv_def
431              split: Structures_A.kernel_object.splits)
432  done
433
434lemma drop_Suc0_iff:
435  "xs \<noteq> [] \<Longrightarrow> (drop (Suc 0) xs = ys) = (\<exists>x. xs = x # ys)"
436  by (auto simp: neq_Nil_conv)
437
438lemma receive_blocked_on_def3:
439  "receive_blocked_on ref ts =
440     ((\<exists>pl. ts = Structures_A.BlockedOnReceive ref pl)
441      \<or> ts = Structures_A.BlockedOnNotification ref)"
442  by (cases ts, auto)
443
444
445lemma integrity_receive_blocked_chain:
446  "\<lbrakk> st_tcb_at (receive_blocked_on ep) p s; integrity aag X st s; \<not> is_subject aag p \<rbrakk> \<Longrightarrow> st_tcb_at (receive_blocked_on ep) p st"
447  apply (clarsimp simp: integrity_def st_tcb_at_tcb_states_of_state)
448  apply (drule (1) tsos_tro [where p = p] )
449    apply (fastforce simp: tcb_states_of_state_def)
450   apply simp
451  apply simp
452  done
453
454crunch integrity[wp]: possible_switch_to "integrity aag X st"
455  (ignore: tcb_sched_action)
456
457abbreviation
458  "integrity_once_ts_upd t ts aag X st s
459    == integrity aag X st (s \<lparr> kheap := (kheap s) ( t := Some (TCB ((the (get_tcb t s)) \<lparr>tcb_state := ts\<rparr>)))\<rparr>)"
460
461lemma set_scheduler_action_integrity_once_ts_upd:
462  "\<lbrace>integrity_once_ts_upd t ts aag X st\<rbrace>
463    set_scheduler_action sa \<lbrace>\<lambda>_. integrity_once_ts_upd t ts aag X st\<rbrace>"
464  apply (simp add: set_scheduler_action_def, wp)
465  apply clarsimp
466  apply (erule rsubst[where P="\<lambda>x. x"])
467  apply (rule trans, rule_tac f="\<lambda>x. sa" in eintegrity_sa_update[symmetric])
468  apply (rule arg_cong[where f="integrity aag X st"])
469  apply (simp add: get_tcb_def)
470  done
471
472crunch integrity_once_ts_upd: set_thread_state_ext "integrity_once_ts_upd t ts aag X st"
473
474lemma set_thread_state_integrity_once_ts_upd:
475  "\<lbrace>integrity_once_ts_upd t ts aag X st\<rbrace>
476    set_thread_state t ts' \<lbrace>\<lambda>_. integrity_once_ts_upd t ts aag X st\<rbrace>"
477  apply (simp add: set_thread_state_def)
478  apply (wpsimp wp: set_object_wp set_thread_state_ext_integrity_once_ts_upd)
479  apply (clarsimp simp: fun_upd_def dest!: get_tcb_SomeD)
480  apply (simp add: get_tcb_def cong: if_cong)
481  done
482
483lemma get_tcb_recv_blocked_implies_receive:
484  "\<lbrakk>pas_refined aag s; get_tcb t s = Some tcb; ep_recv_blocked ep (tcb_state tcb) \<rbrakk>
485          \<Longrightarrow> (pasObjectAbs aag t, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag"
486  apply (erule pas_refined_mem[rotated])
487  apply (rule sta_ts)
488  apply (simp add: thread_states_def tcb_states_of_state_def)
489  apply (case_tac "tcb_state tcb", simp_all)
490  done
491
492lemma cancel_ipc_receive_blocked_respects:
493  "\<lbrace>integrity aag X st and pas_refined aag and st_tcb_at (receive_blocked) t and
494       (sym_refs o state_refs_of) and
495       bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) t and
496       K ((pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and>
497             (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag)\<rbrace>
498    cancel_ipc t \<lbrace>\<lambda>_. integrity_once_ts_upd t Running aag X st\<rbrace>"
499  apply (clarsimp simp: cancel_ipc_def bind_assoc)
500  apply (rule hoare_seq_ext[OF _ gts_sp])
501  apply (rule hoare_name_pre_state)
502  apply (subgoal_tac "case state of BlockedOnReceive x y \<Rightarrow> True | _ \<Rightarrow> False")
503   apply (simp add: blocked_cancel_ipc_def bind_assoc set_simple_ko_def set_object_def
504                    get_ep_queue_def get_blocking_object_def
505             split: thread_state.splits)
506   apply (rule hoare_pre)
507    apply (wp set_thread_state_integrity_once_ts_upd get_object_wp get_simple_ko_wp
508          | wpc)+
509   apply (clarsimp simp: st_tcb_at_def2 obj_at_def)
510   apply (rename_tac ep payload s tcb ntfn)
511   apply (drule_tac t="tcb_state tcb" in sym)
512   apply (subgoal_tac "st_tcb_at ((=) (tcb_state tcb)) t s")
513    apply (drule(1) sym_refs_st_tcb_atD)
514    apply (clarsimp simp: obj_at_def ep_q_refs_of_def fun_upd_def get_tcb_def
515                   split: endpoint.splits cong: if_cong)
516    apply (intro impI conjI, simp_all)[1]
517    apply (erule integrity_trans)
518    apply (simp add: integrity_def)
519    apply (intro impI conjI allI)
520     apply clarsimp
521     apply (rule tro_ep_unblock; simp?)
522     apply (erule get_tcb_recv_blocked_implies_receive, erule get_tcb_rev; solves\<open>simp\<close>)
523    apply (rule_tac ep=ep in tro_tcb_send[OF refl refl];
524           fastforce intro!: tcb.equality arch_tcb_context_set_eq[symmetric]
525                       simp: indirect_send_def pred_tcb_at_def obj_at_def)
526   apply (fastforce simp: indirect_send_def pred_tcb_at_def obj_at_def)
527  apply (fastforce simp: pred_tcb_at_def obj_at_def receive_blocked_def)
528  done
529
530lemma set_thread_state_integrity':
531  "\<lbrace>integrity_once_ts_upd t ts aag X st\<rbrace> set_thread_state t ts \<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
532  apply (simp add: set_thread_state_def)
533  by (wpsimp wp: set_object_wp)
534
535lemma as_user_set_register_respects_indirect:
536  "\<lbrace>integrity aag X st and st_tcb_at ((=) Structures_A.Running) thread and
537    K ((\<not> is_subject aag thread \<longrightarrow> st_tcb_at receive_blocked thread st
538           \<and> bound_tcb_at ((=) (Some ntfnptr)) thread st)
539        \<and> (aag_has_auth_to aag Notify ntfnptr)) \<rbrace>
540   as_user thread (set_register r v)
541   \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
542  apply (simp add: as_user_def split_def set_object_def get_object_def)
543  apply wp
544  apply (clarsimp simp: in_monad setRegister_def)
545  apply (cases "is_subject aag thread")
546   apply (erule (1) integrity_update_autarch [unfolded fun_upd_def])
547  apply (clarsimp simp: st_tcb_def2 receive_blocked_def)
548  apply (simp split: thread_state.split_asm)
549  apply (rule send_upd_ctxintegrity [OF disjI2, unfolded fun_upd_def],
550         auto simp: st_tcb_def2 indirect_send_def pred_tcb_def2 dest: sym)
551  done
552
553lemma integrity_receive_blocked_chain':
554  "\<lbrakk> st_tcb_at receive_blocked p s; integrity aag X st s; \<not> is_subject aag p \<rbrakk> \<Longrightarrow> st_tcb_at receive_blocked p st"
555  apply (clarsimp simp: integrity_def st_tcb_at_tcb_states_of_state receive_blocked_def)
556  apply (simp split: thread_state.split_asm)
557  apply (rename_tac word pl)
558  apply (drule_tac ep=word in tsos_tro [where p = p], simp+ )
559  done
560
561lemma tba_Some:
562  "thread_bound_ntfns s t = Some a \<Longrightarrow> bound_tcb_at ((=) (Some a)) t s"
563  by (clarsimp simp: thread_bound_ntfns_def pred_tcb_at_def obj_at_def get_tcb_def
564              split: option.splits kernel_object.splits)
565
566
567lemma tsos_tro':
568  "\<lbrakk>\<forall>x. integrity_obj aag activate subjects (pasObjectAbs aag x) (kheap s x) (kheap s' x);
569    thread_bound_ntfns s' p = Some a; pasObjectAbs aag p \<notin> subjects \<rbrakk>
570   \<Longrightarrow> thread_bound_ntfns s p = Some a"
571  apply (drule_tac x=p in spec)
572  apply (erule integrity_objE;
573         simp?;
574         fastforce simp: thread_bound_ntfns_def get_tcb_def
575                         tcb_bound_notification_reset_integrity_def)
576  done
577
578lemma integrity_receive_blocked_chain_bound:
579  "\<lbrakk>bound_tcb_at ((=) (Some ntfnptr)) p s; integrity aag X st s; \<not> is_subject aag p\<rbrakk>
580   \<Longrightarrow> bound_tcb_at ((=) (Some ntfnptr)) p st"
581  apply (clarsimp simp: integrity_def)
582  apply (drule bound_tcb_at_thread_bound_ntfns)
583  apply (drule tsos_tro' [where p = p], simp+ )
584  apply (clarsimp simp:tba_Some)
585  done
586
587lemma send_signal_respects:
588  "\<lbrace>integrity aag X st and pas_refined aag
589         and valid_objs
590         and sym_refs \<circ> state_refs_of
591         and K (aag_has_auth_to aag Notify ntfnptr)\<rbrace>
592     send_signal ntfnptr badge
593   \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
594  apply (simp add: send_signal_def)
595  apply (rule hoare_seq_ext[OF _ get_simple_ko_sp])
596  apply (rule hoare_name_pre_state)
597  apply (case_tac "ntfn_obj ntfn = IdleNtfn \<and> ntfn_bound_tcb ntfn \<noteq> None")
598   \<comment> \<open>ntfn-binding case\<close>
599   apply (rule hoare_pre)
600    apply (wp set_notification_respects[where auth=Notify]
601                 as_user_set_register_respects_indirect[where ntfnptr=ntfnptr]
602                 set_thread_state_integrity' sts_st_tcb_at' static_imp_wp
603                 cancel_ipc_receive_blocked_respects[where ntfnptr=ntfnptr]
604                 gts_wp
605               | wpc | simp)+
606   apply (clarsimp, rule conjI, clarsimp simp: st_tcb_def2)
607   apply (clarsimp simp: receive_blocked_def)
608   apply (simp split: thread_state.split_asm)
609   apply (clarsimp simp: obj_at_def)
610   apply (drule (3) ntfn_bound_tcb_at[where ntfnptr=ntfnptr and P="\<lambda>ntfn. ntfn = Some ntfnptr"], simp+)[1]
611   apply (rule conjI)
612    apply (drule_tac x=ntfnptr and t=y in bound_tcb_at_implies_receive)
613     apply (clarsimp simp: pred_tcb_at_def obj_at_def, simp)
614   apply clarsimp
615   apply (rule conjI)
616    apply (rule_tac s=sa in integrity_receive_blocked_chain')
617      apply (clarsimp simp add: pred_tcb_at_def obj_at_def receive_blocked_def)
618      apply (fastforce split: thread_state.split)
619     apply simp+
620   apply (rule_tac s=sa in integrity_receive_blocked_chain_bound)
621     apply (clarsimp simp: pred_tcb_at_def obj_at_def)
622    apply simp+
623  apply (rule hoare_pre)
624   apply clarsimp
625   apply (wpc, clarsimp)
626     apply (wp set_notification_respects[where auth=Notify]
627               sts_st_tcb_at' as_user_set_register_respects
628               set_thread_state_pas_refined set_simple_ko_pas_refined
629               set_thread_state_respects_in_signalling [where ntfnptr = ntfnptr]
630               set_ntfn_valid_objs_at hoare_vcg_disj_lift static_imp_wp
631          | wpc
632          | simp add: update_waiting_ntfn_def)+
633  apply clarsimp
634  apply (subgoal_tac "st_tcb_at (receive_blocked_on ntfnptr) (hd x) sa")
635   prefer 2
636   apply (rule ntfn_queued_st_tcb_at', assumption)
637      apply (fastforce simp: obj_at_def valid_obj_def valid_ntfn_def)
638     apply assumption+
639   apply simp
640  apply simp
641  apply (intro impI conjI)
642     \<comment> \<open>st_tcb_at receive_blocked st\<close>
643   apply (erule (2) integrity_receive_blocked_chain)
644  apply clarsimp
645  done
646
647section\<open>Sync IPC\<close>
648
649text\<open>
650
651When transferring caps, i.e. when the grant argument is true on the
652IPC operations, the currently-running thread owns the receiver. Either
653it is the receiver (and ?thesis by well-formedness) or it is the
654sender, and that can send arbitrary caps, hence ?thesis by sbta_ipc
655etc.
656
657\<close>
658
659subsection\<open>auxiliary\<close>
660
661
662lemma cap_master_cap_masked_as_full:
663  "cap_master_cap (masked_as_full a a) = cap_master_cap a "
664  apply(clarsimp simp: cap_master_cap_def split: cap.splits simp: masked_as_full_def)
665  done
666
667lemma cap_badge_masked_as_full:
668  "(cap_badge (masked_as_full a a), cap_badge a) \<in> capBadge_ordering False"
669  apply(case_tac a, simp_all add: masked_as_full_def)
670  done
671
672
673
674lemma masked_as_full_double:
675  "masked_as_full (masked_as_full ab ab) cap' = masked_as_full ab ab"
676  apply(case_tac ab, simp_all add: masked_as_full_def)
677  done
678
679lemma transfer_caps_loop_pres_dest_aux:
680  assumes x: "\<And>cap src dest.
681              \<lbrace>\<lambda>s. P s \<and> dest \<in> slots' \<and> src \<in> snd ` caps'
682                                   \<and> (valid_objs s \<and> real_cte_at dest s \<and> s \<turnstile> cap \<and> tcb_cap_valid cap dest s
683                                   \<and> real_cte_at src s
684                                   \<and> cte_wp_at (is_derived (cdt s) src cap) src s \<and> cap \<noteq> cap.NullCap) \<rbrace>
685                 cap_insert cap src dest \<lbrace>\<lambda>rv. P\<rbrace>"
686  assumes eb: "\<And>b n'. n' \<le> N \<Longrightarrow> \<lbrace>P\<rbrace> set_extra_badge buffer b n' \<lbrace>\<lambda>_. P\<rbrace>"
687  shows      "n + length caps \<le> N \<Longrightarrow>
688                 \<lbrace>\<lambda>s. P s \<and> set slots \<subseteq> slots' \<and> set caps \<subseteq> caps' \<and>
689                     (valid_objs s \<and> valid_mdb s \<and> distinct slots \<and>
690                     (\<forall>x \<in> set slots. real_cte_at x s) \<and>
691                     (\<forall>x \<in> set caps. s \<turnstile> fst x \<and>
692                                     cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s
693                                           \<and> real_cte_at (snd x) s))\<rbrace>
694                  transfer_caps_loop ep buffer n caps slots mi
695              \<lbrace>\<lambda>rv. P\<rbrace>" (is "?L \<Longrightarrow> ?P n caps slots mi")
696proof (induct caps arbitrary: slots n mi)
697  case Nil
698  thus ?case by (simp, wp, simp)
699next
700  case (Cons m ms)
701  hence nN: "n \<le> N" by simp
702
703  from Cons have "\<And>slots mi. ?P (n + 1) ms slots mi" by clarsimp
704  thus ?case
705    apply (cases m)
706    apply (clarsimp simp add: Let_def split_def whenE_def
707                    cong: if_cong list.case_cong split del: if_split)
708  apply (rule hoare_pre)
709   apply (wp eb [OF nN] hoare_vcg_const_imp_lift hoare_vcg_const_Ball_lift
710           | assumption | simp split del: if_split)+
711
712      apply (rule cap_insert_assume_null)
713      apply (wp x hoare_vcg_const_Ball_lift cap_insert_cte_wp_at)+
714      (* cannot blindly use derive_cap_is_derived_foo here , need to first hoist
715         out of the postcondition the conjunct that the return value is derived,
716         and solve this using derived_cap_is_derived, and then solve the rest
717         using derive_cap_is_derived_foo *)
718    apply (rule_tac Q'="\<lambda>r s. S r s \<and> Q r s" for S Q in hoare_post_imp_R)
719     apply (rule hoare_vcg_conj_lift_R)
720      apply (rule derive_cap_is_derived)
721     prefer 2
722     apply clarsimp
723     apply assumption
724    apply(wp derive_cap_is_derived_foo)+
725  apply (simp only: tl_drop_1[symmetric])
726  apply (clarsimp simp: cte_wp_at_caps_of_state
727                        ex_cte_cap_to_cnode_always_appropriate_strg
728                        real_cte_tcb_valid caps_of_state_valid
729             split del: if_split)
730  apply (clarsimp simp: remove_rights_def caps_of_state_valid
731                        neq_Nil_conv cte_wp_at_caps_of_state
732                        imp_conjR[symmetric] cap_master_cap_masked_as_full
733                        cap_badge_masked_as_full
734                 split del: if_split)
735  apply(intro conjI)
736   apply clarsimp
737   apply (case_tac "cap = a",clarsimp simp: remove_rights_def)
738   apply (clarsimp simp:masked_as_full_def is_cap_simps)
739   apply (clarsimp simp: cap_master_cap_simps remove_rights_def split:if_splits)
740  apply clarsimp
741  apply (intro conjI)
742    apply (clarsimp split:if_splits elim!: image_eqI[rotated])
743   apply (clarsimp split:if_splits simp: remove_rights_def)
744  apply (rule ballI)
745  apply (drule(1) bspec)
746  apply clarsimp
747  apply (intro conjI)
748   apply clarsimp
749  apply clarsimp
750   apply (case_tac "capa = ab",clarsimp simp: masked_as_full_def is_cap_simps split: if_splits)
751  apply (clarsimp simp: masked_as_full_double)
752  done
753qed
754
755
756(* FIXME: move *)
757lemma transfer_caps_loop_pres_dest:
758  assumes x: "\<And>cap src dest.
759              \<lbrace>\<lambda>s. P s \<and> dest \<in> set slots \<and> src \<in> snd ` set caps
760                                   \<and> (valid_objs s \<and> real_cte_at dest s \<and> s \<turnstile> cap \<and> tcb_cap_valid cap dest s
761                                   \<and> real_cte_at src s
762                                   \<and> cte_wp_at (is_derived (cdt s) src cap) src s \<and> cap \<noteq> cap.NullCap) \<rbrace>
763                 cap_insert cap src dest \<lbrace>\<lambda>rv. P\<rbrace>"
764  assumes eb: "\<And>b n'. n' \<le> n + length caps \<Longrightarrow> \<lbrace>P\<rbrace> set_extra_badge buffer b n' \<lbrace>\<lambda>_. P\<rbrace>"
765  shows      "\<lbrace>\<lambda>s. P s \<and> (valid_objs s \<and> valid_mdb s \<and> distinct slots \<and>
766                                 (\<forall>x \<in> set slots. real_cte_at x s) \<and>
767                                 (\<forall>x \<in> set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s
768                                           \<and> real_cte_at (snd x) s))\<rbrace>
769                  transfer_caps_loop ep buffer n caps slots mi
770              \<lbrace>\<lambda>rv. P\<rbrace>"
771  apply (rule hoare_pre)
772  apply (rule transfer_caps_loop_pres_dest_aux [OF x eb])
773  apply assumption
774  apply simp
775  apply simp
776  done
777
778subsection\<open>pas_refined\<close>
779
780lemma lookup_slot_for_thread_authorised:
781  "\<lbrace>pas_refined aag and K (is_subject aag thread)\<rbrace>
782    lookup_slot_for_thread thread cref
783   \<lbrace>\<lambda>rv s. is_subject aag (fst (fst rv))\<rbrace>,-"
784  unfolding lookup_slot_for_thread_def
785  apply wp
786  apply (clarsimp simp: owns_thread_owns_cspace)
787  done
788
789lemma cnode_cap_all_auth_owns:
790  "(\<exists>s. is_cnode_cap cap \<and> (\<forall>x\<in>obj_refs cap.
791          \<forall>auth\<in>cap_auth_conferred cap. aag_has_auth_to aag auth x)
792            \<and> pas_refined aag s)
793          \<longrightarrow> (\<forall>x\<in>obj_refs cap. is_subject aag x)"
794  apply (clarsimp simp: is_cap_simps)
795  apply (clarsimp simp: cap_auth_conferred_def pas_refined_all_auth_is_owns)
796  done
797
798lemma get_receive_slots_authorised:
799  "\<lbrace>pas_refined aag and K (\<forall>rbuf. recv_buf = Some rbuf \<longrightarrow> is_subject aag receiver)\<rbrace>
800     get_receive_slots receiver recv_buf
801  \<lbrace>\<lambda>rv s. \<forall>slot \<in> set rv. is_subject aag (fst slot)\<rbrace>"
802  apply (rule hoare_gen_asm)
803  apply (cases recv_buf)
804   apply (simp, wp, simp)
805  apply clarsimp
806  apply (wp get_cap_auth_wp[where aag=aag] lookup_slot_for_thread_authorised
807       | rule hoare_drop_imps
808       | simp add: add: lookup_cap_def split_def)+
809   apply (strengthen cnode_cap_all_auth_owns, simp add: aag_cap_auth_def)
810   apply (wp hoare_vcg_all_lift_R hoare_drop_imps)+
811  apply clarsimp
812  apply (fastforce simp: is_cap_simps)
813  done
814
815crunch pas_refined[wp]: set_extra_badge "pas_refined aag"
816
817lemma remove_rights_clas [simp]:
818  "cap_links_asid_slot aag p (remove_rights R cap) = cap_links_asid_slot aag p cap"
819  unfolding cap_links_asid_slot_def remove_rights_def cap_rights_update_def acap_rights_update_def
820  by (clarsimp split: cap.splits arch_cap.splits bool.splits)
821
822lemma remove_rights_cap_auth_conferred_subset:
823  "x \<in> cap_auth_conferred (remove_rights R cap) \<Longrightarrow> x \<in> cap_auth_conferred cap"
824  unfolding remove_rights_def cap_rights_update_def
825  apply (clarsimp split: if_split_asm cap.splits arch_cap.splits bool.splits
826    simp: cap_auth_conferred_def vspace_cap_rights_to_auth_def acap_rights_update_def
827          validate_vm_rights_def vm_read_only_def vm_kernel_only_def)
828  apply (erule set_mp [OF cap_rights_to_auth_mono, rotated], clarsimp)+
829  apply (auto simp: is_page_cap_def cap_rights_to_auth_def reply_cap_rights_to_auth_def split:if_splits)
830  done
831
832lemma remove_rights_cli [simp]:
833  "cap_links_irq aag l (remove_rights R cap) = cap_links_irq aag l cap"
834  unfolding remove_rights_def cap_rights_update_def
835  by (clarsimp split: cap.splits arch_cap.splits bool.splits simp: cap_links_irq_def)
836
837lemma remove_rights_untyped_range [simp]:
838  "untyped_range (remove_rights R c) = untyped_range c"
839  unfolding remove_rights_def cap_rights_update_def
840  by (clarsimp split: cap.splits arch_cap.splits bool.splits simp: )
841
842lemma obj_refs_remove_rights [simp]:
843  "obj_refs (remove_rights rs cap) = obj_refs cap"
844  unfolding remove_rights_def
845  by (cases cap, simp_all add: cap_rights_update_def acap_rights_update_def split: arch_cap.splits bool.splits)
846
847lemma remove_rights_cur_auth:
848  "pas_cap_cur_auth aag cap \<Longrightarrow> pas_cap_cur_auth aag (remove_rights R cap)"
849  unfolding aag_cap_auth_def
850  by (clarsimp dest!: remove_rights_cap_auth_conferred_subset)
851
852(* FIXME MOVE *)
853lemmas hoare_gen_asmE2 = hoare_gen_asmE[where P'=\<top>,simplified pred_and_true_var]
854
855
856lemma derive_cap_is_transferable:
857  "\<lbrace>K(is_transferable_cap cap) \<rbrace> derive_cap slot cap \<lbrace>\<lambda>r s. is_transferable_cap r\<rbrace>, -"
858  apply (rule hoare_gen_asmE2)
859  by (erule is_transferable_capE; wpsimp simp: derive_cap_def)
860
861lemma auth_derived_refl[simp]:
862  " auth_derived cap cap"
863  by (simp add:auth_derived_def)
864
865lemma derive_cap_auth_derived:
866  "\<lbrace>\<top>\<rbrace> derive_cap slot cap \<lbrace>\<lambda>rv _. rv \<noteq> NullCap \<longrightarrow> auth_derived rv cap \<rbrace>,-"
867  apply (cases cap ; (wpsimp simp:derive_cap_def)?)
868  apply (case_tac x12 ;
869         simp add:derive_cap_def arch_derive_cap_def;
870         wpc?;
871         wp?;
872         simp add:auth_derived_def cap_auth_conferred_def)
873  done
874
875(* FIXME MOVE *)
876lemma auth_derived_pas_cur_auth:
877  "auth_derived cap cap' \<Longrightarrow> pas_cap_cur_auth aag cap' \<Longrightarrow> pas_cap_cur_auth aag cap"
878  by (force simp:aag_cap_auth_def auth_derived_def cap_links_asid_slot_def cap_links_irq_def)
879
880lemma derive_cap_is_derived_foo':
881  "\<lbrace>\<lambda>s. \<forall>cap'. (cte_wp_at (\<lambda>capa.
882                 cap_master_cap capa = cap_master_cap cap \<and>
883                 (cap_badge capa, cap_badge cap) \<in> capBadge_ordering False \<and>
884                 cap_asid capa = cap_asid cap \<and> vs_cap_ref capa = vs_cap_ref cap)
885      slot s \<and> valid_objs s \<and> cap' \<noteq> NullCap
886          \<longrightarrow> cte_at slot s )
887            \<and> (s \<turnstile> cap \<longrightarrow> s \<turnstile> cap')
888            \<and> (cap' \<noteq> NullCap \<longrightarrow> auth_derived cap' cap \<and> cap \<noteq> NullCap \<and> \<not> is_zombie cap \<and> cap \<noteq> IRQControlCap)
889          \<longrightarrow> Q cap' s \<rbrace>
890      derive_cap slot cap \<lbrace>Q\<rbrace>,-"
891  apply (clarsimp simp add: validE_R_def validE_def valid_def
892                     split: sum.splits)
893  apply (frule in_inv_by_hoareD[OF derive_cap_inv], clarsimp)
894  apply (erule allE)
895  apply (erule impEM)
896   apply (frule use_validE_R[OF _ cap_derive_not_null_helper, OF _ _ imp_refl])
897    apply (rule derive_cap_inv[THEN valid_validE_R])
898    apply (intro conjI)
899     apply (clarsimp simp:cte_wp_at_caps_of_state)+
900     apply (erule(1) use_validE_R[OF _ derive_cap_valid_cap])
901    apply simp
902    apply (erule use_validE_R[OF _ derive_cap_auth_derived],simp)
903  apply simp
904  done
905
906(* FIXME: cleanup *)
907lemma transfer_caps_loop_presM_extended:
908  fixes P vo em ex buffer slots caps n mi
909  assumes x: "\<And>cap src dest.
910              \<lbrace>\<lambda>s::('state_ext :: state_ext) state .
911                               P s \<and> (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> real_cte_at dest s \<and>
912                                             s \<turnstile> cap \<and> Psrc src \<and> Pdest dest \<and> Pcap cap \<and>
913                                             tcb_cap_valid cap dest s
914                                   \<and> real_cte_at src s
915                                   \<and> cte_wp_at (is_derived (cdt s) src cap) src s \<and>
916                                                cap \<noteq> cap.NullCap)
917                       \<and> (em \<longrightarrow> cte_wp_at ((=) cap.NullCap) dest s)
918                       \<and> (ex \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) dest s)\<rbrace>
919                 cap_insert cap src dest \<lbrace>\<lambda>rv. P\<rbrace>"
920  assumes eb: "\<And>b n. \<lbrace>P\<rbrace> set_extra_badge buffer b n \<lbrace>\<lambda>_. P\<rbrace>"
921  assumes pcap_auth_derived :
922    "\<And>cap cap'. \<lbrakk>auth_derived cap cap'; Pcap cap'\<rbrakk> \<Longrightarrow> Pcap cap"
923  shows "\<lbrace>\<lambda>s. P s \<and>
924             (vo \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and>
925                     (\<forall>x \<in> set slots. cte_wp_at (\<lambda>cap. cap = cap.NullCap) x s \<and>
926                                             real_cte_at x s \<and> Pdest x) \<and>
927                     (\<forall>x \<in> set caps. valid_cap (fst x) s \<and> Psrc (snd x) \<and> Pcap (fst x) \<and>
928                                     cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp \<noteq> fst x
929                                                     \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s
930                     \<and> real_cte_at (snd x) s))
931             \<and> (ex \<longrightarrow> (\<forall>x \<in> set slots. ex_cte_cap_wp_to is_cnode_cap x s))\<rbrace>
932          transfer_caps_loop ep buffer n caps slots mi
933        \<lbrace>\<lambda>rv. P\<rbrace>"
934  apply (induct caps arbitrary: slots n mi)
935   apply (simp, wp, simp)
936  apply (clarsimp simp add: Let_def split_def whenE_def
937                      cong: if_cong list.case_cong split del: if_split)
938  apply (rule hoare_pre)
939   apply (wp eb hoare_vcg_const_imp_lift hoare_vcg_const_Ball_lift static_imp_wp
940           | assumption | simp split del: if_split)+
941      apply (rule cap_insert_assume_null)
942      apply (wp x hoare_vcg_const_Ball_lift cap_insert_cte_wp_at static_imp_wp)+
943    apply (rule hoare_vcg_conj_liftE_R)
944     apply (rule derive_cap_is_derived_foo')
945    apply (rule_tac Q' ="\<lambda>cap' s. (vo \<longrightarrow> cap'\<noteq> cap.NullCap \<longrightarrow>
946                            cte_wp_at (is_derived (cdt s) (aa, b) cap') (aa, b) s)
947                            \<and> (cap'\<noteq> cap.NullCap \<longrightarrow> QM s cap')" for QM
948                    in hoare_post_imp_R)
949     prefer 2
950     apply clarsimp
951     apply assumption
952    apply (rule hoare_vcg_conj_liftE_R)
953     apply (rule hoare_vcg_const_imp_lift_R)
954     apply (rule derive_cap_is_derived)
955    apply (wp derive_cap_is_derived_foo')+
956  apply (clarsimp simp: cte_wp_at_caps_of_state
957                        ex_cte_cap_to_cnode_always_appropriate_strg
958                        real_cte_tcb_valid caps_of_state_valid
959             split del: if_split)
960  apply (clarsimp simp: remove_rights_def caps_of_state_valid
961                        neq_Nil_conv cte_wp_at_caps_of_state
962                        imp_conjR[symmetric] conj_comms
963             split del: if_split)
964  apply (rule conjI)
965   apply clarsimp
966   apply (case_tac "cap = a",clarsimp)
967   apply (clarsimp simp:masked_as_full_def is_cap_simps)
968   apply (fastforce simp: cap_master_cap_simps split: if_splits)
969  apply (clarsimp split del: if_split)
970  apply (intro conjI)
971     apply (fastforce split: if_split elim!: pcap_auth_derived)
972    apply (fastforce)
973   apply (clarsimp)
974  apply (rule ballI)
975  apply (drule(1) bspec)
976  apply clarsimp
977  apply (intro conjI)
978   apply (case_tac "capa = ac",clarsimp+)
979  apply (case_tac "capa = ac")
980  by (clarsimp simp: masked_as_full_def is_cap_simps split: if_splits)+
981
982lemma transfer_caps_loop_pas_refined:
983  "\<lbrace>pas_refined aag and valid_objs and valid_mdb
984            and (\<lambda>s. (\<forall>x \<in> set caps. valid_cap (fst x) s \<and>
985                                      cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s
986                     \<and> real_cte_at (snd x) s) \<and>
987                     (\<forall>x\<in>set slots. real_cte_at x s \<and> cte_wp_at (\<lambda>cap. cap = NullCap) x s))
988            and K ((\<forall>slot \<in> set slots. is_subject aag (fst slot)) \<and>
989                   (\<forall>x \<in> set caps. is_subject aag (fst (snd x)) \<and>
990                   pas_cap_cur_auth aag (fst x)) \<and> distinct slots)\<rbrace>
991    transfer_caps_loop ep buffer n caps slots mi
992   \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>"
993  apply (rule hoare_pre)
994  apply (rule transfer_caps_loop_presM_extended
995              [where vo=True and em=True and ex=False and
996                     Psrc="\<lambda>slot . is_subject aag (fst slot)" and
997                     Pcap="pas_cap_cur_auth aag" and
998                     Pdest="\<lambda>slot . is_subject aag (fst slot)"])
999  apply (wp cap_insert_pas_refined)
1000     apply (fastforce simp: cte_wp_at_caps_of_state elim!: is_derived_is_transferable)
1001    apply (rule set_extra_badge_pas_refined)
1002   apply (erule(1) auth_derived_pas_cur_auth)
1003  apply (fastforce elim: cte_wp_at_weakenE)
1004  done
1005
1006
1007lemma transfer_caps_pas_refined:
1008  "\<lbrace>pas_refined aag and valid_objs and valid_mdb
1009    and (\<lambda>s. (\<forall>x \<in> set caps. valid_cap (fst x) s \<and> valid_cap (fst x) s \<and>
1010                                      cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s
1011                     \<and> real_cte_at (snd x) s))
1012    and K (is_subject aag receiver \<and> (\<forall>x \<in> set caps. is_subject aag (fst (snd x))) \<and> (\<forall>x \<in> set caps. pas_cap_cur_auth aag (fst x))) \<rbrace>
1013     transfer_caps info caps endpoint receiver recv_buf
1014   \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>"
1015  unfolding transfer_caps_def
1016  apply (rule hoare_pre)
1017  by (wp transfer_caps_loop_pas_refined get_receive_slots_authorised get_recv_slot_inv
1018         hoare_vcg_const_imp_lift hoare_vcg_all_lift grs_distinct
1019     | wpc | simp del: get_receive_slots.simps add: ball_conj_distrib)+
1020
1021
1022
1023crunch pas_refined[wp]: copy_mrs "pas_refined aag"
1024  (wp: crunch_wps)
1025
1026lemma lookup_cap_and_slot_authorised:
1027  "\<lbrace>pas_refined aag and K (is_subject aag thread)\<rbrace>
1028     lookup_cap_and_slot thread xs
1029   \<lbrace>\<lambda>rv s. is_subject aag (fst (snd rv))\<rbrace>, -"
1030  unfolding lookup_cap_and_slot_def
1031  apply (rule hoare_pre)
1032   apply (wp lookup_slot_for_thread_authorised
1033        | simp add: split_def)+
1034  done
1035
1036lemma lookup_extra_caps_authorised:
1037  "\<lbrace>pas_refined aag and K (is_subject aag thread)\<rbrace>
1038    lookup_extra_caps thread buffer mi
1039   \<lbrace>\<lambda>rv s. \<forall>cap \<in> set rv. is_subject aag (fst (snd cap))\<rbrace>, -"
1040  apply (simp add: lookup_extra_caps_def)
1041  apply (wp mapME_set lookup_cap_and_slot_authorised
1042       | simp)+
1043  done
1044
1045lemma lookup_cap_and_slot_cur_auth:
1046   "\<lbrace>pas_refined aag and K (is_subject aag thread)\<rbrace>
1047     lookup_cap_and_slot thread xs
1048   \<lbrace>\<lambda>rv s. pas_cap_cur_auth aag (fst rv)\<rbrace>, -"
1049  unfolding lookup_cap_and_slot_def
1050  apply (rule hoare_pre)
1051   apply (wp get_cap_auth_wp [where aag = aag] lookup_slot_for_thread_authorised
1052        | simp add: split_def)+
1053  done
1054
1055lemma lookup_extra_caps_auth:
1056  "\<lbrace>pas_refined aag and K (is_subject aag thread)\<rbrace>
1057    lookup_extra_caps thread buffer mi
1058   \<lbrace>\<lambda>rv s. \<forall>cap \<in> set rv. pas_cap_cur_auth aag (fst cap)\<rbrace>, -"
1059  apply (simp add: lookup_extra_caps_def)
1060  apply (wp mapME_set lookup_cap_and_slot_cur_auth
1061       | simp)+
1062  done
1063
1064lemma transfer_caps_empty_inv:
1065  "\<lbrace>P\<rbrace>  transfer_caps mi [] endpoint receiver rbuf \<lbrace>\<lambda>_. P\<rbrace>"
1066  unfolding transfer_caps_def
1067  by (wp | wpc | simp) +
1068
1069lemma lcs_valid':
1070  "\<lbrace>valid_objs\<rbrace> lookup_cap_and_slot thread xs \<lbrace>\<lambda>x s. s \<turnstile> fst x\<rbrace>, -"
1071  unfolding lookup_cap_and_slot_def
1072  apply (rule hoare_pre)
1073  apply wp
1074   apply (simp add: split_def)
1075   apply (wp lookup_slot_for_thread_inv | simp)+
1076  done
1077
1078lemma lec_valid_cap':
1079  "\<lbrace>valid_objs\<rbrace> lookup_extra_caps thread xa mi \<lbrace>\<lambda>rv s. (\<forall>x\<in>set rv. s \<turnstile> fst x)\<rbrace>, -"
1080  unfolding lookup_extra_caps_def
1081  by (wpsimp wp: mapME_set lcs_valid')
1082
1083(* FIXME: MOVE *)
1084lemma hoare_conjDR1:
1085  "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> R rv s\<rbrace>,- \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-"
1086  by (simp add:validE_def validE_R_def valid_def) blast
1087
1088lemma hoare_conjDR2:
1089  "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> R rv s\<rbrace>,- \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>,-"
1090  by (simp add:validE_def validE_R_def valid_def) blast
1091
1092lemma do_normal_transfer_pas_refined:
1093  "\<lbrace>pas_refined aag
1094        and valid_objs and valid_mdb
1095        and K (grant \<longrightarrow> is_subject aag sender)
1096        and K (grant \<longrightarrow> is_subject aag receiver)\<rbrace>
1097     do_normal_transfer sender sbuf endpoint badge grant receiver rbuf
1098   \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>"
1099proof(cases grant)
1100  case True thus ?thesis
1101    apply -
1102    apply (rule hoare_gen_asm)
1103    apply (simp add: do_normal_transfer_def)
1104    by (simp
1105         | wp copy_mrs_pas_refined transfer_caps_pas_refined lec_valid_cap'
1106           copy_mrs_cte_wp_at
1107           hoare_vcg_ball_lift
1108           lookup_extra_caps_srcs[simplified ball_conj_distrib,THEN hoare_conjDR1]
1109           lookup_extra_caps_srcs[simplified ball_conj_distrib,THEN hoare_conjDR2]
1110           lookup_extra_caps_authorised lookup_extra_caps_auth lec_valid_cap'
1111         | wpc | simp add:ball_conj_distrib)+
1112next
1113  case False thus ?thesis
1114    apply (simp add: do_normal_transfer_def)
1115    by (simp
1116          | wp copy_mrs_pas_refined transfer_caps_empty_inv
1117               copy_mrs_cte_wp_at
1118              hoare_vcg_const_imp_lift hoare_vcg_all_lift
1119         | wpc)+
1120qed
1121
1122crunch pas_refined[wp]: do_fault_transfer "pas_refined aag"
1123
1124lemma do_ipc_transfer_pas_refined:
1125  "\<lbrace>pas_refined aag
1126        and valid_objs and valid_mdb
1127        and K (grant \<longrightarrow> is_subject aag sender)
1128        and K (grant \<longrightarrow> is_subject aag receiver)\<rbrace>
1129     do_ipc_transfer sender ep badge grant receiver
1130   \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>"
1131  apply (simp add: do_ipc_transfer_def)
1132  apply (wp do_normal_transfer_pas_refined
1133            hoare_vcg_conj_lift hoare_vcg_all_lift
1134       | rule hoare_drop_imps
1135       | wpc)+
1136  by simp
1137
1138
1139(* FIXME MOVE*)
1140lemma cap_insert_pas_refined_transferable:
1141  "\<lbrace>pas_refined aag and valid_mdb
1142     and K (is_transferable_cap new_cap
1143            \<and> aag_cap_auth aag (pasObjectAbs aag (fst dest_slot)) new_cap
1144            \<and> (pasObjectAbs aag (fst src_slot), DeleteDerived, pasObjectAbs aag (fst dest_slot))
1145                           \<in> pasPolicy aag) \<rbrace>
1146     cap_insert new_cap src_slot dest_slot
1147   \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>"
1148  apply (rule hoare_gen_asm)
1149  apply (simp add: cap_insert_def)
1150  apply (rule hoare_pre)
1151  apply (wp set_cap_pas_refined set_cdt_pas_refined update_cdt_pas_refined hoare_vcg_imp_lift
1152            hoare_weak_lift_imp hoare_vcg_all_lift set_cap_caps_of_state2
1153            set_untyped_cap_as_full_cdt_is_original_cap get_cap_wp
1154            tcb_domain_map_wellformed_lift hoare_vcg_disj_lift
1155            set_untyped_cap_as_full_is_transferable'
1156        | simp split del: if_split del: split_paired_All fun_upd_apply
1157        | strengthen update_one_strg)+
1158  by (fastforce split: if_split_asm
1159                 simp: cte_wp_at_caps_of_state pas_refined_refl valid_mdb_def2
1160                       mdb_cte_at_def Option.is_none_def
1161             simp del: split_paired_All
1162                 dest: aag_cdt_link_Control aag_cdt_link_DeleteDerived cap_auth_caps_of_state
1163                intro: aag_wellformed_delete_derived_trans[OF _ _ pas_refined_wellformed])
1164
1165
1166lemma setup_caller_cap_pas_refined:
1167  "\<lbrace>pas_refined aag
1168         and valid_mdb
1169         and K((grant \<longrightarrow> is_subject aag sender \<and> is_subject aag receiver) \<and>
1170             (pasObjectAbs aag receiver, Reply, pasObjectAbs aag sender) \<in> pasPolicy aag )\<rbrace>
1171     setup_caller_cap sender receiver grant
1172   \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>"
1173  apply (simp add: setup_caller_cap_def)
1174  apply (rule conjI)
1175   (* if grant *)
1176   apply clarsimp
1177   apply (rule hoare_pre)
1178    apply (wpsimp wp: cap_insert_pas_refined set_thread_state_pas_refined)
1179   apply (fastforce simp: aag_cap_auth_def clas_no_asid cli_no_irqs pas_refined_refl)
1180   (* if not grant *)
1181  apply clarsimp
1182  apply (rule hoare_pre)
1183   apply (wp cap_insert_pas_refined_transferable set_thread_state_pas_refined)
1184  by (fastforce simp: aag_cap_auth_def cap_links_irq_def cap_links_asid_slot_def
1185                      cap_auth_conferred_def reply_cap_rights_to_auth_def
1186               intro: aag_wellformed_delete_derived[OF _ pas_refined_wellformed])
1187
1188(* FIXME: MOVE *)
1189lemma sym_ref_endpoint_recvD:
1190  assumes sym: "sym_refs (state_refs_of s)"
1191  and ep: "ko_at (Endpoint (RecvEP l)) epptr s"
1192  and inl: "t \<in> set l"
1193  shows "\<exists> pl. st_tcb_at ((=) (BlockedOnReceive epptr pl)) t s"
1194proof -
1195  have "(t, EPRecv) \<in> state_refs_of s epptr"
1196    using ep inl by (force simp: state_refs_of_def dest:ko_atD)
1197  hence "(epptr, TCBBlockedRecv) \<in> state_refs_of s t"
1198    using sym by (force dest:sym_refsD[rotated])
1199  thus ?thesis
1200    by (force simp: st_tcb_at_tcb_states_of_state_eq tcb_states_of_state_def get_tcb_def
1201                    state_refs_of_def tcb_st_refs_of_def tcb_bound_refs_def ep_q_refs_of_def
1202                    ntfn_q_refs_of_def ntfn_bound_refs_def
1203             split: ntfn.splits endpoint.splits thread_state.splits option.splits
1204                    kernel_object.splits)
1205qed
1206
1207lemma pas_refined_ep_recv:
1208  assumes policy: "pas_refined aag s"
1209  and invs: "invs s"
1210  and ep: "ko_at (Endpoint (RecvEP l)) epptr s"
1211  and inl: "t \<in> set l"
1212  shows "(pasObjectAbs aag t, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag"
1213  apply (insert sym_ref_endpoint_recvD[OF invs_sym_refs[OF invs] ep inl])
1214  apply clarsimp
1215  apply (clarsimp simp:st_tcb_at_tcb_states_of_state_eq)
1216  apply (rule pas_refined_mem[OF _ policy])
1217  apply (rule sta_ts[of epptr Receive])
1218  apply (simp add:thread_states_def)
1219  done
1220
1221lemma send_ipc_valid_ep_helper:
1222  "\<lbrakk>invs s ; ko_at (Endpoint (RecvEP (h # t))) epptr s \<rbrakk> \<Longrightarrow>
1223   valid_ep (case t of [] \<Rightarrow> IdleEP | h' # t'  \<Rightarrow> RecvEP t) s"
1224  apply (drule invs_valid_objs)
1225  apply (drule ko_atD)
1226  apply (erule(1) valid_objsE)
1227  by (cases t; simp add: valid_obj_def valid_ep_def)
1228
1229lemmas head_in_set = list.set_intros(1)[of h t for h t]
1230
1231
1232lemma send_ipc_pas_refined:
1233  "\<lbrace>pas_refined aag
1234       and invs
1235       and K (is_subject aag thread
1236              \<and> aag_has_auth_to aag SyncSend epptr
1237              \<and> (can_grant_reply \<longrightarrow> aag_has_auth_to aag Call epptr)
1238              \<and> (can_grant \<longrightarrow> aag_has_auth_to aag Grant epptr \<and> aag_has_auth_to aag Call epptr))\<rbrace>
1239     send_ipc block call badge can_grant can_grant_reply thread epptr
1240   \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>"
1241  apply (rule hoare_gen_asm)
1242  apply (simp add: send_ipc_def)
1243  apply (rule hoare_seq_ext[OF _ get_simple_ko_sp])
1244  apply (rule hoare_pre)
1245   apply (wpc | wp set_thread_state_pas_refined)+
1246         apply (simp add: hoare_if_r_and split del:if_split)
1247         apply (wp setup_caller_cap_pas_refined set_thread_state_pas_refined)+
1248       apply (simp split del:if_split)
1249       apply (rule_tac Q="\<lambda>rv.  valid_mdb
1250                            and pas_refined aag and K(
1251                      (can_grant \<or> can_grant_reply \<longrightarrow>   (reply_can_grant \<longrightarrow> is_subject aag x21) \<and>
1252                       (pasObjectAbs aag x21, Reply, pasSubject aag) \<in> pasPolicy aag))"
1253              in hoare_strengthen_post[rotated])
1254        apply simp
1255       apply (wp set_thread_state_pas_refined do_ipc_transfer_pas_refined static_imp_wp gts_wp
1256             | wpc
1257             | simp add: hoare_if_r_and)+
1258   apply (wp hoare_vcg_all_lift hoare_imp_lift_something | simp add:st_tcb_at_tcb_states_of_state_eq)+
1259  subgoal for ep s (* post-wp proof *)
1260    apply (intro conjI impI; clarsimp;
1261           frule(2) pas_refined_ep_recv[OF _ _ _ head_in_set])
1262
1263    subgoal (* can_grant *)
1264      apply (frule(2) aag_wellformed_grant_Control_to_recv[OF _ _ pas_refined_wellformed])
1265      apply (frule(2) aag_wellformed_reply[OF _ _ pas_refined_wellformed])
1266      apply (force elim: send_ipc_valid_ep_helper simp:aag_has_auth_to_Control_eq_owns)
1267      done
1268    subgoal (* can_grant_reply and not can_grant*)
1269      apply (frule(2) aag_wellformed_reply[OF _ _ pas_refined_wellformed])
1270      apply (frule(1) tcb_states_of_state_to_auth)
1271      (* Make the blockedOnReceive state point to epptr *)
1272      apply (frule(1) sym_ref_endpoint_recvD[OF invs_sym_refs _ head_in_set],
1273             clarsimp simp:st_tcb_at_tcb_states_of_state_eq)
1274      apply (fastforce elim: send_ipc_valid_ep_helper
1275                       simp: aag_has_auth_to_Control_eq_owns
1276                       dest: aag_wellformed_grant_Control_to_recv_by_reply
1277                               [OF _ _ _ pas_refined_wellformed])
1278      done
1279    subgoal (* not can_grant_reply and not can_grant*)
1280      by (force elim: send_ipc_valid_ep_helper)
1281    done
1282  done
1283
1284lemma set_simple_ko_get_tcb:
1285  "\<lbrace>\<lambda>s. P (get_tcb p s)\<rbrace> set_simple_ko f ep epptr \<lbrace>\<lambda>_ s. P (get_tcb p s) \<rbrace>"
1286  unfolding set_simple_ko_def set_object_def
1287  apply (wp get_object_wp)
1288  apply (auto simp: partial_inv_def a_type_def get_tcb_def obj_at_def the_equality
1289                 split: Structures_A.kernel_object.splits option.splits)
1290  done
1291
1292lemma get_tcb_is_Some_iff_typ_at:
1293  "(\<exists>y. get_tcb p s = Some y) = typ_at ATCB p s"
1294  by (simp add: tcb_at_typ [symmetric] tcb_at_def)
1295
1296lemma case_list_cons_cong:
1297  "(case xxs of [] \<Rightarrow> f | x # xs \<Rightarrow> g xxs)
1298 = (case xxs of [] \<Rightarrow> f | x # xs \<Rightarrow> g (x # xs))"
1299  by (simp split: list.split)
1300
1301lemma complete_signal_integrity:
1302  "\<lbrace>integrity aag X st and pas_refined aag and valid_objs
1303           and bound_tcb_at ((=) (Some ntfnptr)) thread
1304           and K (is_subject aag thread)\<rbrace>
1305     complete_signal ntfnptr thread
1306   \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
1307  apply (simp add: complete_signal_def)
1308  apply (rule hoare_seq_ext [OF _ get_simple_ko_sp])
1309  apply (rule hoare_pre)
1310  apply ((wp set_notification_respects[where auth=Receive] set_thread_state_integrity_autarch as_user_integrity_autarch
1311       | wpc
1312       | simp)+)[1]
1313  apply clarsimp
1314  apply (drule_tac t="pasSubject aag" in sym)
1315  apply (fastforce intro!: bound_tcb_at_implies_receive)
1316  done
1317
1318
1319match_abbreviation (input) receive_ipc_base2
1320  in concl receive_ipc_def
1321  select "case_endpoint X Y Z A" (for X Y Z A)
1322
1323abbreviation (input) receive_ipc_base
1324where
1325  "receive_ipc_base aag thread ep epptr rights is_blocking
1326    \<equiv> receive_ipc_base2 thread is_blocking epptr rights ep"
1327
1328
1329lemma sym_ref_endpoint_sendD:
1330  assumes sym: "sym_refs (state_refs_of s)"
1331  and ep: "ko_at (Endpoint (SendEP l)) epptr s"
1332  and inl: "t \<in> set l"
1333  shows "\<exists> pl. st_tcb_at ((=) (BlockedOnSend epptr pl)) t s"
1334proof -
1335  have "(t, EPSend) \<in> state_refs_of s epptr"
1336    using ep inl by (force simp: state_refs_of_def dest:ko_atD)
1337  hence "(epptr, TCBBlockedSend) \<in> state_refs_of s t"
1338    using sym by (force dest:sym_refsD[rotated])
1339  thus ?thesis
1340    by (force simp: st_tcb_at_tcb_states_of_state_eq tcb_states_of_state_def get_tcb_def
1341                    state_refs_of_def tcb_st_refs_of_def tcb_bound_refs_def ep_q_refs_of_def
1342                    ntfn_q_refs_of_def ntfn_bound_refs_def
1343             split: ntfn.splits endpoint.splits thread_state.splits option.splits
1344                    kernel_object.splits)
1345qed
1346
1347lemma receive_ipc_valid_ep_helper:
1348  "\<lbrakk> invs s; ko_at (Endpoint (SendEP list)) epptr s \<rbrakk> \<Longrightarrow>
1349   valid_ep (case tl list of [] \<Rightarrow> IdleEP | a # t \<Rightarrow> SendEP (tl list)) s"
1350  apply (drule_tac invs_valid_objs)
1351  apply (drule ko_atD)
1352  apply (erule(1) valid_objsE)
1353  apply (cases list, solves \<open>simp add: valid_obj_def valid_ep_def\<close>)
1354  by (cases "tl list"; clarsimp simp:valid_obj_def valid_ep_def)
1355
1356lemma receive_ipc_sender_helper:
1357  "\<lbrakk>pas_refined aag s ; kheap s thread = Some (TCB tcb) ; tcb_state tcb = BlockedOnSend ep pl\<rbrakk>
1358   \<Longrightarrow> (pasObjectAbs aag thread, SyncSend, pasObjectAbs aag ep) \<in> pasPolicy aag"
1359  apply (erule pas_refined_mem[rotated])
1360  apply (rule sta_ts)
1361  apply (simp add: thread_states_def tcb_states_of_state_def get_tcb_def)
1362  done
1363
1364lemma receive_ipc_sender_can_grant_helper:
1365  "\<lbrakk>invs s; pas_refined aag s ; kheap s thread = Some (TCB tcb) ; tcb_state tcb = BlockedOnSend ep pl;
1366    sender_can_grant pl ; aag_has_auth_to aag Receive ep\<rbrakk>
1367   \<Longrightarrow> is_subject aag thread"
1368  apply (frule pas_refined_mem[rotated,where x = "thread" and auth=Grant])
1369   apply (rule sta_ts)
1370   apply (simp add:thread_states_def tcb_states_of_state_def get_tcb_def)
1371  apply (frule(2) aag_wellformed_grant_Control_to_send[OF _ _ pas_refined_wellformed])
1372  apply (simp add:aag_has_auth_to_Control_eq_owns)
1373  done
1374
1375
1376lemma receive_ipc_base_pas_refined:
1377  "\<lbrace>pas_refined aag and invs
1378           and ko_at (Endpoint ep) epptr
1379           and K (is_subject aag thread
1380               \<and> (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and>
1381               (\<forall> auth \<in> cap_rights_to_auth rights True . aag_has_auth_to aag auth epptr))\<rbrace>
1382    receive_ipc_base aag thread ep epptr rights is_blocking
1383   \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>"
1384  (* FIXME: proof structure *)
1385  apply (rule hoare_gen_asm)
1386  apply (clarsimp simp: thread_get_def cong: endpoint.case_cong)
1387  apply (rule hoare_pre)
1388   apply (wp set_thread_state_pas_refined get_simple_ko_wp setup_caller_cap_pas_refined
1389        | wpc | simp add: thread_get_def do_nbrecv_failed_transfer_def split del: if_split)+
1390        apply (rename_tac list sss data)
1391        apply (rule_tac Q="\<lambda>rv s. pas_refined aag s \<and> valid_mdb s \<and>
1392                             (sender_can_grant data \<longrightarrow> is_subject aag (hd list)) \<and>
1393                             (sender_can_grant_reply data \<longrightarrow>
1394                             (AllowGrant \<in> rights \<longrightarrow> is_subject aag (hd list)) \<and>
1395                             (pasSubject aag, Reply, pasObjectAbs aag (hd list)) \<in> pasPolicy aag)"
1396                     in hoare_strengthen_post[rotated])
1397         apply (fastforce simp: cap_auth_conferred_def pas_refined_all_auth_is_owns
1398                                pas_refined_refl)
1399        apply (wp static_imp_wp do_ipc_transfer_pas_refined set_simple_ko_pas_refined
1400                  set_thread_state_pas_refined get_simple_ko_wp hoare_vcg_all_lift
1401                  hoare_vcg_imp_lift [OF set_simple_ko_get_tcb, unfolded disj_not1]
1402             | wpc
1403             | simp add: thread_get_def  get_thread_state_def do_nbrecv_failed_transfer_def)+
1404  apply (clarsimp simp: tcb_at_def [symmetric] tcb_at_st_tcb_at)
1405  subgoal premises prems for s
1406  proof -
1407    have "\<And>P Q R. \<lbrakk> R ; P \<Longrightarrow> R \<Longrightarrow> Q \<rbrakk> \<Longrightarrow> (P \<longrightarrow> Q) \<and> (\<not>P \<longrightarrow> R)" by blast
1408    thus ?thesis
1409      apply this
1410      using prems
1411       apply clarsimp
1412      subgoal premises prems for list ep' pl
1413      proof -
1414        have "sender_can_grant pl \<Longrightarrow> is_subject aag (hd list)"
1415          using prems
1416          apply (clarsimp elim!: tcb_atE simp:tcb_at_st_tcb_at[symmetric] get_tcb_def)
1417          apply (frule(1) sym_ref_endpoint_sendD[OF invs_sym_refs,where t= "hd list"],force)
1418          apply (clarsimp simp:st_tcb_at_def elim!:obj_atE)
1419          by (rule receive_ipc_sender_can_grant_helper)
1420        moreover have
1421          "sender_can_grant_reply pl \<Longrightarrow>
1422              (pasSubject aag, Reply, pasObjectAbs aag (hd list)) \<in> pasPolicy aag"
1423          using prems
1424          apply (clarsimp elim!: tcb_atE simp:tcb_at_st_tcb_at[symmetric] get_tcb_def)
1425          apply (frule(1) sym_ref_endpoint_sendD[OF invs_sym_refs,where t= "hd list"],force)
1426          apply (clarsimp simp:st_tcb_at_def elim!:obj_atE)
1427          apply (frule pas_refined_mem[rotated,where x = "(hd list)" and auth=Call])
1428           apply (rule sta_ts)
1429           apply (simp add:thread_states_def tcb_states_of_state_def get_tcb_def)
1430          by (erule(2) aag_wellformed_reply[OF _ _ pas_refined_wellformed])
1431        ultimately show ?thesis
1432          using prems by (force dest:receive_ipc_valid_ep_helper)
1433      qed
1434      apply clarsimp
1435      using prems
1436      apply (intro conjI;clarsimp simp add:cap_rights_to_auth_def)
1437      apply (clarsimp elim!: tcb_atE simp:tcb_at_st_tcb_at[symmetric] get_tcb_def
1438                             cap_rights_to_auth_def)
1439      apply (frule_tac t="hd x" in sym_ref_endpoint_sendD[OF invs_sym_refs],assumption,force)
1440      apply (clarsimp simp:st_tcb_at_def elim!:obj_atE)
1441      apply (frule_tac x="hd x" in pas_refined_mem[rotated,where auth=Call])
1442       apply (rule sta_ts)
1443       apply (simp add:thread_states_def tcb_states_of_state_def get_tcb_def)
1444      apply (frule aag_wellformed_grant_Control_to_send_by_reply[OF _ _ _ pas_refined_wellformed])
1445      by (force simp:aag_has_auth_to_Control_eq_owns)+
1446  qed
1447  done
1448
1449lemma complete_signal_pas_refined:
1450  "\<lbrace>pas_refined aag and bound_tcb_at ((=) (Some ntfnptr)) thread\<rbrace>
1451     complete_signal ntfnptr thread
1452   \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>"
1453  apply (simp add: complete_signal_def)
1454  apply (rule hoare_seq_ext [OF _ get_simple_ko_sp])
1455  apply (rule hoare_pre)
1456  apply (wp set_simple_ko_pas_refined set_thread_state_pas_refined
1457       | wpc)+
1458  apply clarsimp
1459  done
1460
1461lemma receive_ipc_pas_refined:
1462  "\<lbrace>pas_refined aag
1463         and invs
1464         and K (is_subject aag thread
1465              \<and> pas_cap_cur_auth aag ep_cap \<and> AllowRead \<in> cap_rights ep_cap)\<rbrace>
1466     receive_ipc thread ep_cap is_blocking
1467   \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>"
1468  apply (rule hoare_gen_asm)
1469  apply (simp add: receive_ipc_def thread_get_def  split: cap.split)
1470  apply clarsimp
1471  apply (rule hoare_seq_ext[OF _ get_simple_ko_sp])
1472  apply (rule hoare_seq_ext[OF _ gbn_sp])
1473  apply (case_tac ntfnptr, simp_all)
1474  (* old receive_ipc stuff *)
1475   apply (rule hoare_pre)
1476    apply (wp receive_ipc_base_pas_refined)[1]
1477   apply (fastforce simp: aag_cap_auth_def cap_auth_conferred_def cap_rights_to_auth_def)
1478   (* ntfn-binding case *)
1479  apply clarsimp
1480  apply (rule hoare_seq_ext[OF _ get_simple_ko_sp])
1481  apply (case_tac "isActive ntfn", simp_all)
1482   apply (wp complete_signal_pas_refined, clarsimp)
1483   (* regular case again *)
1484  apply (rule hoare_pre, wp receive_ipc_base_pas_refined)
1485  apply (fastforce simp: aag_cap_auth_def cap_auth_conferred_def cap_rights_to_auth_def)
1486  done
1487
1488
1489subsection \<open>@{term "integrity"}\<close>
1490
1491subsubsection\<open>autarchy\<close>
1492
1493text\<open>
1494
1495  For the case when the currently-running thread owns the receiver
1496  (i.e. receiver last to the IPC rendezvous or sender owns receiver).
1497
1498\<close>
1499
1500
1501lemma set_extra_badge_integrity_autarch:
1502  "\<lbrace>(integrity aag X st and
1503         K (is_subject aag thread \<and>
1504            ipc_buffer_has_auth aag thread (Some buf) \<and>
1505            buffer_cptr_index + n < 2 ^ (msg_align_bits - 2)))\<rbrace>
1506  set_extra_badge buf badge n
1507  \<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
1508  unfolding set_extra_badge_def
1509  by (wp store_word_offs_integrity_autarch)
1510
1511lemma transfer_caps_integrity_autarch:
1512  "\<lbrace>pas_refined aag
1513        and integrity aag X st
1514        and valid_objs and valid_mdb
1515        and (\<lambda> s. (\<forall>x\<in>set caps.
1516               s \<turnstile> fst x) \<and>
1517              (\<forall>x\<in>set caps.
1518               cte_wp_at
1519                (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow>
1520                      cp = fst x)
1521                (snd x) s \<and>
1522               real_cte_at (snd x) s))
1523        and K (is_subject aag receiver \<and> ipc_buffer_has_auth aag receiver receive_buffer \<and>
1524               (\<forall>x\<in>set caps. is_subject aag (fst (snd x))) \<and> length caps < 6)\<rbrace>
1525    transfer_caps mi caps endpoint receiver receive_buffer
1526   \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
1527  apply (rule hoare_gen_asm)
1528  apply (simp add: transfer_caps_def)
1529  apply (wpc | wp)+
1530  apply (rule_tac P = "\<forall>x \<in> set dest_slots. is_subject aag (fst x)" in hoare_gen_asm)
1531  apply (wp transfer_caps_loop_pres_dest cap_insert_integrity_autarch set_extra_badge_integrity_autarch [where aag = aag and thread = receiver]
1532            get_receive_slots_authorised hoare_vcg_all_lift hoare_vcg_imp_lift
1533       | simp add: msg_align_bits buffer_cptr_index_def msg_max_length_def cte_wp_at_caps_of_state
1534       | blast)+
1535  done
1536
1537(* FIXME: duplicate somehow *)
1538lemma load_word_offs_inv[wp]:
1539  "\<lbrace>P\<rbrace> load_word_offs buf off \<lbrace>\<lambda>rv. P\<rbrace>"
1540  apply (simp add: load_word_offs_def do_machine_op_def split_def)
1541  apply wp
1542  apply clarsimp
1543  apply (drule in_inv_by_hoareD[OF loadWord_inv])
1544  apply simp
1545  done
1546
1547lemma copy_mrs_integrity_autarch:
1548  "\<lbrace>pas_refined aag and integrity aag X st and K (is_subject aag receiver \<and> ipc_buffer_has_auth aag receiver rbuf \<and> unat n < 2 ^ (msg_align_bits - 2))\<rbrace>
1549     copy_mrs sender sbuf receiver rbuf n
1550   \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
1551  apply (rule hoare_gen_asm)
1552  apply (simp add: copy_mrs_def cong: if_cong split del: if_split)
1553  apply (wp mapM_wp' as_user_integrity_autarch
1554            store_word_offs_integrity_autarch [where aag = aag and thread = receiver]
1555       | wpc
1556       | simp
1557       | fastforce simp: length_msg_registers msg_align_bits split: if_split_asm)+
1558  done
1559
1560(* FIXME: Why was the [wp] attribute clobbered by interpretation of the Arch locale? *)
1561declare as_user_thread_bound_ntfn[wp]
1562
1563lemma get_mi_valid':
1564  "\<lbrace>\<top>\<rbrace> get_message_info a \<lbrace>\<lambda>rv s. valid_message_info rv\<rbrace>"
1565  apply (simp add: get_message_info_def)
1566  apply (wp, rule hoare_post_imp, rule data_to_message_info_valid)
1567   apply wp+
1568  done
1569
1570lemma lookup_extra_caps_length:
1571  "\<lbrace>K (valid_message_info mi)\<rbrace> lookup_extra_caps thread buf mi \<lbrace>\<lambda>rv s. length rv < 6\<rbrace>, -"
1572  unfolding lookup_extra_caps_def
1573  apply (cases buf, simp_all)
1574   apply (wp mapME_length | simp add: comp_def  valid_message_info_def msg_max_extra_caps_def word_le_nat_alt)+
1575  done
1576
1577lemma get_mi_length:
1578  "\<lbrace>\<top>\<rbrace> get_message_info sender \<lbrace>\<lambda>rv s. unat (mi_length rv) < 2 ^ (msg_align_bits - 2)\<rbrace>"
1579  apply (rule hoare_post_imp [OF _ get_mi_valid'])
1580  apply (clarsimp simp: valid_message_info_def msg_align_bits msg_max_length_def word_le_nat_alt)
1581  done
1582
1583lemma do_normal_transfer_send_integrity_autarch:
1584  notes lec_valid_cap[wp del]
1585  shows
1586  "\<lbrace>pas_refined aag
1587        and integrity aag X st
1588        and valid_objs and valid_mdb
1589        and K (is_subject aag receiver \<and>
1590               ipc_buffer_has_auth aag receiver rbuf \<and>
1591               (grant \<longrightarrow> is_subject aag sender))\<rbrace>
1592     do_normal_transfer sender sbuf endpoint badge grant receiver rbuf
1593   \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
1594  apply (simp add: do_normal_transfer_def)
1595  apply (wp as_user_integrity_autarch set_message_info_integrity_autarch transfer_caps_integrity_autarch
1596            copy_mrs_integrity_autarch
1597            copy_mrs_tcb copy_mrs_cte_wp_at lookup_extra_caps_authorised
1598            lookup_extra_caps_length get_mi_length get_mi_valid'
1599            hoare_vcg_conj_lift hoare_vcg_ball_lift lec_valid_cap' static_imp_wp
1600       | wpc
1601       | simp)+
1602  done
1603
1604crunch integrity_autarch: setup_caller_cap "integrity aag X st"
1605
1606lemma do_fault_transfer_integrity_autarch:
1607  "\<lbrace>integrity aag X st and K (is_subject aag receiver \<and> ipc_buffer_has_auth aag receiver recv_buf) \<rbrace>
1608    do_fault_transfer badge sender receiver recv_buf
1609   \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
1610  apply (simp add: do_fault_transfer_def split_def)
1611  apply (wp as_user_integrity_autarch set_message_info_integrity_autarch set_mrs_integrity_autarch
1612            thread_get_wp'
1613       | wpc | simp)+
1614  done
1615
1616lemma do_ipc_transfer_integrity_autarch:
1617  "\<lbrace>pas_refined aag
1618        and integrity aag X st
1619        and valid_objs and valid_mdb
1620        and K (is_subject aag receiver \<and> (grant \<longrightarrow> is_subject aag sender))\<rbrace>
1621     do_ipc_transfer sender ep badge grant receiver
1622   \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
1623  apply (simp add: do_ipc_transfer_def)
1624  apply (wp do_normal_transfer_send_integrity_autarch do_fault_transfer_integrity_autarch
1625            thread_get_wp' lookup_ipc_buffer_has_auth hoare_vcg_all_lift
1626       | wpc | simp | wp (once) hoare_drop_imps)+
1627  done
1628
1629lemma set_thread_state_running_respects:
1630  "\<lbrace>integrity aag X st
1631        and (\<lambda>s. \<exists>ep. aag_has_auth_to aag Receive ep
1632                   \<and> st_tcb_at (send_blocked_on ep) sender s)\<rbrace>
1633     set_thread_state sender Structures_A.Running
1634   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
1635  apply (simp add: set_thread_state_def)
1636  apply (wpsimp wp: set_object_wp)
1637  apply (erule integrity_trans)
1638  apply (clarsimp simp: integrity_def obj_at_def st_tcb_at_def)
1639  apply (clarsimp dest!: get_tcb_SomeD)
1640  apply (rule_tac new_st=Running in tro_tcb_receive)
1641  apply (auto simp: tcb_bound_notification_reset_integrity_def)
1642  done
1643
1644(* FIXME move *)
1645lemma set_simple_ko_obj_at:
1646  "\<lbrace>obj_at P ptr and K (ptr \<noteq> epptr)\<rbrace>
1647     set_simple_ko f epptr ep
1648   \<lbrace>\<lambda>rv. obj_at P ptr\<rbrace>"
1649  apply (simp add: set_simple_ko_def set_object_def)
1650  apply (wp get_object_wp)
1651  apply (auto simp: obj_at_def)
1652  done
1653
1654(* ep is free here *)
1655lemma sts_receive_Inactive_respects:
1656  "\<lbrace>integrity aag X st and st_tcb_at (send_blocked_on ep) thread
1657    and (\<lambda>s. \<forall>tcb. get_tcb thread s = Some tcb \<longrightarrow> call_blocked ep (tcb_state tcb))
1658    and K (aag_has_auth_to aag Receive ep)\<rbrace>
1659    set_thread_state thread Structures_A.thread_state.Inactive
1660   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
1661  apply (simp add: set_thread_state_def set_object_def get_object_def)
1662  apply wp
1663  apply clarsimp
1664  apply (erule integrity_trans)
1665  apply (clarsimp simp: integrity_def)
1666  apply (drule get_tcb_SomeD)
1667  apply (rule_tac new_st=Inactive in tro_tcb_receive, simp_all)
1668  apply (fastforce simp add: st_tcb_at_def obj_at_def)
1669  done
1670
1671crunch pred_tcb: do_ipc_transfer "pred_tcb_at proj P t"
1672  (wp: crunch_wps transfer_caps_loop_pres make_fault_message_inv simp: zipWithM_x_mapM)
1673
1674lemma set_untyped_cap_as_full_not_untyped:
1675  "\<lbrace> P and K(\<not> is_untyped_cap cap') \<rbrace>
1676   set_untyped_cap_as_full cap cap' slot
1677   \<lbrace> \<lambda>rv. P\<rbrace>"
1678  unfolding set_untyped_cap_as_full_def
1679  apply wp
1680  apply (rule hoare_pre_cont)
1681   apply wpsimp+
1682  done
1683
1684
1685lemma cap_insert_integrity_autarch_not_untyped:
1686  "\<lbrace>integrity aag X st and
1687     K (\<not> is_untyped_cap cap \<and> is_subject aag (fst dest_slot))\<rbrace>
1688   cap_insert cap src_slot dest_slot
1689   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
1690  apply (simp add:cap_insert_def)
1691  apply (wp set_original_integrity_autarch cap_insert_ext_extended.list_integ_lift
1692            cap_insert_list_integrity update_cdt_fun_upd_integrity_autarch gets_inv
1693            set_cap_integrity_autarch set_untyped_cap_as_full_not_untyped assert_inv)
1694  apply fastforce
1695  done
1696
1697(* FIXME MOVE*)
1698lemma pred_tcb_atE:
1699  assumes hyp: "pred_tcb_at proj pred t s"
1700  obtains tcb where "kheap s t = Some (TCB tcb)" and " pred (proj (tcb_to_itcb tcb))"
1701  using hyp by (fastforce elim:obj_atE simp:pred_tcb_at_def)
1702
1703
1704lemma set_thread_state_blocked_on_reply_respects:
1705  "\<lbrace> integrity aag X st and
1706       st_tcb_at (send_blocked_on ep) thread and
1707       pred_tcb_at id (\<lambda>itcb. allowed_call_blocked ep (itcb_state itcb)) thread
1708       and K(aag_has_auth_to aag Receive ep)\<rbrace>
1709     set_thread_state thread BlockedOnReply
1710   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
1711  apply (rule hoare_gen_asm)
1712  apply (rule hoare_pre)
1713  apply (simp add: set_thread_state_def set_object_def get_object_def)
1714  apply wp
1715  apply clarsimp
1716  apply (erule integrity_trans)
1717  apply (clarsimp simp:integrity_def dest!:get_tcb_SomeD elim!: pred_tcb_atE)
1718  apply (rule tro_tcb_receive[where new_st=BlockedOnReply])
1719  by fastforce+
1720
1721lemma setup_caller_cap_integrity_recv:
1722  "\<lbrace>integrity aag X st and valid_mdb
1723       and st_tcb_at (send_blocked_on ep) sender and
1724       pred_tcb_at id (\<lambda>itcb. allowed_call_blocked ep (itcb_state itcb)) sender
1725      and K (aag_has_auth_to aag Receive ep \<and> is_subject aag receiver
1726             \<and> (grant \<longrightarrow> is_subject aag sender))\<rbrace>
1727     setup_caller_cap sender receiver grant
1728   \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
1729  apply (rule hoare_gen_asm)
1730  apply (rule hoare_pre)
1731  apply (unfold setup_caller_cap_def)
1732  apply (wp cap_insert_integrity_autarch_not_untyped set_thread_state_blocked_on_reply_respects)
1733  by fastforce
1734
1735lemma pred_tcb_atI:
1736  "\<lbrakk>kheap s t = Some (TCB tcb) ;pred (proj (tcb_to_itcb tcb))\<rbrakk> \<Longrightarrow> pred_tcb_at proj pred t s"
1737  by (fastforce simp:pred_tcb_at_def obj_at_def)
1738
1739(* FIXME MOVE *)
1740abbreviation
1741  sender_can_call :: "sender_payload \<Rightarrow> bool"
1742where
1743  "sender_can_call pl \<equiv> sender_can_grant pl \<or> sender_can_grant_reply pl"
1744
1745lemma receive_ipc_base_integrity:
1746  notes do_nbrecv_failed_transfer_def[simp]
1747  shows "\<lbrace>pas_refined aag and integrity aag X st and invs
1748          and ko_at (Endpoint ep) epptr
1749          and K (is_subject aag receiver
1750                \<and> (pasSubject aag, Receive, pasObjectAbs aag epptr) \<in> pasPolicy aag
1751                \<and> (\<forall>auth \<in> cap_rights_to_auth rights True. aag_has_auth_to aag auth epptr))\<rbrace>
1752          receive_ipc_base aag receiver ep epptr rights is_blocking
1753         \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
1754  apply (rule hoare_gen_asm)
1755  apply (clarsimp simp: thread_get_def get_thread_state_def cong: endpoint.case_cong)
1756  apply (rule hoare_pre)
1757   apply (wp set_endpoinintegrity set_thread_state_running_respects
1758             setup_caller_cap_integrity_recv[where ep = epptr]
1759             do_ipc_transfer_integrity_autarch
1760             set_thread_state_integrity_autarch[where param_a=receiver]
1761             sts_receive_Inactive_respects[where ep = epptr]
1762             as_user_integrity_autarch
1763       | wpc | simp)+
1764        apply (rename_tac list tcb data)
1765        apply (rule_tac Q="\<lambda>rv s. integrity aag X st s
1766                           \<and> valid_mdb s
1767                           \<and> is_subject aag receiver
1768                           \<and> (sender_can_call data \<longrightarrow> AllowGrant \<in> rights
1769                                                   \<longrightarrow> is_subject aag (hd list))
1770                           \<and> (sender_can_grant data \<longrightarrow> is_subject aag (hd list))
1771                           \<and> st_tcb_at (send_blocked_on epptr) (hd list) s
1772                           \<and> st_tcb_at (\<lambda>st. st = BlockedOnSend epptr data) (hd list) s"
1773                     in hoare_strengthen_post[rotated])
1774         apply (fastforce simp: st_tcb_at_def obj_at_def get_tcb_rev call_blocked_def
1775                                allowed_call_blocked_def
1776                         dest!: get_tcb_SomeD
1777                         elim: pred_tcb_atI)
1778        apply (wp do_ipc_transfer_integrity_autarch do_ipc_transfer_pred_tcb set_endpoinintegrity
1779                  get_simple_ko_wp
1780                  set_thread_state_integrity_autarch[where param_a=receiver]
1781                  hoare_vcg_imp_lift [OF set_simple_ko_get_tcb, unfolded disj_not1]
1782                  hoare_vcg_all_lift as_user_integrity_autarch
1783              | wpc | simp)+
1784  apply clarsimp
1785  apply (subgoal_tac "ep_at epptr s \<and> (\<exists>auth. aag_has_auth_to aag auth epptr
1786                                    \<and> (auth = Receive \<or> auth = SyncSend \<or> auth = Reset))")
1787   prefer 2
1788   apply (fastforce simp: obj_at_def is_ep)
1789  apply simp
1790  apply (thin_tac "ep_at epptr s \<and> (\<exists>auth. aag_has_auth_to aag auth epptr
1791                                 \<and> (auth = Receive \<or> auth = SyncSend \<or> auth = Reset))")
1792  apply (clarsimp simp: st_tcb_def2 a_type_def)
1793  apply (frule_tac t="hd x" in sym_ref_endpoint_sendD[OF invs_sym_refs],assumption,force)
1794  apply (clarsimp simp: get_tcb_def elim!: pred_tcb_atE)
1795  apply (intro conjI;
1796         (force elim: receive_ipc_valid_ep_helper receive_ipc_sender_can_grant_helper)?)
1797  apply (intro impI)
1798  apply (frule_tac x= "hd x" in pas_refined_mem[rotated,where auth=Call])
1799   apply (rule sta_ts)
1800   apply (simp add: thread_states_def tcb_states_of_state_def get_tcb_def)
1801  apply (simp add: cap_rights_to_auth_def)
1802  apply (rule aag_has_auth_to_Control_eq_owns[THEN iffD1],assumption)
1803  apply (erule aag_wellformed_grant_Control_to_send_by_reply[OF _ _ _ pas_refined_wellformed];force)
1804  done
1805
1806lemma receive_ipc_integrity_autarch:
1807  "\<lbrace>pas_refined aag and integrity aag X st and invs
1808        and K (is_subject aag receiver
1809            \<and> pas_cap_cur_auth aag cap \<and> AllowRead \<in> cap_rights cap)\<rbrace>
1810    receive_ipc receiver cap is_blocking
1811   \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
1812  apply (rule hoare_gen_asm)
1813  apply (simp add: receive_ipc_def split: cap.splits)
1814  apply clarsimp
1815  apply (rule hoare_seq_ext[OF _ get_simple_ko_sp])
1816  apply (rule hoare_seq_ext[OF _ gbn_sp])
1817  apply (case_tac ntfnptr, simp_all)
1818  (* old receive case, not bound *)
1819   apply (rule hoare_pre, wp receive_ipc_base_integrity)
1820   apply (fastforce simp:aag_cap_auth_def cap_auth_conferred_def cap_rights_to_auth_def)
1821  apply (rule hoare_seq_ext[OF _ get_simple_ko_sp])
1822  apply (case_tac "isActive ntfn", simp_all)
1823  (* new ntfn-binding case *)
1824   apply (rule hoare_pre, wp complete_signal_integrity, clarsimp)
1825   (* old receive case, bound ntfn not active *)
1826  apply (rule hoare_pre, wp receive_ipc_base_integrity)
1827  apply (fastforce simp:aag_cap_auth_def cap_auth_conferred_def cap_rights_to_auth_def)
1828  done
1829
1830subsubsection\<open>Non-autarchy: the sender is running\<close>
1831
1832text\<open>
1833
1834  If the sender is running (i.e. last to the IPC rendezvous) then we
1835  need this auxiliary machinery to show that the sequence of TCB
1836  updates ends up in the tcb_send, tcb_call or tcb_reply case of @{term integrity_obj}.
1837
1838  This machinery is used for both send_ipc and do_reply_transfer
1839
1840  The sender can update an IPC receiver's context as much as it likes,
1841  provided it eventually changes the thread state to Running.
1842
1843\<close>
1844
1845datatype tcb_respects_state = TRContext | TRFinal | TRFinalOrCall | TRReplyContext
1846
1847inductive
1848  tcb_in_ipc for aag tst l' epptr ko ko'
1849where
1850  tii_lrefl: "\<lbrakk> l' = pasSubject aag \<rbrakk> \<Longrightarrow> tcb_in_ipc aag tst l' epptr ko ko'"
1851| tii_context: "\<lbrakk> ko  = Some (TCB tcb);
1852                  ko' = Some (TCB tcb');
1853                  can_receive_ipc (tcb_state tcb);
1854                  \<exists>ctxt'. tcb' = tcb \<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb)\<rparr>;
1855                  tst = TRContext\<rbrakk>
1856        \<Longrightarrow> tcb_in_ipc aag tst l' epptr ko ko'"
1857| tii_final: "\<lbrakk> ko  = Some (TCB tcb);
1858                ko' = Some (TCB tcb');
1859                receive_blocked_on epptr (tcb_state tcb);
1860                \<exists>ctxt'. tcb' = tcb \<lparr> tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb)
1861                                   , tcb_state := Structures_A.Running\<rparr>;
1862                aag_has_auth_to aag SyncSend epptr;
1863                tst = TRFinal \<or> tst = TRFinalOrCall\<rbrakk>
1864         \<Longrightarrow> tcb_in_ipc aag tst l' epptr ko ko'"
1865| tii_call:  "\<lbrakk> ko  = Some (TCB tcb);
1866                ko' = Some (TCB tcb');
1867                ep_recv_blocked epptr (tcb_state tcb);
1868                \<exists>ctxt'. tcb' = tcb \<lparr> tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb),
1869                                     tcb_state := Structures_A.Running,
1870                                     tcb_caller := ReplyCap caller False R\<rparr>;
1871                is_subject aag caller;
1872                aag_has_auth_to aag Call epptr;
1873                tst = TRFinal\<rbrakk>
1874         \<Longrightarrow> tcb_in_ipc aag tst l' epptr ko ko'"
1875| tii_reply:  "\<lbrakk> ko  = Some (TCB tcb);
1876                ko' = Some (TCB tcb');
1877                \<exists>ctxt'. tcb' = tcb \<lparr> tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb),
1878                                     tcb_fault := None,
1879                                     tcb_state := Structures_A.Running\<rparr>;
1880                (pasSubject aag, Reply, l') \<in> pasPolicy aag;
1881                tcb_state tcb = BlockedOnReply;
1882                tst = TRFinal\<rbrakk>
1883         \<Longrightarrow> tcb_in_ipc aag tst l' epptr ko ko'"
1884
1885lemmas tii_subject[simp] = tii_lrefl [OF refl]
1886
1887definition integrity_tcb_in_ipc
1888  :: "'a PAS \<Rightarrow> obj_ref set \<Rightarrow> obj_ref \<Rightarrow> obj_ref \<Rightarrow> tcb_respects_state \<Rightarrow>
1889      det_ext state \<Rightarrow> det_ext state \<Rightarrow> bool"
1890where
1891  "integrity_tcb_in_ipc aag X thread epptr tst st \<equiv> \<lambda>s.
1892     \<not> is_subject aag thread \<and> pas_refined aag st \<and>
1893     (integrity aag X st (s\<lparr>kheap := (kheap s)(thread := kheap st thread),
1894                            machine_state :=
1895                               (machine_state s)\<lparr>underlying_memory :=
1896                                    (\<lambda>p. if p \<in> auth_ipc_buffers st thread then
1897                                         underlying_memory (machine_state st) p
1898                                         else underlying_memory (machine_state s) p) \<rparr>\<rparr>)
1899   \<and> (tcb_in_ipc aag tst (pasObjectAbs aag thread) epptr (kheap st thread) (kheap s thread)))"
1900
1901lemma tcb_context_no_change:
1902  "\<exists>ctxt. tcb = tcb\<lparr> tcb_arch :=  arch_tcb_context_set ctxt (tcb_arch tcb)\<rparr>"
1903  apply (cases tcb, clarsimp)
1904  apply (case_tac tcb_arch)
1905  apply (auto simp: arch_tcb_context_set_def)
1906  done
1907
1908lemma auth_ipc_buffers_mem_Write:
1909  "\<lbrakk> x \<in> auth_ipc_buffers s thread; pas_refined aag s; valid_objs s; is_subject aag thread \<rbrakk>
1910  \<Longrightarrow> aag_has_auth_to aag Write x"
1911  apply (clarsimp simp add: auth_ipc_buffers_member_def)
1912  apply (drule (1) cap_cur_auth_caps_of_state)
1913   apply simp
1914  apply (clarsimp simp: aag_cap_auth_def cap_auth_conferred_def
1915                        vspace_cap_rights_to_auth_def vm_read_write_def
1916                        is_page_cap_def
1917                 split: if_split_asm)
1918  apply (auto dest: ipcframe_subset_page)
1919  done
1920
1921
1922lemma integrity_tcb_in_ipc_final:
1923  "\<lbrakk> integrity_tcb_in_ipc aag X thread epptr TRFinal st s \<rbrakk> \<Longrightarrow> integrity aag X st s"
1924  unfolding integrity_tcb_in_ipc_def
1925  apply clarsimp
1926  apply (erule integrity_trans)
1927  apply (clarsimp simp: integrity_def)
1928  apply (rule conjI)
1929   apply (erule tcb_in_ipc.cases; simp)
1930     apply (fastforce intro!: tro_tcb_send simp: direct_send_def)
1931    apply (fastforce intro!: tro_tcb_call  simp: direct_call_def)
1932    apply clarsimp
1933   apply (fastforce intro!: tro_tcb_reply tcb.equality simp: direct_reply_def)
1934    \<comment> \<open>rm\<close>
1935  apply clarsimp
1936  apply (cases "is_subject aag thread")
1937   apply (rule trm_write)
1938   apply (solves\<open>simp\<close>)
1939  \<comment> \<open>doesn't own\<close>
1940  apply (erule tcb_in_ipc.cases, simp_all)[1]
1941    apply clarsimp
1942    apply (rule trm_ipc [where p' = thread])
1943       apply (simp add: tcb_states_of_state_def get_tcb_def)
1944      apply (simp add: tcb_states_of_state_def get_tcb_def)
1945     apply (simp add: auth_ipc_buffers_def get_tcb_def
1946      split: option.split_asm cap.split_asm arch_cap.split_asm if_split_asm  split del: if_split)
1947    apply simp
1948   apply clarsimp
1949   apply (rule trm_ipc [where p' = thread])
1950      apply (simp add: tcb_states_of_state_def get_tcb_def split:thread_state.splits)
1951     apply (simp add: tcb_states_of_state_def get_tcb_def)
1952    apply (simp add: auth_ipc_buffers_def get_tcb_def
1953      split: option.split_asm cap.split_asm arch_cap.split_asm if_split_asm  split del: if_split)
1954   apply simp
1955  apply clarsimp
1956  apply (rule trm_ipc [where p' = thread])
1957     apply (simp add: tcb_states_of_state_def get_tcb_def split:thread_state.splits)
1958    apply (simp add: tcb_states_of_state_def get_tcb_def)
1959   apply (simp add: auth_ipc_buffers_def get_tcb_def
1960     split: option.split_asm cap.split_asm arch_cap.split_asm if_split_asm  split del: if_split)
1961  apply simp
1962  done
1963
1964lemma update_tcb_context_in_ipc:
1965  "\<lbrakk> integrity_tcb_in_ipc aag X thread epptr TRContext st s;
1966     get_tcb thread s = Some tcb;
1967     tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb)\<rparr>\<rbrakk>
1968     \<Longrightarrow> integrity_tcb_in_ipc aag X thread epptr TRContext st
1969                              (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb')\<rparr>)"
1970  unfolding integrity_tcb_in_ipc_def
1971  apply (elim conjE)
1972  apply (intro conjI)
1973    apply assumption+
1974   apply (erule integrity_trans)
1975   apply (simp cong: if_cong)
1976  apply clarsimp
1977  apply (erule tcb_in_ipc.cases, simp_all)
1978   apply (auto intro!: tii_context[OF refl refl] tii_lrefl[OF refl]  tcb_context_no_change
1979                dest!: get_tcb_SomeD simp: arch_tcb_context_set_def)
1980  done
1981
1982
1983lemma update_tcb_state_in_ipc:
1984  "\<lbrakk> integrity_tcb_in_ipc aag X thread epptr TRContext st s;
1985      receive_blocked_on epptr (tcb_state tcb); aag_has_auth_to aag SyncSend epptr;
1986     get_tcb thread s = Some tcb; tcb' = tcb\<lparr>tcb_state := Structures_A.thread_state.Running\<rparr> \<rbrakk>
1987     \<Longrightarrow> integrity_tcb_in_ipc aag X thread epptr TRFinalOrCall st
1988                              (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB tcb')\<rparr>)"
1989  unfolding integrity_tcb_in_ipc_def
1990  apply (elim conjE)
1991  apply (intro conjI)
1992     apply assumption+
1993   apply (erule integrity_trans)
1994   apply (simp cong: if_cong)
1995  apply clarsimp
1996  apply (erule tcb_in_ipc.cases, simp_all)
1997  apply (drule get_tcb_SomeD)
1998  apply (rule tii_final[OF refl refl])
1999     apply (solves\<open>clarsimp\<close>)
2000    apply (elim exE, intro exI tcb.equality; solves \<open>simp\<close>)
2001   apply fastforce
2002  apply fastforce
2003  done
2004
2005lemma as_user_respects_in_ipc:
2006  "\<lbrace>integrity_tcb_in_ipc aag X thread epptr TRContext st\<rbrace>
2007     as_user thread m
2008   \<lbrace>\<lambda>rv. integrity_tcb_in_ipc aag X thread epptr TRContext st\<rbrace>"
2009  apply (simp add: as_user_def set_object_def get_object_def)
2010  apply (wp gets_the_wp get_wp put_wp mapM_x_wp'
2011       | wpc
2012       | simp split del: if_split add: zipWithM_x_mapM_x split_def store_word_offs_def)+
2013  apply (clarsimp simp: st_tcb_def2 tcb_at_def fun_upd_def[symmetric])
2014  apply (auto elim: update_tcb_context_in_ipc)
2015  done
2016
2017lemma set_message_info_respects_in_ipc:
2018  "\<lbrace>integrity_tcb_in_ipc aag X thread epptr TRContext st\<rbrace>
2019     set_message_info thread m
2020   \<lbrace>\<lambda>rv. integrity_tcb_in_ipc aag X thread epptr TRContext st\<rbrace>"
2021  unfolding set_message_info_def
2022  by (wp as_user_respects_in_ipc)
2023
2024lemma mul_add_word_size_lt_msg_align_bits_ofnat:
2025  "\<lbrakk> p < 2 ^ (msg_align_bits - 2); k < 4 \<rbrakk>
2026   \<Longrightarrow> of_nat p * of_nat word_size + k < (2 :: word32) ^ msg_align_bits"
2027  unfolding word_size_def
2028  apply simp
2029  apply (rule is_aligned_add_less_t2n[where n=2])
2030     apply (simp_all add: msg_align_bits word_bits_conv
2031                          is_aligned_word_size_2[simplified word_size_def, simplified])
2032  apply (erule word_less_power_trans_ofnat [where k = 2 and m=9, simplified], simp)
2033  done
2034
2035
2036lemmas ptr_range_off_off_mems =
2037    ptr_range_add_memI [OF _ mul_word_size_lt_msg_align_bits_ofnat]
2038    ptr_range_add_memI [OF _ mul_add_word_size_lt_msg_align_bits_ofnat,
2039                        simplified add.assoc [symmetric]]
2040
2041lemma store_word_offs_respects_in_ipc:
2042  "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st and
2043     K ((\<not> is_subject aag receiver \<longrightarrow> auth_ipc_buffers st receiver = ptr_range buf msg_align_bits)
2044        \<and> is_aligned buf msg_align_bits \<and> r < 2 ^ (msg_align_bits - 2))\<rbrace>
2045    store_word_offs buf r v
2046  \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace>"
2047  apply (simp add: store_word_offs_def storeWord_def pred_conj_def)
2048  apply (rule hoare_pre)
2049  apply (wp dmo_wp)
2050  apply (unfold integrity_tcb_in_ipc_def)
2051  apply (elim conjE)
2052  apply (intro impI conjI)
2053    apply assumption+
2054   apply (erule integrity_trans)
2055   apply (clarsimp simp:  ptr_range_off_off_mems integrity_def is_aligned_mask [symmetric]
2056     cong: imp_cong )
2057 apply simp
2058 done
2059
2060crunch respects_in_ipc: set_extra_badge "integrity_tcb_in_ipc aag X receiver epptr TRContext st"
2061  (wp: store_word_offs_respects_in_ipc)
2062
2063lemma set_object_respects_in_ipc_autarch:
2064  "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr ctxt st
2065          and K (is_subject aag ptr)\<rbrace>
2066     set_object ptr obj
2067   \<lbrace>\<lambda>rv. integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace>"
2068  apply (simp add: integrity_tcb_in_ipc_def)
2069  apply (rule hoare_pre, wp)
2070   apply (wpsimp wp: set_object_wp)
2071  apply (simp only: pred_conj_def)
2072  apply (elim conjE)
2073  apply (intro conjI ; (solves \<open>simp\<close>)?)
2074  apply (erule integrity_trans)
2075  apply (clarsimp simp: integrity_def)
2076  done
2077
2078lemma set_cap_respects_in_ipc_autarch:
2079  "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr ctxt st
2080          and K (is_subject aag (fst ptr))\<rbrace>
2081     set_cap cap ptr
2082   \<lbrace>\<lambda>rv. integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace>"
2083  apply (simp add: set_cap_def split_def)
2084  apply (wp set_object_respects_in_ipc_autarch get_object_wp
2085       | wpc)+
2086  apply simp
2087  done
2088
2089lemma set_original_respects_in_ipc_autarch:
2090  "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr ctxt st
2091          and K (is_subject aag (fst slot))\<rbrace>
2092     set_original slot orig
2093   \<lbrace>\<lambda>rv. integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace>"
2094  apply (wp set_original_wp)
2095  apply (clarsimp simp: integrity_tcb_in_ipc_def)
2096  apply (simp add: integrity_def
2097                   tcb_states_of_state_def get_tcb_def map_option_def
2098                 split del: if_split cong: if_cong)
2099  by (fastforce intro :integrity_cdt_direct)
2100
2101lemma update_cdt_fun_upd_respects_in_ipc_autarch:
2102  "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st
2103           and K (is_subject aag (fst slot))\<rbrace>
2104      update_cdt (\<lambda>cdt. cdt (slot := v cdt))
2105   \<lbrace>\<lambda>rv. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace>"
2106  apply (simp add: update_cdt_def set_cdt_def)
2107  apply wp
2108  apply (clarsimp simp: integrity_tcb_in_ipc_def integrity_def
2109                        tcb_states_of_state_def get_tcb_def
2110             split del: if_split cong: if_cong)
2111  by (fastforce intro :integrity_cdt_direct)
2112
2113lemma set_untyped_cap_as_full_integrity_tcb_in_ipc_autarch:
2114  "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st and
2115    K (is_subject aag (fst src_slot))\<rbrace>
2116   set_untyped_cap_as_full src_cap new_cap src_slot
2117   \<lbrace>\<lambda>ya. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace>"
2118  apply(rule hoare_pre)
2119  apply(clarsimp simp: set_untyped_cap_as_full_def)
2120  apply(intro conjI impI)
2121  apply (wp set_cap_respects_in_ipc_autarch | simp)+
2122  done
2123
2124
2125lemma cap_insert_ext_integrity_in_ipc_autarch:
2126  "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr ctxt st and K(is_subject aag (fst src_slot))
2127        and K(is_subject aag (fst dest_slot))\<rbrace>
2128      cap_insert_ext src_parent src_slot dest_slot src_p dest_p
2129   \<lbrace>\<lambda>yd. integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace>"
2130  apply (rule hoare_gen_asm)+
2131  apply (simp add: integrity_tcb_in_ipc_def split del: if_split)
2132  apply (unfold integrity_def)
2133  apply (simp only: integrity_cdt_list_as_list_integ)
2134  apply (rule hoare_lift_Pf[where f="ekheap"])
2135   apply (clarsimp simp: integrity_tcb_in_ipc_def integrity_def
2136                         tcb_states_of_state_def get_tcb_def
2137              split del: if_split cong: if_cong)
2138   including no_pre
2139   apply wp
2140   apply (rule hoare_vcg_conj_lift)
2141    apply (simp add: list_integ_def del: split_paired_All)
2142    apply (fold list_integ_def)
2143    apply (wp cap_insert_list_integrity | simp | force)+
2144  done
2145
2146lemma cap_inserintegrity_in_ipc_autarch:
2147  "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st
2148         and K (is_subject aag (fst dest_slot) \<and> is_subject aag (fst src_slot))\<rbrace>
2149     cap_insert new_cap src_slot dest_slot
2150   \<lbrace>\<lambda>rv. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace>"
2151  apply (rule hoare_gen_asm)
2152  apply (simp add: cap_insert_def cong: if_cong)
2153  apply (rule hoare_pre)
2154   apply (wp set_original_respects_in_ipc_autarch
2155             set_untyped_cap_as_full_integrity_tcb_in_ipc_autarch
2156             update_cdt_fun_upd_respects_in_ipc_autarch
2157             set_cap_respects_in_ipc_autarch get_cap_wp
2158             cap_insert_ext_integrity_in_ipc_autarch
2159              | simp split del: if_split)+
2160  done
2161
2162lemma transfer_caps_loop_respects_in_ipc_autarch:
2163  "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st
2164         and valid_objs and valid_mdb
2165         and (\<lambda>s. (\<forall>slot \<in> set slots. real_cte_at slot s)
2166                \<and> (\<forall>x \<in> set caps. s \<turnstile> fst x
2167                                \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s
2168                                \<and> real_cte_at (snd x) s))
2169         and K ((\<forall>cap \<in> set caps. is_subject aag (fst (snd cap)))
2170              \<and> (\<forall>slot \<in> set slots. is_subject aag (fst slot))
2171              \<and> (\<not> is_subject aag receiver \<longrightarrow>
2172                           auth_ipc_buffers st receiver = ptr_range buffer msg_align_bits)
2173              \<and> is_aligned buffer msg_align_bits
2174              \<and> n + length caps < 6 \<and> distinct slots)\<rbrace>
2175     transfer_caps_loop ep buffer n caps slots mi
2176   \<lbrace>\<lambda>rv. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace>"
2177  apply (rule hoare_gen_asm)
2178  apply (wp transfer_caps_loop_pres_dest cap_inserintegrity_in_ipc_autarch
2179            set_extra_badge_respects_in_ipc
2180       | simp
2181       | simp add: msg_align_bits buffer_cptr_index_def msg_max_length_def
2182       | blast)+
2183  apply (auto simp: cte_wp_at_caps_of_state)
2184  done
2185
2186lemma transfer_caps_respects_in_ipc:
2187  "\<lbrace>pas_refined aag
2188         and integrity_tcb_in_ipc aag X receiver epptr TRContext st
2189         and valid_objs and valid_mdb
2190         and tcb_at receiver
2191         and (\<lambda>s. (\<forall>x \<in> set caps. s \<turnstile> fst x)
2192                \<and> (\<forall>x \<in> set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> cap.NullCap \<longrightarrow> cp = fst x) (snd x) s
2193                                \<and> real_cte_at (snd x) s))
2194         and K ((\<not> null caps \<longrightarrow> is_subject aag receiver)
2195              \<and> (\<forall>cap \<in> set caps. is_subject aag (fst (snd cap)))
2196              \<and> (\<not> is_subject aag receiver \<longrightarrow>
2197                      case_option True (\<lambda>buf'. auth_ipc_buffers st receiver
2198                                             = ptr_range buf' msg_align_bits) recv_buf)
2199              \<and> (case_option True (\<lambda>buf'. is_aligned buf' msg_align_bits) recv_buf)
2200              \<and> length caps < 6)\<rbrace>
2201     transfer_caps mi caps endpoint receiver recv_buf
2202   \<lbrace>\<lambda>rv. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace>"
2203  apply (rule hoare_gen_asm)
2204  apply (cases recv_buf)
2205   apply (simp add: transfer_caps_def, wp, simp)
2206  apply (cases caps)
2207   apply (simp add: transfer_caps_def del: get_receive_slots.simps, wp, simp)
2208  apply (simp add: transfer_caps_def del: get_receive_slots.simps)
2209  apply (wp transfer_caps_loop_respects_in_ipc_autarch
2210            get_receive_slots_authorised
2211            hoare_vcg_all_lift
2212       | wpc
2213       | rule hoare_drop_imps
2214       | simp add: null_def del: get_receive_slots.simps)+
2215  done
2216
2217lemma copy_mrs_respects_in_ipc:
2218  "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st
2219        and K ((\<not> is_subject aag receiver \<longrightarrow>
2220                      case_option True (\<lambda>buf'. auth_ipc_buffers st receiver
2221                                             = ptr_range buf' msg_align_bits) rbuf)
2222              \<and> (case_option True (\<lambda>buf'. is_aligned buf' msg_align_bits) rbuf)
2223              \<and> unat n < 2 ^ (msg_align_bits - 2))\<rbrace>
2224     copy_mrs sender sbuf receiver rbuf n
2225   \<lbrace>\<lambda>rv. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace>"
2226  unfolding copy_mrs_def
2227  apply (rule hoare_gen_asm)
2228  apply (wp as_user_respects_in_ipc store_word_offs_respects_in_ipc
2229            mapM_wp'
2230            hoare_vcg_const_imp_lift hoare_vcg_all_lift
2231       | wpc
2232       | fastforce split: if_split_asm simp: length_msg_registers)+
2233  done
2234
2235lemma do_normal_transfer_respects_in_ipc:
2236  notes lec_valid_cap[wp del]
2237  shows
2238  "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st
2239         and pas_refined aag
2240         and valid_objs and valid_mdb
2241         and st_tcb_at can_receive_ipc receiver
2242         and (\<lambda>s. grant \<longrightarrow> is_subject aag sender
2243                         \<and> is_subject aag receiver)
2244         and K ((\<not> is_subject aag receiver \<longrightarrow>
2245                      (case recv_buf of None \<Rightarrow> True
2246                                      | Some buf' \<Rightarrow> auth_ipc_buffers st receiver
2247                                                   = ptr_range buf' msg_align_bits)) \<and>
2248                (case recv_buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits))\<rbrace>
2249     do_normal_transfer sender sbuf epopt badge grant receiver recv_buf
2250   \<lbrace>\<lambda>rv. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace>"
2251  apply (simp add: do_normal_transfer_def)
2252  apply (wp as_user_respects_in_ipc set_message_info_respects_in_ipc
2253            transfer_caps_respects_in_ipc copy_mrs_respects_in_ipc get_mi_valid'
2254            lookup_extra_caps_authorised lookup_extra_caps_length get_mi_length
2255            hoare_vcg_const_Ball_lift hoare_vcg_conj_lift_R hoare_vcg_const_imp_lift
2256            lec_valid_cap'
2257       | rule hoare_drop_imps
2258       | simp)+
2259  apply (auto simp: null_def intro: st_tcb_at_tcb_at)
2260  done
2261
2262lemma set_mrs_respects_in_ipc:
2263  "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st and
2264    K ((\<not> is_subject aag receiver \<longrightarrow> (case recv_buf of None \<Rightarrow> True | Some buf' \<Rightarrow> auth_ipc_buffers st receiver = ptr_range buf' msg_align_bits)) \<and>
2265       (case recv_buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits))\<rbrace>
2266     set_mrs receiver recv_buf msgs
2267   \<lbrace>\<lambda>rv. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace>"
2268  unfolding set_mrs_def set_object_def get_object_def
2269  apply (rule hoare_gen_asm)
2270  apply (wp mapM_x_wp' store_word_offs_respects_in_ipc
2271       | wpc
2272       | simp split del: if_split add: zipWithM_x_mapM_x split_def)+
2273   apply (clarsimp simp add: set_zip nth_append simp: msg_align_bits msg_max_length_def
2274                   split: if_split_asm)
2275   apply (simp add: length_msg_registers)
2276   apply arith
2277   apply simp
2278   apply wp+
2279  apply (clarsimp simp: arch_tcb_set_registers_def)
2280  by (rule update_tcb_context_in_ipc [unfolded fun_upd_def]; fastforce)
2281
2282lemma do_fault_transfer_respects_in_ipc:
2283  "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st and
2284    K ((\<not> is_subject aag receiver \<longrightarrow> (case recv_buf of None \<Rightarrow> True | Some buf' \<Rightarrow> auth_ipc_buffers st receiver = ptr_range buf' msg_align_bits)) \<and>
2285       (case recv_buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits))\<rbrace>
2286    do_fault_transfer badge sender receiver recv_buf
2287   \<lbrace>\<lambda>rv. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace>"
2288  apply (simp add: do_fault_transfer_def split_def)
2289  apply (wp as_user_respects_in_ipc set_message_info_respects_in_ipc set_mrs_respects_in_ipc
2290       | wpc
2291       | simp
2292       | rule hoare_drop_imps)+
2293  done
2294
2295lemma lookup_ipc_buffer_ptr_range_in_ipc:
2296  "\<lbrace>valid_objs and integrity_tcb_in_ipc aag X thread epptr tst st\<rbrace>
2297  lookup_ipc_buffer True thread
2298  \<lbrace>\<lambda>rv s. \<not> is_subject aag thread \<longrightarrow>
2299         (case rv of None \<Rightarrow> True
2300                   | Some buf' \<Rightarrow> auth_ipc_buffers st thread = ptr_range buf' msg_align_bits) \<rbrace>"
2301  unfolding lookup_ipc_buffer_def
2302  apply (rule hoare_pre)
2303  apply (wp get_cap_wp thread_get_wp' | wpc)+
2304  apply (clarsimp simp: cte_wp_at_caps_of_state ipc_buffer_has_auth_def get_tcb_ko_at [symmetric])
2305  apply (frule caps_of_state_tcb_cap_cases [where idx = "tcb_cnode_index 4"])
2306   apply (simp add: dom_tcb_cap_cases)
2307  apply (clarsimp simp: auth_ipc_buffers_def get_tcb_ko_at [symmetric] integrity_tcb_in_ipc_def)
2308  apply (drule get_tcb_SomeD)
2309  apply (erule(1) valid_objsE)
2310  apply (clarsimp simp: valid_obj_def valid_tcb_def valid_ipc_buffer_cap_def case_bool_if
2311                 split: if_split_asm)
2312  apply (erule tcb_in_ipc.cases; clarsimp simp: get_tcb_def vm_read_write_def)
2313  done
2314
2315lemma lookup_ipc_buffer_aligned:
2316  "\<lbrace>valid_objs\<rbrace>
2317  lookup_ipc_buffer True thread
2318  \<lbrace>\<lambda>rv s. (case rv of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits) \<rbrace>"
2319  unfolding lookup_ipc_buffer_def
2320  apply (rule hoare_pre)
2321   apply (wp get_cap_wp thread_get_wp' | wpc)+
2322  apply (clarsimp simp: cte_wp_at_caps_of_state get_tcb_ko_at [symmetric])
2323  apply (frule caps_of_state_tcb_cap_cases [where idx = "tcb_cnode_index 4"])
2324   apply (simp add: dom_tcb_cap_cases)
2325  apply (frule (1) caps_of_state_valid_cap)
2326  apply (clarsimp simp: valid_cap_simps cap_aligned_def)
2327  apply (erule aligned_add_aligned)
2328    apply (rule is_aligned_andI1)
2329    apply (drule (1) valid_tcb_objs)
2330    apply (clarsimp simp: valid_obj_def valid_tcb_def valid_ipc_buffer_cap_def
2331                   split: if_splits)
2332  apply (rule order_trans [OF _ pbfs_atleast_pageBits])
2333  apply (simp add: msg_align_bits pageBits_def)
2334  done
2335
2336lemma do_ipc_transfer_respects_in_ipc:
2337  "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st
2338         and pas_refined aag
2339         and valid_objs and valid_mdb
2340         and st_tcb_at can_receive_ipc receiver
2341         and (\<lambda>s. grant \<longrightarrow> is_subject aag sender
2342                         \<and> is_subject aag receiver)
2343         \<rbrace>
2344     do_ipc_transfer sender epopt badge grant receiver
2345   \<lbrace>\<lambda>rv. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace>"
2346  apply (simp add: do_ipc_transfer_def)
2347  apply (wp do_normal_transfer_respects_in_ipc do_fault_transfer_respects_in_ipc
2348            lookup_ipc_buffer_ptr_range_in_ipc lookup_ipc_buffer_aligned
2349            hoare_vcg_conj_lift
2350       | wpc
2351       | simp
2352       | rule hoare_drop_imps)+
2353  apply (auto intro: st_tcb_at_tcb_at)
2354  done
2355
2356
2357lemma sts_ext_running_noop:
2358  "\<lbrace>P and st_tcb_at (runnable) receiver\<rbrace> set_thread_state_ext receiver \<lbrace>\<lambda>_. P\<rbrace>"
2359  apply (simp add: set_thread_state_ext_def get_thread_state_def thread_get_def
2360        | wp set_scheduler_action_wp)+
2361  apply (clarsimp simp add: st_tcb_at_def obj_at_def get_tcb_def)
2362  done
2363
2364lemma set_thread_state_running_respects_in_ipc:
2365  "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st and st_tcb_at(receive_blocked_on epptr) receiver and K(aag_has_auth_to aag SyncSend epptr)\<rbrace>
2366     set_thread_state receiver Structures_A.thread_state.Running
2367   \<lbrace>\<lambda>rv. integrity_tcb_in_ipc aag X receiver epptr TRFinalOrCall st\<rbrace>"
2368  apply (simp add: set_thread_state_def)
2369  apply (wpsimp wp: set_object_wp sts_ext_running_noop)
2370  apply (auto simp: st_tcb_at_def obj_at_def get_tcb_def
2371                    get_tcb_rev update_tcb_state_in_ipc
2372              cong: if_cong
2373              elim: update_tcb_state_in_ipc[unfolded fun_upd_def])
2374  done
2375
2376lemma set_endpoinintegrity_in_ipc:
2377  "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st
2378          and K (aag_has_auth_to aag SyncSend epptr)\<rbrace>
2379    set_endpoint epptr ep'
2380   \<lbrace>\<lambda>rv. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace>"
2381  apply (simp add: set_simple_ko_def set_object_def)
2382  apply (wp get_object_wp)
2383  apply (clarsimp split: Structures_A.kernel_object.splits
2384                  simp: obj_at_def is_tcb is_ep integrity_tcb_in_ipc_def
2385                        partial_inv_def a_type_def)
2386  apply (intro impI conjI)
2387    apply (erule integrity_trans)
2388    apply (clarsimp simp: integrity_def)
2389   apply clarsimp
2390   apply (erule tcb_in_ipc.cases, simp_all)
2391  apply (erule integrity_trans)
2392  apply (clarsimp simp: integrity_def)
2393  apply (fastforce intro: tro_ep)
2394  done
2395
2396(* FIXME: move *)
2397lemma valid_ep_recv_dequeue:
2398  "\<lbrakk> ko_at (Endpoint (Structures_A.endpoint.RecvEP (t # ts))) epptr s;
2399     valid_objs s; sym_refs (state_refs_of s) \<rbrakk>
2400     \<Longrightarrow> valid_ep (case ts of [] \<Rightarrow> Structures_A.endpoint.IdleEP
2401                            | b # bs \<Rightarrow> Structures_A.endpoint.RecvEP ts) s"
2402  unfolding valid_objs_def valid_obj_def valid_ep_def obj_at_def
2403  apply (drule bspec)
2404  apply (auto split: list.splits)
2405  done
2406
2407lemma integrity_tcb_in_ipc_refl:
2408  "\<lbrakk> st_tcb_at can_receive_ipc receiver s; \<not> is_subject aag receiver; pas_refined aag s\<rbrakk>
2409  \<Longrightarrow> integrity_tcb_in_ipc aag X receiver epptr TRContext s s"
2410  unfolding integrity_tcb_in_ipc_def
2411  apply (clarsimp simp: st_tcb_def2)
2412  apply (rule tii_context [OF get_tcb_SomeD get_tcb_SomeD], assumption+)
2413    apply (rule tcb_context_no_change)
2414   apply simp
2415  done
2416
2417(* stronger *)
2418(* MOVE *)
2419lemma ep_queued_st_tcb_at'':
2420  "\<And>P. \<lbrakk>ko_at (Endpoint ep) ptr s; (t, rt) \<in> ep_q_refs_of ep;
2421         valid_objs s; sym_refs (state_refs_of s);
2422         \<And>pl pl'. (rt = EPSend \<and> P (Structures_A.BlockedOnSend ptr pl)) \<or>
2423                  (rt = EPRecv \<and> P (Structures_A.BlockedOnReceive ptr pl')) \<rbrakk>
2424    \<Longrightarrow> st_tcb_at P t s"
2425  apply (case_tac ep, simp_all)
2426  apply (frule (1) sym_refs_ko_atD, fastforce simp: st_tcb_at_def obj_at_def refs_of_rev)+
2427  done
2428
2429subsubsection \<open>Inserting the reply cap\<close>
2430
2431lemma integrity_tcb_in_ipc_no_call:
2432  "integrity_tcb_in_ipc aag X receiver epptr TRFinalOrCall st s
2433   \<Longrightarrow> integrity_tcb_in_ipc aag X receiver epptr TRFinal st s"
2434  unfolding integrity_tcb_in_ipc_def tcb_in_ipc.simps by clarsimp
2435
2436lemma set_original_respects_in_ipc_reply:
2437  "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr ctxt st
2438          and K(st_tcb_at (\<lambda>st. direct_call {pasSubject aag} aag epptr st) receiver st)\<rbrace>
2439     set_original (receiver, tcb_cnode_index 3) orig
2440   \<lbrace>\<lambda>rv. integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace>"
2441  apply (wp set_original_wp)
2442  apply (clarsimp simp: integrity_tcb_in_ipc_def)
2443  apply (simp add: integrity_def tcb_states_of_state_def get_tcb_def
2444              split del: if_split cong: if_cong)
2445  apply (fold get_tcb_def tcb_states_of_state_def)
2446  apply (clarsimp simp:st_tcb_at_tcb_states_of_state)
2447  apply (rule integrity_cdt_change_allowed)
2448  apply (rule cca_reply; force)
2449  done
2450
2451lemma cap_insert_ext_integrity_in_ipc_reply:
2452  "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr ctxt st
2453       and K(is_subject aag (fst src_slot)
2454           \<and> st_tcb_at (\<lambda>st. direct_call {pasSubject aag} aag epptr st) receiver st)\<rbrace>
2455    cap_insert_ext src_parent src_slot (receiver, tcb_cnode_index 3) src_p dest_p
2456   \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace>"
2457  apply (rule hoare_gen_asm)+
2458  apply (simp add: integrity_tcb_in_ipc_def split del: if_split)
2459  apply (unfold integrity_def)
2460  apply (simp only: integrity_cdt_list_as_list_integ)
2461  apply (clarsimp simp: integrity_tcb_in_ipc_def integrity_def
2462                        tcb_states_of_state_def get_tcb_def
2463             split del: if_split cong: if_cong)
2464  apply wp
2465   apply (simp add: list_integ_def del: split_paired_All)
2466   apply (fold list_integ_def get_tcb_def tcb_states_of_state_def)
2467   apply (wp cap_insert_list_integrity)
2468   apply simp
2469   apply (simp add: list_integ_def del: split_paired_All)
2470   apply (fold list_integ_def get_tcb_def tcb_states_of_state_def)
2471   apply (clarsimp simp: st_tcb_at_tcb_states_of_state)
2472   apply (rule cca_reply; force)
2473  done
2474
2475lemma update_cdt_wp:
2476  "\<lbrace>\<lambda>s.  P (s\<lparr> cdt := f (cdt s) \<rparr>)\<rbrace>
2477     update_cdt f
2478   \<lbrace>\<lambda>_. P \<rbrace>"
2479  by (wpsimp simp: update_cdt_def set_cdt_def)
2480
2481lemma update_cdt_reply_in_ipc:
2482  "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr ctxt st
2483       and K(st_tcb_at (\<lambda>st. direct_call {pasSubject aag} aag epptr st) receiver st)\<rbrace>
2484    update_cdt (\<lambda>cdt. cdt ((receiver, tcb_cnode_index 3) := val cdt))
2485   \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace>"
2486  apply (wp update_cdt_wp)
2487  apply (clarsimp simp: integrity_tcb_in_ipc_def)
2488  apply (simp add: integrity_def tcb_states_of_state_def get_tcb_def
2489              split del: if_split cong: if_cong)
2490  apply (fold get_tcb_def tcb_states_of_state_def)
2491  apply (clarsimp simp:st_tcb_at_tcb_states_of_state)
2492  apply (rule integrity_cdt_change_allowed)
2493  apply (rule cca_reply; force)
2494  done
2495
2496(* FIXME: move to NondetMonad *)
2497lemma spec_valid_direct:
2498  "\<lbrakk> P s \<Longrightarrow> s \<turnstile> \<lbrace> \<top> \<rbrace> f \<lbrace> Q \<rbrace> \<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace> Q \<rbrace>"
2499  by (simp add: spec_valid_def valid_def)
2500
2501lemma set_cap_respects_in_ipc_reply:
2502   "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRFinalOrCall st
2503     and K(st_tcb_at (\<lambda>st. direct_call {pasSubject aag} aag epptr st) receiver st
2504           \<and> is_subject aag caller)\<rbrace>
2505      set_cap (ReplyCap caller False R) (receiver, tcb_cnode_index 3)
2506    \<lbrace>\<lambda>rv. integrity_tcb_in_ipc aag X receiver epptr TRFinal st\<rbrace>"
2507  unfolding set_cap_def
2508  apply simp
2509  apply (rule hoare_seq_ext[OF _ get_object_sp])
2510  including no_pre
2511  apply (wp set_object_wp)
2512  apply (rule use_spec')
2513  apply (rule spec_valid_direct)
2514  apply (clarsimp simp:tcb_at_def get_tcb_def dest!:ko_atD split:kernel_object.splits)
2515  apply (simp add: spec_valid_def valid_def return_def)
2516  unfolding integrity_tcb_in_ipc_def
2517  apply (clarsimp simp:st_tcb_at_tcb_states_of_state )
2518  apply (clarsimp simp:tcb_states_of_state_def direct_call_def dest!:get_tcb_SomeD)
2519  by (erule tcb_in_ipc.cases; (force intro:tii_call))
2520
2521
2522lemma cap_insert_reply_cap_respects_in_ipc:
2523  "\<lbrace> integrity_tcb_in_ipc aag X receiver epptr TRFinalOrCall st and
2524    K (st_tcb_at (direct_call {pasSubject aag} aag epptr) receiver st \<and>
2525       is_subject aag caller \<and> is_subject aag (fst master_slot))\<rbrace>
2526    cap_insert
2527          (ReplyCap caller False R)
2528          master_slot (receiver, tcb_cnode_index 3)
2529   \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRFinal st\<rbrace>"
2530  unfolding cap_insert_def
2531  apply (rule hoare_pre)
2532  apply (wp add:set_original_respects_in_ipc_reply)
2533  apply simp
2534  apply (wp cap_insert_ext_integrity_in_ipc_reply update_cdt_reply_in_ipc
2535            set_cap_respects_in_ipc_reply set_untyped_cap_as_full_not_untyped get_cap_wp)+
2536  by fastforce
2537
2538lemma set_scheduler_action_respects_in_ipc_autarch:
2539  "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace>
2540    set_scheduler_action action
2541   \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace>"
2542   unfolding set_scheduler_action_def
2543   by (wpsimp simp: integrity_tcb_in_ipc_def integrity_def tcb_states_of_state_def get_tcb_def)
2544
2545lemma exists_cons_append:
2546  "\<exists>xs. xs @ ys = zs \<Longrightarrow> \<exists>xs. xs @ ys = z # zs"
2547  by auto
2548
2549lemma tcb_sched_action_respects_in_ipc_autarch:
2550  "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace>
2551      tcb_sched_action tcb_sched_enqueue target
2552   \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace>"
2553  apply (simp add: tcb_sched_action_def)
2554  apply wp
2555  apply (clarsimp simp: integrity_def integrity_tcb_in_ipc_def tcb_states_of_state_def get_tcb_def
2556                        integrity_ready_queues_def pas_refined_def tcb_domain_map_wellformed_aux_def
2557                        tcb_at_def get_etcb_def tcb_sched_enqueue_def etcb_at_def
2558                 split: option.splits)
2559  apply (fastforce intro: exists_cons_append)
2560  done
2561
2562
2563crunches possible_switch_to, set_thread_state for respects_in_ipc_autarch: "integrity_tcb_in_ipc aag X receiver epptr ctxt st"
2564  (wp: tcb_sched_action_respects_in_ipc_autarch ignore:tcb_sched_action )
2565
2566lemma setup_caller_cap_respects_in_ipc_reply:
2567  "\<lbrace> integrity_tcb_in_ipc aag X receiver epptr TRFinalOrCall st
2568      and K (is_subject aag sender \<and> st_tcb_at (direct_call {pasSubject aag} aag epptr) receiver st) \<rbrace>
2569   setup_caller_cap sender receiver grant
2570   \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRFinal st \<rbrace>"
2571  unfolding setup_caller_cap_def
2572  by (wpsimp wp: cap_insert_reply_cap_respects_in_ipc set_thread_state_respects_in_ipc_autarch)
2573
2574
2575lemma send_ipc_integrity_autarch:
2576  "\<lbrace>integrity aag X st and pas_refined aag
2577          and invs
2578          and is_subject aag \<circ> cur_thread
2579          and obj_at (\<lambda>ep. can_grant \<longrightarrow> (\<forall>r \<in> refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r))) epptr
2580          and K (is_subject aag sender \<and> aag_has_auth_to aag SyncSend epptr \<and>
2581                (can_grant_reply \<longrightarrow> aag_has_auth_to aag Call epptr))\<rbrace>
2582     send_ipc block call badge can_grant can_grant_reply sender epptr
2583   \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
2584  apply (rule hoare_gen_asm)
2585  apply (simp add: send_ipc_def)
2586  apply (rule hoare_seq_ext[OF _ get_simple_ko_sp])
2587  apply (case_tac ep)
2588    \<comment> \<open>IdleEP\<close>
2589    apply simp
2590    apply (rule hoare_pre)
2591     apply (wp set_endpoinintegrity  set_thread_state_integrity_autarch
2592                 | wpc | simp)+
2593    apply (fastforce simp: obj_at_def is_ep) \<comment> \<open>ep_at and has_auth\<close>
2594   \<comment> \<open>SendEP\<close>
2595   apply simp
2596   apply (rule hoare_pre)
2597    apply (wp set_endpoinintegrity  set_thread_state_integrity_autarch
2598               | wpc | simp)+
2599   apply (fastforce simp: obj_at_def is_ep) \<comment> \<open>ep_at and has_auth\<close>
2600  \<comment> \<open>WaitingEP\<close>
2601  apply (rename_tac list)
2602  apply simp
2603  apply (case_tac "is_subject aag (hd list)") \<comment> \<open>autarch or not on receiver side\<close>
2604   apply clarsimp
2605   apply (rule hoare_pre)
2606    apply (wp setup_caller_cap_integrity_autarch set_thread_state_integrity_autarch thread_get_wp'
2607                  | wpc)+
2608          apply (rule_tac Q="\<lambda>rv s. integrity aag X st s\<and> (can_grant \<longrightarrow> is_subject aag (hd list))"
2609                       in hoare_strengthen_post[rotated])
2610          apply simp+
2611          apply (wp set_thread_state_integrity_autarch thread_get_wp'
2612                    do_ipc_transfer_integrity_autarch
2613                    hoare_vcg_all_lift hoare_drop_imps set_endpoinintegrity
2614                   | wpc | simp add: get_thread_state_def split del: if_split
2615                                del: hoare_True_E_R)+
2616   apply (fastforce simp: a_type_def obj_at_def is_ep elim: send_ipc_valid_ep_helper)
2617  \<comment> \<open>we don't own head of queue\<close>
2618  apply clarsimp
2619  apply (rule use_spec') \<comment> \<open>Name initial state\<close>
2620  apply (simp add: spec_valid_def) \<comment> \<open>no imp rule?\<close>
2621  apply (rule hoare_pre)
2622   apply (wpc, wp)
2623   apply (rename_tac list s receiver queue)
2624   apply (rule_tac Q =  "\<lambda>_ s'. integrity aag X st s \<and>
2625                         integrity_tcb_in_ipc aag X receiver epptr TRFinal s s'" in hoare_post_imp)
2626    apply (fastforce dest!: integrity_tcb_in_ipc_final elim!: integrity_trans)
2627   apply (wp setup_caller_cap_respects_in_ipc_reply
2628             set_thread_state_respects_in_ipc_autarch[where param_b = Inactive]
2629             hoare_vcg_if_lift static_imp_wp possible_switch_to_respects_in_ipc_autarch
2630             set_thread_state_running_respects_in_ipc do_ipc_transfer_respects_in_ipc thread_get_inv
2631             set_endpoinintegrity_in_ipc
2632          | wpc
2633          | strengthen integrity_tcb_in_ipc_no_call
2634          | wp hoare_drop_imps
2635          | simp add:get_thread_state_def)+
2636
2637  apply (clarsimp intro:integrity_tcb_in_ipc_refl)
2638  apply (frule_tac t=x in sym_ref_endpoint_recvD[OF invs_sym_refs],assumption,simp)
2639  apply (clarsimp simp:st_tcb_at_tcb_states_of_state_eq st_tcb_at_tcb_states_of_state direct_call_def)
2640  apply (subgoal_tac "\<not> can_grant")
2641   apply (force intro!: integrity_tcb_in_ipc_refl
2642                  simp: st_tcb_at_tcb_states_of_state
2643                  elim: send_ipc_valid_ep_helper)
2644  apply (force elim:obj_at_ko_atE)
2645  done
2646
2647section\<open>Faults\<close>
2648
2649(* FIXME: move *)
2650lemma valid_tcb_fault_update:
2651  "\<lbrakk> valid_tcb p t s; valid_fault fault \<rbrakk> \<Longrightarrow> valid_tcb p (t\<lparr>tcb_fault := Some fault\<rparr>) s"
2652  by (simp add: valid_tcb_def ran_tcb_cap_cases)
2653
2654lemma thread_set_fault_pas_refined:
2655  "\<lbrace>pas_refined aag\<rbrace>
2656     thread_set (tcb_fault_update (\<lambda>_. Some fault)) thread
2657   \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>"
2658  apply (wp send_ipc_pas_refined thread_set_pas_refined
2659            thread_set_refs_trivial thread_set_obj_at_impossible
2660       | simp)+
2661  done
2662
2663lemma owns_ep_owns_receivers':
2664  "\<lbrakk> (\<forall>auth. aag_has_auth_to aag auth epptr); pas_refined aag s; valid_objs s;
2665     sym_refs (state_refs_of s); ko_at (Endpoint ep) epptr s; (t, EPRecv) \<in> ep_q_refs_of ep\<rbrakk>
2666  \<Longrightarrow> is_subject aag t"
2667  apply (drule (1) ep_rcv_queued_st_tcb_at [where P = "receive_blocked_on epptr"])
2668      apply clarsimp
2669     apply clarsimp
2670    apply clarsimp
2671   apply (rule refl)
2672  apply (drule st_tcb_at_to_thread_states)
2673  apply (clarsimp simp: receive_blocked_on_def2)
2674  apply (drule spec [where x = Grant])
2675  apply (frule aag_wellformed_grant_Control_to_recv [OF _ _ pas_refined_wellformed])
2676    apply (rule pas_refined_mem [OF sta_ts])
2677     apply fastforce
2678    apply assumption
2679   apply assumption
2680  apply (erule (1) aag_Control_into_owns)
2681  done
2682
2683lemma send_fault_ipc_pas_refined:
2684  "\<lbrace>pas_refined aag
2685         and invs
2686         and is_subject aag \<circ> cur_thread
2687         and K (valid_fault fault)
2688         and K (is_subject aag thread)\<rbrace>
2689     send_fault_ipc thread fault
2690   \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>"
2691  apply (rule hoare_gen_asm)+
2692  apply (simp add: send_fault_ipc_def Let_def lookup_cap_def split_def)
2693  apply (wp send_ipc_pas_refined thread_set_fault_pas_refined thread_set_tcb_fault_set_invs
2694            thread_set_refs_trivial thread_set_obj_at_impossible
2695            get_cap_wp thread_set_valid_objs''
2696            hoare_vcg_conj_lift hoare_vcg_ex_lift hoare_vcg_all_lift
2697       | wpc
2698       | rule hoare_drop_imps
2699       | simp add: split_def split del: if_split)+
2700    apply (rule_tac Q'="\<lambda>rv s. pas_refined aag s
2701                            \<and> is_subject aag (cur_thread s)
2702                            \<and> invs s
2703                            \<and> valid_fault fault
2704                            \<and> is_subject aag (fst (fst rv))"
2705                 in hoare_post_imp_R[rotated])
2706     apply (fastforce dest!: cap_auth_caps_of_state
2707                       simp: invs_valid_objs invs_sym_refs cte_wp_at_caps_of_state aag_cap_auth_def
2708                             cap_auth_conferred_def cap_rights_to_auth_def AllowSend_def)
2709    apply (wp get_cap_auth_wp[where aag=aag] lookup_slot_for_thread_authorised
2710          | simp add: lookup_cap_def split_def)+
2711  done
2712
2713lemma handle_fault_pas_refined:
2714  "\<lbrace>pas_refined aag
2715          and invs
2716          and is_subject aag \<circ> cur_thread
2717          and K (valid_fault fault)
2718          and K (is_subject aag thread)\<rbrace>
2719     handle_fault thread fault
2720   \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>"
2721  apply (simp add: handle_fault_def)
2722  apply (wp set_thread_state_pas_refined send_fault_ipc_pas_refined
2723        | simp add: handle_double_fault_def)+
2724  done
2725
2726
2727
2728lemma thread_set_tcb_fault_update_valid_mdb:
2729  "\<lbrace>valid_mdb\<rbrace>
2730     thread_set (tcb_fault_update (\<lambda>_. Some fault)) thread
2731          \<lbrace>\<lambda>rv. valid_mdb\<rbrace>"
2732  apply(rule thread_set_mdb)
2733  apply(clarsimp simp: tcb_cap_cases_def)
2734  apply auto
2735  done
2736
2737
2738(* FIXME: MOVE *)
2739lemma obj_at_conj_distrib:
2740  "obj_at (\<lambda>ko. P ko \<and> Q ko) p s = (obj_at (\<lambda>ko. P ko) p s \<and> obj_at (\<lambda>ko. Q ko) p s)"
2741  by (auto simp: obj_at_def)
2742
2743lemma send_fault_ipc_integrity_autarch:
2744  "\<lbrace>pas_refined aag
2745          and invs
2746          and integrity aag X st
2747          and is_subject aag \<circ> cur_thread
2748          and K (valid_fault fault)
2749          and K (is_subject aag thread)\<rbrace>
2750     send_fault_ipc thread fault
2751   \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
2752  apply (rule hoare_gen_asm)+
2753  apply (simp add: send_fault_ipc_def Let_def)
2754  apply (wp send_ipc_integrity_autarch
2755            thread_set_integrity_autarch thread_set_fault_pas_refined
2756            thread_set_valid_objs'' thread_set_refs_trivial
2757            thread_set_tcb_fault_update_valid_mdb
2758            thread_set_tcb_fault_set_invs
2759        | wpc
2760        | simp add: is_obj_defs)+
2761  (* 14 subgoals *)
2762  apply (rename_tac word1 word2 set)
2763  apply (rule_tac R="\<lambda>rv s. ep_at word1 s" in hoare_post_add)
2764  apply (simp only: obj_at_conj_distrib[symmetric] flip: conj_assoc)
2765  apply (wp thread_set_obj_at_impossible thread_set_tcb_fault_set_invs
2766            get_cap_auth_wp[where aag=aag]
2767        | simp add: lookup_cap_def is_obj_defs split_def)+
2768  (* down to 3 : normal indentation *)
2769    apply (rule_tac Q'="\<lambda>rv s. integrity aag X st s \<and> pas_refined aag s
2770                          \<and> invs s
2771                          \<and> valid_fault fault
2772                          \<and> is_subject aag (cur_thread s)
2773                          \<and> is_subject aag (fst (fst rv))"
2774               in hoare_post_imp_R[rotated])
2775     apply (clarsimp simp: invs_valid_objs invs_sym_refs cte_wp_at_caps_of_state obj_at_def)
2776
2777     apply (frule(1) caps_of_state_valid)
2778     apply (clarsimp simp: valid_cap_def  is_ep aag_cap_auth_def cap_auth_conferred_def
2779                           cap_rights_to_auth_def AllowSend_def
2780                    elim!: obj_atE)
2781
2782     apply (intro conjI ; fastforce ?)
2783     apply (clarsimp simp:ep_q_refs_of_def split:endpoint.splits)
2784     apply (frule(1) pas_refined_ep_recv, simp add:obj_at_def,assumption)
2785     apply (frule(1) aag_wellformed_grant_Control_to_recv[OF _ _ pas_refined_wellformed,rotated],
2786            blast)
2787     apply (simp add:aag_has_auth_to_Control_eq_owns)
2788
2789    apply (wp lookup_slot_for_thread_authorised)+
2790  apply simp
2791  done
2792
2793lemma handle_fault_integrity_autarch:
2794  "\<lbrace>pas_refined aag
2795         and integrity aag X st
2796         and is_subject aag \<circ> cur_thread
2797         and invs
2798         and K (valid_fault fault)
2799         and K (is_subject aag thread)\<rbrace>
2800     handle_fault thread fault
2801   \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
2802  apply (simp add: handle_fault_def)
2803  apply (wp set_thread_state_integrity_autarch send_fault_ipc_integrity_autarch
2804       | simp add: handle_double_fault_def)+
2805  done
2806
2807section\<open>Replies\<close>
2808
2809crunch pas_refined[wp]: handle_fault_reply "pas_refined aag"
2810
2811lemma handle_fault_reply_respects:
2812  "\<lbrace>integrity aag X st and K (is_subject aag thread)\<rbrace>
2813     handle_fault_reply fault thread x y
2814    \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
2815  apply (cases fault, simp_all)
2816  apply (wp as_user_integrity_autarch
2817        | simp add: handle_arch_fault_reply_def arch_get_sanitise_register_info_def)+
2818  done
2819
2820lemma tcb_st_to_auth_Restart_Inactive [simp]:
2821  "tcb_st_to_auth (if P then Restart else Inactive) = {}"
2822  by simp
2823
2824
2825lemma do_reply_transfer_pas_refined:
2826  "\<lbrace>pas_refined aag
2827         and invs and K (is_subject aag sender)
2828         and K ((grant \<longrightarrow> is_subject aag receiver) \<and> is_subject aag (fst slot))\<rbrace>
2829     do_reply_transfer sender receiver slot grant
2830   \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>"
2831  apply (simp add: do_reply_transfer_def)
2832  apply (rule hoare_pre)
2833  apply (wp set_thread_state_pas_refined do_ipc_transfer_pas_refined
2834            thread_set_pas_refined K_valid
2835       | wpc
2836       | simp add: thread_get_def split del: if_split)+
2837  (* otherwise simp does too much *)
2838  apply (rule hoare_strengthen_post, rule gts_inv)
2839   apply (rule impI)
2840   apply assumption
2841  apply auto
2842  done
2843
2844lemma update_tcb_state_in_ipc_reply:
2845  "\<lbrakk> integrity_tcb_in_ipc aag X thread epptr TRContext st s;
2846     tcb_state tcb = BlockedOnReply; aag_has_auth_to aag Reply thread; tcb_fault tcb = None;
2847     get_tcb thread s = Some tcb; tcb' = tcb\<lparr>tcb_state := Structures_A.thread_state.Running\<rparr>
2848   \<rbrakk> \<Longrightarrow>
2849   integrity_tcb_in_ipc aag X thread epptr TRFinal st
2850                        (s \<lparr> kheap := (kheap s)(thread \<mapsto> TCB tcb') \<rparr>)"
2851  unfolding integrity_tcb_in_ipc_def
2852  apply (elim conjE)
2853  apply (intro conjI)
2854    apply assumption+
2855   apply (erule integrity_trans)
2856   apply (simp cong: if_cong)
2857  apply clarsimp
2858  apply (erule tcb_in_ipc.cases, simp_all)
2859  apply (drule get_tcb_SomeD)
2860  apply (rule tii_reply[OF refl refl])
2861     apply (elim exE, intro exI tcb.equality; solves \<open>simp\<close>)
2862    apply auto
2863  done
2864
2865
2866abbreviation "fault_tcb_at \<equiv> pred_tcb_at itcb_fault"
2867
2868lemma fault_tcb_atI:
2869  "\<lbrakk>kheap s ptr = Some (TCB tcb); P (tcb_fault tcb) \<rbrakk> \<Longrightarrow> fault_tcb_at P ptr s"
2870  by (fastforce simp:pred_tcb_at_def obj_at_def)
2871
2872lemma fault_tcb_atE:
2873  assumes hyp:"fault_tcb_at P ptr s"
2874  obtains tcb where "kheap s ptr = Some (TCB tcb)" and "P (tcb_fault tcb)"
2875  using hyp by (fastforce simp:pred_tcb_at_def elim: obj_atE)
2876
2877lemma set_thread_state_running_respects_in_ipc_reply:
2878  "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st
2879      and st_tcb_at awaiting_reply receiver
2880      and fault_tcb_at ((=) None) receiver
2881      and K (aag_has_auth_to aag Reply receiver)\<rbrace>
2882     set_thread_state receiver Structures_A.thread_state.Running
2883   \<lbrace>\<lambda>rv. integrity_tcb_in_ipc aag X receiver epptr TRFinal st\<rbrace>"
2884  apply (simp add: set_thread_state_def set_object_def get_object_def)
2885  apply (wp sts_ext_running_noop)
2886  apply (auto simp: st_tcb_at_def obj_at_def get_tcb_def
2887              cong: if_cong
2888              elim!: fault_tcb_atE elim: update_tcb_state_in_ipc_reply[unfolded fun_upd_def])
2889  done
2890
2891end
2892
2893context is_extended begin
2894
2895interpretation Arch . (*FIXME: arch_split*)
2896
2897lemma list_integ_lift_in_ipc:
2898  assumes li:
2899   "\<lbrace>list_integ (cdt_change_allowed aag {pasSubject aag} (cdt st) (tcb_states_of_state st)) st and Q\<rbrace>
2900       f
2901    \<lbrace>\<lambda>_. list_integ (cdt_change_allowed aag {pasSubject aag}  (cdt st) (tcb_states_of_state st)) st\<rbrace>"
2902  assumes ekh: "\<And>P. \<lbrace>\<lambda>s. P (ekheap s)\<rbrace> f \<lbrace>\<lambda>rv s. P (ekheap s)\<rbrace>"
2903  assumes rq: "\<And>P. \<lbrace> \<lambda>s. P (ready_queues s) \<rbrace> f \<lbrace> \<lambda>rv s. P (ready_queues s) \<rbrace>"
2904  shows "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr ctxt st and Q\<rbrace> f \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace>"
2905  apply (unfold integrity_tcb_in_ipc_def integrity_def[abs_def])
2906  apply (simp del:split_paired_All)
2907  apply (rule hoare_pre)
2908   apply (simp only: integrity_cdt_list_as_list_integ)
2909   apply (rule hoare_lift_Pf2[where f="ekheap"])
2910    apply (simp add: tcb_states_of_state_def get_tcb_def)
2911    apply (wp li[simplified tcb_states_of_state_def get_tcb_def] ekh rq)+
2912  apply (simp only: integrity_cdt_list_as_list_integ)
2913  apply (simp add: tcb_states_of_state_def get_tcb_def)
2914  done
2915
2916end
2917
2918context begin interpretation Arch . (*FIXME: arch_split*)
2919
2920lemma fast_finalise_reply_respects_in_ipc_autarch:
2921  "\<lbrace> integrity_tcb_in_ipc aag X receiver epptr ctxt st  and K (is_reply_cap cap) \<rbrace>
2922     fast_finalise cap final
2923   \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr ctxt st \<rbrace>"
2924  by (rule hoare_gen_asm) (fastforce simp: is_cap_simps)
2925
2926lemma empty_slot_list_integrity':
2927  notes split_paired_All[simp del]
2928  shows
2929  "\<lbrace>list_integ P st and (\<lambda>s . cdt_list s slot = []) and K(P slot)\<rbrace> empty_slot_ext slot slot_p \<lbrace>\<lambda>_. list_integ P st\<rbrace>"
2930  apply (simp add: empty_slot_ext_def split del: if_split)
2931  apply (wp update_cdt_list_wp)
2932  apply (intro impI conjI allI | simp add: list_filter_replace_list list_filter_remove split: option.splits | elim conjE  | simp add: list_integ_def)+
2933  done
2934
2935
2936lemma tcb_state_of_states_cdt_update_behind_kheap[simp]:
2937  "tcb_states_of_state (kheap_update g (cdt_update f s)) = tcb_states_of_state (kheap_update g s)"
2938  by (simp add:tcb_states_of_state_def get_tcb_def)
2939
2940lemma set_cdt_empty_slot_respects_in_ipc_autarch:
2941  "\<lbrace> integrity_tcb_in_ipc aag X receiver epptr ctxt st and (\<lambda>s. m =cdt s)
2942     and (\<lambda>s. descendants_of slot m = {}) and K(is_subject aag (fst slot))\<rbrace>
2943      set_cdt ((\<lambda>p. if m p = Some slot then m slot else m p)(slot := None))
2944   \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr ctxt st \<rbrace>"
2945  unfolding set_cdt_def
2946  apply wp
2947  apply (simp add: integrity_tcb_in_ipc_def integrity_def)
2948  apply (force simp:no_children_empty_desc[symmetric])
2949  done
2950
2951lemma reply_cap_no_children':
2952  "\<lbrakk> valid_mdb s; caps_of_state s p = Some (ReplyCap t False r) \<rbrakk> \<Longrightarrow> \<forall>p' .cdt s p' \<noteq> Some p"
2953  using reply_cap_no_children ..
2954
2955lemma valid_list_empty:
2956  "\<lbrakk> valid_list_2 list m; descendants_of slot m = {}\<rbrakk> \<Longrightarrow> list slot = []"
2957  unfolding valid_list_2_def
2958  apply (drule no_children_empty_desc[THEN iffD2])
2959  apply (rule classical)
2960  by (fastforce simp del:split_paired_All split_paired_Ex simp add:neq_Nil_conv)
2961
2962
2963lemma empty_slot_respects_in_ipc_autarch:
2964  "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr ctxt st and valid_mdb and valid_list
2965    and cte_wp_at is_reply_cap slot and K (is_subject aag (fst slot))\<rbrace>
2966     empty_slot slot NullCap
2967   \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace>"
2968  unfolding empty_slot_def apply simp
2969  apply (wp add: set_cap_respects_in_ipc_autarch set_original_respects_in_ipc_autarch)
2970       apply (wp empty_slot_extended.list_integ_lift_in_ipc empty_slot_list_integrity')
2971          apply simp
2972         apply wp+
2973      apply (wp set_cdt_empty_slot_respects_in_ipc_autarch)
2974      apply (simp add: set_cdt_def)
2975      apply wp
2976     apply wp
2977    apply wp
2978   apply (wp get_cap_wp)
2979  apply (clarsimp simp: integrity_tcb_in_ipc_def cte_wp_at_caps_of_state is_cap_simps)
2980  apply (drule(1) reply_cap_no_children')
2981  by (force dest: valid_list_empty simp: no_children_empty_desc simp del: split_paired_All)
2982
2983lemma cte_delete_one_respects_in_ipc_autharch:
2984  "\<lbrace> integrity_tcb_in_ipc aag X receiver epptr ctxt st and valid_mdb and valid_list and
2985       cte_wp_at is_reply_cap slot and K (is_subject aag (fst slot)) \<rbrace>
2986     cap_delete_one slot
2987   \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr ctxt st \<rbrace>"
2988  unfolding cap_delete_one_def
2989  apply (wp empty_slot_respects_in_ipc_autarch
2990            fast_finalise_reply_respects_in_ipc_autarch get_cap_wp)
2991  by (fastforce simp:cte_wp_at_caps_of_state is_cap_simps)
2992
2993
2994
2995text \<open>The special case of fault reply need a different machinery than *_in_ipc stuff because,
2996        there is no @{term underlying_memory} modification\<close>
2997
2998datatype tcb_respects_fault_state = TRFContext | TRFRemoveFault | TRFFinal
2999
3000inductive tcb_in_fault_reply for aag tst l' ko ko'
3001where
3002  tifr_lrefl: "\<lbrakk> l' = pasSubject aag \<rbrakk> \<Longrightarrow> tcb_in_fault_reply aag tst l' ko ko'"
3003| tifr_context: "\<lbrakk> ko  = Some (TCB tcb);
3004                  ko' = Some (TCB tcb');
3005                  \<exists>ctxt'. tcb' = tcb \<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb)\<rparr>;
3006                  (pasSubject aag, Reply, l') \<in> pasPolicy aag;
3007                  tcb_state tcb = BlockedOnReply;
3008                  tcb_fault tcb = Some fault;
3009                  tst = TRFContext\<rbrakk>
3010        \<Longrightarrow> tcb_in_fault_reply aag tst l' ko ko'"
3011| tifr_remove_fault: "\<lbrakk> ko  = Some (TCB tcb);
3012                   ko' = Some (TCB tcb');
3013                   \<exists>ctxt'. tcb' = tcb \<lparr> tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb)
3014                                   , tcb_fault := None\<rparr>;
3015                   (pasSubject aag, Reply, l') \<in> pasPolicy aag;
3016                   tcb_state tcb = BlockedOnReply;
3017                   tcb_fault tcb = Some fault;
3018                   tst = TRFRemoveFault\<rbrakk>
3019         \<Longrightarrow> tcb_in_fault_reply aag tst l' ko ko'"
3020| tifr_reply:  "\<lbrakk> ko  = Some (TCB tcb);
3021                ko' = Some (TCB tcb');
3022                \<exists>ctxt'. tcb' = tcb \<lparr> tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb),
3023                                     tcb_fault := None,
3024                                     tcb_state := new_st\<rparr>;
3025                new_st = Structures_A.Restart \<or> new_st = Structures_A.Inactive;
3026                (pasSubject aag, Reply, l') \<in> pasPolicy aag;
3027                tcb_state tcb = BlockedOnReply;
3028                tcb_fault tcb = Some fault;
3029                tst = TRFFinal\<rbrakk>
3030         \<Longrightarrow> tcb_in_fault_reply aag tst l' ko ko'"
3031
3032definition integrity_tcb_in_fault_reply ::
3033  "'a PAS \<Rightarrow> obj_ref set \<Rightarrow> obj_ref \<Rightarrow> tcb_respects_fault_state \<Rightarrow> det_ext state
3034    \<Rightarrow> det_ext state \<Rightarrow> bool"
3035where
3036  "integrity_tcb_in_fault_reply aag X thread tst st \<equiv> \<lambda>s.
3037     \<not> is_subject aag thread \<and> pas_refined aag st \<and> \<comment> \<open>more or less convenience\<close>
3038     (integrity aag X st (s\<lparr>kheap := (kheap s)(thread := kheap st thread)\<rparr>)
3039   \<and> (tcb_in_fault_reply aag tst (pasObjectAbs aag thread) (kheap st thread) (kheap s thread)))"
3040
3041lemma integrity_tcb_in_fault_reply_final:
3042  "\<lbrakk> integrity_tcb_in_fault_reply aag X thread TRFFinal st s \<rbrakk> \<Longrightarrow> integrity aag X st s"
3043  unfolding integrity_tcb_in_fault_reply_def
3044  apply clarsimp
3045  apply (erule integrity_trans)
3046  apply (clarsimp simp: integrity_def)
3047  apply (erule tcb_in_fault_reply.cases; clarsimp)
3048  apply (fastforce intro!:tcb.equality tro_tcb_reply)
3049  done
3050
3051lemma set_scheduler_action_respects_in_fault_reply:
3052  "\<lbrace>integrity_tcb_in_fault_reply aag X receiver ctxt st\<rbrace>
3053    set_scheduler_action action
3054   \<lbrace>\<lambda>_. integrity_tcb_in_fault_reply aag X receiver ctxt st\<rbrace>"
3055  unfolding set_scheduler_action_def
3056  by (wpsimp simp: integrity_tcb_in_fault_reply_def integrity_def
3057                   tcb_states_of_state_def get_tcb_def)
3058
3059crunches set_thread_state_ext
3060  for respects_in_fault_reply:"integrity_tcb_in_fault_reply aag X receiver ctxt st"
3061
3062lemma as_user_respects_in_fault_reply:
3063  "\<lbrace>integrity_tcb_in_fault_reply aag X thread TRFContext st\<rbrace>
3064     as_user thread m
3065   \<lbrace>\<lambda>rv. integrity_tcb_in_fault_reply aag X thread TRFContext st\<rbrace>"
3066  apply (simp add: as_user_def)
3067  apply (wpsimp wp: set_object_wp)
3068  apply (clarsimp simp: integrity_tcb_in_fault_reply_def)
3069  apply (erule tcb_in_fault_reply.cases; clarsimp dest!: get_tcb_SomeD)
3070  apply (rule tifr_context[OF refl refl])
3071      apply (intro exI tcb.equality; simp add: arch_tcb_context_set_def)
3072  by fastforce+
3073
3074lemma handle_fault_reply_respects_in_fault_reply:
3075  "\<lbrace>integrity_tcb_in_fault_reply aag X thread TRFContext st\<rbrace>
3076   handle_fault_reply f thread label mrs
3077   \<lbrace>\<lambda>_. integrity_tcb_in_fault_reply aag X thread TRFContext st\<rbrace>"
3078  by (cases f;
3079      wpsimp simp: handle_arch_fault_reply_def arch_get_sanitise_register_info_def
3080               wp: as_user_respects_in_fault_reply)
3081
3082lemma thread_set_no_fault_respects_in_fault_reply:
3083  "\<lbrace>integrity_tcb_in_fault_reply aag X thread TRFContext st\<rbrace>
3084   thread_set (\<lambda>tcb. tcb \<lparr> tcb_fault := None \<rparr>) thread
3085   \<lbrace>\<lambda>_. integrity_tcb_in_fault_reply aag X thread TRFRemoveFault st\<rbrace>"
3086  apply (simp add: thread_set_def)
3087  apply (wp set_thread_state_ext_respects_in_fault_reply set_object_wp)
3088  apply (clarsimp simp: integrity_tcb_in_fault_reply_def)
3089  apply (erule tcb_in_fault_reply.cases; clarsimp dest!: get_tcb_SomeD)
3090  apply (rule tifr_remove_fault[OF refl refl])
3091      apply (intro exI tcb.equality ; simp add: arch_tcb_context_set_def)
3092  by fastforce+
3093
3094lemma set_thread_state_respects_in_fault_reply:
3095  "tst = Restart \<or> tst = Inactive \<Longrightarrow>
3096   \<lbrace>integrity_tcb_in_fault_reply aag X thread TRFRemoveFault st\<rbrace>
3097   set_thread_state thread tst
3098   \<lbrace>\<lambda>_. integrity_tcb_in_fault_reply aag X thread TRFFinal st\<rbrace>"
3099  apply (simp add: set_thread_state_def)
3100  apply (wp set_thread_state_ext_respects_in_fault_reply set_object_wp)
3101  apply (clarsimp simp: integrity_tcb_in_fault_reply_def)
3102  apply (erule tcb_in_fault_reply.cases; clarsimp dest!: get_tcb_SomeD)
3103  apply (rule tifr_reply[OF refl refl])
3104       apply (intro exI tcb.equality; simp add: arch_tcb_context_set_def)
3105  by fastforce+
3106
3107lemma integrity_tcb_in_fault_reply_refl:
3108  "\<lbrakk> st_tcb_at awaiting_reply receiver s; fault_tcb_at (flip (\<noteq>) None) receiver s;
3109     aag_has_auth_to aag Reply receiver;
3110     \<not> is_subject aag receiver; pas_refined aag s \<rbrakk>
3111  \<Longrightarrow> integrity_tcb_in_fault_reply aag X receiver TRFContext s s"
3112  unfolding integrity_tcb_in_fault_reply_def
3113  apply (clarsimp elim!: pred_tcb_atE)
3114  apply (rule tifr_context[OF refl refl])
3115      apply (rule tcb_context_no_change)
3116     apply fastforce+
3117  done
3118
3119lemma emptyable_not_master:
3120  "\<lbrakk> valid_objs s; caps_of_state s slot = Some cap; \<not> is_master_reply_cap cap\<rbrakk>
3121   \<Longrightarrow> emptyable slot s"
3122  apply (rule emptyable_cte_wp_atD[rotated 2])
3123    apply (intro allI impI, assumption)
3124   by (fastforce simp:is_cap_simps cte_wp_at_caps_of_state)+
3125
3126lemma do_reply_transfer_respects:
3127  "\<lbrace>pas_refined aag
3128        and integrity aag X st
3129        and einvs \<comment> \<open>cap_delete_one\<close>
3130        and tcb_at sender
3131        and cte_wp_at (is_reply_cap_to receiver) slot
3132        and K (is_subject aag sender)
3133        and K (aag_has_auth_to aag Reply receiver)
3134        and K (is_subject aag (fst slot) \<and> (grant \<longrightarrow> is_subject aag receiver))\<rbrace>
3135     do_reply_transfer sender receiver slot grant
3136   \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
3137  apply (rule hoare_gen_asm)+
3138  apply (simp add: do_reply_transfer_def thread_get_def get_thread_state_def)
3139  apply (rule hoare_seq_ext[OF _ assert_get_tcb_sp];force?)
3140  apply (rule hoare_seq_ext[OF _ assert_sp])
3141  apply (rule hoare_seq_ext[OF _ assert_get_tcb_sp];force?)
3142  apply wpc
3143    \<comment> \<open>No fault case\<close>
3144    apply (rule hoare_vcg_if_split[where P= "is_subject aag receiver" and f=f and g=f for f,
3145                                   simplified if_cancel])
3146     \<comment> \<open>receiver is a subject\<close>
3147     apply ((wp set_thread_state_integrity_autarch thread_set_integrity_autarch
3148                handle_fault_reply_respects do_ipc_transfer_integrity_autarch
3149                do_ipc_transfer_pas_refined
3150             | simp
3151             | intro conjI impI)+)[1]
3152    \<comment> \<open>receiver is not a subject\<close>
3153    apply (rule use_spec') \<comment> \<open>Name initial state\<close>
3154    apply (simp add: spec_valid_def) \<comment> \<open>no imp rule?\<close>
3155
3156    apply (rule_tac Q =  "\<lambda>_ s'. integrity aag X st s \<and>
3157                         integrity_tcb_in_ipc aag X receiver _ TRFinal s s'" in hoare_post_imp)
3158     apply (fastforce dest!: integrity_tcb_in_ipc_final elim!: integrity_trans)
3159    apply ((wp possible_switch_to_respects_in_ipc_autarch
3160               set_thread_state_running_respects_in_ipc_reply
3161               cte_delete_one_respects_in_ipc_autharch cap_delete_one_reply_st_tcb_at
3162               do_ipc_transfer_pred_tcb do_ipc_transfer_respects_in_ipc
3163               do_ipc_transfer_non_null_cte_wp_at2
3164           | simp add: is_cap_simps is_reply_cap_to_def
3165           | clarsimp)+)[1]
3166   \<comment> \<open>fault case\<close>
3167   apply (rule hoare_vcg_if_split[where P= "is_subject aag receiver" and f=f and g=f for f,
3168                                  simplified if_cancel])
3169    \<comment> \<open>receiver is a subject\<close>
3170    apply ((wp set_thread_state_integrity_autarch thread_set_integrity_autarch
3171               handle_fault_reply_respects
3172           | simp
3173           | intro conjI impI)+)[1]
3174    \<comment> \<open>receiver is not a subject\<close>
3175   apply (rule hoare_seq_ext, simp)
3176    apply (rule use_spec') \<comment> \<open>Name initial state\<close>
3177    apply (simp add: spec_valid_def) \<comment> \<open>no imp rule?\<close>
3178    apply wp
3179          apply (rule_tac Q = "\<lambda>_ s'. integrity aag X st s \<and>
3180                                      integrity_tcb_in_fault_reply aag X receiver TRFFinal s s'"
3181                       in hoare_post_imp)
3182     apply (fastforce dest!: integrity_tcb_in_fault_reply_final elim!: integrity_trans)
3183   apply (wp set_thread_state_respects_in_fault_reply
3184             thread_set_no_fault_respects_in_fault_reply
3185             handle_fault_reply_respects_in_fault_reply
3186         | simp)+
3187   apply force
3188   apply (strengthen integrity_tcb_in_fault_reply_refl)+
3189   apply (wp cap_delete_one_reply_st_tcb_at)
3190
3191  \<comment> \<open>the end\<close>
3192  by (force simp: st_tcb_at_tcb_states_of_state cte_wp_at_caps_of_state is_cap_simps
3193                  is_reply_cap_to_def
3194           dest!: tcb_states_of_state_kheapD get_tcb_SomeD tcb_atD ko_atD
3195           intro: tcb_atI fault_tcb_atI emptyable_not_master
3196          intro!: integrity_tcb_in_ipc_refl tcb_states_of_state_kheapI
3197           elim!: fault_tcb_atE)
3198
3199
3200lemma reply_from_kernel_integrity_autarch:
3201  "\<lbrace>integrity aag X st and pas_refined aag and valid_objs and K (is_subject aag thread)\<rbrace>
3202    reply_from_kernel thread x
3203   \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
3204  apply (simp add: reply_from_kernel_def split_def)
3205  apply (wp set_message_info_integrity_autarch set_mrs_integrity_autarch as_user_integrity_autarch | simp)+
3206  done
3207
3208end
3209
3210end
3211