theory TCB_DP

lemma restart_cdl_current_domain:
  "\<lbrace>\<lambda>s. <(ptr,tcb_pending_op_slot) \<mapsto>c cap \<and>* \<top> > s \<and> \<not> is_pending_cap cap
      \<and> P (cdl_current_domain s)\<rbrace> restart ptr \<lbrace>\<lambda>r s. P (cdl_current_domain s)\<rbrace>" apply (simp add:restart_def) apply wp apply (simp add:cancel_ipc_def) apply (wpsimp wp: hoare_pre_cont[where f="revoke_cap_simple sl" for sl])+ apply (drule opt_cap_sep_imp) apply (clarsimp dest!: reset_cap_asid_pending) apply (auto simp add: is_pending_cap_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cdl.lift ((ptr, tcb_pending_op_slot) \<mapsto>c cap \<and>* (\<lambda>_. True)) s \<and> \<not> is_pending_cap cap \<and> P (cdl_current_domain s)\<rbrace> restart ptr \<lbrace>\<lambda>r s. P (cdl_current_domain s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cdl.lift ((ptr, tcb_pending_op_slot) \<mapsto>c cap \<and>* (\<lambda>_. True)) s \<and> \<not> is_pending_cap cap \<and> P (cdl_current_domain s)\<rbrace> do cap <- get_cap (ptr, tcb_pending_op_slot);
when (cap \<noteq> RestartCap \<and> cap \<noteq> RunningCap) (do y <- cancel_ipc ptr;
y <- set_cap (ptr, tcb_replycap_slot) (MasterReplyCap ptr);
set_cap (ptr, tcb_pending_op_slot) RestartCap
od)
od \<lbrace>\<lambda>r s. P (cdl_current_domain s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>cap. cap \<noteq> RestartCap \<and> cap \<noteq> RunningCap \<Longrightarrow> \<lbrace>?Q2 cap\<rbrace> cancel_ipc ptr \<lbrace>\<lambda>y s. P (cdl_current_domain s)\<rbrace>
 2. \<lbrace>?Q\<rbrace> get_cap (ptr, tcb_pending_op_slot) \<lbrace>\<lambda>cap. if cap \<noteq> RestartCap \<and> cap \<noteq> RunningCap then ?Q2 cap else (\<lambda>s. P (cdl_current_domain s))\<rbrace>
 3. \<And>s. cdl.lift ((ptr, tcb_pending_op_slot) \<mapsto>c cap \<and>* (\<lambda>_. True)) s \<and> \<not> is_pending_cap cap \<and> P (cdl_current_domain s) \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>cap. cap \<noteq> RestartCap \<and> cap \<noteq> RunningCap \<Longrightarrow> \<lbrace>?Q2 cap\<rbrace> do cap <- get_cap (ptr, tcb_pending_op_slot);
case cap of PendingSyncSendCap x xa xb xc xd xe \<Rightarrow> do revoke_cap_simple (ptr, tcb_replycap_slot);
set_cap (ptr, tcb_pending_op_slot) NullCap
od | PendingSyncRecvCap x is_reply xa \<Rightarrow> do when is_reply $ update_thread_fault ptr (\<lambda>x. False);
revoke_cap_simple (ptr, tcb_replycap_slot);
when (\<not> is_reply) $ set_cap (ptr, tcb_pending_op_slot) NullCap
od | PendingNtfnRecvCap x \<Rightarrow> do revoke_cap_simple (ptr, tcb_replycap_slot);
set_cap (ptr, tcb_pending_op_slot) NullCap
od | _ \<Rightarrow> return ()
od \<lbrace>\<lambda>y s. P (cdl_current_domain s)\<rbrace>
 2. \<lbrace>?Q\<rbrace> get_cap (ptr, tcb_pending_op_slot) \<lbrace>\<lambda>cap. if cap \<noteq> RestartCap \<and> cap \<noteq> RunningCap then ?Q2 cap else (\<lambda>s. P (cdl_current_domain s))\<rbrace>
 3. \<And>s. cdl.lift ((ptr, tcb_pending_op_slot) \<mapsto>c cap \<and>* (\<lambda>_. True)) s \<and> \<not> is_pending_cap cap \<and> P (cdl_current_domain s) \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>cdl.lift ((ptr, tcb_pending_op_slot) \<mapsto>c cap \<and>* (\<lambda>_. True)) s; \<not> is_pending_cap cap; P (cdl_current_domain s); y \<noteq> RestartCap; y \<noteq> RunningCap; opt_cap (ptr, tcb_pending_op_slot) s = Some y\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd xe. y \<noteq> PendingSyncSendCap x xa xb xc xd xe) \<and> (\<forall>x xa xb. y \<noteq> PendingSyncRecvCap x xa xb) \<and> (\<forall>x. y \<noteq> PendingNtfnRecvCap x) proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>\<not> is_pending_cap cap; P (cdl_current_domain s); y \<noteq> RestartCap; y \<noteq> RunningCap; opt_cap (ptr, tcb_pending_op_slot) s = Some y; \<exists>cap'. opt_cap (ptr, tcb_pending_op_slot) s = Some cap' \<and> reset_cap_asid cap' = reset_cap_asid cap\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd xe. y \<noteq> PendingSyncSendCap x xa xb xc xd xe) \<and> (\<forall>x xa xb. y \<noteq> PendingSyncRecvCap x xa xb) \<and> (\<forall>x. y \<noteq> PendingNtfnRecvCap x) proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>P (cdl_current_domain s); y \<noteq> RestartCap; y \<noteq> RunningCap; opt_cap (ptr, tcb_pending_op_slot) s = Some y; \<not> is_pending_cap y; \<not> is_pending_cap cap\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd xe. y \<noteq> PendingSyncSendCap x xa xb xc xd xe) \<and> (\<forall>x xa xb. y \<noteq> PendingSyncRecvCap x xa xb) \<and> (\<forall>x. y \<noteq> PendingNtfnRecvCap x) proof (prove)
goal:
No subgoals!