theory Finalise_AC

lemma reply_cancel_ipc_pas_refined[wp]:
  "\<lbrace>pas_refined aag and invs and tcb_at t and K (is_subject aag t)\<rbrace>
   reply_cancel_ipc t
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" apply (rule hoare_gen_asm) apply (simp add: reply_cancel_ipc_def) apply (wp add: wp_transferable del: wp_not_transferable) apply (rule hoare_strengthen_post[where Q="\<lambda>_. invs and tcb_at t and pas_refined aag"]) apply (wpsimp wp: hoare_wp_combs thread_set_tcb_fault_reset_invs thread_set_pas_refined)+ apply (frule(1) reply_cap_descends_from_master0) apply (fastforce simp: cte_wp_at_caps_of_state intro:it_Reply) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and invs and tcb_at t and K (is_subject aag t)\<rbrace> reply_cancel_ipc t \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_subject aag t \<Longrightarrow> \<lbrace>pas_refined aag and invs and tcb_at t\<rbrace> reply_cancel_ipc t \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_subject aag t \<Longrightarrow> \<lbrace>pas_refined aag and invs and tcb_at t\<rbrace> do y <- thread_set (tcb_fault_update (\<lambda>_. None)) t;
cap <- get_cap (t, tcb_cnode_index 2);
descs <- gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt);
when (descs \<noteq> {}) (do y <- assert (\<exists>a b. descs = {(a, b)});
select descs >>= cap_delete_one
od)
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (2 subgoals):
 1. is_subject aag t \<Longrightarrow> \<lbrace>?Q2\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>\<lambda>y s. (if (descendants_of (t, tcb_cnode_index 2) \<circ> cdt) s \<noteq> {} then \<lambda>sa. (\<exists>a b. (descendants_of (t, tcb_cnode_index 2) \<circ> cdt) s = {(a, b)}) \<longrightarrow> (\<forall>x\<in>(descendants_of (t, tcb_cnode_index 2) \<circ> cdt) s. (pas_refined aag and (pspace_aligned and valid_vspace_objs and valid_arch_state) and (valid_mdb and is_transferable_in x)) sa) else pas_refined aag) s\<rbrace>
 2. \<And>s. \<lbrakk>is_subject aag t; (pas_refined aag and invs and tcb_at t) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (3 subgoals):
 1. is_subject aag t \<Longrightarrow> \<lbrace>?Q2\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>\<lambda>_. invs and tcb_at t and pas_refined aag\<rbrace>
 2. \<And>rv s. \<lbrakk>is_subject aag t; (invs and tcb_at t and pas_refined aag) s\<rbrakk> \<Longrightarrow> (if (descendants_of (t, tcb_cnode_index 2) \<circ> cdt) s \<noteq> {} then \<lambda>sa. (\<exists>a b. (descendants_of (t, tcb_cnode_index 2) \<circ> cdt) s = {(a, b)}) \<longrightarrow> (\<forall>x\<in>(descendants_of (t, tcb_cnode_index 2) \<circ> cdt) s. (pas_refined aag and (pspace_aligned and valid_vspace_objs and valid_arch_state) and (valid_mdb and is_transferable_in x)) sa) else pas_refined aag) s
 3. \<And>s. \<lbrakk>is_subject aag t; (pas_refined aag and invs and tcb_at t) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (2 subgoals):
 1. \<And>s b aa. \<lbrakk>is_subject aag t; invs s; tcb_at t s; pas_refined aag s; descendants_of (t, tcb_cnode_index 2) (cdt s) = {(aa, b)}\<rbrakk> \<Longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> is_transferable_in (aa, b) s
 2. \<And>s. \<lbrakk>is_subject aag t; (pas_refined aag and invs and tcb_at t) s\<rbrakk> \<Longrightarrow> (invs s \<and> tcb_at t s) \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state) s proof (prove)
goal (2 subgoals):
 1. \<And>s b aa. \<lbrakk>is_subject aag t; invs s; tcb_at t s; pas_refined aag s; descendants_of (t, tcb_cnode_index 2) (cdt s) = {(aa, b)}; \<forall>sl\<in>descendants_of (t, tcb_cnode_index 2) (cdt s). \<exists>R. caps_of_state s sl = Some (ReplyCap t False R)\<rbrakk> \<Longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> is_transferable_in (aa, b) s
 2. \<And>s. \<lbrakk>is_subject aag t; (pas_refined aag and invs and tcb_at t) s\<rbrakk> \<Longrightarrow> (invs s \<and> tcb_at t s) \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_subject aag t; (pas_refined aag and invs and tcb_at t) s\<rbrakk> \<Longrightarrow> (invs s \<and> tcb_at t s) \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state) s proof (prove)
goal:
No subgoals!