theory CSpace_AI

lemma cap_insert_reply [wp]:
  "\<lbrace>valid_reply_caps and cte_at dest and
      (\<lambda>s. \<forall>t R. cap = cap.ReplyCap t False R \<longrightarrow>
           st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s)\<rbrace>
   cap_insert cap src dest \<lbrace>\<lambda>_. valid_reply_caps\<rbrace>" apply (simp add: cap_insert_def update_cdt_def) apply (wp
         | simp split del: if_split
         | rule hoare_drop_imp
         | clarsimp simp: valid_reply_caps_def)+ apply (wp hoare_vcg_all_lift hoare_vcg_imp_lift set_untyped_cap_as_full_has_reply_cap_neg
                set_untyped_cap_as_full_unique_reply_caps set_untyped_cap_as_full_cte_wp_at get_cap_wp)+ apply (clarsimp simp:cte_wp_at_caps_of_state valid_reply_caps_def)+ 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 R. cap = ReplyCap t False R \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s)\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>_. valid_reply_caps\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_reply_caps and cte_wp_at (\<lambda>_. True) dest and (\<lambda>s. \<forall>t. (\<exists>R. cap = ReplyCap t False R) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s)\<rbrace> do src_cap <- get_cap src;
old_cap <- get_cap dest;
y <- assert (old_cap = NullCap);
y <- set_untyped_cap_as_full src_cap cap src;
y <- set_cap cap dest;
is_original <- gets is_original_cap;
src_p <- gets (\<lambda>s. cdt s src);
dest_p <- gets (\<lambda>s. cdt s dest);
y <- do t <- gets cdt;
set_cdt (t(dest := if should_be_parent_of src_cap (is_original src) cap (is_cap_revocable cap src_cap) then Some src else t src))
od;
y <- do_extended_op (cap_insert_ext (should_be_parent_of src_cap (is_original src) cap (is_cap_revocable cap src_cap)) src dest src_p dest_p);
set_original dest (is_cap_revocable cap src_cap)
od \<lbrace>\<lambda>_. valid_reply_caps\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>src_cap x. \<lbrace>?B6 src_cap x ()\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>ya s. (\<forall>t. has_reply_cap t s \<longrightarrow> st_tcb_at awaiting_reply t s) \<and> unique_reply_caps (caps_of_state s) \<and> cte_wp_at (\<lambda>_. True) dest s \<and> (\<forall>t. (\<exists>rights. cap = ReplyCap t False rights) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> (has_reply_cap t s \<longrightarrow> cte_wp_at (is_reply_cap_to t) dest s))\<rbrace>
 2. \<And>src_cap x. \<lbrace>?B5 src_cap x\<rbrace> assert (x = NullCap) \<lbrace>?B6 src_cap x\<rbrace>
 3. \<And>src_cap. \<lbrace>?B4 src_cap\<rbrace> get_cap dest \<lbrace>?B5 src_cap\<rbrace>
 4. \<lbrace>?Q3\<rbrace> get_cap src \<lbrace>?B4\<rbrace>
 5. \<And>s. (valid_reply_caps and cte_wp_at (\<lambda>_. True) dest and (\<lambda>s. \<forall>t. (\<exists>R. cap = ReplyCap t False R) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s)) s \<Longrightarrow> ?Q3 s proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_reply_caps and cte_wp_at (\<lambda>_. True) dest and (\<lambda>s. \<forall>t. (\<exists>R. cap = ReplyCap t False R) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s)) s \<Longrightarrow> (\<forall>x cap. cte_wp_at ((=) cap) src s \<longrightarrow> (\<forall>cap. cte_wp_at ((=) cap) dest s \<longrightarrow> cap \<noteq> NullCap) \<or> (\<forall>capa. cte_wp_at ((=) capa) dest s \<longrightarrow> \<not> has_reply_cap x s \<and> cte_wp_at ((=) cap) src s \<or> st_tcb_at awaiting_reply x s)) \<and> (\<forall>capa. cte_wp_at ((=) capa) src s \<longrightarrow> (\<forall>cap. cte_wp_at ((=) cap) dest s \<longrightarrow> cap \<noteq> NullCap) \<or> (\<forall>capb. cte_wp_at ((=) capb) dest s \<longrightarrow> (unique_reply_caps (caps_of_state s) \<and> cte_wp_at ((=) capa) src s) \<and> ((dest \<noteq> src \<and> cte_wp_at (\<lambda>a. True) dest s \<or> dest = src \<and> cte_wp_at (\<lambda>a. True) src s) \<and> cte_wp_at ((=) capa) src s) \<and> (\<forall>x. (\<nexists>rights. cap = ReplyCap x False rights) \<or> st_tcb_at awaiting_reply x s \<and> (\<not> has_reply_cap x s \<and> cte_wp_at ((=) capa) src s \<or> (dest \<noteq> src \<and> cte_wp_at (is_reply_cap_to x) dest s \<or> dest = src \<and> cte_wp_at (\<lambda>a. is_reply_cap_to x (masked_as_full a cap)) src s) \<and> cte_wp_at ((=) capa) src s)))) proof (prove)
goal:
No subgoals!