theory TCB_DP

lemma tcb_update_cspace_root_wp:
 "\<lbrace>< (crt_slot) \<mapsto>c cap \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c (TcbCap target_tcb) \<and>*  R>
   and  K (\<not> is_untyped_cap (crt_cap) \<and> is_cnode_cap cap \<and> cap_object cap = cap_object crt_cap)\<rbrace>
 tcb_update_cspace_root target_tcb tcb_cap_slot (crt_cap, crt_slot)
\<lbrace>\<lambda>_. < (target_tcb, tcb_cspace_slot) \<mapsto>c crt_cap \<and>* tcb_cap_slot \<mapsto>c (TcbCap target_tcb) \<and>* (crt_slot) \<mapsto>c cap \<and>* R>\<rbrace>, \<lbrace>E\<rbrace>" apply (rule hoare_name_pre_stateE) apply (clarsimp simp: tcb_update_cspace_root_def sep_any_All_side cong:cap_type_bad_cong) apply (wpsimp wp: whenE_wp tcb_update_thread_slot_wp[sep_wand_side_wpE] get_cap_rv
                    hoare_vcg_conj_liftE1) apply (wpsimp wp: tcb_empty_thread_slot_wpE[sep_wand_wpE] simp: sep_conj_assoc) apply (wpsimp wp: hoare_vcg_all_lift_R[THEN hoare_vcg_E_elim[rotated]]
                     hoare_vcg_const_imp_lift_R
                     tcb_empty_thread_slot_wpE[sep_wand_wpE]
          split_del: if_split simp: if_apply_def2) apply (clarsimp) apply (repeat_new \<open>rule conjI | clarsimp simp: sep_conj_assoc | sep_cancel\<close>) apply (drule not_memory_cap_reset_asid') apply (erule is_cnode_cap_not_memory_cap) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift (crt_slot \<mapsto>c cap \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) and K (cap_type crt_cap \<noteq> Some UntypedType \<and> is_cnode_cap cap \<and> cap_object cap = cap_object crt_cap)\<rbrace> tcb_update_cspace_root target_tcb tcb_cap_slot (crt_cap, crt_slot) \<lbrace>\<lambda>_. cdl.lift ((target_tcb, tcb_cspace_slot) \<mapsto>c crt_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* crt_slot \<mapsto>c cap \<and>* R)\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (cdl.lift (crt_slot \<mapsto>c cap \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) and K (cap_type crt_cap \<noteq> Some UntypedType \<and> is_cnode_cap cap \<and> cap_object cap = cap_object crt_cap)) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> tcb_update_cspace_root target_tcb tcb_cap_slot (crt_cap, crt_slot) \<lbrace>\<lambda>_. cdl.lift ((target_tcb, tcb_cspace_slot) \<mapsto>c crt_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* crt_slot \<mapsto>c cap \<and>* R)\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cdl.lift (crt_slot \<mapsto>c cap \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) s; cap_type crt_cap \<noteq> Some UntypedType; is_cnode_cap cap; cap_object cap = cap_object crt_cap\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> doE y <- tcb_empty_thread_slot target_tcb tcb_cspace_slot;
src_cap <- liftE (get_cap crt_slot);
whenE (is_cnode_cap src_cap \<and> cap_object src_cap = cap_object crt_cap) (tcb_update_thread_slot target_tcb tcb_cap_slot tcb_cspace_slot (crt_cap, crt_slot))
odE \<lbrace>\<lambda>_. cdl.lift ((target_tcb, tcb_cspace_slot) \<mapsto>c crt_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* crt_slot \<mapsto>c cap \<and>* R)\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>cdl.lift (crt_slot \<mapsto>c cap \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) s; cap_type crt_cap \<noteq> Some UntypedType; is_cnode_cap cap; cap_object cap = cap_object crt_cap\<rbrakk> \<Longrightarrow> \<lbrace>?P16 s\<rbrace> tcb_empty_thread_slot target_tcb tcb_cspace_slot \<lbrace>\<lambda>rv. cdl.lift (crt_slot \<mapsto>c ?cap13 s () \<and>* ?R13 s ())\<rbrace>, -
 2. \<And>s. \<lbrakk>cdl.lift (crt_slot \<mapsto>c cap \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) s; cap_type crt_cap \<noteq> Some UntypedType; is_cnode_cap cap; cap_object cap = cap_object crt_cap\<rbrakk> \<Longrightarrow> \<lbrace>?P'16 s\<rbrace> tcb_empty_thread_slot target_tcb tcb_cspace_slot \<lbrace>\<lambda>rv sa. \<forall>c. reset_cap_asid c = reset_cap_asid (?cap13 s rv) \<longrightarrow> (if is_cnode_cap c \<and> cap_object c = cap_object crt_cap then cdl.lift (((target_tcb, tcb_cspace_slot) \<mapsto>c - \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb) \<and>* ((target_tcb, tcb_cspace_slot) \<mapsto>c crt_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<longrightarrow>* (target_tcb, tcb_cspace_slot) \<mapsto>c crt_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* crt_slot \<mapsto>c cap \<and>* R)) else cdl.lift ((target_tcb, tcb_cspace_slot) \<mapsto>c crt_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* crt_slot \<mapsto>c cap \<and>* R)) sa\<rbrace>, \<lbrace>E\<rbrace>
 3. \<And>s sa. \<lbrakk>cdl.lift (crt_slot \<mapsto>c cap \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) s; cap_type crt_cap \<noteq> Some UntypedType; is_cnode_cap cap; cap_object cap = cap_object crt_cap; s = sa\<rbrakk> \<Longrightarrow> (?P16 s and ?P'16 s) sa proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>cdl.lift (crt_slot \<mapsto>c cap \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) s; cap_type crt_cap \<noteq> Some UntypedType; is_cnode_cap cap; cap_object cap = cap_object crt_cap\<rbrakk> \<Longrightarrow> \<lbrace>?P'16 s\<rbrace> tcb_empty_thread_slot target_tcb tcb_cspace_slot \<lbrace>\<lambda>rv sa. \<forall>c. reset_cap_asid c = reset_cap_asid (?cap13 s rv) \<longrightarrow> (if is_cnode_cap c \<and> cap_object c = cap_object crt_cap then cdl.lift (((target_tcb, tcb_cspace_slot) \<mapsto>c - \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb) \<and>* ((target_tcb, tcb_cspace_slot) \<mapsto>c crt_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<longrightarrow>* (target_tcb, tcb_cspace_slot) \<mapsto>c crt_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* crt_slot \<mapsto>c cap \<and>* R)) else cdl.lift ((target_tcb, tcb_cspace_slot) \<mapsto>c crt_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* crt_slot \<mapsto>c cap \<and>* R)) sa\<rbrace>, \<lbrace>E\<rbrace>
 2. \<And>s sa. \<lbrakk>cdl.lift (crt_slot \<mapsto>c cap \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) s; cap_type crt_cap \<noteq> Some UntypedType; is_cnode_cap cap; cap_object cap = cap_object crt_cap; s = sa\<rbrakk> \<Longrightarrow> (cdl.lift ((target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<and>* ((target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<longrightarrow>* crt_slot \<mapsto>c ?cap13 s () \<and>* ?R13 s ())) and ?P'16 s) sa proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>cdl.lift (crt_slot \<mapsto>c cap \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) s; cap_type crt_cap \<noteq> Some UntypedType; is_cnode_cap cap; cap_object cap = cap_object crt_cap; s = sa\<rbrakk> \<Longrightarrow> (cdl.lift ((target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<and>* ((target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<longrightarrow>* crt_slot \<mapsto>c ?cap34 s \<and>* ?R13 s ())) and (\<lambda>sa. cdl.lift ((target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<and>* ((target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<longrightarrow>* (\<lambda>a. True))) sa \<and> (\<forall>x. reset_cap_asid x = reset_cap_asid (?cap34 s) \<longrightarrow> (is_cnode_cap x \<and> cap_object x = cap_object crt_cap \<longrightarrow> cdl.lift ((target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<and>* ((target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<longrightarrow>* ((target_tcb, tcb_cspace_slot) \<mapsto>c - \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb) \<and>* ((target_tcb, tcb_cspace_slot) \<mapsto>c crt_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<longrightarrow>* (target_tcb, tcb_cspace_slot) \<mapsto>c crt_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* crt_slot \<mapsto>c cap \<and>* R))) sa) \<and> ((is_cnode_cap x \<longrightarrow> cap_object x \<noteq> cap_object crt_cap) \<longrightarrow> cdl.lift ((target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<and>* ((target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<longrightarrow>* (target_tcb, tcb_cspace_slot) \<mapsto>c crt_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* crt_slot \<mapsto>c cap \<and>* R)) sa)))) sa proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>cdl.lift (crt_slot \<mapsto>c cap \<and>* (target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) sa; cap_type crt_cap \<noteq> Some UntypedType; is_cnode_cap cap; cap_object cap = cap_object crt_cap\<rbrakk> \<Longrightarrow> cdl.lift ((target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<and>* ((target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<longrightarrow>* crt_slot \<mapsto>c ?cap34 sa \<and>* ?R13 sa ())) sa \<and> cdl.lift ((target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<and>* (\<lambda>s. True)) sa \<and> (\<forall>x. reset_cap_asid x = reset_cap_asid (?cap34 sa) \<longrightarrow> (is_cnode_cap x \<and> cap_object x = cap_object crt_cap \<longrightarrow> cdl.lift ((target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<and>* ((target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<longrightarrow>* ((target_tcb, tcb_cspace_slot) \<mapsto>c - \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb) \<and>* ((target_tcb, tcb_cspace_slot) \<mapsto>c crt_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<longrightarrow>* (target_tcb, tcb_cspace_slot) \<mapsto>c crt_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* crt_slot \<mapsto>c cap \<and>* R))) sa) \<and> ((is_cnode_cap x \<longrightarrow> cap_object x \<noteq> cap_object crt_cap) \<longrightarrow> cdl.lift ((target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<and>* ((target_tcb, tcb_cspace_slot) \<mapsto>c NullCap \<longrightarrow>* (target_tcb, tcb_cspace_slot) \<mapsto>c crt_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* crt_slot \<mapsto>c cap \<and>* R)) sa)) proof (prove)
goal (1 subgoal):
 1. \<And>sa x s. \<lbrakk>cap_type crt_cap \<noteq> Some UntypedType; is_cnode_cap cap; cap_object cap = cap_object crt_cap; reset_cap_asid x = reset_cap_asid cap; is_cnode_cap x \<longrightarrow> cap_object x \<noteq> cap_object crt_cap; ((target_tcb, tcb_cspace_slot) \<mapsto>c NullCap) s\<rbrakk> \<Longrightarrow> ((target_tcb, tcb_cspace_slot) \<mapsto>c crt_cap) s proof (prove)
goal (2 subgoals):
 1. \<And>sa x s. \<lbrakk>cap_type crt_cap \<noteq> Some UntypedType; is_cnode_cap cap; cap_object cap = cap_object crt_cap; is_cnode_cap x \<longrightarrow> cap_object x \<noteq> cap_object crt_cap; ((target_tcb, tcb_cspace_slot) \<mapsto>c NullCap) s\<rbrakk> \<Longrightarrow> \<not> is_memory_cap cap
 2. \<And>sa x s. \<lbrakk>cap_type crt_cap \<noteq> Some UntypedType; is_cnode_cap cap; cap_object cap = cap_object crt_cap; is_cnode_cap x \<longrightarrow> cap_object x \<noteq> cap_object crt_cap; ((target_tcb, tcb_cspace_slot) \<mapsto>c NullCap) s; x = cap\<rbrakk> \<Longrightarrow> ((target_tcb, tcb_cspace_slot) \<mapsto>c crt_cap) s proof (prove)
goal (1 subgoal):
 1. \<And>sa x s. \<lbrakk>cap_type crt_cap \<noteq> Some UntypedType; is_cnode_cap cap; cap_object cap = cap_object crt_cap; is_cnode_cap x \<longrightarrow> cap_object x \<noteq> cap_object crt_cap; ((target_tcb, tcb_cspace_slot) \<mapsto>c NullCap) s; x = cap\<rbrakk> \<Longrightarrow> ((target_tcb, tcb_cspace_slot) \<mapsto>c crt_cap) s proof (prove)
goal:
No subgoals!