theory Ipc_IF

lemma do_reply_transfer_reads_respects_f_g:
  assumes domains_distinct: "pas_domains_distinct aag"
  shows
    "reads_respects_f_g aag l (silc_inv aag st and invs and pas_refined aag and pas_cur_domain aag
                                               and tcb_at receiver and tcb_at sender
                                               and emptyable slot and is_subject aag \<circ> cur_thread
                                               and K (grant \<longrightarrow> is_subject aag receiver)
                                               and K (is_subject aag sender \<and>
                                                      aag_can_read aag receiver \<and>
                                                      is_subject aag (fst slot)))
                        (do_reply_transfer sender receiver slot grant)" apply (rule equiv_valid_guard_imp[OF reads_respects_f_g]) apply (rule do_reply_transfer_reads_respects_f[OF domains_distinct]) apply (rule doesnt_touch_globalsI) apply (wp do_reply_transfer_globals_equiv | simp)+ apply (simp add: invs_def valid_state_def valid_pspace_def | blast)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects_f_g aag l (silc_inv aag st and invs and pas_refined aag and pas_cur_domain aag and tcb_at receiver and tcb_at sender and emptyable slot and is_subject aag \<circ> cur_thread and K (grant \<longrightarrow> is_subject aag receiver) and K (is_subject aag sender \<and> aag_can_read aag receiver \<and> is_subject aag (fst slot))) (do_reply_transfer sender receiver slot grant) proof (prove)
goal (3 subgoals):
 1. reads_respects_f aag l ?P1 (do_reply_transfer sender receiver slot grant)
 2. doesnt_touch_globals ?Q1 (do_reply_transfer sender receiver slot grant)
 3. \<And>s. (silc_inv aag st and invs and pas_refined aag and pas_cur_domain aag and tcb_at receiver and tcb_at sender and emptyable slot and is_subject aag \<circ> cur_thread and K (grant \<longrightarrow> is_subject aag receiver) and K (is_subject aag sender \<and> aag_can_read aag receiver \<and> is_subject aag (fst slot))) s \<Longrightarrow> (?P1 and ?Q1) s proof (prove)
goal (2 subgoals):
 1. doesnt_touch_globals ?Q1 (do_reply_transfer sender receiver slot grant)
 2. \<And>s. (silc_inv aag st and invs and pas_refined aag and pas_cur_domain aag and tcb_at receiver and tcb_at sender and emptyable slot and is_subject aag \<circ> cur_thread and K (grant \<longrightarrow> is_subject aag receiver) and K (is_subject aag sender \<and> aag_can_read aag receiver \<and> is_subject aag (fst slot))) s \<Longrightarrow> (silc_inv aag ?st5 and invs and pas_refined aag and pas_cur_domain aag and tcb_at receiver and tcb_at sender and emptyable slot and is_subject aag \<circ> cur_thread and K (grant \<longrightarrow> is_subject aag receiver) and K (is_subject aag sender \<and> aag_can_read aag receiver \<and> is_subject aag (fst slot)) and ?Q1) s proof (prove)
goal (2 subgoals):
 1. \<And>st. \<lbrace>globals_equiv st and ?Q1\<rbrace> do_reply_transfer sender receiver slot grant \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<And>s. (silc_inv aag st and invs and pas_refined aag and pas_cur_domain aag and tcb_at receiver and tcb_at sender and emptyable slot and is_subject aag \<circ> cur_thread and K (grant \<longrightarrow> is_subject aag receiver) and K (is_subject aag sender \<and> aag_can_read aag receiver \<and> is_subject aag (fst slot))) s \<Longrightarrow> (silc_inv aag ?st5 and invs and pas_refined aag and pas_cur_domain aag and tcb_at receiver and tcb_at sender and emptyable slot and is_subject aag \<circ> cur_thread and K (grant \<longrightarrow> is_subject aag receiver) and K (is_subject aag sender \<and> aag_can_read aag receiver \<and> is_subject aag (fst slot)) and ?Q1) s proof (prove)
goal (1 subgoal):
 1. \<And>s. silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> tcb_at receiver s \<and> tcb_at sender s \<and> emptyable slot s \<and> is_subject aag (cur_thread s) \<and> (grant \<longrightarrow> is_subject aag receiver) \<and> is_subject aag sender \<and> aag_can_read aag receiver \<and> is_subject aag (fst slot) \<Longrightarrow> silc_inv aag ?st5 s \<and> 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 proof (prove)
goal:
No subgoals!