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 (\<not> is_untyped_cap (vrt_cap) \<and> cdl_same_arch_obj_as vrt_cap cap \<and> ~is_memory_cap 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 get_cap_rv'[where cap=cap]) apply (clarsimp) apply (wp tcb_empty_thread_slot_wpE[sep_wand_wpE]) apply (clarsimp) apply (sep_cancel) apply (sep_cancel, safe, sep_solve+) 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 (cap_type vrt_cap \<noteq> Some UntypedType \<and> cdl_same_arch_obj_as vrt_cap cap \<and> \<not> is_memory_cap 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 (cap_type vrt_cap \<noteq> Some UntypedType \<and> cdl_same_arch_obj_as vrt_cap cap \<and> \<not> is_memory_cap 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; cap_type vrt_cap \<noteq> Some UntypedType; cdl_same_arch_obj_as vrt_cap cap; \<not> is_memory_cap 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 (3 subgoals):
 1. \<And>s y. \<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; cap_type vrt_cap \<noteq> Some UntypedType; cdl_same_arch_obj_as vrt_cap cap; \<not> is_memory_cap cap\<rbrakk> \<Longrightarrow> \<lbrace>?B6 s y\<rbrace> liftE (get_cap vrt_slot) \<lbrace>\<lambda>src_cap. if cdl_same_arch_obj_as vrt_cap src_cap 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)) 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)\<rbrace>, \<lbrace>E\<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; cap_type vrt_cap \<noteq> Some UntypedType; cdl_same_arch_obj_as vrt_cap cap; \<not> is_memory_cap cap\<rbrakk> \<Longrightarrow> \<lbrace>?Q5 s\<rbrace> tcb_empty_thread_slot target_tcb tcb_vspace_slot \<lbrace>?B6 s\<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; cap_type vrt_cap \<noteq> Some UntypedType; cdl_same_arch_obj_as vrt_cap cap; \<not> is_memory_cap cap; s = sa\<rbrakk> \<Longrightarrow> ?Q5 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; cap_type vrt_cap \<noteq> Some UntypedType; cdl_same_arch_obj_as vrt_cap cap; \<not> is_memory_cap cap\<rbrakk> \<Longrightarrow> \<lbrace>?Q5 s\<rbrace> tcb_empty_thread_slot target_tcb tcb_vspace_slot \<lbrace>\<lambda>y sa. cdl.lift (vrt_slot \<mapsto>c cap \<and>* ?R12 s y) sa \<and> (if cdl_same_arch_obj_as vrt_cap cap 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)) 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 \<and> \<not> is_memory_cap cap\<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; cap_type vrt_cap \<noteq> Some UntypedType; cdl_same_arch_obj_as vrt_cap cap; \<not> is_memory_cap cap; s = sa\<rbrakk> \<Longrightarrow> ?Q5 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; cap_type vrt_cap \<noteq> Some UntypedType; cdl_same_arch_obj_as vrt_cap cap; \<not> is_memory_cap cap\<rbrakk> \<Longrightarrow> \<lbrace>?Q5 s\<rbrace> tcb_empty_thread_slot target_tcb tcb_vspace_slot \<lbrace>\<lambda>y sa. cdl.lift (vrt_slot \<mapsto>c cap \<and>* ?R12 s ()) sa \<and> 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\<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; cap_type vrt_cap \<noteq> Some UntypedType; cdl_same_arch_obj_as vrt_cap cap; \<not> is_memory_cap cap; s = sa\<rbrakk> \<Longrightarrow> ?Q5 s sa proof (prove)
goal (1 subgoal):
 1. \<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; cap_type vrt_cap \<noteq> Some UntypedType; cdl_same_arch_obj_as vrt_cap cap; \<not> is_memory_cap 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>* (\<lambda>a. (vrt_slot \<mapsto>c cap \<and>* ?R12 s ()) a \<and> (((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))) 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; cap_type vrt_cap \<noteq> Some UntypedType; cdl_same_arch_obj_as vrt_cap cap; \<not> is_memory_cap cap\<rbrakk> \<Longrightarrow> cdl.lift ((target_tcb, tcb_vspace_slot) \<mapsto>c NullCap \<and>* ((target_tcb, tcb_vspace_slot) \<mapsto>c NullCap \<longrightarrow>* (\<lambda>a. (vrt_slot \<mapsto>c cap \<and>* ?R12 sa ()) a \<and> (((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))) sa proof (prove)
goal (1 subgoal):
 1. \<And>sa s. \<lbrakk>cap_type vrt_cap \<noteq> Some UntypedType; cdl_same_arch_obj_as vrt_cap cap; \<not> is_memory_cap cap; (vrt_slot \<mapsto>c cap \<and>* tcb_cap_slot \<mapsto>c TcbCap target_tcb \<and>* R) s\<rbrakk> \<Longrightarrow> ((target_tcb, tcb_vspace_slot) \<mapsto>c NullCap \<longrightarrow>* (\<lambda>a. (vrt_slot \<mapsto>c cap \<and>* ?R12 sa ()) a \<and> ((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)) s proof (prove)
goal:
No subgoals!