theory Ipc_IF

lemma send_ipc_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 invs and is_subject aag \<circ> cur_thread
                        and (\<lambda>s. (can_grant \<longrightarrow> aag_has_auth_to aag Grant epptr))
                        and K (is_subject aag thread \<and> aag_has_auth_to aag SyncSend epptr))
       (send_ipc block call badge can_grant can_grant_reply thread epptr)" apply (rule equiv_valid_guard_imp[OF reads_respects_g]) apply (rule send_ipc_reads_respects[OF domains_distinct]) apply (rule doesnt_touch_globalsI) apply (wp send_ipc_globals_equiv | simp)+ by fastforce

(* 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 invs and is_subject aag \<circ> cur_thread and (\<lambda>s. can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag) and K (is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag)) (send_ipc block call badge can_grant can_grant_reply thread epptr) proof (prove)
goal (3 subgoals):
 1. reads_respects aag l ?P1 (send_ipc block call badge can_grant can_grant_reply thread epptr)
 2. doesnt_touch_globals ?Q1 (send_ipc block call badge can_grant can_grant_reply thread epptr)
 3. \<And>s. (pas_refined aag and pas_cur_domain aag and invs and is_subject aag \<circ> cur_thread and (\<lambda>s. can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag) and K (is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag)) s \<Longrightarrow> (?P1 and ?Q1) s proof (prove)
goal (2 subgoals):
 1. doesnt_touch_globals ?Q1 (send_ipc block call badge can_grant can_grant_reply thread epptr)
 2. \<And>s. (pas_refined aag and pas_cur_domain aag and invs and is_subject aag \<circ> cur_thread and (\<lambda>s. can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag) and K (is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag)) s \<Longrightarrow> (pas_refined aag and invs and pas_cur_domain aag and is_subject aag \<circ> cur_thread and K (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag) and K (is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag) and ?Q1) s proof (prove)
goal (2 subgoals):
 1. \<And>st. \<lbrace>globals_equiv st and ?Q1\<rbrace> send_ipc block call badge can_grant can_grant_reply thread epptr \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<And>s. (pas_refined aag and pas_cur_domain aag and invs and is_subject aag \<circ> cur_thread and (\<lambda>s. can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag) and K (is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag)) s \<Longrightarrow> (pas_refined aag and invs and pas_cur_domain aag and is_subject aag \<circ> cur_thread and K (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag) and K (is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag) and ?Q1) s proof (prove)
goal (1 subgoal):
 1. \<And>s. pas_refined aag s \<and> pas_cur_domain aag s \<and> invs s \<and> is_subject aag (cur_thread s) \<and> (can_grant \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag epptr) \<in> pasPolicy aag) \<and> is_subject aag thread \<and> (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag \<Longrightarrow> valid_objs s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_global_objs s \<and> valid_idle s \<and> sym_refs (state_refs_of s)