kings-crown/FVELER_Isabelle huggingface dataset:
theory IpcCancel_AI

lemma reply_mdb_cte_at_master_None:
  "\<lbrakk> reply_mdb m cs; mdb_cte_at (\<lambda>p. \<exists>c. cs p = Some c \<and> cap.NullCap \<noteq> c) m;
     cs ptr = Some cap; is_master_reply_cap cap \<rbrakk> \<Longrightarrow>
    m ptr = None" unfolding reply_mdb_def reply_masters_mdb_def by (fastforce simp: is_cap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reply_mdb m cs; mdb_cte_at (\<lambda>p. \<exists>c. cs p = Some c \<and> NullCap \<noteq> c) m; cs ptr = Some cap; is_master_reply_cap cap\<rbrakk> \<Longrightarrow> m ptr = None proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reply_caps_mdb m cs \<and> (\<forall>ptr t rights. cs ptr = Some (ReplyCap t True rights) \<longrightarrow> m ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))); mdb_cte_at (\<lambda>p. \<exists>c. cs p = Some c \<and> NullCap \<noteq> c) m; cs ptr = Some cap; is_master_reply_cap cap\<rbrakk> \<Longrightarrow> m ptr = None
theory IpcCancel_AI

lemma reply_slot_not_descendant:
  "\<And>ptr. \<lbrakk> invs s; tcb_at t s \<rbrakk> \<Longrightarrow>
   (t, tcb_cnode_index 2) \<notin> descendants_of ptr (cdt s)" apply (subgoal_tac "cte_wp_at (\<lambda>c. is_master_reply_cap c \<or> c = cap.NullCap)
                                (t, tcb_cnode_index 2) s") apply (fastforce simp: invs_def valid_state_def valid_mdb_def2
                         cte_wp_at_caps_of_state
                   dest: reply_mdb_cte_at_master_None mdb_cte_at_Null_None
                         descendants_of_NoneD) apply (clarsimp simp: tcb_cap_wp_at invs_valid_objs
                        tcb_cap_cases_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>ptr. \<lbrakk>invs s; tcb_at t s\<rbrakk> \<Longrightarrow> (t, tcb_cnode_index 2) \<notin> descendants_of ptr (cdt s) proof (prove)
goal (2 subgoals):
 1. \<And>ptr. \<lbrakk>invs s; tcb_at t s; cte_wp_at (\<lambda>c. is_master_reply_cap c \<or> c = NullCap) (t, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> (t, tcb_cnode_index 2) \<notin> descendants_of ptr (cdt s)
 2. \<And>ptr. \<lbrakk>invs s; tcb_at t s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. is_master_reply_cap c \<or> c = NullCap) (t, tcb_cnode_index 2) s proof (prove)
goal (1 subgoal):
 1. \<And>ptr. \<lbrakk>invs s; tcb_at t s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. is_master_reply_cap c \<or> c = NullCap) (t, tcb_cnode_index 2) s proof (prove)
goal:
No subgoals!
theory IpcCancel_AI

lemma (in delete_one_abs) cancel_ipc_invs[wp]:
  "\<lbrace>invs\<rbrace> (cancel_ipc t :: (unit,'a) s_monad) \<lbrace>\<lambda>rv. invs\<rbrace>" apply (simp add: cancel_ipc_def) apply (rule hoare_seq_ext [OF _ gts_sp]) apply (case_tac state, simp_all) apply (auto intro!: hoare_weaken_pre [OF return_wp]
                            hoare_weaken_pre [OF blocked_cancel_ipc_invs]
                            hoare_weaken_pre [OF cancel_signal_invs]
                            hoare_weaken_pre [OF reply_cancel_ipc_invs]
                            delete_one_invs
                     elim!: pred_tcb_weakenE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> cancel_ipc t \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<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. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>state. \<lbrace>st_tcb_at ((=) state) t and invs\<rbrace> 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 () \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<lbrace>st_tcb_at ((=) Running) t and invs\<rbrace> return () \<lbrace>\<lambda>rv. invs\<rbrace>
 2. \<lbrace>st_tcb_at ((=) Inactive) t and invs\<rbrace> return () \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<lbrace>st_tcb_at ((=) Restart) t and invs\<rbrace> return () \<lbrace>\<lambda>rv. invs\<rbrace>
 4. \<And>state x41 x42. state = BlockedOnReceive x41 x42 \<Longrightarrow> \<lbrace>st_tcb_at ((=) (BlockedOnReceive x41 x42)) t and invs\<rbrace> blocked_cancel_ipc (BlockedOnReceive x41 x42) t \<lbrace>\<lambda>rv. invs\<rbrace>
 5. \<And>state x51 x52. state = BlockedOnSend x51 x52 \<Longrightarrow> \<lbrace>st_tcb_at ((=) (BlockedOnSend x51 x52)) t and invs\<rbrace> blocked_cancel_ipc (BlockedOnSend x51 x52) t \<lbrace>\<lambda>rv. invs\<rbrace>
 6. \<lbrace>st_tcb_at ((=) BlockedOnReply) t and invs\<rbrace> reply_cancel_ipc t \<lbrace>\<lambda>rv. invs\<rbrace>
 7. \<And>state x7. state = BlockedOnNotification x7 \<Longrightarrow> \<lbrace>st_tcb_at ((=) (BlockedOnNotification x7)) t and invs\<rbrace> cancel_signal t x7 \<lbrace>\<lambda>rv. invs\<rbrace>
 8. \<lbrace>st_tcb_at ((=) IdleThreadState) t and invs\<rbrace> return () \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal:
No subgoals!
theory IpcCancel_AI

lemma cancel_ipc_valid_cap:
  "\<lbrace>valid_cap c\<rbrace> cancel_ipc p \<lbrace>\<lambda>_. (valid_cap c) :: 'a state \<Rightarrow> bool\<rbrace>" by (wp valid_cap_typ)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_cap c\<rbrace> cancel_ipc p \<lbrace>\<lambda>_. valid_cap c\<rbrace>
theory IpcCancel_AI

lemma cancel_ipc_cte_at[wp]:
  "\<lbrace>cte_at p\<rbrace> cancel_ipc t \<lbrace>\<lambda>_. (cte_at p) :: 'a state \<Rightarrow> bool\<rbrace>" by (wp valid_cte_at_typ)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at (\<lambda>_. True) p\<rbrace> cancel_ipc t \<lbrace>\<lambda>_. cte_wp_at (\<lambda>_. True) p\<rbrace>
theory IpcCancel_AI

lemma valid_ep_queue_subset:
  "\<lbrace>\<lambda>s. valid_ep ep s\<rbrace>
     get_ep_queue ep
   \<lbrace>\<lambda>queue s. valid_ep (case (remove1 t queue) of [] \<Rightarrow> Structures_A.endpoint.IdleEP
                       | a # list \<Rightarrow> update_ep_queue ep (remove1 t queue)) s\<rbrace>" apply (simp add: get_ep_queue_def) apply (case_tac ep, simp_all) apply wp apply (clarsimp simp: ep_redux_simps2 valid_ep_def) apply wp apply (clarsimp simp: ep_redux_simps2 valid_ep_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_ep ep\<rbrace> get_ep_queue ep \<lbrace>\<lambda>queue. valid_ep (case remove1 t queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep (remove1 t queue))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_ep ep\<rbrace> case ep of IdleEP \<Rightarrow> fail | SendEP q \<Rightarrow> return q | RecvEP q \<Rightarrow> return q \<lbrace>\<lambda>queue. valid_ep (case remove1 t queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep (remove1 t queue))\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x2. ep = SendEP x2 \<Longrightarrow> \<lbrace>valid_ep (SendEP x2)\<rbrace> return x2 \<lbrace>\<lambda>queue. valid_ep (case remove1 t queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep (remove1 t queue))\<rbrace>
 2. \<And>x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>valid_ep (RecvEP x3)\<rbrace> return x3 \<lbrace>\<lambda>queue. valid_ep (case remove1 t queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep (remove1 t queue))\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x2 s. \<lbrakk>ep = SendEP x2; valid_ep (SendEP x2) s\<rbrakk> \<Longrightarrow> valid_ep (case remove1 t x2 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep (remove1 t x2)) s
 2. \<And>x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>valid_ep (RecvEP x3)\<rbrace> return x3 \<lbrace>\<lambda>queue. valid_ep (case remove1 t queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep (remove1 t queue))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>valid_ep (RecvEP x3)\<rbrace> return x3 \<lbrace>\<lambda>queue. valid_ep (case remove1 t queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep (remove1 t queue))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x3 s. \<lbrakk>ep = RecvEP x3; valid_ep (RecvEP x3) s\<rbrakk> \<Longrightarrow> valid_ep (case remove1 t x3 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep (remove1 t x3)) s proof (prove)
goal:
No subgoals!
theory IpcCancel_AI

lemma blocked_cancel_ipc_valid_objs[wp]:
  "\<lbrace>valid_objs\<rbrace> blocked_cancel_ipc st t \<lbrace>\<lambda>_. valid_objs\<rbrace>" apply (simp add: blocked_cancel_ipc_def) apply (wp get_simple_ko_valid[where f=Endpoint, simplified valid_ep_def2[symmetric]]
            valid_ep_queue_subset
         | simp only: valid_inactive simp_thms
                cong: imp_cong
         | rule hoare_drop_imps
         | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> blocked_cancel_ipc st t \<lbrace>\<lambda>_. valid_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> do epptr <- get_blocking_object st;
ep <- get_endpoint epptr;
queue <- get_ep_queue ep;
y <- set_endpoint epptr (case remove1 t queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep (remove1 t queue));
set_thread_state t Inactive
od \<lbrace>\<lambda>_. valid_objs\<rbrace> proof (prove)
goal:
No subgoals!
theory IpcCancel_AI

lemma tcb_in_valid_state:
  "\<lbrakk> st_tcb_at P t s; valid_objs s \<rbrakk> \<Longrightarrow> \<exists>st. P st \<and> valid_tcb_state st s" apply (clarsimp simp add: valid_objs_def pred_tcb_at_def obj_at_def) apply (erule my_BallE, erule domI) apply (simp add: valid_obj_def valid_tcb_def) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>st_tcb_at P t s; valid_objs s\<rbrakk> \<Longrightarrow> \<exists>st. P st \<and> valid_tcb_state st s proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>\<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; kheap s t = Some (TCB tcb); P (tcb_state tcb)\<rbrakk> \<Longrightarrow> \<exists>st. P st \<and> valid_tcb_state st s proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>kheap s t = Some (TCB tcb); P (tcb_state tcb); \<exists>obj. kheap s t = Some obj \<and> valid_obj t obj s\<rbrakk> \<Longrightarrow> \<exists>st. P st \<and> valid_tcb_state st s proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>kheap s t = Some (TCB tcb); P (tcb_state tcb); (\<forall>x\<in>ran tcb_cap_cases. case x of (getF, ab) \<Rightarrow> s \<turnstile> getF tcb \<and> (case ab of (setF, restr) \<Rightarrow> restr t (tcb_state tcb) (getF tcb))) \<and> valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb) \<and> valid_tcb_state (tcb_state tcb) s \<and> (case tcb_fault tcb of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f) \<and> length (tcb_fault_handler tcb) = word_bits \<and> valid_bound_ntfn (tcb_bound_notification tcb) s \<and> valid_arch_tcb (tcb_arch tcb) s\<rbrakk> \<Longrightarrow> \<exists>st. P st \<and> valid_tcb_state st s proof (prove)
goal:
No subgoals!
theory IpcCancel_AI

lemma no_refs_simple_strg:
  "st_tcb_at simple t s \<and> P {} \<longrightarrow> st_tcb_at (\<lambda>st. P (tcb_st_refs_of st)) t s" by (fastforce elim!: pred_tcb_weakenE)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t s \<and> P {} \<longrightarrow> st_tcb_at (\<lambda>st. P (tcb_st_refs_of st)) t s
theory IpcCancel_AI

lemma (in delete_one_abs) suspend_invs[wp]:
  "\<lbrace>invs and tcb_at t and (\<lambda>s. t \<noteq> idle_thread s)\<rbrace>
   (suspend t :: (unit,'a) s_monad) \<lbrace>\<lambda>rv. invs\<rbrace>" by (wp sts_invs_minor user_getreg_inv as_user_invs sts_invs_minor cancel_ipc_invs
         cancel_ipc_no_reply_cap
     | strengthen no_refs_simple_strg
     | simp add: suspend_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and tcb_at t and (\<lambda>s. t \<noteq> idle_thread s)\<rbrace> suspend t \<lbrace>\<lambda>rv. invs\<rbrace>
theory IpcCancel_AI

lemma suspend_typ_at [wp]:
  "\<lbrace>\<lambda>(s::'a state). P (typ_at T p s)\<rbrace> suspend t \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>" by (wpsimp simp: suspend_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> suspend t \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>
theory IpcCancel_AI

lemma suspend_valid_cap:
  "\<lbrace>valid_cap c\<rbrace> suspend tcb \<lbrace>\<lambda>_. (valid_cap c) :: 'a state \<Rightarrow> bool\<rbrace>" by (wp valid_cap_typ)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_cap c\<rbrace> suspend tcb \<lbrace>\<lambda>_. valid_cap c\<rbrace>
theory IpcCancel_AI

lemma (in delete_one_pre) reply_cancel_ipc_cte_wp_at_preserved:
  "(\<And>cap. P cap \<Longrightarrow> \<not> can_fast_finalise cap) \<Longrightarrow>
  \<lbrace>cte_wp_at P p\<rbrace> (reply_cancel_ipc t :: (unit,'a) s_monad) \<lbrace>\<lambda>rv. cte_wp_at P p\<rbrace>" unfolding reply_cancel_ipc_def apply (wpsimp wp: delete_one_cte_wp_at_preserved) apply (rule_tac Q="\<lambda>_. cte_wp_at P p" in hoare_post_imp, clarsimp) apply (wpsimp wp: thread_set_cte_wp_at_trivial simp: ran_tcb_cap_cases) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>cap. P cap \<Longrightarrow> \<not> can_fast_finalise cap) \<Longrightarrow> \<lbrace>cte_wp_at P p\<rbrace> reply_cancel_ipc t \<lbrace>\<lambda>rv. cte_wp_at P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>cap. P cap \<Longrightarrow> \<not> can_fast_finalise cap) \<Longrightarrow> \<lbrace>cte_wp_at P p\<rbrace> do thread_set (tcb_fault_update (\<lambda>_. None)) t;
cap <- get_cap (t, tcb_cnode_index 2);
descs <- gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt);
when (descs \<noteq> {}) $ do assert (\<exists>cslot_ptr. descs = {cslot_ptr});
select descs >>= cap_delete_one
od
od \<lbrace>\<lambda>rv. cte_wp_at P p\<rbrace> proof (prove)
goal (2 subgoals):
 1. (\<And>cap. P cap \<Longrightarrow> \<not> can_fast_finalise cap) \<Longrightarrow> \<lbrace>?Q1\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>\<lambda>x s. (descendants_of (t, tcb_cnode_index 2) (cdt s) \<noteq> {} \<longrightarrow> (\<exists>a b. descendants_of (t, tcb_cnode_index 2) (cdt s) = {(a, b)}) \<longrightarrow> (\<exists>a b. (a, b) \<in> descendants_of (t, tcb_cnode_index 2) (cdt s)) \<longrightarrow> cte_wp_at P p s) \<and> (descendants_of (t, tcb_cnode_index 2) (cdt s) = {} \<longrightarrow> cte_wp_at P p s)\<rbrace>
 2. \<And>s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> \<not> can_fast_finalise cap; cte_wp_at P p s\<rbrakk> \<Longrightarrow> ?Q1 s proof (prove)
goal (2 subgoals):
 1. (\<And>cap. P cap \<Longrightarrow> \<not> can_fast_finalise cap) \<Longrightarrow> \<lbrace>?Q1\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>\<lambda>_. cte_wp_at P p\<rbrace>
 2. \<And>s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> \<not> can_fast_finalise cap; cte_wp_at P p s\<rbrakk> \<Longrightarrow> ?Q1 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> \<not> can_fast_finalise cap; cte_wp_at P p s\<rbrakk> \<Longrightarrow> cte_wp_at P p s proof (prove)
goal:
No subgoals!
theory IpcCancel_AI

lemma (in delete_one_pre) cancel_ipc_cte_wp_at_preserved:
  "(\<And>cap. P cap \<Longrightarrow> \<not> can_fast_finalise cap) \<Longrightarrow>
  \<lbrace>cte_wp_at P p\<rbrace> (cancel_ipc t :: (unit,'a) s_monad) \<lbrace>\<lambda>rv. cte_wp_at P p\<rbrace>" apply (simp add: cancel_ipc_def) apply (rule hoare_pre) apply (wp reply_cancel_ipc_cte_wp_at_preserved | wpcw | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>cap. P cap \<Longrightarrow> \<not> can_fast_finalise cap) \<Longrightarrow> \<lbrace>cte_wp_at P p\<rbrace> cancel_ipc t \<lbrace>\<lambda>rv. cte_wp_at P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>cap. P cap \<Longrightarrow> \<not> can_fast_finalise cap) \<Longrightarrow> \<lbrace>cte_wp_at P p\<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. cte_wp_at P p\<rbrace> proof (prove)
goal (2 subgoals):
 1. (\<And>cap. P cap \<Longrightarrow> \<not> can_fast_finalise cap) \<Longrightarrow> \<lbrace>?Q\<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. cte_wp_at P p\<rbrace>
 2. \<And>s. \<lbrakk>\<And>cap. P cap \<Longrightarrow> \<not> can_fast_finalise cap; cte_wp_at P p s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory IpcCancel_AI

lemma (in delete_one_pre) suspend_cte_wp_at_preserved:
  "(\<And>cap. P cap \<Longrightarrow> \<not> can_fast_finalise cap) \<Longrightarrow>
  \<lbrace>cte_wp_at P p\<rbrace> (suspend tcb :: (unit,'a) s_monad) \<lbrace>\<lambda>_. cte_wp_at P p\<rbrace>" by (simp add: suspend_def) (wpsimp wp: cancel_ipc_cte_wp_at_preserved)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>cap. P cap \<Longrightarrow> \<not> can_fast_finalise cap) \<Longrightarrow> \<lbrace>cte_wp_at P p\<rbrace> suspend tcb \<lbrace>\<lambda>_. cte_wp_at P p\<rbrace>
theory IpcCancel_AI

lemma set_thread_state_bound_tcb_at[wp]:
  "\<lbrace>bound_tcb_at P t\<rbrace> set_thread_state p ts \<lbrace>\<lambda>_. bound_tcb_at P t\<rbrace>" unfolding set_thread_state_def set_object_def get_object_def by (wpsimp simp: pred_tcb_at_def obj_at_def get_tcb_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>bound_tcb_at P t\<rbrace> set_thread_state p ts \<lbrace>\<lambda>_. bound_tcb_at P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>bound_tcb_at P t\<rbrace> do tcb <- gets_the $ get_tcb p;
do kobj <- do kh <- gets kheap;
assert (kh p \<noteq> None);
return $ the $ kh p
od;
assert (a_type kobj = a_type (TCB (tcb\<lparr>tcb_state := ts\<rparr>)));
s <- get;
put (s\<lparr>kheap := (kheap s)(p \<mapsto> TCB (tcb\<lparr>tcb_state := ts\<rparr>))\<rparr>)
od;
do_extended_op (set_thread_state_ext p)
od \<lbrace>\<lambda>_. bound_tcb_at P t\<rbrace>
theory IpcCancel_AI

lemma fast_finalise_bound_tcb_at:
  "\<lbrace>\<lambda>s. bound_tcb_at P t s \<and> (\<exists>tt b R. cap = ReplyCap tt b R) \<rbrace> fast_finalise cap final \<lbrace>\<lambda>_. bound_tcb_at P t\<rbrace>" by (case_tac cap, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. bound_tcb_at P t s \<and> (\<exists>tt b R. cap = ReplyCap tt b R)\<rbrace> fast_finalise cap final \<lbrace>\<lambda>_. bound_tcb_at P t\<rbrace>
theory IpcCancel_AI

lemma get_cap_reply_cap_helper:
  "\<lbrace>\<lambda>s. \<exists>t b R. Some (ReplyCap t b R) = caps_of_state s slot \<rbrace> get_cap slot \<lbrace>\<lambda>rv s. \<exists>t b R. rv = ReplyCap t b R\<rbrace>" by (auto simp: valid_def get_cap_caps_of_state[symmetric])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<exists>t b R. Some (ReplyCap t b R) = caps_of_state s slot\<rbrace> get_cap slot \<lbrace>\<lambda>rv s. \<exists>t b R. rv = ReplyCap t b R\<rbrace>
theory IpcCancel_AI

lemma cap_delete_one_bound_tcb_at:
  "\<lbrace>\<lambda>s. bound_tcb_at P t s \<and> (\<exists>t b R. caps_of_state s c = Some (ReplyCap t b R)) \<rbrace>
     cap_delete_one c
   \<lbrace>\<lambda>_. bound_tcb_at P t\<rbrace>" apply (clarsimp simp: unless_def cap_delete_one_def) apply (wp fast_finalise_bound_tcb_at) apply (wp hoare_vcg_if_lift2, simp) apply (wp hoare_conjI) apply (wp only:hoare_drop_imp) apply (wp hoare_vcg_conj_lift) apply (wp get_cap_reply_cap_helper hoare_drop_imp | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. bound_tcb_at P t s \<and> (\<exists>t b R. caps_of_state s c = Some (ReplyCap t b R))\<rbrace> cap_delete_one c \<lbrace>\<lambda>_. bound_tcb_at P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. bound_tcb_at P t s \<and> (\<exists>t b R. caps_of_state s c = Some (ReplyCap t b R))\<rbrace> do cap <- get_cap c;
when (cap \<noteq> NullCap) (do final <- is_final_cap cap;
y <- fast_finalise cap final;
empty_slot c NullCap
od)
od \<lbrace>\<lambda>_. bound_tcb_at P t\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> get_cap c \<lbrace>\<lambda>cap. if cap \<noteq> NullCap then \<lambda>s. bound_tcb_at P t s \<and> (\<exists>tt b R. cap = ReplyCap tt b R) else bound_tcb_at P t\<rbrace>
 2. \<And>s. bound_tcb_at P t s \<and> (\<exists>t b R. caps_of_state s c = Some (ReplyCap t b R)) \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> get_cap c \<lbrace>\<lambda>cap s. (cap \<noteq> NullCap \<longrightarrow> bound_tcb_at P t s \<and> (\<exists>tt b R. cap = ReplyCap tt b R)) \<and> (cap = NullCap \<longrightarrow> bound_tcb_at P t s)\<rbrace>
 2. \<And>s. bound_tcb_at P t s \<and> (\<exists>t b R. caps_of_state s c = Some (ReplyCap t b R)) \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?Q\<rbrace> get_cap c \<lbrace>\<lambda>r s. r \<noteq> NullCap \<longrightarrow> bound_tcb_at P t s \<and> (\<exists>tt b R. r = ReplyCap tt b R)\<rbrace>
 2. \<lbrace>?Q\<rbrace> get_cap c \<lbrace>\<lambda>r s. r = NullCap \<longrightarrow> bound_tcb_at P t s\<rbrace>
 3. \<And>s. bound_tcb_at P t s \<and> (\<exists>t b R. caps_of_state s c = Some (ReplyCap t b R)) \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?Q\<rbrace> get_cap c \<lbrace>\<lambda>rv s. bound_tcb_at P t s \<and> (\<exists>tt b R. rv = ReplyCap tt b R)\<rbrace>
 2. \<lbrace>?Q\<rbrace> get_cap c \<lbrace>\<lambda>r s. r = NullCap \<longrightarrow> bound_tcb_at P t s\<rbrace>
 3. \<And>s. bound_tcb_at P t s \<and> (\<exists>t b R. caps_of_state s c = Some (ReplyCap t b R)) \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P'21\<rbrace> get_cap c \<lbrace>\<lambda>rv s. \<exists>tt b R. rv = ReplyCap tt b R\<rbrace>
 2. \<lbrace>\<lambda>s. bound_tcb_at P t s \<and> ?P'21 s\<rbrace> get_cap c \<lbrace>\<lambda>r s. r = NullCap \<longrightarrow> bound_tcb_at P t s\<rbrace>
 3. \<And>s. bound_tcb_at P t s \<and> (\<exists>t b R. caps_of_state s c = Some (ReplyCap t b R)) \<Longrightarrow> bound_tcb_at P t s \<and> ?P'21 s proof (prove)
goal:
No subgoals!