theory TCB_DP

lemma restart_null_wp:
  "\<lbrace> <  (tcb,tcb_pending_op_slot) \<mapsto>c NullCap
     \<and>*  (tcb, tcb_replycap_slot) \<mapsto>c-
     \<and>*  R > \<rbrace>
     restart tcb
  \<lbrace>\<lambda>_.  < (tcb,tcb_pending_op_slot) \<mapsto>c RestartCap
     \<and>* (tcb, tcb_replycap_slot) \<mapsto>c (MasterReplyCap tcb) \<and>* R > \<rbrace>" apply (clarsimp simp:restart_def) apply (wp set_cap_wp[sep_wand_wp]) apply (rule hoare_post_imp[OF _ cancel_ipc_return]) apply (assumption) apply (wp get_cap_wp) apply (frule opt_cap_sep_imp) apply (clarsimp dest!:reset_cap_asid_simps2) apply (rule conjI) apply sep_solve apply sep_solve done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift ((tcb, tcb_pending_op_slot) \<mapsto>c NullCap \<and>* (tcb, tcb_replycap_slot) \<mapsto>c - \<and>* R)\<rbrace> restart tcb \<lbrace>\<lambda>_. cdl.lift ((tcb, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (tcb, tcb_replycap_slot) \<mapsto>c MasterReplyCap tcb \<and>* R)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift ((tcb, tcb_pending_op_slot) \<mapsto>c NullCap \<and>* (tcb, tcb_replycap_slot) \<mapsto>c - \<and>* R)\<rbrace> do cap <- get_cap (tcb, tcb_pending_op_slot);
when (cap \<noteq> RestartCap \<and> cap \<noteq> RunningCap) (do y <- cancel_ipc tcb;
y <- set_cap (tcb, tcb_replycap_slot) (MasterReplyCap tcb);
set_cap (tcb, tcb_pending_op_slot) RestartCap
od)
od \<lbrace>\<lambda>_. cdl.lift ((tcb, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (tcb, tcb_replycap_slot) \<mapsto>c MasterReplyCap tcb \<and>* R)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>cap. cap \<noteq> RestartCap \<and> cap \<noteq> RunningCap \<Longrightarrow> \<lbrace>?Q2 cap\<rbrace> cancel_ipc tcb \<lbrace>\<lambda>y. cdl.lift ((tcb, tcb_replycap_slot) \<mapsto>c - \<and>* ((tcb, tcb_replycap_slot) \<mapsto>c MasterReplyCap tcb \<longrightarrow>* (tcb, tcb_pending_op_slot) \<mapsto>c - \<and>* ((tcb, tcb_pending_op_slot) \<mapsto>c RestartCap \<longrightarrow>* (tcb, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (tcb, tcb_replycap_slot) \<mapsto>c MasterReplyCap tcb \<and>* R)))\<rbrace>
 2. \<lbrace>?Q\<rbrace> get_cap (tcb, tcb_pending_op_slot) \<lbrace>\<lambda>cap. if cap \<noteq> RestartCap \<and> cap \<noteq> RunningCap then ?Q2 cap else cdl.lift ((tcb, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (tcb, tcb_replycap_slot) \<mapsto>c MasterReplyCap tcb \<and>* R)\<rbrace>
 3. \<And>s. cdl.lift ((tcb, tcb_pending_op_slot) \<mapsto>c NullCap \<and>* (tcb, tcb_replycap_slot) \<mapsto>c - \<and>* R) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>cap rv s. \<lbrakk>cap \<noteq> RestartCap \<and> cap \<noteq> RunningCap; ?Q9 cap s\<rbrakk> \<Longrightarrow> cdl.lift ((tcb, tcb_replycap_slot) \<mapsto>c - \<and>* ((tcb, tcb_replycap_slot) \<mapsto>c MasterReplyCap tcb \<longrightarrow>* (tcb, tcb_pending_op_slot) \<mapsto>c - \<and>* ((tcb, tcb_pending_op_slot) \<mapsto>c RestartCap \<longrightarrow>* (tcb, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (tcb, tcb_replycap_slot) \<mapsto>c MasterReplyCap tcb \<and>* R))) s
 2. \<lbrace>?Q\<rbrace> get_cap (tcb, tcb_pending_op_slot) \<lbrace>\<lambda>cap. if cap \<noteq> RestartCap \<and> cap \<noteq> RunningCap then cdl.lift ((tcb, tcb_pending_op_slot) \<mapsto>c NullCap \<and>* (\<lambda>_. True)) and ?Q9 cap else cdl.lift ((tcb, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (tcb, tcb_replycap_slot) \<mapsto>c MasterReplyCap tcb \<and>* R)\<rbrace>
 3. \<And>s. cdl.lift ((tcb, tcb_pending_op_slot) \<mapsto>c NullCap \<and>* (tcb, tcb_replycap_slot) \<mapsto>c - \<and>* R) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> get_cap (tcb, tcb_pending_op_slot) \<lbrace>\<lambda>cap. if cap \<noteq> RestartCap \<and> cap \<noteq> RunningCap then cdl.lift ((tcb, tcb_pending_op_slot) \<mapsto>c NullCap \<and>* (\<lambda>_. True)) and cdl.lift ((tcb, tcb_replycap_slot) \<mapsto>c - \<and>* ((tcb, tcb_replycap_slot) \<mapsto>c MasterReplyCap tcb \<longrightarrow>* (tcb, tcb_pending_op_slot) \<mapsto>c - \<and>* ((tcb, tcb_pending_op_slot) \<mapsto>c RestartCap \<longrightarrow>* (tcb, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (tcb, tcb_replycap_slot) \<mapsto>c MasterReplyCap tcb \<and>* R))) else cdl.lift ((tcb, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (tcb, tcb_replycap_slot) \<mapsto>c MasterReplyCap tcb \<and>* R)\<rbrace>
 2. \<And>s. cdl.lift ((tcb, tcb_pending_op_slot) \<mapsto>c NullCap \<and>* (tcb, tcb_replycap_slot) \<mapsto>c - \<and>* R) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. cdl.lift ((tcb, tcb_pending_op_slot) \<mapsto>c NullCap \<and>* (tcb, tcb_replycap_slot) \<mapsto>c - \<and>* R) s \<Longrightarrow> opt_cap (tcb, tcb_pending_op_slot) s \<noteq> None \<longrightarrow> (if the (opt_cap (tcb, tcb_pending_op_slot) s) \<noteq> RestartCap \<and> the (opt_cap (tcb, tcb_pending_op_slot) s) \<noteq> RunningCap then cdl.lift ((tcb, tcb_pending_op_slot) \<mapsto>c NullCap \<and>* (\<lambda>_. True)) and cdl.lift ((tcb, tcb_replycap_slot) \<mapsto>c - \<and>* ((tcb, tcb_replycap_slot) \<mapsto>c MasterReplyCap tcb \<longrightarrow>* (tcb, tcb_pending_op_slot) \<mapsto>c - \<and>* ((tcb, tcb_pending_op_slot) \<mapsto>c RestartCap \<longrightarrow>* (tcb, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (tcb, tcb_replycap_slot) \<mapsto>c MasterReplyCap tcb \<and>* R))) else cdl.lift ((tcb, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (tcb, tcb_replycap_slot) \<mapsto>c MasterReplyCap tcb \<and>* R)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cdl.lift ((tcb, tcb_pending_op_slot) \<mapsto>c NullCap \<and>* (tcb, tcb_replycap_slot) \<mapsto>c - \<and>* R) s; \<exists>cap'. opt_cap (tcb, tcb_pending_op_slot) s = Some cap' \<and> reset_cap_asid cap' = reset_cap_asid NullCap\<rbrakk> \<Longrightarrow> opt_cap (tcb, tcb_pending_op_slot) s \<noteq> None \<longrightarrow> (if the (opt_cap (tcb, tcb_pending_op_slot) s) \<noteq> RestartCap \<and> the (opt_cap (tcb, tcb_pending_op_slot) s) \<noteq> RunningCap then cdl.lift ((tcb, tcb_pending_op_slot) \<mapsto>c NullCap \<and>* (\<lambda>_. True)) and cdl.lift ((tcb, tcb_replycap_slot) \<mapsto>c - \<and>* ((tcb, tcb_replycap_slot) \<mapsto>c MasterReplyCap tcb \<longrightarrow>* (tcb, tcb_pending_op_slot) \<mapsto>c - \<and>* ((tcb, tcb_pending_op_slot) \<mapsto>c RestartCap \<longrightarrow>* (tcb, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (tcb, tcb_replycap_slot) \<mapsto>c MasterReplyCap tcb \<and>* R))) else cdl.lift ((tcb, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (tcb, tcb_replycap_slot) \<mapsto>c MasterReplyCap tcb \<and>* R)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cdl.lift ((tcb, tcb_pending_op_slot) \<mapsto>c NullCap \<and>* (tcb, tcb_replycap_slot) \<mapsto>c - \<and>* R) s; opt_cap (tcb, tcb_pending_op_slot) s = Some NullCap\<rbrakk> \<Longrightarrow> cdl.lift ((tcb, tcb_pending_op_slot) \<mapsto>c NullCap \<and>* (\<lambda>_. True)) s \<and> cdl.lift ((tcb, tcb_replycap_slot) \<mapsto>c - \<and>* ((tcb, tcb_replycap_slot) \<mapsto>c MasterReplyCap tcb \<longrightarrow>* (tcb, tcb_pending_op_slot) \<mapsto>c - \<and>* ((tcb, tcb_pending_op_slot) \<mapsto>c RestartCap \<longrightarrow>* (tcb, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (tcb, tcb_replycap_slot) \<mapsto>c MasterReplyCap tcb \<and>* R))) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>cdl.lift ((tcb, tcb_pending_op_slot) \<mapsto>c NullCap \<and>* (tcb, tcb_replycap_slot) \<mapsto>c - \<and>* R) s; opt_cap (tcb, tcb_pending_op_slot) s = Some NullCap\<rbrakk> \<Longrightarrow> cdl.lift ((tcb, tcb_pending_op_slot) \<mapsto>c NullCap \<and>* (\<lambda>_. True)) s
 2. \<And>s. \<lbrakk>cdl.lift ((tcb, tcb_pending_op_slot) \<mapsto>c NullCap \<and>* (tcb, tcb_replycap_slot) \<mapsto>c - \<and>* R) s; opt_cap (tcb, tcb_pending_op_slot) s = Some NullCap\<rbrakk> \<Longrightarrow> cdl.lift ((tcb, tcb_replycap_slot) \<mapsto>c - \<and>* ((tcb, tcb_replycap_slot) \<mapsto>c MasterReplyCap tcb \<longrightarrow>* (tcb, tcb_pending_op_slot) \<mapsto>c - \<and>* ((tcb, tcb_pending_op_slot) \<mapsto>c RestartCap \<longrightarrow>* (tcb, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (tcb, tcb_replycap_slot) \<mapsto>c MasterReplyCap tcb \<and>* R))) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cdl.lift ((tcb, tcb_pending_op_slot) \<mapsto>c NullCap \<and>* (tcb, tcb_replycap_slot) \<mapsto>c - \<and>* R) s; opt_cap (tcb, tcb_pending_op_slot) s = Some NullCap\<rbrakk> \<Longrightarrow> cdl.lift ((tcb, tcb_replycap_slot) \<mapsto>c - \<and>* ((tcb, tcb_replycap_slot) \<mapsto>c MasterReplyCap tcb \<longrightarrow>* (tcb, tcb_pending_op_slot) \<mapsto>c - \<and>* ((tcb, tcb_pending_op_slot) \<mapsto>c RestartCap \<longrightarrow>* (tcb, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (tcb, tcb_replycap_slot) \<mapsto>c MasterReplyCap tcb \<and>* R))) s proof (prove)
goal:
No subgoals!