theory TCB_DP

lemma has_restart_cap_wp:
    "\<lbrace>\<lambda>s. < (ptr,tcb_pending_op_slot) \<mapsto>c (cap) \<and>* R > s \<and> Q (cap = RestartCap) s \<rbrace> has_restart_cap ptr \<lbrace>Q\<rbrace>" apply (clarsimp simp: has_restart_cap_def) apply (wp get_thread_sep_wp) apply (clarsimp simp: get_thread_def) apply (wp) apply (wpc) apply (wp)+ apply (safe) apply (sep_drule (direct) opt_cap_sep_imp) apply (clarsimp simp: opt_cap_def) apply (clarsimp simp: slots_of_def) apply (clarsimp simp: object_slots_def) apply (clarsimp simp: reset_cap_asid_def) apply (clarsimp split: cdl_cap.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cdl.lift ((ptr, tcb_pending_op_slot) \<mapsto>c cap \<and>* R) s \<and> Q (cap = RestartCap) s\<rbrace> has_restart_cap ptr \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cdl.lift ((ptr, tcb_pending_op_slot) \<mapsto>c cap \<and>* R) s \<and> Q (cap = RestartCap) s\<rbrace> do t <- get_thread ptr;
return (cdl_tcb_caps t tcb_pending_op_slot = Some RestartCap)
od \<lbrace>Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> get_thread ptr \<lbrace>\<lambda>t. Q (cdl_tcb_caps t tcb_pending_op_slot = Some RestartCap)\<rbrace>
 2. \<And>s. cdl.lift ((ptr, tcb_pending_op_slot) \<mapsto>c cap \<and>* R) s \<and> Q (cap = RestartCap) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do t <- get_object ptr;
case t of Tcb tcb \<Rightarrow> return tcb | _ \<Rightarrow> fail
od \<lbrace>\<lambda>t. Q (cdl_tcb_caps t tcb_pending_op_slot = Some RestartCap)\<rbrace>
 2. \<And>s. cdl.lift ((ptr, tcb_pending_op_slot) \<mapsto>c cap \<and>* R) s \<and> Q (cap = RestartCap) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>t. \<lbrace>?B6 t\<rbrace> case t of Tcb tcb \<Rightarrow> return tcb | _ \<Rightarrow> fail \<lbrace>\<lambda>t. Q (cdl_tcb_caps t tcb_pending_op_slot = Some RestartCap)\<rbrace>
 2. \<lbrace>?Q\<rbrace> get_object ptr \<lbrace>?B6\<rbrace>
 3. \<And>s. cdl.lift ((ptr, tcb_pending_op_slot) \<mapsto>c cap \<and>* R) s \<and> Q (cap = RestartCap) s \<Longrightarrow> ?Q s proof (prove)
goal (12 subgoals):
 1. \<And>t. t = Endpoint \<Longrightarrow> \<lbrace>?R38 t\<rbrace> fail \<lbrace>\<lambda>t. Q (cdl_tcb_caps t tcb_pending_op_slot = Some RestartCap)\<rbrace>
 2. \<And>t. t = Notification \<Longrightarrow> \<lbrace>?R39 t\<rbrace> fail \<lbrace>\<lambda>t. Q (cdl_tcb_caps t tcb_pending_op_slot = Some RestartCap)\<rbrace>
 3. \<And>t x3. t = Tcb x3 \<Longrightarrow> \<lbrace>?R40 t x3\<rbrace> return x3 \<lbrace>\<lambda>t. Q (cdl_tcb_caps t tcb_pending_op_slot = Some RestartCap)\<rbrace>
 4. \<And>t x4. t = CNode x4 \<Longrightarrow> \<lbrace>?R41 t x4\<rbrace> fail \<lbrace>\<lambda>t. Q (cdl_tcb_caps t tcb_pending_op_slot = Some RestartCap)\<rbrace>
 5. \<And>t x5. t = AsidPool x5 \<Longrightarrow> \<lbrace>?R42 t x5\<rbrace> fail \<lbrace>\<lambda>t. Q (cdl_tcb_caps t tcb_pending_op_slot = Some RestartCap)\<rbrace>
 6. \<And>t x6. t = PageTable x6 \<Longrightarrow> \<lbrace>?R43 t x6\<rbrace> fail \<lbrace>\<lambda>t. Q (cdl_tcb_caps t tcb_pending_op_slot = Some RestartCap)\<rbrace>
 7. \<And>t x7. t = PageDirectory x7 \<Longrightarrow> \<lbrace>?R44 t x7\<rbrace> fail \<lbrace>\<lambda>t. Q (cdl_tcb_caps t tcb_pending_op_slot = Some RestartCap)\<rbrace>
 8. \<And>t x8. t = Frame x8 \<Longrightarrow> \<lbrace>?R45 t x8\<rbrace> fail \<lbrace>\<lambda>t. Q (cdl_tcb_caps t tcb_pending_op_slot = Some RestartCap)\<rbrace>
 9. \<And>t. t = Untyped \<Longrightarrow> \<lbrace>?R46 t\<rbrace> fail \<lbrace>\<lambda>t. Q (cdl_tcb_caps t tcb_pending_op_slot = Some RestartCap)\<rbrace>
 10. \<And>t x10. t = IRQNode x10 \<Longrightarrow> \<lbrace>?R47 t x10\<rbrace> fail \<lbrace>\<lambda>t. Q (cdl_tcb_caps t tcb_pending_op_slot = Some RestartCap)\<rbrace>
A total of 12 subgoals... proof (prove)
goal (1 subgoal):
 1. \<And>s. cdl.lift ((ptr, tcb_pending_op_slot) \<mapsto>c cap \<and>* R) s \<and> Q (cap = RestartCap) s \<Longrightarrow> cdl_objects s ptr \<noteq> None \<longrightarrow> (the (cdl_objects s ptr) = Endpoint \<longrightarrow> True) \<and> (the (cdl_objects s ptr) = Notification \<longrightarrow> True) \<and> (\<forall>x. the (cdl_objects s ptr) = Tcb x \<longrightarrow> Q (cdl_tcb_caps x tcb_pending_op_slot = Some RestartCap) s) \<and> (\<forall>x. the (cdl_objects s ptr) = CNode x \<longrightarrow> True) \<and> (\<forall>x. the (cdl_objects s ptr) = AsidPool x \<longrightarrow> True) \<and> (\<forall>x. the (cdl_objects s ptr) = PageTable x \<longrightarrow> True) \<and> (\<forall>x. the (cdl_objects s ptr) = PageDirectory x \<longrightarrow> True) \<and> (\<forall>x. the (cdl_objects s ptr) = Frame x \<longrightarrow> True) \<and> (the (cdl_objects s ptr) = Untyped \<longrightarrow> True) \<and> (\<forall>x. the (cdl_objects s ptr) = IRQNode x \<longrightarrow> True) proof (prove)
goal (1 subgoal):
 1. \<And>s y x. \<lbrakk>cdl.lift ((ptr, tcb_pending_op_slot) \<mapsto>c cap \<and>* R) s; Q (cap = RestartCap) s; cdl_objects s ptr = Some y; the (cdl_objects s ptr) = Tcb x\<rbrakk> \<Longrightarrow> Q (cdl_tcb_caps x tcb_pending_op_slot = Some RestartCap) s proof (prove)
goal (1 subgoal):
 1. \<And>s y x. \<lbrakk>Q (cap = RestartCap) s; cdl_objects s ptr = Some y; the (cdl_objects s ptr) = Tcb x; \<exists>cap'. opt_cap (ptr, tcb_pending_op_slot) s = Some cap' \<and> reset_cap_asid cap' = reset_cap_asid cap\<rbrakk> \<Longrightarrow> Q (cdl_tcb_caps x tcb_pending_op_slot = Some RestartCap) s proof (prove)
goal (1 subgoal):
 1. \<And>s x cap'. \<lbrakk>Q (cap = RestartCap) s; cdl_objects s ptr = Some (Tcb x); slots_of ptr s tcb_pending_op_slot = Some cap'; reset_cap_asid cap' = reset_cap_asid cap\<rbrakk> \<Longrightarrow> Q (cdl_tcb_caps x tcb_pending_op_slot = Some RestartCap) s proof (prove)
goal (1 subgoal):
 1. \<And>s x cap'. \<lbrakk>Q (cap = RestartCap) s; cdl_objects s ptr = Some (Tcb x); object_slots (Tcb x) tcb_pending_op_slot = Some cap'; reset_cap_asid cap' = reset_cap_asid cap\<rbrakk> \<Longrightarrow> Q (cdl_tcb_caps x tcb_pending_op_slot = Some RestartCap) s proof (prove)
goal (1 subgoal):
 1. \<And>s x cap'. \<lbrakk>Q (cap = RestartCap) s; cdl_objects s ptr = Some (Tcb x); cdl_tcb_caps x tcb_pending_op_slot = Some cap'; reset_cap_asid cap' = reset_cap_asid cap\<rbrakk> \<Longrightarrow> Q (cap' = RestartCap) s proof (prove)
goal (1 subgoal):
 1. \<And>s x cap'. \<lbrakk>Q (cap = RestartCap) s; cdl_objects s ptr = Some (Tcb x); cdl_tcb_caps x tcb_pending_op_slot = Some cap'; (case cap' of FrameCap dev f1 f2 f3 f4 ad \<Rightarrow> FrameCap dev f1 f2 f3 f4 None | PageTableCap f1 f2 ad \<Rightarrow> PageTableCap f1 f2 None | PageDirectoryCap f1 f2 ad \<Rightarrow> PageDirectoryCap f1 f2 None | _ \<Rightarrow> cap') = (case cap of FrameCap dev f1 f2 f3 f4 ad \<Rightarrow> FrameCap dev f1 f2 f3 f4 None | PageTableCap f1 f2 ad \<Rightarrow> PageTableCap f1 f2 None | PageDirectoryCap f1 f2 ad \<Rightarrow> PageDirectoryCap f1 f2 None | _ \<Rightarrow> cap)\<rbrakk> \<Longrightarrow> Q (cap' = RestartCap) s proof (prove)
goal:
No subgoals!