theory Ipc_IF

lemma receive_signal_reads_respects_g:
  assumes domains_distinct: "pas_domains_distinct aag"
  shows
    "reads_respects_g aag (l :: 'a subject_label)
       (valid_global_objs and valid_objs and valid_arch_state and valid_global_refs
                          and pspace_distinct and pas_refined aag and (\<lambda>s. thread \<noteq> idle_thread s)
                          and is_subject aag \<circ> cur_thread
                          and K (\<forall>nptr\<in>obj_refs_ac cap.
                                   (pasSubject aag, Receive, pasObjectAbs aag nptr) \<in> pasPolicy aag
                                 \<and> is_subject aag thread))
       (receive_signal thread cap is_blocking)" apply (rule equiv_valid_guard_imp[OF reads_respects_g]) apply (rule receive_signal_reads_respects[OF domains_distinct]) apply (rule doesnt_touch_globalsI) apply (wp receive_signal_globals_equiv | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag (valid_global_objs and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pas_refined aag and (\<lambda>s. thread \<noteq> idle_thread s) and is_subject aag \<circ> cur_thread and K (\<forall>nptr\<in>obj_refs_ac cap. (pasSubject aag, Receive, pasObjectAbs aag nptr) \<in> pasPolicy aag \<and> is_subject aag thread)) (receive_signal thread cap is_blocking) proof (prove)
goal (3 subgoals):
 1. reads_respects aag l ?P1 (receive_signal thread cap is_blocking)
 2. doesnt_touch_globals ?Q1 (receive_signal thread cap is_blocking)
 3. \<And>s. (valid_global_objs and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pas_refined aag and (\<lambda>s. thread \<noteq> idle_thread s) and is_subject aag \<circ> cur_thread and K (\<forall>nptr\<in>obj_refs_ac cap. (pasSubject aag, Receive, pasObjectAbs aag nptr) \<in> pasPolicy aag \<and> is_subject aag thread)) s \<Longrightarrow> (?P1 and ?Q1) s proof (prove)
goal (2 subgoals):
 1. doesnt_touch_globals ?Q1 (receive_signal thread cap is_blocking)
 2. \<And>s. (valid_global_objs and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pas_refined aag and (\<lambda>s. thread \<noteq> idle_thread s) and is_subject aag \<circ> cur_thread and K (\<forall>nptr\<in>obj_refs_ac cap. (pasSubject aag, Receive, pasObjectAbs aag nptr) \<in> pasPolicy aag \<and> is_subject aag thread)) s \<Longrightarrow> (valid_objs and pas_refined aag and (\<lambda>s. is_subject aag (cur_thread s)) and K (\<forall>ntfnptr\<in>obj_refs_ac cap. (pasSubject aag, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> is_subject aag thread) and ?Q1) s proof (prove)
goal (2 subgoals):
 1. \<And>st. \<lbrace>globals_equiv st and ?Q1\<rbrace> receive_signal thread cap is_blocking \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<And>s. (valid_global_objs and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pas_refined aag and (\<lambda>s. thread \<noteq> idle_thread s) and is_subject aag \<circ> cur_thread and K (\<forall>nptr\<in>obj_refs_ac cap. (pasSubject aag, Receive, pasObjectAbs aag nptr) \<in> pasPolicy aag \<and> is_subject aag thread)) s \<Longrightarrow> (valid_objs and pas_refined aag and (\<lambda>s. is_subject aag (cur_thread s)) and K (\<forall>ntfnptr\<in>obj_refs_ac cap. (pasSubject aag, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> is_subject aag thread) and ?Q1) s proof (prove)
goal:
No subgoals!