theory CSpaceInv_AI

lemma set_cap_reply[wp]:
  notes split_paired_Ex[simp del] split_paired_All[simp del]
  shows
  "\<lbrace>valid_reply_caps and cte_at dest and
      (\<lambda>s. \<forall>t rights. cap = cap.ReplyCap t False rights \<longrightarrow>
               st_tcb_at awaiting_reply t s \<and>
               (\<not> has_reply_cap t s \<or>
                cte_wp_at (is_reply_cap_to t) dest s))\<rbrace>
     set_cap cap dest
   \<lbrace>\<lambda>_. valid_reply_caps\<rbrace>" apply (simp add: valid_reply_caps_def has_reply_cap_def) apply (wpsimp wp: hoare_vcg_imp_lift hoare_vcg_all_lift set_cap_cte_wp_at_neg) apply (clarsimp simp: is_reply_cap_to_def) apply (rule conjI, fastforce) 
  (* Merging the simp and the fastforce fails miserably. I've no clue why *)
   apply (simp add:unique_reply_caps_def) apply (fastforce simp: is_cap_simps reply_cap_get_tcb_def cte_wp_at_caps_of_state) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_reply_caps and cte_wp_at (\<lambda>_. True) dest and (\<lambda>s. \<forall>t rights. cap = ReplyCap t False rights \<longrightarrow> st_tcb_at awaiting_reply t s \<and> (\<not> has_reply_cap t s \<or> cte_wp_at (is_reply_cap_to t) dest s))\<rbrace> set_cap cap dest \<lbrace>\<lambda>_. valid_reply_caps\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. (\<forall>t. (\<exists>p. cte_wp_at (is_reply_cap_to t) p s) \<longrightarrow> st_tcb_at awaiting_reply t s) \<and> unique_reply_caps (caps_of_state s)) and cte_wp_at (\<lambda>_. True) dest and (\<lambda>s. \<forall>t. (\<exists>rights. cap = ReplyCap t False rights) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> ((\<forall>p. \<not> cte_wp_at (is_reply_cap_to t) p s) \<or> cte_wp_at (is_reply_cap_to t) dest s))\<rbrace> set_cap cap dest \<lbrace>\<lambda>_ s. (\<forall>t. (\<exists>p. cte_wp_at (is_reply_cap_to t) p s) \<longrightarrow> st_tcb_at awaiting_reply t s) \<and> unique_reply_caps (caps_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>t. (\<exists>p. cte_wp_at (is_reply_cap_to t) p s) \<longrightarrow> st_tcb_at awaiting_reply t s; unique_reply_caps (caps_of_state s); cte_wp_at (\<lambda>_. True) dest s; \<forall>t. (\<exists>rights. cap = ReplyCap t False rights) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> ((\<forall>p. \<not> cte_wp_at (is_reply_cap_to t) p s) \<or> cte_wp_at (is_reply_cap_to t) dest s)\<rbrakk> \<Longrightarrow> (\<forall>x. (\<forall>xa. (xa = dest \<longrightarrow> \<not> is_reply_cap_to x cap) \<and> (xa \<noteq> dest \<longrightarrow> \<not> cte_wp_at (is_reply_cap_to x) xa s)) \<or> st_tcb_at awaiting_reply x s) \<and> unique_reply_caps (\<lambda>a. if a = dest then Some cap else caps_of_state s a) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>t. (\<exists>p. cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) p s) \<longrightarrow> st_tcb_at awaiting_reply t s; unique_reply_caps (caps_of_state s); cte_wp_at (\<lambda>_. True) dest s; \<forall>t. (\<exists>rights. cap = ReplyCap t False rights) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> ((\<forall>p. \<not> cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) p s) \<or> cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) dest s)\<rbrakk> \<Longrightarrow> (\<forall>x. (\<forall>xa. (xa = dest \<longrightarrow> (\<forall>rights. cap \<noteq> ReplyCap x False rights)) \<and> (xa \<noteq> dest \<longrightarrow> \<not> cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap x False rights) xa s)) \<or> st_tcb_at awaiting_reply x s) \<and> unique_reply_caps (\<lambda>a. if a = dest then Some cap else caps_of_state s a) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>t. (\<exists>p. cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) p s) \<longrightarrow> st_tcb_at awaiting_reply t s; unique_reply_caps (caps_of_state s); cte_wp_at (\<lambda>_. True) dest s; \<forall>t. (\<exists>rights. cap = ReplyCap t False rights) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> ((\<forall>p. \<not> cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) p s) \<or> cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) dest s)\<rbrakk> \<Longrightarrow> unique_reply_caps (\<lambda>a. if a = dest then Some cap else caps_of_state s a) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>t. (\<exists>p. cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) p s) \<longrightarrow> st_tcb_at awaiting_reply t s; unique_reply_caps (caps_of_state s); cte_wp_at (\<lambda>_. True) dest s; \<forall>t. (\<exists>rights. cap = ReplyCap t False rights) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> ((\<forall>p. \<not> cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) p s) \<or> cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) dest s)\<rbrakk> \<Longrightarrow> unique_reply_caps (\<lambda>a. if a = dest then Some cap else caps_of_state s a) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>t. (\<exists>p. cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) p s) \<longrightarrow> st_tcb_at awaiting_reply t s; \<forall>ptr ptr' t. (\<exists>R. caps_of_state s ptr = Some (ReplyCap t False R)) \<longrightarrow> (\<exists>R'. caps_of_state s ptr' = Some (ReplyCap t False R')) \<longrightarrow> ptr = ptr'; cte_wp_at (\<lambda>_. True) dest s; \<forall>t. (\<exists>rights. cap = ReplyCap t False rights) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> ((\<forall>p. \<not> cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) p s) \<or> cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) dest s)\<rbrakk> \<Longrightarrow> \<forall>ptr. (ptr = dest \<longrightarrow> (\<forall>ptr'. ptr' \<noteq> dest \<longrightarrow> (\<forall>t. (\<exists>R. cap = ReplyCap t False R) \<longrightarrow> (\<forall>R'. caps_of_state s ptr' \<noteq> Some (ReplyCap t False R'))))) \<and> (ptr \<noteq> dest \<longrightarrow> (\<forall>t. (\<exists>R. caps_of_state s ptr = Some (ReplyCap t False R)) \<longrightarrow> (\<forall>R'. cap \<noteq> ReplyCap t False R'))) proof (prove)
goal:
No subgoals!