theory Ipc_IF

lemma update_waiting_ntfn_reads_respects:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows
    "reads_respects aag l (pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs
                                          and sym_refs \<circ> state_refs_of and pas_refined aag
                                          and pas_cur_domain aag and ko_at (Notification ntfn) nptr
                                          and (\<lambda>s. is_subject aag (cur_thread s))
                                          and K (ntfn_obj ntfn = WaitingNtfn queue))
                    (update_waiting_ntfn nptr queue bound_tcb badge)" unfolding update_waiting_ntfn_def fun_app_def apply (wp assert_sp possible_switch_to_reads_respects gets_cur_thread_ev | simp add: split_def)+ by (wp as_user_set_register_reads_respects' set_thread_state_reads_respects
         set_simple_ko_reads_respects set_thread_state_pas_refined
         set_simple_ko_valid_objs hoare_vcg_disj_lift set_simple_ko_pas_refined
      | simp add: split_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and sym_refs \<circ> state_refs_of and pas_refined aag and pas_cur_domain aag and ko_at (Notification ntfn) nptr and (\<lambda>s. is_subject aag (cur_thread s)) and K (ntfn_obj ntfn = WaitingNtfn queue)) (update_waiting_ntfn nptr queue bound_tcb badge) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and sym_refs \<circ> state_refs_of and pas_refined aag and pas_cur_domain aag and ko_at (Notification ntfn) nptr and (\<lambda>s. is_subject aag (cur_thread s)) and K (ntfn_obj ntfn = WaitingNtfn queue)) (do assert (queue \<noteq> []);
(dest, rest) <- return (hd queue, tl queue);
set_notification nptr \<lparr>ntfn_obj = case rest of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn rest, ntfn_bound_tcb = bound_tcb\<rparr>;
set_thread_state dest Running;
as_user dest (setRegister badge_register badge);
do_extended_op (possible_switch_to dest)
od) proof (prove)
goal (11 subgoals):
 1. \<And>rva. reads_respects aag l (?P'9 rva () ()) (as_user (fst rva) (setRegister badge_register badge))
 2. \<And>rva rv rvb. \<lbrace>?P''9 rva rv rvb\<rbrace> as_user (fst rva) (setRegister badge_register badge) \<lbrace>\<lambda>rvc. pas_refined aag and pas_cur_domain aag and (\<lambda>s. is_subject aag (cur_thread s))\<rbrace>
 3. \<And>rva rv. reads_respects aag l (?P'8 rva rv) (set_thread_state (fst rva) Running)
 4. \<And>rva rv. \<lbrace>?P''8 rva rv\<rbrace> set_thread_state (fst rva) Running \<lbrace>\<lambda>rvb s. ?P'9 rva rv rvb s \<and> ?P''9 rva rv rvb s\<rbrace>
 5. \<And>rva. reads_respects aag l (?P'7 () rva) (set_notification nptr \<lparr>ntfn_obj = case snd rva of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn (snd rva), ntfn_bound_tcb = bound_tcb\<rparr>)
 6. \<And>rva. \<lbrace>?P''6 () rva\<rbrace> set_notification nptr \<lparr>ntfn_obj = case snd rva of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn (snd rva), ntfn_bound_tcb = bound_tcb\<rparr> \<lbrace>\<lambda>rv s. ?P'8 rva rv s \<and> ?P''8 rva rv s\<rbrace>
 7. \<And>rv. reads_respects aag l (?P'2 rv) (return (hd queue, tl queue))
 8. \<And>rv. \<lbrace>?P''2 rv\<rbrace> return (hd queue, tl queue) \<lbrace>\<lambda>a b. ?P'7 rv a b \<and> ?P''6 rv a b\<rbrace>
 9. reads_respects aag l ?P' (assert (queue \<noteq> []))
 10. \<lbrace>?P''\<rbrace> assert (queue \<noteq> []) \<lbrace>\<lambda>rv s. ?P'2 rv s \<and> ?P''2 rv s\<rbrace>
A total of 11 subgoals...