theory Untyped_AI

lemma create_cap_valid_reply_caps[wp]:
  "\<lbrace>valid_reply_caps\<rbrace>
     create_cap tp sz p dev (cref, oref)
   \<lbrace>\<lambda>rv. valid_reply_caps\<rbrace>" apply (simp add: valid_reply_caps_def has_reply_cap_def
                   cte_wp_at_caps_of_state create_cap_def is_reply_cap_to_def
                   set_cdt_def) apply (simp only: imp_conv_disj) apply (rule hoare_pre) apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift | simp)+ apply (clarsimp simp: default_cap_reply) apply (erule conjI [OF allEI], fastforce) apply (simp add: unique_reply_caps_def default_cap_reply) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_reply_caps\<rbrace> create_cap tp sz p dev (cref, oref) \<lbrace>\<lambda>rv. valid_reply_caps\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>t. (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (\<exists>rights. cap = ReplyCap t False rights)) \<longrightarrow> st_tcb_at awaiting_reply t s) \<and> unique_reply_caps (caps_of_state s)\<rbrace> do dest_p <- gets (\<lambda>s. cdt s cref);
cdt <- gets cdt;
y <- do s <- get;
put (s\<lparr>cdt := cdt(cref \<mapsto> p)\<rparr>)
od;
y <- do_extended_op (create_cap_ext p cref dest_p);
y <- set_original cref True;
set_cap (default_cap tp oref sz dev) cref
od \<lbrace>\<lambda>rv s. (\<forall>t. (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (\<exists>rights. cap = ReplyCap t False rights)) \<longrightarrow> st_tcb_at awaiting_reply t s) \<and> unique_reply_caps (caps_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>t. (\<nexists>a b cap. caps_of_state s (a, b) = Some cap \<and> (\<exists>rights. cap = ReplyCap t False rights)) \<or> st_tcb_at awaiting_reply t s) \<and> unique_reply_caps (caps_of_state s)\<rbrace> do dest_p <- gets (\<lambda>s. cdt s cref);
cdt <- gets cdt;
y <- do s <- get;
put (s\<lparr>cdt := cdt(cref \<mapsto> p)\<rparr>)
od;
y <- do_extended_op (create_cap_ext p cref dest_p);
y <- set_original cref True;
set_cap (default_cap tp oref sz dev) cref
od \<lbrace>\<lambda>rv s. (\<forall>t. (\<nexists>a b cap. caps_of_state s (a, b) = Some cap \<and> (\<exists>rights. cap = ReplyCap t False rights)) \<or> st_tcb_at awaiting_reply t s) \<and> unique_reply_caps (caps_of_state s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q3\<rbrace> do dest_p <- gets (\<lambda>s. cdt s cref);
cdt <- gets cdt;
y <- do s <- get;
put (s\<lparr>cdt := cdt(cref \<mapsto> p)\<rparr>)
od;
y <- do_extended_op (create_cap_ext p cref dest_p);
y <- set_original cref True;
set_cap (default_cap tp oref sz dev) cref
od \<lbrace>\<lambda>rv s. (\<forall>t. (\<nexists>a b cap. caps_of_state s (a, b) = Some cap \<and> (\<exists>rights. cap = ReplyCap t False rights)) \<or> st_tcb_at awaiting_reply t s) \<and> unique_reply_caps (caps_of_state s)\<rbrace>
 2. \<And>s. (\<forall>t. (\<nexists>a b cap. caps_of_state s (a, b) = Some cap \<and> (\<exists>rights. cap = ReplyCap t False rights)) \<or> st_tcb_at awaiting_reply t s) \<and> unique_reply_caps (caps_of_state s) \<Longrightarrow> ?Q3 s proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>t. (\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (\<forall>rights. cap \<noteq> ReplyCap t False rights)) \<or> st_tcb_at awaiting_reply t s) \<and> unique_reply_caps (caps_of_state s) \<Longrightarrow> (\<forall>x. (\<forall>a b. ((a, b) = cref \<longrightarrow> (\<forall>rights. default_cap tp oref sz dev \<noteq> ReplyCap x False rights)) \<and> ((a, b) \<noteq> cref \<longrightarrow> (\<forall>cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (\<forall>rights. cap \<noteq> ReplyCap x False rights)))) \<or> st_tcb_at awaiting_reply x s) \<and> unique_reply_caps (\<lambda>a. if a = cref then Some (default_cap tp oref sz dev) else caps_of_state s a) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>t. (\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (\<forall>rights. cap \<noteq> ReplyCap t False rights)) \<or> st_tcb_at awaiting_reply t s; unique_reply_caps (caps_of_state s)\<rbrakk> \<Longrightarrow> (\<forall>x. (\<forall>a b. (a, b) \<noteq> cref \<longrightarrow> (\<forall>cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (\<forall>rights. cap \<noteq> ReplyCap x False rights))) \<or> st_tcb_at awaiting_reply x s) \<and> unique_reply_caps (\<lambda>a. if a = cref then Some (default_cap tp oref sz dev) else caps_of_state s a) proof (prove)
goal (1 subgoal):
 1. \<And>s. unique_reply_caps (caps_of_state s) \<Longrightarrow> unique_reply_caps (\<lambda>a. if a = cref then Some (default_cap tp oref sz dev) else caps_of_state s a) proof (prove)
goal:
No subgoals!