theory FinalCaps

lemma reply_cancel_ipc_silc_inv:
  "\<lbrace>silc_inv aag st and valid_mdb and pas_refined aag and K (is_subject aag t)\<rbrace>
   reply_cancel_ipc t
   \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" unfolding reply_cancel_ipc_def apply (wp cap_delete_one_silc_inv hoare_vcg_if_lift | simp)+ apply wps apply (wp hoare_weak_lift_imp hoare_vcg_all_lift hoare_vcg_ball_lift) apply clarsimp apply (rename_tac b a) apply (frule(1) descendants_of_owned_or_transferable, force, force, elim disjE) apply (clarsimp simp add:silc_inv_def) apply (case_tac "cdt s (a,b)") apply (fastforce dest: descendants_of_NoneD) apply (elim is_transferable.cases) apply (fastforce dest: mdb_cte_atD valid_mdb_mdb_cte_at simp:  cte_wp_at_caps_of_state) apply (fastforce dest: mdb_cte_atD valid_mdb_mdb_cte_at simp:  cte_wp_at_caps_of_state) apply (erule(1) silc_inv_no_transferableD') apply (force simp add:cte_wp_at_caps_of_state) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and valid_mdb and pas_refined aag and K (is_subject aag t)\<rbrace> reply_cancel_ipc t \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and valid_mdb and pas_refined aag and K (is_subject aag t)\<rbrace> do 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 assert (\<exists>cslot_ptr. descs = {cslot_ptr});
select descs >>= cap_delete_one
od
od \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>\<lambda>x s. (descendants_of (t, tcb_cnode_index 2) (cdt s) \<noteq> {} \<longrightarrow> (\<exists>a b. descendants_of (t, tcb_cnode_index 2) (cdt s) = {(a, b)}) \<longrightarrow> (\<forall>x\<in>descendants_of (t, tcb_cnode_index 2) (cdt s). silc_inv aag st s \<and> pasObjectAbs aag (fst x) \<noteq> SilcLabel)) \<and> (descendants_of (t, tcb_cnode_index 2) (cdt s) = {} \<longrightarrow> silc_inv aag st s)\<rbrace>
 2. \<And>s. (silc_inv aag st and valid_mdb and pas_refined aag and K (is_subject aag t)) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>prev_s. \<lbrace>?P26 prev_s\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>\<lambda>rv s'. (descendants_of (t, tcb_cnode_index 2) (cdt prev_s) \<noteq> {} \<longrightarrow> (\<exists>a b. descendants_of (t, tcb_cnode_index 2) (cdt prev_s) = {(a, b)}) \<longrightarrow> (\<forall>x\<in>descendants_of (t, tcb_cnode_index 2) (cdt prev_s). silc_inv aag st s' \<and> pasObjectAbs aag (fst x) \<noteq> SilcLabel)) \<and> (descendants_of (t, tcb_cnode_index 2) (cdt prev_s) = {} \<longrightarrow> silc_inv aag st s')\<rbrace>
 2. \<And>s. (silc_inv aag st and valid_mdb and pas_refined aag and K (is_subject aag t)) s \<Longrightarrow> ?P26 s s proof (prove)
goal (1 subgoal):
 1. \<And>s. (silc_inv aag st and valid_mdb and pas_refined aag and K (is_subject aag t)) s \<Longrightarrow> (descendants_of (t, tcb_cnode_index 2) (cdt s) \<noteq> {} \<longrightarrow> (\<exists>a b. descendants_of (t, tcb_cnode_index 2) (cdt s) = {(a, b)}) \<longrightarrow> (\<forall>x\<in>descendants_of (t, tcb_cnode_index 2) (cdt s). silc_inv aag st s \<and> pasObjectAbs aag (fst x) \<noteq> SilcLabel)) \<and> (descendants_of (t, tcb_cnode_index 2) (cdt s) = {} \<longrightarrow> silc_inv aag st s) proof (prove)
goal (1 subgoal):
 1. \<And>s b aa. \<lbrakk>silc_inv aag st s; valid_mdb s; pas_refined aag s; is_subject aag t; descendants_of (t, tcb_cnode_index 2) (cdt s) = {(aa, b)}; pasObjectAbs aag aa = SilcLabel\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s b a. \<lbrakk>silc_inv aag st s; valid_mdb s; pas_refined aag s; is_subject aag t; descendants_of (t, tcb_cnode_index 2) (cdt s) = {(a, b)}; pasObjectAbs aag a = SilcLabel\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s b a. \<lbrakk>silc_inv aag st s; valid_mdb s; pas_refined aag s; is_subject aag t; descendants_of (t, tcb_cnode_index 2) (cdt s) = {(a, b)}; pasObjectAbs aag a = SilcLabel; is_subject aag (fst (a, b))\<rbrakk> \<Longrightarrow> False
 2. \<And>s b a. \<lbrakk>silc_inv aag st s; valid_mdb s; pas_refined aag s; is_subject aag t; descendants_of (t, tcb_cnode_index 2) (cdt s) = {(a, b)}; pasObjectAbs aag a = SilcLabel; is_transferable_in (a, b) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s b a. \<lbrakk>silc_inv aag st s; valid_mdb s; pas_refined aag s; is_subject aag t; descendants_of (t, tcb_cnode_index 2) (cdt s) = {(a, b)}; pasObjectAbs aag a = SilcLabel; is_transferable_in (a, b) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s b a. \<lbrakk>silc_inv aag st s; valid_mdb s; pas_refined aag s; is_subject aag t; descendants_of (t, tcb_cnode_index 2) (cdt s) = {(a, b)}; pasObjectAbs aag a = SilcLabel; is_transferable_in (a, b) s; cdt s (a, b) = None\<rbrakk> \<Longrightarrow> False
 2. \<And>s b a aa. \<lbrakk>silc_inv aag st s; valid_mdb s; pas_refined aag s; is_subject aag t; descendants_of (t, tcb_cnode_index 2) (cdt s) = {(a, b)}; pasObjectAbs aag a = SilcLabel; is_transferable_in (a, b) s; cdt s (a, b) = Some aa\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s b a aa. \<lbrakk>silc_inv aag st s; valid_mdb s; pas_refined aag s; is_subject aag t; descendants_of (t, tcb_cnode_index 2) (cdt s) = {(a, b)}; pasObjectAbs aag a = SilcLabel; is_transferable_in (a, b) s; cdt s (a, b) = Some aa\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s b a aa. \<lbrakk>silc_inv aag st s; valid_mdb s; pas_refined aag s; is_subject aag t; descendants_of (t, tcb_cnode_index 2) (cdt s) = {(a, b)}; pasObjectAbs aag a = SilcLabel; cdt s (a, b) = Some aa; caps_of_state s (a, b) = None\<rbrakk> \<Longrightarrow> False
 2. \<And>s b a aa. \<lbrakk>silc_inv aag st s; valid_mdb s; pas_refined aag s; is_subject aag t; descendants_of (t, tcb_cnode_index 2) (cdt s) = {(a, b)}; pasObjectAbs aag a = SilcLabel; cdt s (a, b) = Some aa; caps_of_state s (a, b) = Some NullCap\<rbrakk> \<Longrightarrow> False
 3. \<And>s b a aa ta R. \<lbrakk>silc_inv aag st s; valid_mdb s; pas_refined aag s; is_subject aag t; descendants_of (t, tcb_cnode_index 2) (cdt s) = {(a, b)}; pasObjectAbs aag a = SilcLabel; cdt s (a, b) = Some aa; caps_of_state s (a, b) = Some (ReplyCap ta False R)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s b a aa. \<lbrakk>silc_inv aag st s; valid_mdb s; pas_refined aag s; is_subject aag t; descendants_of (t, tcb_cnode_index 2) (cdt s) = {(a, b)}; pasObjectAbs aag a = SilcLabel; cdt s (a, b) = Some aa; caps_of_state s (a, b) = Some NullCap\<rbrakk> \<Longrightarrow> False
 2. \<And>s b a aa ta R. \<lbrakk>silc_inv aag st s; valid_mdb s; pas_refined aag s; is_subject aag t; descendants_of (t, tcb_cnode_index 2) (cdt s) = {(a, b)}; pasObjectAbs aag a = SilcLabel; cdt s (a, b) = Some aa; caps_of_state s (a, b) = Some (ReplyCap ta False R)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s b a aa ta R. \<lbrakk>silc_inv aag st s; valid_mdb s; pas_refined aag s; is_subject aag t; descendants_of (t, tcb_cnode_index 2) (cdt s) = {(a, b)}; pasObjectAbs aag a = SilcLabel; cdt s (a, b) = Some aa; caps_of_state s (a, b) = Some (ReplyCap ta False R)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s b a aa ta R. \<lbrakk>valid_mdb s; pas_refined aag s; is_subject aag t; descendants_of (t, tcb_cnode_index 2) (cdt s) = {(a, b)}; pasObjectAbs aag a = SilcLabel; cdt s (a, b) = Some aa; caps_of_state s (a, b) = Some (ReplyCap ta False R)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, ?b88 s b a aa ta R) s proof (prove)
goal:
No subgoals!