theory TCB_DP

lemma tcb_update_vspace_root_wp':
 "\<lbrace>< (vrt_slot) \<mapsto>c cap \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c (TcbCap target_tcb) \<and>*  R>
    and K (is_pd_cap cap \<and> reset_cap_asid cap = reset_cap_asid vrt_cap) \<rbrace>
 tcb_update_vspace_root target_tcb tcb_cap_slot (vrt_cap, vrt_slot)
\<lbrace>\<lambda>_. < (target_tcb, tcb_vspace_slot) \<mapsto>c vrt_cap \<and>* tcb_cap_slot \<mapsto>c (TcbCap target_tcb) \<and>* (vrt_slot) \<mapsto>c cap \<and>* R>\<rbrace>, \<lbrace>E\<rbrace>" apply (rule hoare_name_pre_stateE) apply (clarsimp simp: tcb_update_vspace_root_def sep_any_All) apply (wp whenE_wp tcb_update_thread_slot_wp[sep_wand_side_wpE'] get_cap_rv)+ apply (wp hoare_vcg_conj_liftE1) apply (wp tcb_empty_thread_slot_wpE[sep_wand_wpE], (clarsimp simp: sep_conj_assoc | sep_solve) +) apply (wp tcb_empty_thread_slot_wpE[sep_wand_wpE], (clarsimp simp: sep_conj_assoc | sep_solve) +) apply (repeat_new \<open>rule conjI | clarsimp simp: sep_conj_assoc | sep_cancel\<close>) apply (drule reset_cap_asid_cap_type)+ apply (clarsimp simp: cap_type_def split: cdl_cap.splits ) apply (clarsimp simp: sep_conj_assoc | sep_cancel+)+ apply (clarsimp simp: cdl_same_arch_obj_as_def cap_type_def split: cdl_cap.splits dest!:reset_cap_asid_cap_type) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift (vrt_slot \<mapsto>c cap \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) and K (is_pd_cap cap \<and> reset_cap_asid cap = reset_cap_asid vrt_cap)\<rbrace> tcb_update_vspace_root target_tcb tcb_cap_slot (vrt_cap, vrt_slot) \<lbrace>\<lambda>_. cdl.lift ((target_tcb, tcb_vspace_slot) \<mapsto>c vrt_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* vrt_slot \<mapsto>c cap \<and>* R)\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (cdl.lift (vrt_slot \<mapsto>c cap \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) and K (is_pd_cap cap \<and> reset_cap_asid cap = reset_cap_asid vrt_cap)) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> tcb_update_vspace_root target_tcb tcb_cap_slot (vrt_cap, vrt_slot) \<lbrace>\<lambda>_. cdl.lift ((target_tcb, tcb_vspace_slot) \<mapsto>c vrt_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* vrt_slot \<mapsto>c cap \<and>* R)\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cdl.lift (vrt_slot \<mapsto>c cap \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) s; is_pd_cap cap; reset_cap_asid cap = reset_cap_asid vrt_cap\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> doE y <- tcb_empty_thread_slot target_tcb tcb_vspace_slot;
src_cap <- liftE (get_cap vrt_slot);
whenE (cdl_same_arch_obj_as vrt_cap src_cap) (tcb_update_thread_slot target_tcb tcb_cap_slot tcb_vspace_slot (vrt_cap, vrt_slot))
odE \<lbrace>\<lambda>_. cdl.lift ((target_tcb, tcb_vspace_slot) \<mapsto>c vrt_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* vrt_slot \<mapsto>c cap \<and>* R)\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>cdl.lift (vrt_slot \<mapsto>c cap \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) s; is_pd_cap cap; reset_cap_asid cap = reset_cap_asid vrt_cap\<rbrakk> \<Longrightarrow> \<lbrace>?Q4 s\<rbrace> tcb_empty_thread_slot target_tcb tcb_vspace_slot \<lbrace>\<lambda>y sa. cdl.lift (vrt_slot \<mapsto>c ?cap10 s y \<and>* ?R10 s y) sa \<and> (\<forall>c. reset_cap_asid c = reset_cap_asid (?cap10 s y) \<longrightarrow> (if cdl_same_arch_obj_as vrt_cap c then cdl.lift (((target_tcb, tcb_vspace_slot) \<mapsto>c - \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb) \<and>* ((target_tcb, tcb_vspace_slot) \<mapsto>c vrt_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<longrightarrow>* (target_tcb, tcb_vspace_slot) \<mapsto>c vrt_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* vrt_slot \<mapsto>c cap \<and>* R) and K (cap_type vrt_cap \<noteq> Some UntypedType)) else cdl.lift ((target_tcb, tcb_vspace_slot) \<mapsto>c vrt_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* vrt_slot \<mapsto>c cap \<and>* R)) sa)\<rbrace>, \<lbrace>E\<rbrace>
 2. \<And>s sa. \<lbrakk>cdl.lift (vrt_slot \<mapsto>c cap \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) s; is_pd_cap cap; reset_cap_asid cap = reset_cap_asid vrt_cap; s = sa\<rbrakk> \<Longrightarrow> ?Q4 s sa proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>cdl.lift (vrt_slot \<mapsto>c cap \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) s; is_pd_cap cap; reset_cap_asid cap = reset_cap_asid vrt_cap\<rbrakk> \<Longrightarrow> \<lbrace>?P12 s\<rbrace> tcb_empty_thread_slot target_tcb tcb_vspace_slot \<lbrace>\<lambda>rv. cdl.lift (vrt_slot \<mapsto>c ?cap10 s rv \<and>* ?R10 s rv)\<rbrace>, -
 2. \<And>s. \<lbrakk>cdl.lift (vrt_slot \<mapsto>c cap \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) s; is_pd_cap cap; reset_cap_asid cap = reset_cap_asid vrt_cap\<rbrakk> \<Longrightarrow> \<lbrace>?P'12 s\<rbrace> tcb_empty_thread_slot target_tcb tcb_vspace_slot \<lbrace>\<lambda>rv sa. \<forall>c. reset_cap_asid c = reset_cap_asid (?cap10 s rv) \<longrightarrow> (if cdl_same_arch_obj_as vrt_cap c then cdl.lift (((target_tcb, tcb_vspace_slot) \<mapsto>c - \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb) \<and>* ((target_tcb, tcb_vspace_slot) \<mapsto>c vrt_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<longrightarrow>* (target_tcb, tcb_vspace_slot) \<mapsto>c vrt_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* vrt_slot \<mapsto>c cap \<and>* R) and K (cap_type vrt_cap \<noteq> Some UntypedType)) else cdl.lift ((target_tcb, tcb_vspace_slot) \<mapsto>c vrt_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* vrt_slot \<mapsto>c cap \<and>* R)) sa\<rbrace>, \<lbrace>E\<rbrace>
 3. \<And>s sa. \<lbrakk>cdl.lift (vrt_slot \<mapsto>c cap \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) s; is_pd_cap cap; reset_cap_asid cap = reset_cap_asid vrt_cap; s = sa\<rbrakk> \<Longrightarrow> (?P12 s and ?P'12 s) sa proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>cdl.lift (vrt_slot \<mapsto>c cap \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) s; is_pd_cap cap; reset_cap_asid cap = reset_cap_asid vrt_cap\<rbrakk> \<Longrightarrow> \<lbrace>?P'12 s\<rbrace> tcb_empty_thread_slot target_tcb tcb_vspace_slot \<lbrace>\<lambda>rv sa. \<forall>c. (cdl_same_arch_obj_as vrt_cap c \<longrightarrow> reset_cap_asid c = reset_cap_asid (?cap22 s) \<longrightarrow> cdl.lift ((target_tcb, tcb_vspace_slot) \<mapsto>c - \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* ((target_tcb, tcb_vspace_slot) \<mapsto>c vrt_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<longrightarrow>* (target_tcb, tcb_vspace_slot) \<mapsto>c vrt_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* vrt_slot \<mapsto>c cap \<and>* R)) sa \<and> cap_type vrt_cap \<noteq> Some UntypedType) \<and> (\<not> cdl_same_arch_obj_as vrt_cap c \<longrightarrow> reset_cap_asid c = reset_cap_asid (?cap22 s) \<longrightarrow> cdl.lift ((target_tcb, tcb_vspace_slot) \<mapsto>c vrt_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* vrt_slot \<mapsto>c cap \<and>* R) sa)\<rbrace>, \<lbrace>E\<rbrace>
 2. \<And>s sa. \<lbrakk>cdl.lift (vrt_slot \<mapsto>c cap \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) s; is_pd_cap cap; reset_cap_asid cap = reset_cap_asid vrt_cap; s = sa\<rbrakk> \<Longrightarrow> (cdl.lift ((target_tcb, tcb_vspace_slot) \<mapsto>c NullCap \<and>* ((target_tcb, tcb_vspace_slot) \<mapsto>c NullCap \<longrightarrow>* vrt_slot \<mapsto>c ?cap22 s \<and>* ?R20 s)) and ?P'12 s) sa proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>cdl.lift (vrt_slot \<mapsto>c cap \<and>* (target_tcb, tcb_vspace_slot) \<mapsto>c NullCap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) sa; is_pd_cap cap; reset_cap_asid cap = reset_cap_asid vrt_cap\<rbrakk> \<Longrightarrow> cdl.lift ((target_tcb, tcb_vspace_slot) \<mapsto>c NullCap \<and>* ((target_tcb, tcb_vspace_slot) \<mapsto>c NullCap \<longrightarrow>* vrt_slot \<mapsto>c ?cap22 sa \<and>* ?R20 sa)) sa \<and> cdl.lift ((target_tcb, tcb_vspace_slot) \<mapsto>c NullCap \<and>* ((target_tcb, tcb_vspace_slot) \<mapsto>c NullCap \<longrightarrow>* (\<lambda>a. \<forall>c. (cdl_same_arch_obj_as vrt_cap c \<longrightarrow> reset_cap_asid c = reset_cap_asid (?cap22 sa) \<longrightarrow> ((target_tcb, tcb_vspace_slot) \<mapsto>c - \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* ((target_tcb, tcb_vspace_slot) \<mapsto>c vrt_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<longrightarrow>* (target_tcb, tcb_vspace_slot) \<mapsto>c vrt_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* vrt_slot \<mapsto>c cap \<and>* R)) a \<and> cap_type vrt_cap \<noteq> Some UntypedType) \<and> (\<not> cdl_same_arch_obj_as vrt_cap c \<longrightarrow> reset_cap_asid c = reset_cap_asid (?cap22 sa) \<longrightarrow> ((target_tcb, tcb_vspace_slot) \<mapsto>c vrt_cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* vrt_slot \<mapsto>c cap \<and>* R) a)))) sa proof (prove)
goal (2 subgoals):
 1. \<And>sa sb c. \<lbrakk>is_pd_cap cap; reset_cap_asid cap = reset_cap_asid vrt_cap; ((target_tcb, tcb_vspace_slot) \<mapsto>c NullCap \<and>* vrt_slot \<mapsto>c cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) sb; cdl_same_arch_obj_as vrt_cap c; reset_cap_asid c = reset_cap_asid cap; is_untyped_cap vrt_cap\<rbrakk> \<Longrightarrow> False
 2. \<And>sa c s. \<lbrakk>is_pd_cap cap; reset_cap_asid cap = reset_cap_asid vrt_cap; \<not> cdl_same_arch_obj_as vrt_cap c; reset_cap_asid c = reset_cap_asid cap; ((target_tcb, tcb_vspace_slot) \<mapsto>c NullCap) s\<rbrakk> \<Longrightarrow> ((target_tcb, tcb_vspace_slot) \<mapsto>c vrt_cap) s proof (prove)
goal (2 subgoals):
 1. \<And>sa sb c. \<lbrakk>is_pd_cap cap; ((target_tcb, tcb_vspace_slot) \<mapsto>c NullCap \<and>* vrt_slot \<mapsto>c cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) sb; cdl_same_arch_obj_as vrt_cap c; is_untyped_cap vrt_cap; cap_type cap = cap_type vrt_cap; cap_type c = cap_type cap\<rbrakk> \<Longrightarrow> False
 2. \<And>sa c s. \<lbrakk>is_pd_cap cap; reset_cap_asid cap = reset_cap_asid vrt_cap; \<not> cdl_same_arch_obj_as vrt_cap c; reset_cap_asid c = reset_cap_asid cap; ((target_tcb, tcb_vspace_slot) \<mapsto>c NullCap) s\<rbrakk> \<Longrightarrow> ((target_tcb, tcb_vspace_slot) \<mapsto>c vrt_cap) s proof (prove)
goal (1 subgoal):
 1. \<And>sa c s. \<lbrakk>is_pd_cap cap; reset_cap_asid cap = reset_cap_asid vrt_cap; \<not> cdl_same_arch_obj_as vrt_cap c; reset_cap_asid c = reset_cap_asid cap; ((target_tcb, tcb_vspace_slot) \<mapsto>c NullCap) s\<rbrakk> \<Longrightarrow> ((target_tcb, tcb_vspace_slot) \<mapsto>c vrt_cap) s proof (prove)
goal (1 subgoal):
 1. \<And>c s. \<lbrakk>is_pd_cap cap; reset_cap_asid cap = reset_cap_asid vrt_cap; \<not> cdl_same_arch_obj_as vrt_cap c; reset_cap_asid c = reset_cap_asid vrt_cap; ((target_tcb, tcb_vspace_slot) \<mapsto>c NullCap) s\<rbrakk> \<Longrightarrow> ((target_tcb, tcb_vspace_slot) \<mapsto>c vrt_cap) s proof (prove)
goal:
No subgoals!