theory IpcCancel_AI

lemma (in delete_one_abs) cancel_ipc_no_reply_cap[wp]:
  shows "\<lbrace>invs and tcb_at t\<rbrace> (cancel_ipc t :: (unit,'a) s_monad) \<lbrace>\<lambda>rv s. \<not> has_reply_cap t s\<rbrace>" apply (simp add: cancel_ipc_def) apply (wpsimp wp: hoare_post_imp [OF invs_valid_reply_caps]
                  reply_cancel_ipc_no_reply_cap
                  cancel_signal_invs cancel_signal_st_tcb_at_general
                  blocked_cancel_ipc_invs blocked_ipc_st_tcb_at_general
        | strengthen reply_cap_doesnt_exist_strg)+ apply (rule_tac Q="\<lambda>rv. st_tcb_at ((=) rv) t and invs" in hoare_strengthen_post) apply (wpsimp wp: gts_st_tcb) apply (fastforce simp: invs_def valid_state_def st_tcb_at_tcb_at
                   elim!: pred_tcb_weakenE)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and tcb_at t\<rbrace> cancel_ipc t \<lbrace>\<lambda>rv s. \<not> has_reply_cap t s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and tcb_at t\<rbrace> do state <- get_thread_state t;
case state of BlockedOnReceive x y \<Rightarrow> blocked_cancel_ipc state t | BlockedOnSend x y \<Rightarrow> blocked_cancel_ipc state t | BlockedOnReply \<Rightarrow> reply_cancel_ipc t | BlockedOnNotification event \<Rightarrow> cancel_signal t event | _ \<Rightarrow> return ()
od \<lbrace>\<lambda>rv s. \<not> has_reply_cap t s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q1\<rbrace> get_thread_state t \<lbrace>\<lambda>r s. (r = Running \<longrightarrow> valid_reply_caps s \<and> st_tcb_at (Not \<circ> awaiting_reply) t s) \<and> (inactive r \<longrightarrow> valid_reply_caps s \<and> st_tcb_at (Not \<circ> awaiting_reply) t s) \<and> (r = Restart \<longrightarrow> valid_reply_caps s \<and> st_tcb_at (Not \<circ> awaiting_reply) t s) \<and> (\<forall>x xa. r = BlockedOnReceive x xa \<longrightarrow> invs s \<and> st_tcb_at ((=) (BlockedOnReceive x xa)) t s \<and> st_tcb_at (\<lambda>a. a \<noteq> BlockedOnReply) t s) \<and> (\<forall>x xa. r = BlockedOnSend x xa \<longrightarrow> invs s \<and> st_tcb_at ((=) (BlockedOnSend x xa)) t s \<and> st_tcb_at (\<lambda>a. a \<noteq> BlockedOnReply) t s) \<and> (awaiting_reply r \<longrightarrow> invs s \<and> tcb_at t s) \<and> (\<forall>x. r = BlockedOnNotification x \<longrightarrow> invs s \<and> st_tcb_at ((=) (BlockedOnNotification x)) t s \<and> st_tcb_at (\<lambda>a. a \<noteq> BlockedOnReply) t s) \<and> (idle r \<longrightarrow> valid_reply_caps s \<and> st_tcb_at (Not \<circ> awaiting_reply) t s)\<rbrace>
 2. \<And>s. (invs and tcb_at t) s \<Longrightarrow> ?Q1 s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?Q1\<rbrace> get_thread_state t \<lbrace>\<lambda>rv. st_tcb_at ((=) rv) t and invs\<rbrace>
 2. \<And>rv s. (st_tcb_at ((=) rv) t and invs) s \<Longrightarrow> (rv = Running \<longrightarrow> valid_reply_caps s \<and> st_tcb_at (Not \<circ> awaiting_reply) t s) \<and> (inactive rv \<longrightarrow> valid_reply_caps s \<and> st_tcb_at (Not \<circ> awaiting_reply) t s) \<and> (rv = Restart \<longrightarrow> valid_reply_caps s \<and> st_tcb_at (Not \<circ> awaiting_reply) t s) \<and> (\<forall>x xa. rv = BlockedOnReceive x xa \<longrightarrow> invs s \<and> st_tcb_at ((=) (BlockedOnReceive x xa)) t s \<and> st_tcb_at (\<lambda>a. a \<noteq> BlockedOnReply) t s) \<and> (\<forall>x xa. rv = BlockedOnSend x xa \<longrightarrow> invs s \<and> st_tcb_at ((=) (BlockedOnSend x xa)) t s \<and> st_tcb_at (\<lambda>a. a \<noteq> BlockedOnReply) t s) \<and> (awaiting_reply rv \<longrightarrow> invs s \<and> tcb_at t s) \<and> (\<forall>x. rv = BlockedOnNotification x \<longrightarrow> invs s \<and> st_tcb_at ((=) (BlockedOnNotification x)) t s \<and> st_tcb_at (\<lambda>a. a \<noteq> BlockedOnReply) t s) \<and> (idle rv \<longrightarrow> valid_reply_caps s \<and> st_tcb_at (Not \<circ> awaiting_reply) t s)
 3. \<And>s. (invs and tcb_at t) s \<Longrightarrow> ?Q1 s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. (st_tcb_at ((=) rv) t and invs) s \<Longrightarrow> (rv = Running \<longrightarrow> valid_reply_caps s \<and> st_tcb_at (Not \<circ> awaiting_reply) t s) \<and> (inactive rv \<longrightarrow> valid_reply_caps s \<and> st_tcb_at (Not \<circ> awaiting_reply) t s) \<and> (rv = Restart \<longrightarrow> valid_reply_caps s \<and> st_tcb_at (Not \<circ> awaiting_reply) t s) \<and> (\<forall>x xa. rv = BlockedOnReceive x xa \<longrightarrow> invs s \<and> st_tcb_at ((=) (BlockedOnReceive x xa)) t s \<and> st_tcb_at (\<lambda>a. a \<noteq> BlockedOnReply) t s) \<and> (\<forall>x xa. rv = BlockedOnSend x xa \<longrightarrow> invs s \<and> st_tcb_at ((=) (BlockedOnSend x xa)) t s \<and> st_tcb_at (\<lambda>a. a \<noteq> BlockedOnReply) t s) \<and> (awaiting_reply rv \<longrightarrow> invs s \<and> tcb_at t s) \<and> (\<forall>x. rv = BlockedOnNotification x \<longrightarrow> invs s \<and> st_tcb_at ((=) (BlockedOnNotification x)) t s \<and> st_tcb_at (\<lambda>a. a \<noteq> BlockedOnReply) t s) \<and> (idle rv \<longrightarrow> valid_reply_caps s \<and> st_tcb_at (Not \<circ> awaiting_reply) t s)
 2. \<And>s. (invs and tcb_at t) s \<Longrightarrow> True \<and> invs s proof (prove)
goal:
No subgoals!