theory Ipc_IF

lemma send_signal_reads_respects_g:
  assumes domains_distinct: "pas_domains_distinct aag"
  shows
  "reads_respects_g aag l
     (pas_refined aag and pas_cur_domain aag and valid_etcbs and pspace_aligned
                      and valid_vspace_objs and valid_arch_state and valid_objs
                      and valid_global_objs and valid_arch_state and valid_global_refs
                      and pspace_distinct and valid_idle and ct_active
                      and sym_refs \<circ> state_refs_of and is_subject aag \<circ> cur_thread
                      and K ((pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag))
     (send_signal ntfnptr badge)" apply (rule equiv_valid_guard_imp[OF reads_respects_g]) apply (rule send_signal_reads_respects[OF domains_distinct]) apply (rule doesnt_touch_globalsI) apply (wp send_signal_globals_equiv | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag (pas_refined aag and pas_cur_domain aag and valid_etcbs and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_global_objs and valid_arch_state and valid_global_refs and pspace_distinct and valid_idle and ct_active and sym_refs \<circ> state_refs_of and is_subject aag \<circ> cur_thread and K ((pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag)) (send_signal ntfnptr badge) proof (prove)
goal (3 subgoals):
 1. reads_respects aag l ?P1 (send_signal ntfnptr badge)
 2. doesnt_touch_globals ?Q1 (send_signal ntfnptr badge)
 3. \<And>s. (pas_refined aag and pas_cur_domain aag and valid_etcbs and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_global_objs and valid_arch_state and valid_global_refs and pspace_distinct and valid_idle and ct_active and sym_refs \<circ> state_refs_of and is_subject aag \<circ> cur_thread and K ((pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag)) s \<Longrightarrow> (?P1 and ?Q1) s proof (prove)
goal (2 subgoals):
 1. doesnt_touch_globals ?Q1 (send_signal ntfnptr badge)
 2. \<And>s. (pas_refined aag and pas_cur_domain aag and valid_etcbs and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_global_objs and valid_arch_state and valid_global_refs and pspace_distinct and valid_idle and ct_active and sym_refs \<circ> state_refs_of and is_subject aag \<circ> cur_thread and K ((pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag)) s \<Longrightarrow> (pas_refined aag and pas_cur_domain aag and pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. is_subject aag (cur_thread s)) and valid_etcbs and ct_active and (\<lambda>s. sym_refs (state_refs_of s)) and valid_objs and K ((pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag) and ?Q1) s proof (prove)
goal (2 subgoals):
 1. \<And>st. \<lbrace>globals_equiv st and ?Q1\<rbrace> send_signal ntfnptr badge \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<And>s. (pas_refined aag and pas_cur_domain aag and valid_etcbs and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_global_objs and valid_arch_state and valid_global_refs and pspace_distinct and valid_idle and ct_active and sym_refs \<circ> state_refs_of and is_subject aag \<circ> cur_thread and K ((pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag)) s \<Longrightarrow> (pas_refined aag and pas_cur_domain aag and pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. is_subject aag (cur_thread s)) and valid_etcbs and ct_active and (\<lambda>s. sym_refs (state_refs_of s)) and valid_objs and K ((pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag) and ?Q1) s proof (prove)
goal:
No subgoals!