theory Ipc_IF

lemma receive_ipc_reads_respects_g:
  assumes domains_distinct: "pas_domains_distinct aag"
  shows
    "reads_respects_g aag l
       (invs and (\<lambda>s. receiver \<noteq> idle_thread s) and pas_refined aag
             and pas_cur_domain aag and valid_cap cap and is_subject aag \<circ> cur_thread
             and K (is_subject aag receiver \<and> pas_cap_cur_auth aag cap \<and> AllowRead \<in> cap_rights cap))
       (receive_ipc receiver cap is_blocking)" apply (rule equiv_valid_guard_imp[OF reads_respects_g]) apply (rule receive_ipc_reads_respects[OF domains_distinct]) apply (rule doesnt_touch_globalsI) apply (wp receive_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 (invs and (\<lambda>s. receiver \<noteq> idle_thread s) and pas_refined aag and pas_cur_domain aag and valid_cap cap and is_subject aag \<circ> cur_thread and K (is_subject aag receiver \<and> pas_cap_cur_auth aag cap \<and> AllowRead \<in> cap_rights cap)) (receive_ipc receiver cap is_blocking) proof (prove)
goal (3 subgoals):
 1. reads_respects aag l ?P1 (receive_ipc receiver cap is_blocking)
 2. doesnt_touch_globals ?Q1 (receive_ipc receiver cap is_blocking)
 3. \<And>s. (invs and (\<lambda>s. receiver \<noteq> idle_thread s) and pas_refined aag and pas_cur_domain aag and valid_cap cap and is_subject aag \<circ> cur_thread and K (is_subject aag receiver \<and> pas_cap_cur_auth aag cap \<and> AllowRead \<in> cap_rights cap)) s \<Longrightarrow> (?P1 and ?Q1) s proof (prove)
goal (2 subgoals):
 1. doesnt_touch_globals ?Q1 (receive_ipc receiver cap is_blocking)
 2. \<And>s. (invs and (\<lambda>s. receiver \<noteq> idle_thread s) and pas_refined aag and pas_cur_domain aag and valid_cap cap and is_subject aag \<circ> cur_thread and K (is_subject aag receiver \<and> pas_cap_cur_auth aag cap \<and> AllowRead \<in> cap_rights cap)) s \<Longrightarrow> (invs and pas_refined aag and pas_cur_domain aag and valid_cap cap and is_subject aag \<circ> cur_thread and K (is_subject aag receiver \<and> pas_cap_cur_auth aag cap \<and> AllowRead \<in> cap_rights cap) and ?Q1) s proof (prove)
goal (2 subgoals):
 1. \<And>st. \<lbrace>globals_equiv st and ?Q1\<rbrace> receive_ipc receiver cap is_blocking \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<And>s. (invs and (\<lambda>s. receiver \<noteq> idle_thread s) and pas_refined aag and pas_cur_domain aag and valid_cap cap and is_subject aag \<circ> cur_thread and K (is_subject aag receiver \<and> pas_cap_cur_auth aag cap \<and> AllowRead \<in> cap_rights cap)) s \<Longrightarrow> (invs and pas_refined aag and pas_cur_domain aag and valid_cap cap and is_subject aag \<circ> cur_thread and K (is_subject aag receiver \<and> pas_cap_cur_auth aag cap \<and> AllowRead \<in> cap_rights cap) and ?Q1) s proof (prove)
goal (1 subgoal):
 1. \<And>s. invs s \<and> receiver \<noteq> idle_thread s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> s \<turnstile> cap \<and> is_subject aag (cur_thread s) \<and> is_subject aag receiver \<and> pas_cap_cur_auth aag cap \<and> AllowRead \<in> cap_rights cap \<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