theory TCB_DP

lemma cancel_ipc_return:
  "\<lbrace>< (tcb, tcb_pending_op_slot) \<mapsto>c NullCap \<and>* (\<lambda>_. True) > and R \<rbrace>cancel_ipc tcb\<lbrace>\<lambda>_. R\<rbrace>" apply (clarsimp simp:cancel_ipc_def) apply wp apply (rule_tac P = "cap = NullCap" in hoare_gen_asm) apply (wp | simp)+ apply clarsimp apply (drule opt_cap_sep_imp) apply (clarsimp simp:reset_cap_asid_simps2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift ((tcb, tcb_pending_op_slot) \<mapsto>c NullCap \<and>* (\<lambda>_. True)) and R\<rbrace> cancel_ipc tcb \<lbrace>\<lambda>_. R\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift ((tcb, tcb_pending_op_slot) \<mapsto>c NullCap \<and>* (\<lambda>_. True)) and R\<rbrace> do cap <- get_cap (tcb, tcb_pending_op_slot);
case cap of PendingSyncSendCap x xa xb xc xd xe \<Rightarrow> do revoke_cap_simple (tcb, tcb_replycap_slot);
set_cap (tcb, tcb_pending_op_slot) NullCap
od | PendingSyncRecvCap x is_reply xa \<Rightarrow> do when is_reply $ update_thread_fault tcb (\<lambda>x. False);
revoke_cap_simple (tcb, tcb_replycap_slot);
when (\<not> is_reply) $ set_cap (tcb, tcb_pending_op_slot) NullCap
od | PendingNtfnRecvCap x \<Rightarrow> do revoke_cap_simple (tcb, tcb_replycap_slot);
set_cap (tcb, tcb_pending_op_slot) NullCap
od | _ \<Rightarrow> return ()
od \<lbrace>\<lambda>_. R\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>cap. \<lbrace>?B1 cap\<rbrace> case cap of PendingSyncSendCap x xa xb xc xd xe \<Rightarrow> do revoke_cap_simple (tcb, tcb_replycap_slot);
set_cap (tcb, tcb_pending_op_slot) NullCap
od | PendingSyncRecvCap x is_reply xa \<Rightarrow> do when is_reply $ update_thread_fault tcb (\<lambda>x. False);
revoke_cap_simple (tcb, tcb_replycap_slot);
when (\<not> is_reply) $ set_cap (tcb, tcb_pending_op_slot) NullCap
od | PendingNtfnRecvCap x \<Rightarrow> do revoke_cap_simple (tcb, tcb_replycap_slot);
set_cap (tcb, tcb_pending_op_slot) NullCap
od | _ \<Rightarrow> return () \<lbrace>\<lambda>_. R\<rbrace>
 2. \<lbrace>?Q\<rbrace> get_cap (tcb, tcb_pending_op_slot) \<lbrace>?B1\<rbrace>
 3. \<And>s. (cdl.lift ((tcb, tcb_pending_op_slot) \<mapsto>c NullCap \<and>* (\<lambda>_. True)) and R) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>cap. cap = NullCap \<Longrightarrow> \<lbrace>?P'2 cap\<rbrace> case cap of PendingSyncSendCap x xa xb xc xd xe \<Rightarrow> do revoke_cap_simple (tcb, tcb_replycap_slot);
set_cap (tcb, tcb_pending_op_slot) NullCap
od | PendingSyncRecvCap x is_reply xa \<Rightarrow> do when is_reply $ update_thread_fault tcb (\<lambda>x. False);
revoke_cap_simple (tcb, tcb_replycap_slot);
when (\<not> is_reply) $ set_cap (tcb, tcb_pending_op_slot) NullCap
od | PendingNtfnRecvCap x \<Rightarrow> do revoke_cap_simple (tcb, tcb_replycap_slot);
set_cap (tcb, tcb_pending_op_slot) NullCap
od | _ \<Rightarrow> return () \<lbrace>\<lambda>_. R\<rbrace>
 2. \<lbrace>?Q\<rbrace> get_cap (tcb, tcb_pending_op_slot) \<lbrace>\<lambda>cap. ?P'2 cap and K (cap = NullCap)\<rbrace>
 3. \<And>s. (cdl.lift ((tcb, tcb_pending_op_slot) \<mapsto>c NullCap \<and>* (\<lambda>_. True)) 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>* (\<lambda>_. True)) s \<and> R s \<Longrightarrow> (\<exists>y. opt_cap (tcb, tcb_pending_op_slot) s = Some y) \<longrightarrow> the (opt_cap (tcb, tcb_pending_op_slot) s) = NullCap proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>cdl.lift ((tcb, tcb_pending_op_slot) \<mapsto>c NullCap \<and>* (\<lambda>_. True)) s; R s; opt_cap (tcb, tcb_pending_op_slot) s = Some y\<rbrakk> \<Longrightarrow> y = NullCap proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>R s; opt_cap (tcb, tcb_pending_op_slot) s = Some y; \<exists>cap'. opt_cap (tcb, tcb_pending_op_slot) s = Some cap' \<and> reset_cap_asid cap' = reset_cap_asid NullCap\<rbrakk> \<Longrightarrow> y = NullCap proof (prove)
goal:
No subgoals!