theory TCB_DP

lemma restart_wp:
  "cap = RunningCap \<or> cap = RestartCap \<Longrightarrow>
  \<lbrace> <  (tcb,tcb_pending_op_slot) \<mapsto>c cap  \<and>*  R > \<rbrace>
     restart tcb
  \<lbrace>\<lambda>_.  < (tcb,tcb_pending_op_slot) \<mapsto>c cap  \<and>*  R > \<rbrace>" apply (clarsimp simp: restart_def) apply wp apply (wp set_cap_wp[sep_wand_wp])+ apply (clarsimp) apply (rule hoare_pre_cont) apply wp apply (clarsimp) apply (sep_select_asm 2) apply (sep_drule (direct) opt_cap_sep_imp) apply (clarsimp) apply (erule disjE) apply (clarsimp simp: reset_cap_asid_def split:cdl_cap.split_asm)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap = RunningCap \<or> cap = RestartCap \<Longrightarrow> \<lbrace>cdl.lift ((tcb, tcb_pending_op_slot) \<mapsto>c cap \<and>* R)\<rbrace> restart tcb \<lbrace>\<lambda>_. cdl.lift ((tcb, tcb_pending_op_slot) \<mapsto>c cap \<and>* R)\<rbrace> proof (prove)
goal (1 subgoal):
 1. cap = RunningCap \<or> cap = RestartCap \<Longrightarrow> \<lbrace>cdl.lift ((tcb, tcb_pending_op_slot) \<mapsto>c cap \<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 cap \<and>* R)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>capa y ya. \<lbrakk>cap = RunningCap \<or> cap = RestartCap; capa \<noteq> RestartCap \<and> capa \<noteq> RunningCap\<rbrakk> \<Longrightarrow> \<lbrace>?B4 capa y ya\<rbrace> set_cap (tcb, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>_. cdl.lift ((tcb, tcb_pending_op_slot) \<mapsto>c cap \<and>* R)\<rbrace>
 2. \<And>capa y. \<lbrakk>cap = RunningCap \<or> cap = RestartCap; capa \<noteq> RestartCap \<and> capa \<noteq> RunningCap\<rbrakk> \<Longrightarrow> \<lbrace>?B3 capa y\<rbrace> set_cap (tcb, tcb_replycap_slot) (MasterReplyCap tcb) \<lbrace>?B4 capa y\<rbrace>
 3. \<And>capa. \<lbrakk>cap = RunningCap \<or> cap = RestartCap; capa \<noteq> RestartCap \<and> capa \<noteq> RunningCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q2 capa\<rbrace> cancel_ipc tcb \<lbrace>?B3 capa\<rbrace>
 4. cap = RunningCap \<or> cap = RestartCap \<Longrightarrow> \<lbrace>?Q\<rbrace> get_cap (tcb, tcb_pending_op_slot) \<lbrace>\<lambda>capa. if capa \<noteq> RestartCap \<and> capa \<noteq> RunningCap then ?Q2 capa else cdl.lift ((tcb, tcb_pending_op_slot) \<mapsto>c cap \<and>* R)\<rbrace>
 5. \<And>s. \<lbrakk>cap = RunningCap \<or> cap = RestartCap; cdl.lift ((tcb, tcb_pending_op_slot) \<mapsto>c cap \<and>* R) s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>capa. \<lbrakk>cap = RunningCap \<or> cap = RestartCap; capa \<noteq> RestartCap \<and> capa \<noteq> RunningCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q2 capa\<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 cap \<and>* R)))\<rbrace>
 2. cap = RunningCap \<or> cap = RestartCap \<Longrightarrow> \<lbrace>?Q\<rbrace> get_cap (tcb, tcb_pending_op_slot) \<lbrace>\<lambda>capa. if capa \<noteq> RestartCap \<and> capa \<noteq> RunningCap then ?Q2 capa else cdl.lift ((tcb, tcb_pending_op_slot) \<mapsto>c cap \<and>* R)\<rbrace>
 3. \<And>s. \<lbrakk>cap = RunningCap \<or> cap = RestartCap; cdl.lift ((tcb, tcb_pending_op_slot) \<mapsto>c cap \<and>* R) s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>capa. \<lbrakk>cap = RunningCap \<or> cap = RestartCap; capa \<noteq> RestartCap; capa \<noteq> RunningCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q2 capa\<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 cap \<and>* R)))\<rbrace>
 2. cap = RunningCap \<or> cap = RestartCap \<Longrightarrow> \<lbrace>?Q\<rbrace> get_cap (tcb, tcb_pending_op_slot) \<lbrace>\<lambda>capa. if capa \<noteq> RestartCap \<and> capa \<noteq> RunningCap then ?Q2 capa else cdl.lift ((tcb, tcb_pending_op_slot) \<mapsto>c cap \<and>* R)\<rbrace>
 3. \<And>s. \<lbrakk>cap = RunningCap \<or> cap = RestartCap; cdl.lift ((tcb, tcb_pending_op_slot) \<mapsto>c cap \<and>* R) s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. cap = RunningCap \<or> cap = RestartCap \<Longrightarrow> \<lbrace>?Q\<rbrace> get_cap (tcb, tcb_pending_op_slot) \<lbrace>\<lambda>capa. if capa \<noteq> RestartCap \<and> capa \<noteq> RunningCap then \<lambda>_. False else cdl.lift ((tcb, tcb_pending_op_slot) \<mapsto>c cap \<and>* R)\<rbrace>
 2. \<And>s. \<lbrakk>cap = RunningCap \<or> cap = RestartCap; cdl.lift ((tcb, tcb_pending_op_slot) \<mapsto>c cap \<and>* R) s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cap = RunningCap \<or> cap = RestartCap; cdl.lift ((tcb, tcb_pending_op_slot) \<mapsto>c cap \<and>* R) s\<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 \<lambda>_. False else cdl.lift ((tcb, tcb_pending_op_slot) \<mapsto>c cap \<and>* R)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cap = RunningCap \<or> cap = RestartCap; cdl.lift ((tcb, tcb_pending_op_slot) \<mapsto>c cap \<and>* R) s; the (opt_cap (tcb, tcb_pending_op_slot) s) \<noteq> RestartCap; the (opt_cap (tcb, tcb_pending_op_slot) s) \<noteq> RunningCap\<rbrakk> \<Longrightarrow> opt_cap (tcb, tcb_pending_op_slot) s = None proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cap = RunningCap \<or> cap = RestartCap; the (opt_cap (tcb, tcb_pending_op_slot) s) \<noteq> RestartCap; the (opt_cap (tcb, tcb_pending_op_slot) s) \<noteq> RunningCap; cdl.lift (R \<and>* (tcb, tcb_pending_op_slot) \<mapsto>c cap) s\<rbrakk> \<Longrightarrow> opt_cap (tcb, tcb_pending_op_slot) s = None proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cap = RunningCap \<or> cap = RestartCap; the (opt_cap (tcb, tcb_pending_op_slot) s) \<noteq> RestartCap; the (opt_cap (tcb, tcb_pending_op_slot) s) \<noteq> RunningCap; \<exists>cap'. opt_cap (tcb, tcb_pending_op_slot) s = Some cap' \<and> reset_cap_asid cap' = reset_cap_asid cap\<rbrakk> \<Longrightarrow> opt_cap (tcb, tcb_pending_op_slot) s = None proof (prove)
goal (1 subgoal):
 1. \<And>s cap'. \<lbrakk>cap = RunningCap \<or> cap = RestartCap; cap' \<noteq> RestartCap; cap' \<noteq> RunningCap; opt_cap (tcb, tcb_pending_op_slot) s = Some cap'; reset_cap_asid cap' = reset_cap_asid cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s cap'. \<lbrakk>cap' \<noteq> RestartCap; cap' \<noteq> RunningCap; opt_cap (tcb, tcb_pending_op_slot) s = Some cap'; reset_cap_asid cap' = reset_cap_asid cap; cap = RunningCap\<rbrakk> \<Longrightarrow> False
 2. \<And>s cap'. \<lbrakk>cap' \<noteq> RestartCap; cap' \<noteq> RunningCap; opt_cap (tcb, tcb_pending_op_slot) s = Some cap'; reset_cap_asid cap' = reset_cap_asid cap; cap = RestartCap\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!