theory Finalise_IF

lemma reply_cancel_ipc_reads_respects_f:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows "reads_respects_f aag l (silc_inv aag st and pas_refined aag and invs
                                                 and tcb_at tptr and K (is_subject aag tptr))
                          (reply_cancel_ipc tptr)" unfolding reply_cancel_ipc_def apply (rule gen_asm_ev) apply (wp cap_delete_one_reads_respects_f_transferable[where st=st]
            select_singleton_ev select_inv assert_wp
            reads_respects_f[OF get_cap_rev, where st=st]
            reads_respects_f[OF thread_set_reads_respects, where st=st]
            reads_respects_f[OF gets_descendants_of_revrv[folded equiv_valid_def2]]
         | simp add: when_def split del: if_split | elim conjE)+ apply (rule_tac Q="\<lambda> rv s. silc_inv aag st s \<and> invs s \<and> pas_refined aag s
                                                \<and> tcb_at tptr s \<and> is_subject aag tptr"
                in hoare_strengthen_post) apply (wp thread_set_tcb_fault_update_silc_inv hoare_vcg_imp_lift hoare_vcg_ball_lift
              thread_set_fault_empty_invs thread_set_fault_pas_refined'
           | wps | simp)+ apply clarsimp apply (rule conjI,rule TrueI) apply clarsimp apply (frule(1) reply_cap_descends_from_master0) apply (frule all_children_subjectReads[THEN all_children_descendants_of],force,force) apply (fastforce simp: cte_wp_at_caps_of_state
                    elim: silc_inv_no_transferable'[where slot = "(a,b)" for a b,simplified]) by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects_f aag l (silc_inv aag st and pas_refined aag and invs and tcb_at tptr and K (is_subject aag tptr)) (reply_cancel_ipc tptr) proof (prove)
goal (1 subgoal):
 1. reads_respects_f aag l (silc_inv aag st and pas_refined aag and invs and tcb_at tptr and K (is_subject aag tptr)) (do thread_set (tcb_fault_update (\<lambda>_. None)) tptr;
cap <- get_cap (tptr, tcb_cnode_index 2);
descs <- gets (descendants_of (tptr, tcb_cnode_index 2) \<circ> cdt);
when (descs \<noteq> {}) $ do assert (\<exists>cslot_ptr. descs = {cslot_ptr});
select descs >>= cap_delete_one
od
od) proof (prove)
goal (1 subgoal):
 1. is_subject aag tptr \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and pas_refined aag and invs and tcb_at tptr) (do thread_set (tcb_fault_update (\<lambda>_. None)) tptr;
cap <- get_cap (tptr, tcb_cnode_index 2);
descs <- gets (descendants_of (tptr, tcb_cnode_index 2) \<circ> cdt);
when (descs \<noteq> {}) $ do assert (\<exists>cslot_ptr. descs = {cslot_ptr});
select descs >>= cap_delete_one
od
od) proof (prove)
goal (2 subgoals):
 1. is_subject aag tptr \<Longrightarrow> \<lbrace>?P'65\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) tptr \<lbrace>\<lambda>rv s. pas_refined aag s \<and> ?Q43 () s \<and> (descendants_of (tptr, tcb_cnode_index 2) (cdt s) \<noteq> {} \<longrightarrow> (\<exists>a b. descendants_of (tptr, tcb_cnode_index 2) (cdt s) = {(a, b)}) \<longrightarrow> (\<forall>x\<in>descendants_of (tptr, tcb_cnode_index 2) (cdt s). silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> aag_can_read aag (fst x) \<and> pasObjectAbs aag (fst x) \<noteq> SilcLabel \<and> is_transferable_in x s))\<rbrace>
 2. \<And>s. \<lbrakk>is_subject aag tptr; (silc_inv aag st and pas_refined aag and invs and tcb_at tptr) s\<rbrakk> \<Longrightarrow> (silc_inv aag st and (\<lambda>_. True) and ?Q46) s \<and> silc_inv aag st s \<and> K (aag_can_read aag (fst (tptr, tcb_cnode_index 2))) s \<and> valid_global_refs s \<and> silc_inv aag ?st67 s \<and> ?P'65 s proof (prove)
goal (3 subgoals):
 1. is_subject aag tptr \<Longrightarrow> \<lbrace>?P'65\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) tptr \<lbrace>\<lambda>rv s. silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> tcb_at tptr s \<and> is_subject aag tptr\<rbrace>
 2. \<And>rv s. \<lbrakk>is_subject aag tptr; silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> tcb_at tptr s \<and> is_subject aag tptr\<rbrakk> \<Longrightarrow> pas_refined aag s \<and> ?Q43 () s \<and> (descendants_of (tptr, tcb_cnode_index 2) (cdt s) \<noteq> {} \<longrightarrow> (\<exists>a b. descendants_of (tptr, tcb_cnode_index 2) (cdt s) = {(a, b)}) \<longrightarrow> (\<forall>x\<in>descendants_of (tptr, tcb_cnode_index 2) (cdt s). silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> aag_can_read aag (fst x) \<and> pasObjectAbs aag (fst x) \<noteq> SilcLabel \<and> is_transferable_in x s))
 3. \<And>s. \<lbrakk>is_subject aag tptr; (silc_inv aag st and pas_refined aag and invs and tcb_at tptr) s\<rbrakk> \<Longrightarrow> (silc_inv aag st and (\<lambda>_. True) and ?Q46) s \<and> silc_inv aag st s \<and> K (aag_can_read aag (fst (tptr, tcb_cnode_index 2))) s \<and> valid_global_refs s \<and> silc_inv aag ?st67 s \<and> ?P'65 s proof (prove)
goal (2 subgoals):
 1. \<And>s. silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> tcb_at tptr s \<and> is_subject aag tptr \<Longrightarrow> ?Q43 () s \<and> (descendants_of (tptr, tcb_cnode_index 2) (cdt s) \<noteq> {} \<longrightarrow> (\<exists>a b. descendants_of (tptr, tcb_cnode_index 2) (cdt s) = {(a, b)}) \<longrightarrow> (\<forall>x\<in>descendants_of (tptr, tcb_cnode_index 2) (cdt s). aag_can_read aag (fst x) \<and> pasObjectAbs aag (fst x) \<noteq> SilcLabel \<and> is_transferable_in x s))
 2. \<And>s. \<lbrakk>is_subject aag tptr; (silc_inv aag st and pas_refined aag and invs and tcb_at tptr) s\<rbrakk> \<Longrightarrow> (silc_inv aag st and (\<lambda>_. True) and ?Q46) s \<and> silc_inv aag st s \<and> K (aag_can_read aag (fst (tptr, tcb_cnode_index 2))) s \<and> valid_global_refs s \<and> silc_inv aag ?st67 s \<and> silc_inv aag st s \<and> invs s \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state) s \<and> tcb_at tptr s \<and> is_subject aag tptr proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; tcb_at tptr s; is_subject aag tptr\<rbrakk> \<Longrightarrow> ?Q43 () s \<and> (descendants_of (tptr, tcb_cnode_index 2) (cdt s) \<noteq> {} \<longrightarrow> (\<exists>a b. descendants_of (tptr, tcb_cnode_index 2) (cdt s) = {(a, b)}) \<longrightarrow> (\<forall>x\<in>descendants_of (tptr, tcb_cnode_index 2) (cdt s). aag_can_read aag (fst x) \<and> pasObjectAbs aag (fst x) \<noteq> SilcLabel \<and> is_transferable_in x s))
 2. \<And>s. \<lbrakk>is_subject aag tptr; (silc_inv aag st and pas_refined aag and invs and tcb_at tptr) s\<rbrakk> \<Longrightarrow> (silc_inv aag st and (\<lambda>_. True) and ?Q46) s \<and> silc_inv aag st s \<and> K (aag_can_read aag (fst (tptr, tcb_cnode_index 2))) s \<and> valid_global_refs s \<and> silc_inv aag ?st67 s \<and> silc_inv aag st s \<and> invs s \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state) s \<and> tcb_at tptr s \<and> is_subject aag tptr proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; tcb_at tptr s; is_subject aag tptr\<rbrakk> \<Longrightarrow> descendants_of (tptr, tcb_cnode_index 2) (cdt s) \<noteq> {} \<longrightarrow> (\<exists>a b. descendants_of (tptr, tcb_cnode_index 2) (cdt s) = {(a, b)}) \<longrightarrow> (\<forall>x\<in>descendants_of (tptr, tcb_cnode_index 2) (cdt s). aag_can_read aag (fst x) \<and> pasObjectAbs aag (fst x) \<noteq> SilcLabel \<and> is_transferable_in x s)
 2. \<And>s. \<lbrakk>is_subject aag tptr; (silc_inv aag st and pas_refined aag and invs and tcb_at tptr) s\<rbrakk> \<Longrightarrow> (silc_inv aag st and (\<lambda>_. True) and ?Q46) s \<and> silc_inv aag st s \<and> K (aag_can_read aag (fst (tptr, tcb_cnode_index 2))) s \<and> valid_global_refs s \<and> silc_inv aag ?st67 s \<and> silc_inv aag st s \<and> invs s \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state) s \<and> tcb_at tptr s \<and> is_subject aag tptr proof (prove)
goal (2 subgoals):
 1. \<And>s b aa. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; tcb_at tptr s; is_subject aag tptr; descendants_of (tptr, tcb_cnode_index 2) (cdt s) = {(aa, b)}\<rbrakk> \<Longrightarrow> aag_can_read aag aa \<and> pasObjectAbs aag aa \<noteq> SilcLabel \<and> is_transferable_in (aa, b) s
 2. \<And>s. \<lbrakk>is_subject aag tptr; (silc_inv aag st and pas_refined aag and invs and tcb_at tptr) s\<rbrakk> \<Longrightarrow> (silc_inv aag st and (\<lambda>_. True) and ?Q46) s \<and> silc_inv aag st s \<and> K (aag_can_read aag (fst (tptr, tcb_cnode_index 2))) s \<and> valid_global_refs s \<and> silc_inv aag ?st67 s \<and> silc_inv aag st s \<and> invs s \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state) s \<and> tcb_at tptr s \<and> is_subject aag tptr proof (prove)
goal (2 subgoals):
 1. \<And>s b aa. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; tcb_at tptr s; is_subject aag tptr; descendants_of (tptr, tcb_cnode_index 2) (cdt s) = {(aa, b)}; \<forall>sl\<in>descendants_of (tptr, tcb_cnode_index 2) (cdt s). \<exists>R. caps_of_state s sl = Some (ReplyCap tptr False R)\<rbrakk> \<Longrightarrow> aag_can_read aag aa \<and> pasObjectAbs aag aa \<noteq> SilcLabel \<and> is_transferable_in (aa, b) s
 2. \<And>s. \<lbrakk>is_subject aag tptr; (silc_inv aag st and pas_refined aag and invs and tcb_at tptr) s\<rbrakk> \<Longrightarrow> (silc_inv aag st and (\<lambda>_. True) and ?Q46) s \<and> silc_inv aag st s \<and> K (aag_can_read aag (fst (tptr, tcb_cnode_index 2))) s \<and> valid_global_refs s \<and> silc_inv aag ?st67 s \<and> silc_inv aag st s \<and> invs s \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state) s \<and> tcb_at tptr s \<and> is_subject aag tptr proof (prove)
goal (2 subgoals):
 1. \<And>s b aa. \<lbrakk>silc_inv aag st s; invs s; pas_refined aag s; tcb_at tptr s; is_subject aag tptr; descendants_of (tptr, tcb_cnode_index 2) (cdt s) = {(aa, b)}; \<forall>sl\<in>descendants_of (tptr, tcb_cnode_index 2) (cdt s). \<exists>R. caps_of_state s sl = Some (ReplyCap tptr False R); (aag_can_read aag \<circ> fst) (aa, b)\<rbrakk> \<Longrightarrow> aag_can_read aag aa \<and> pasObjectAbs aag aa \<noteq> SilcLabel \<and> is_transferable_in (aa, b) s
 2. \<And>s. \<lbrakk>is_subject aag tptr; (silc_inv aag st and pas_refined aag and invs and tcb_at tptr) s\<rbrakk> \<Longrightarrow> (silc_inv aag st and (\<lambda>_. True) and ?Q46) s \<and> silc_inv aag st s \<and> K (aag_can_read aag (fst (tptr, tcb_cnode_index 2))) s \<and> valid_global_refs s \<and> silc_inv aag ?st67 s \<and> silc_inv aag st s \<and> invs s \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state) s \<and> tcb_at tptr s \<and> is_subject aag tptr proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_subject aag tptr; (silc_inv aag st and pas_refined aag and invs and tcb_at tptr) s\<rbrakk> \<Longrightarrow> (silc_inv aag st and (\<lambda>_. True) and ?Q46) s \<and> silc_inv aag st s \<and> K (aag_can_read aag (fst (tptr, tcb_cnode_index 2))) s \<and> valid_global_refs s \<and> silc_inv aag ?st67 s \<and> silc_inv aag st s \<and> invs s \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state) s \<and> tcb_at tptr s \<and> is_subject aag tptr