theory IpcCancel_AI

lemma (in delete_one_abs) reply_cancel_ipc_no_reply_cap[wp]:
  notes hoare_pre
  shows "\<lbrace>invs and tcb_at t\<rbrace> (reply_cancel_ipc t :: (unit,'a) s_monad) \<lbrace>\<lambda>rv s. \<not> has_reply_cap t s\<rbrace>" apply (simp add: reply_cancel_ipc_def) apply wp apply (rule_tac Q="\<lambda>rvp s. cte_wp_at (\<lambda>c. c = cap.NullCap) x s \<and>
                                (\<forall>sl R. sl \<noteq> x \<longrightarrow>
                                  caps_of_state s sl \<noteq> Some (cap.ReplyCap t False R))"
                  in hoare_strengthen_post) apply (wp hoare_vcg_conj_lift hoare_vcg_all_lift
                   delete_one_deletes delete_one_caps_of_state) apply (clarsimp simp: has_reply_cap_def cte_wp_at_caps_of_state is_reply_cap_to_def) apply (case_tac "(aa, ba) = (a, b)",simp_all)[1] apply (wp hoare_vcg_all_lift | simp del: split_paired_All)+ apply (rule_tac Q="\<lambda>_ s. invs s \<and> tcb_at t s" in hoare_post_imp) apply (erule conjE) apply (frule(1) reply_cap_descends_from_master) apply (auto dest: reply_master_no_descendants_no_reply[rotated -1])[1] apply (wp thread_set_invs_trivial | clarsimp simp: tcb_cap_cases_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and tcb_at t\<rbrace> reply_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 y <- 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 y <- assert (\<exists>a b. descs = {(a, b)});
select descs >>= cap_delete_one
od)
od \<lbrace>\<lambda>rv s. \<not> has_reply_cap t s\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>y cap descs ya x. descs \<noteq> {} \<Longrightarrow> \<lbrace>?B6 y cap descs ya x\<rbrace> cap_delete_one x \<lbrace>\<lambda>rv s. \<not> has_reply_cap t s\<rbrace>
 2. \<And>y cap descs ya. descs \<noteq> {} \<Longrightarrow> \<lbrace>?B5 y cap descs ya\<rbrace> select descs \<lbrace>?B6 y cap descs ya\<rbrace>
 3. \<And>y cap descs. descs \<noteq> {} \<Longrightarrow> \<lbrace>?Q4 y cap descs\<rbrace> assert (\<exists>a b. descs = {(a, b)}) \<lbrace>?B5 y cap descs\<rbrace>
 4. \<And>y cap. \<lbrace>?B2 y cap\<rbrace> gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt) \<lbrace>\<lambda>descs. if descs \<noteq> {} then ?Q4 y cap descs else (\<lambda>s. \<not> has_reply_cap t s)\<rbrace>
 5. \<And>y. \<lbrace>?B1 y\<rbrace> get_cap (t, tcb_cnode_index 2) \<lbrace>?B2 y\<rbrace>
 6. \<lbrace>?Q\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>?B1\<rbrace>
 7. \<And>s. (invs and tcb_at t) s \<Longrightarrow> ?Q s proof (prove)
goal (8 subgoals):
 1. \<And>y cap descs ya x. descs \<noteq> {} \<Longrightarrow> \<lbrace>?B6 y cap descs ya x\<rbrace> cap_delete_one x \<lbrace>\<lambda>rvp s. cte_wp_at (\<lambda>c. c = NullCap) x s \<and> (\<forall>sl R. sl \<noteq> x \<longrightarrow> caps_of_state s sl \<noteq> Some (ReplyCap t False R))\<rbrace>
 2. \<And>y cap descs ya x rv s. \<lbrakk>descs \<noteq> {}; cte_wp_at (\<lambda>c. c = NullCap) x s \<and> (\<forall>sl R. sl \<noteq> x \<longrightarrow> caps_of_state s sl \<noteq> Some (ReplyCap t False R))\<rbrakk> \<Longrightarrow> \<not> has_reply_cap t s
 3. \<And>y cap descs ya. descs \<noteq> {} \<Longrightarrow> \<lbrace>?B5 y cap descs ya\<rbrace> select descs \<lbrace>?B6 y cap descs ya\<rbrace>
 4. \<And>y cap descs. descs \<noteq> {} \<Longrightarrow> \<lbrace>?Q4 y cap descs\<rbrace> assert (\<exists>a b. descs = {(a, b)}) \<lbrace>?B5 y cap descs\<rbrace>
 5. \<And>y cap. \<lbrace>?B2 y cap\<rbrace> gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt) \<lbrace>\<lambda>descs. if descs \<noteq> {} then ?Q4 y cap descs else (\<lambda>s. \<not> has_reply_cap t s)\<rbrace>
 6. \<And>y. \<lbrace>?B1 y\<rbrace> get_cap (t, tcb_cnode_index 2) \<lbrace>?B2 y\<rbrace>
 7. \<lbrace>?Q\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>?B1\<rbrace>
 8. \<And>s. (invs and tcb_at t) s \<Longrightarrow> ?Q s proof (prove)
goal (7 subgoals):
 1. \<And>y cap descs ya x rv s. \<lbrakk>descs \<noteq> {}; cte_wp_at (\<lambda>c. c = NullCap) x s \<and> (\<forall>sl R. sl \<noteq> x \<longrightarrow> caps_of_state s sl \<noteq> Some (ReplyCap t False R))\<rbrakk> \<Longrightarrow> \<not> has_reply_cap t s
 2. \<And>y cap descs ya. descs \<noteq> {} \<Longrightarrow> \<lbrace>?B5 y cap descs ya\<rbrace> select descs \<lbrace>\<lambda>x s. True \<and> (\<forall>xa xb. cte_wp_at can_fast_finalise x s \<longrightarrow> xa \<noteq> x \<longrightarrow> ((caps_of_state s)(x \<mapsto> NullCap)) xa \<noteq> Some (ReplyCap t False xb))\<rbrace>
 3. \<And>y cap descs. descs \<noteq> {} \<Longrightarrow> \<lbrace>?Q4 y cap descs\<rbrace> assert (\<exists>a b. descs = {(a, b)}) \<lbrace>?B5 y cap descs\<rbrace>
 4. \<And>y cap. \<lbrace>?B2 y cap\<rbrace> gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt) \<lbrace>\<lambda>descs. if descs \<noteq> {} then ?Q4 y cap descs else (\<lambda>s. \<not> has_reply_cap t s)\<rbrace>
 5. \<And>y. \<lbrace>?B1 y\<rbrace> get_cap (t, tcb_cnode_index 2) \<lbrace>?B2 y\<rbrace>
 6. \<lbrace>?Q\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>?B1\<rbrace>
 7. \<And>s. (invs and tcb_at t) s \<Longrightarrow> ?Q s proof (prove)
goal (7 subgoals):
 1. \<And>descs a b s aa ba rights. \<lbrakk>descs \<noteq> {}; caps_of_state s (a, b) = Some NullCap; \<forall>aa ba. (aa = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> (\<forall>R. caps_of_state s (aa, ba) \<noteq> Some (ReplyCap t False R)); caps_of_state s (aa, ba) = Some (ReplyCap t False rights)\<rbrakk> \<Longrightarrow> False
 2. \<And>y cap descs ya. descs \<noteq> {} \<Longrightarrow> \<lbrace>?B5 y cap descs ya\<rbrace> select descs \<lbrace>\<lambda>x s. True \<and> (\<forall>xa xb. cte_wp_at can_fast_finalise x s \<longrightarrow> xa \<noteq> x \<longrightarrow> ((caps_of_state s)(x \<mapsto> NullCap)) xa \<noteq> Some (ReplyCap t False xb))\<rbrace>
 3. \<And>y cap descs. descs \<noteq> {} \<Longrightarrow> \<lbrace>?Q4 y cap descs\<rbrace> assert (\<exists>a b. descs = {(a, b)}) \<lbrace>?B5 y cap descs\<rbrace>
 4. \<And>y cap. \<lbrace>?B2 y cap\<rbrace> gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt) \<lbrace>\<lambda>descs. if descs \<noteq> {} then ?Q4 y cap descs else (\<lambda>s. \<not> has_reply_cap t s)\<rbrace>
 5. \<And>y. \<lbrace>?B1 y\<rbrace> get_cap (t, tcb_cnode_index 2) \<lbrace>?B2 y\<rbrace>
 6. \<lbrace>?Q\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>?B1\<rbrace>
 7. \<And>s. (invs and tcb_at t) s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>y cap descs ya. descs \<noteq> {} \<Longrightarrow> \<lbrace>?B5 y cap descs ya\<rbrace> select descs \<lbrace>\<lambda>x s. True \<and> (\<forall>xa xb. cte_wp_at can_fast_finalise x s \<longrightarrow> xa \<noteq> x \<longrightarrow> ((caps_of_state s)(x \<mapsto> NullCap)) xa \<noteq> Some (ReplyCap t False xb))\<rbrace>
 2. \<And>y cap descs. descs \<noteq> {} \<Longrightarrow> \<lbrace>?Q4 y cap descs\<rbrace> assert (\<exists>a b. descs = {(a, b)}) \<lbrace>?B5 y cap descs\<rbrace>
 3. \<And>y cap. \<lbrace>?B2 y cap\<rbrace> gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt) \<lbrace>\<lambda>descs. if descs \<noteq> {} then ?Q4 y cap descs else (\<lambda>s. \<not> has_reply_cap t s)\<rbrace>
 4. \<And>y. \<lbrace>?B1 y\<rbrace> get_cap (t, tcb_cnode_index 2) \<lbrace>?B2 y\<rbrace>
 5. \<lbrace>?Q\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>?B1\<rbrace>
 6. \<And>s. (invs and tcb_at t) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>\<lambda>y 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> (\<forall>x\<in>descendants_of (t, tcb_cnode_index 2) (cdt s). cte_wp_at can_fast_finalise x s \<longrightarrow> (\<forall>xa. xa \<noteq> x \<longrightarrow> (\<forall>x. caps_of_state s xa \<noteq> Some (ReplyCap t False x))))) \<and> (descendants_of (t, tcb_cnode_index 2) (cdt s) = {} \<longrightarrow> \<not> has_reply_cap t s)\<rbrace>
 2. \<And>s. (invs and tcb_at t) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>rv s. invs s \<and> tcb_at t s \<Longrightarrow> (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> (\<forall>x\<in>descendants_of (t, tcb_cnode_index 2) (cdt s). cte_wp_at can_fast_finalise x s \<longrightarrow> (\<forall>xa. xa \<noteq> x \<longrightarrow> (\<forall>x. caps_of_state s xa \<noteq> Some (ReplyCap t False x))))) \<and> (descendants_of (t, tcb_cnode_index 2) (cdt s) = {} \<longrightarrow> \<not> has_reply_cap t s)
 2. \<lbrace>?Q\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>\<lambda>_ s. invs s \<and> tcb_at t s\<rbrace>
 3. \<And>s. (invs and tcb_at t) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>rv s. \<lbrakk>invs s; tcb_at t s\<rbrakk> \<Longrightarrow> (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> (\<forall>x\<in>descendants_of (t, tcb_cnode_index 2) (cdt s). cte_wp_at can_fast_finalise x s \<longrightarrow> (\<forall>xa. xa \<noteq> x \<longrightarrow> (\<forall>x. caps_of_state s xa \<noteq> Some (ReplyCap t False x))))) \<and> (descendants_of (t, tcb_cnode_index 2) (cdt s) = {} \<longrightarrow> \<not> has_reply_cap t s)
 2. \<lbrace>?Q\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>\<lambda>_ s. invs s \<and> tcb_at t s\<rbrace>
 3. \<And>s. (invs and tcb_at t) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>rv s. \<lbrakk>invs s; tcb_at t s; \<forall>sl\<in>descendants_of (t, tcb_cnode_index 2) (cdt s). \<forall>sl' R. sl' \<noteq> sl \<longrightarrow> caps_of_state s sl' \<noteq> Some (ReplyCap t False R)\<rbrakk> \<Longrightarrow> (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> (\<forall>x\<in>descendants_of (t, tcb_cnode_index 2) (cdt s). cte_wp_at can_fast_finalise x s \<longrightarrow> (\<forall>xa. xa \<noteq> x \<longrightarrow> (\<forall>x. caps_of_state s xa \<noteq> Some (ReplyCap t False x))))) \<and> (descendants_of (t, tcb_cnode_index 2) (cdt s) = {} \<longrightarrow> \<not> has_reply_cap t s)
 2. \<lbrace>?Q\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>\<lambda>_ s. invs s \<and> tcb_at t s\<rbrace>
 3. \<And>s. (invs and tcb_at t) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>\<lambda>_ s. invs s \<and> tcb_at t s\<rbrace>
 2. \<And>s. (invs and tcb_at t) s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!