theory Ipc_AI

lemma tcl_reply':
  "\<And>slots caps ep buffer n mi.
    \<lbrace>valid_reply_caps and valid_reply_masters and valid_objs and valid_mdb and K(distinct slots)
          and (\<lambda>s. \<forall>x \<in> set slots. real_cte_at x s \<and> cte_wp_at (\<lambda>cap. cap = cap.NullCap) x s)
          and transfer_caps_srcs caps\<rbrace>
      transfer_caps_loop ep buffer n caps slots mi
    \<lbrace>\<lambda>rv. valid_reply_caps and valid_reply_masters :: 'state_ext state \<Rightarrow> bool\<rbrace>" apply (rule hoare_pre) apply (rule transfer_caps_loop_presM[where vo=True and em=False and ex=False]) apply wp apply (clarsimp simp: real_cte_at_cte) apply (clarsimp simp: cte_wp_at_caps_of_state is_derived_def is_cap_simps) apply (frule(1) valid_reply_mastersD'[OF caps_of_state_cteD]) apply (frule(1) tcb_cap_valid_caps_of_stateD) apply (frule(1) caps_of_state_valid) apply (clarsimp simp: tcb_cap_valid_def valid_cap_def is_cap_simps) apply (clarsimp simp: obj_at_def is_tcb is_cap_table cap_master_cap_def) apply (wpsimp wp: valid_reply_caps_st_cte_lift valid_reply_masters_cte_lift) apply (clarsimp simp:cte_wp_at_caps_of_state | intro conjI)+ apply (drule(1) bspec,clarsimp) apply (frule(1) caps_of_state_valid) apply (fastforce simp:valid_cap_def) apply (drule(1) bspec) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>slots caps ep buffer n mi. \<lbrace>valid_reply_caps and valid_reply_masters and valid_objs and valid_mdb and K (distinct slots) and (\<lambda>s. \<forall>x\<in>set slots. real_cte_at x s \<and> cte_wp_at (\<lambda>cap. cap = NullCap) x s) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. valid_reply_caps and valid_reply_masters\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>slots caps ep buffer n mi. \<lbrace>?Q slots caps ep buffer n mi\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. valid_reply_caps and valid_reply_masters\<rbrace>
 2. \<And>slots caps ep buffer n mi s. (valid_reply_caps and valid_reply_masters and valid_objs and valid_mdb and K (distinct slots) and (\<lambda>s. \<forall>x\<in>set slots. real_cte_at x s \<and> cte_wp_at (\<lambda>cap. cap = NullCap) x s) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s \<Longrightarrow> ?Q slots caps ep buffer n mi s proof (prove)
goal (3 subgoals):
 1. \<And>slots caps ep buffer n mi cap src dest. \<lbrace>\<lambda>s. (valid_reply_caps and valid_reply_masters) s \<and> (True \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> real_cte_at dest s \<and> s \<turnstile> cap \<and> tcb_cap_valid cap dest s \<and> real_cte_at src s \<and> cte_wp_at (is_derived (cdt s) src cap) src s \<and> cap \<noteq> NullCap) \<and> (False \<longrightarrow> cte_wp_at ((=) NullCap) dest s) \<and> (False \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) dest s)\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>rv. valid_reply_caps and valid_reply_masters\<rbrace>
 2. \<And>slots caps ep buffer n mi b na. \<lbrace>valid_reply_caps and valid_reply_masters\<rbrace> set_extra_badge buffer b na \<lbrace>\<lambda>_. valid_reply_caps and valid_reply_masters\<rbrace>
 3. \<And>slots caps ep buffer n mi s. (valid_reply_caps and valid_reply_masters and valid_objs and valid_mdb and K (distinct slots) and (\<lambda>s. \<forall>x\<in>set slots. real_cte_at x s \<and> cte_wp_at (\<lambda>cap. cap = NullCap) x s) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s \<Longrightarrow> (valid_reply_caps and valid_reply_masters) s \<and> (True \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (False \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s)) proof (prove)
goal (3 subgoals):
 1. \<And>slots caps ep buffer n mi cap src dest s. (valid_reply_caps and valid_reply_masters) s \<and> (True \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> real_cte_at dest s \<and> s \<turnstile> cap \<and> tcb_cap_valid cap dest s \<and> real_cte_at src s \<and> cte_wp_at (is_derived (cdt s) src cap) src s \<and> cap \<noteq> NullCap) \<and> (False \<longrightarrow> cte_wp_at ((=) NullCap) dest s) \<and> (False \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) dest s) \<Longrightarrow> (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)) s \<and> (valid_reply_masters and cte_wp_at (\<lambda>_. True) dest and K (\<not> is_master_reply_cap cap)) s
 2. \<And>slots caps ep buffer n mi b na. \<lbrace>valid_reply_caps and valid_reply_masters\<rbrace> set_extra_badge buffer b na \<lbrace>\<lambda>_. valid_reply_caps and valid_reply_masters\<rbrace>
 3. \<And>slots caps ep buffer n mi s. (valid_reply_caps and valid_reply_masters and valid_objs and valid_mdb and K (distinct slots) and (\<lambda>s. \<forall>x\<in>set slots. real_cte_at x s \<and> cte_wp_at (\<lambda>cap. cap = NullCap) x s) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s \<Longrightarrow> (valid_reply_caps and valid_reply_masters) s \<and> (True \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (False \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s)) proof (prove)
goal (3 subgoals):
 1. \<And>cap a b aa ba s. \<lbrakk>valid_reply_caps s; valid_reply_masters s; valid_objs s; valid_mdb s; cap_table_at (length ba) aa s; s \<turnstile> cap; tcb_cap_valid cap (aa, ba) s; cap_table_at (length b) a s; cte_wp_at (is_derived (cdt s) (a, b) cap) (a, b) s; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> (\<forall>t. (\<exists>R. cap = ReplyCap t False R) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s) \<and> \<not> is_master_reply_cap cap
 2. \<And>slots caps ep buffer n mi b na. \<lbrace>valid_reply_caps and valid_reply_masters\<rbrace> set_extra_badge buffer b na \<lbrace>\<lambda>_. valid_reply_caps and valid_reply_masters\<rbrace>
 3. \<And>slots caps ep buffer n mi s. (valid_reply_caps and valid_reply_masters and valid_objs and valid_mdb and K (distinct slots) and (\<lambda>s. \<forall>x\<in>set slots. real_cte_at x s \<and> cte_wp_at (\<lambda>cap. cap = NullCap) x s) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s \<Longrightarrow> (valid_reply_caps and valid_reply_masters) s \<and> (True \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (False \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s)) proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba s t R x Ra. \<lbrakk>valid_reply_caps s; valid_reply_masters s; valid_objs s; valid_mdb s; cap_table_at (length ba) aa s; s \<turnstile> ReplyCap t False R; tcb_cap_valid (ReplyCap t False R) (aa, ba) s; cap_table_at (length b) a s; caps_of_state s (a, b) = Some (ReplyCap x True Ra); cap_master_cap (ReplyCap x True Ra) = cap_master_cap (ReplyCap t False R); is_derived_arch (ReplyCap t False R) (ReplyCap x True Ra)\<rbrakk> \<Longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s
 2. \<And>slots caps ep buffer n mi b na. \<lbrace>valid_reply_caps and valid_reply_masters\<rbrace> set_extra_badge buffer b na \<lbrace>\<lambda>_. valid_reply_caps and valid_reply_masters\<rbrace>
 3. \<And>slots caps ep buffer n mi s. (valid_reply_caps and valid_reply_masters and valid_objs and valid_mdb and K (distinct slots) and (\<lambda>s. \<forall>x\<in>set slots. real_cte_at x s \<and> cte_wp_at (\<lambda>cap. cap = NullCap) x s) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s \<Longrightarrow> (valid_reply_caps and valid_reply_masters) s \<and> (True \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (False \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s)) proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba s t R x Ra. \<lbrakk>valid_reply_caps s; valid_reply_masters s; valid_objs s; valid_mdb s; cap_table_at (length ba) aa s; s \<turnstile> ReplyCap t False R; tcb_cap_valid (ReplyCap t False R) (aa, ba) s; cap_table_at (length b) a s; caps_of_state s (a, b) = Some (ReplyCap x True Ra); cap_master_cap (ReplyCap x True Ra) = cap_master_cap (ReplyCap t False R); is_derived_arch (ReplyCap t False R) (ReplyCap x True Ra); (a, b) = (x, tcb_cnode_index 2)\<rbrakk> \<Longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s
 2. \<And>slots caps ep buffer n mi b na. \<lbrace>valid_reply_caps and valid_reply_masters\<rbrace> set_extra_badge buffer b na \<lbrace>\<lambda>_. valid_reply_caps and valid_reply_masters\<rbrace>
 3. \<And>slots caps ep buffer n mi s. (valid_reply_caps and valid_reply_masters and valid_objs and valid_mdb and K (distinct slots) and (\<lambda>s. \<forall>x\<in>set slots. real_cte_at x s \<and> cte_wp_at (\<lambda>cap. cap = NullCap) x s) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s \<Longrightarrow> (valid_reply_caps and valid_reply_masters) s \<and> (True \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (False \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s)) proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba s t R x Ra. \<lbrakk>valid_reply_caps s; valid_reply_masters s; valid_objs s; valid_mdb s; cap_table_at (length ba) aa s; s \<turnstile> ReplyCap t False R; tcb_cap_valid (ReplyCap t False R) (aa, ba) s; cap_table_at (length b) a s; caps_of_state s (a, b) = Some (ReplyCap x True Ra); cap_master_cap (ReplyCap x True Ra) = cap_master_cap (ReplyCap t False R); is_derived_arch (ReplyCap t False R) (ReplyCap x True Ra); (a, b) = (x, tcb_cnode_index 2); tcb_cap_valid (ReplyCap x True Ra) (a, b) s\<rbrakk> \<Longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s
 2. \<And>slots caps ep buffer n mi b na. \<lbrace>valid_reply_caps and valid_reply_masters\<rbrace> set_extra_badge buffer b na \<lbrace>\<lambda>_. valid_reply_caps and valid_reply_masters\<rbrace>
 3. \<And>slots caps ep buffer n mi s. (valid_reply_caps and valid_reply_masters and valid_objs and valid_mdb and K (distinct slots) and (\<lambda>s. \<forall>x\<in>set slots. real_cte_at x s \<and> cte_wp_at (\<lambda>cap. cap = NullCap) x s) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s \<Longrightarrow> (valid_reply_caps and valid_reply_masters) s \<and> (True \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (False \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s)) proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba s t R x Ra. \<lbrakk>valid_reply_caps s; valid_reply_masters s; valid_objs s; valid_mdb s; cap_table_at (length ba) aa s; s \<turnstile> ReplyCap t False R; tcb_cap_valid (ReplyCap t False R) (aa, ba) s; cap_table_at (length b) a s; caps_of_state s (a, b) = Some (ReplyCap x True Ra); cap_master_cap (ReplyCap x True Ra) = cap_master_cap (ReplyCap t False R); is_derived_arch (ReplyCap t False R) (ReplyCap x True Ra); (a, b) = (x, tcb_cnode_index 2); tcb_cap_valid (ReplyCap x True Ra) (a, b) s; s \<turnstile> ReplyCap x True Ra\<rbrakk> \<Longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s
 2. \<And>slots caps ep buffer n mi b na. \<lbrace>valid_reply_caps and valid_reply_masters\<rbrace> set_extra_badge buffer b na \<lbrace>\<lambda>_. valid_reply_caps and valid_reply_masters\<rbrace>
 3. \<And>slots caps ep buffer n mi s. (valid_reply_caps and valid_reply_masters and valid_objs and valid_mdb and K (distinct slots) and (\<lambda>s. \<forall>x\<in>set slots. real_cte_at x s \<and> cte_wp_at (\<lambda>cap. cap = NullCap) x s) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s \<Longrightarrow> (valid_reply_caps and valid_reply_masters) s \<and> (True \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (False \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s)) proof (prove)
goal (3 subgoals):
 1. \<And>a aa ba s t R Ra. \<lbrakk>valid_reply_caps s; valid_reply_masters s; valid_objs s; valid_mdb s; cap_table_at (length ba) aa s; tcb_at aa s \<longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases ba of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst (aa, ba)) st (ReplyCap t False R)) aa s \<and> (ba = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) aa s \<longrightarrow> valid_ipc_buffer_cap (ReplyCap t False R) (tcb_ipc_buffer tcb))); cap_table_at (length (tcb_cnode_index 2)) a s; caps_of_state s (a, tcb_cnode_index 2) = Some (ReplyCap a True Ra); cap_master_cap (ReplyCap a True Ra) = cap_master_cap (ReplyCap t False R); is_derived_arch (ReplyCap t False R) (ReplyCap a True Ra); st_tcb_at (\<lambda>st. AllowGrant \<in> Ra) a s; cap_aligned (ReplyCap t False R); cap_aligned (ReplyCap a True Ra); tcb_at t s; tcb_at a s; AllowWrite \<in> R; AllowWrite \<in> Ra; AllowRead \<notin> R; AllowGrantReply \<notin> R; AllowRead \<notin> Ra; AllowGrantReply \<notin> Ra\<rbrakk> \<Longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s
 2. \<And>slots caps ep buffer n mi b na. \<lbrace>valid_reply_caps and valid_reply_masters\<rbrace> set_extra_badge buffer b na \<lbrace>\<lambda>_. valid_reply_caps and valid_reply_masters\<rbrace>
 3. \<And>slots caps ep buffer n mi s. (valid_reply_caps and valid_reply_masters and valid_objs and valid_mdb and K (distinct slots) and (\<lambda>s. \<forall>x\<in>set slots. real_cte_at x s \<and> cte_wp_at (\<lambda>cap. cap = NullCap) x s) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s \<Longrightarrow> (valid_reply_caps and valid_reply_masters) s \<and> (True \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (False \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s)) proof (prove)
goal (2 subgoals):
 1. \<And>slots caps ep buffer n mi b na. \<lbrace>valid_reply_caps and valid_reply_masters\<rbrace> set_extra_badge buffer b na \<lbrace>\<lambda>_. valid_reply_caps and valid_reply_masters\<rbrace>
 2. \<And>slots caps ep buffer n mi s. (valid_reply_caps and valid_reply_masters and valid_objs and valid_mdb and K (distinct slots) and (\<lambda>s. \<forall>x\<in>set slots. real_cte_at x s \<and> cte_wp_at (\<lambda>cap. cap = NullCap) x s) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s \<Longrightarrow> (valid_reply_caps and valid_reply_masters) s \<and> (True \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (False \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s)) proof (prove)
goal (1 subgoal):
 1. \<And>slots caps ep buffer n mi s. (valid_reply_caps and valid_reply_masters and valid_objs and valid_mdb and K (distinct slots) and (\<lambda>s. \<forall>x\<in>set slots. real_cte_at x s \<and> cte_wp_at (\<lambda>cap. cap = NullCap) x s) and (\<lambda>s. \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s)) s \<Longrightarrow> (valid_reply_caps and valid_reply_masters) s \<and> (True \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (False \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s)) proof (prove)
goal (2 subgoals):
 1. \<And>slots caps s a aa b. \<lbrakk>(a, aa, b) \<in> set caps; valid_reply_caps s; valid_reply_masters s; valid_objs s; valid_mdb s; distinct slots; \<forall>x\<in>set slots. real_cte_at x s \<and> caps_of_state s x = Some NullCap; \<forall>x\<in>set caps. (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<longrightarrow> cap = fst x)) \<and> real_cte_at (snd x) s\<rbrakk> \<Longrightarrow> s \<turnstile> a
 2. \<And>slots caps s a aa b. \<lbrakk>(a, aa, b) \<in> set caps; valid_reply_caps s; valid_reply_masters s; valid_objs s; valid_mdb s; distinct slots; \<forall>x\<in>set slots. real_cte_at x s \<and> caps_of_state s x = Some NullCap; \<forall>x\<in>set caps. (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<longrightarrow> cap = fst x)) \<and> real_cte_at (snd x) s\<rbrakk> \<Longrightarrow> \<exists>cap. caps_of_state s (aa, b) = Some cap \<and> (a \<noteq> NullCap \<longrightarrow> cap \<noteq> a \<longrightarrow> cap = masked_as_full a a) proof (prove)
goal (2 subgoals):
 1. \<And>slots caps s a aa b cap. \<lbrakk>(a, aa, b) \<in> set caps; valid_reply_caps s; valid_reply_masters s; valid_objs s; valid_mdb s; distinct slots; \<forall>x\<in>set slots. real_cte_at x s \<and> caps_of_state s x = Some NullCap; cap_table_at (length b) aa s; caps_of_state s (aa, b) = Some cap; a \<noteq> NullCap \<longrightarrow> cap = a\<rbrakk> \<Longrightarrow> s \<turnstile> a
 2. \<And>slots caps s a aa b. \<lbrakk>(a, aa, b) \<in> set caps; valid_reply_caps s; valid_reply_masters s; valid_objs s; valid_mdb s; distinct slots; \<forall>x\<in>set slots. real_cte_at x s \<and> caps_of_state s x = Some NullCap; \<forall>x\<in>set caps. (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<longrightarrow> cap = fst x)) \<and> real_cte_at (snd x) s\<rbrakk> \<Longrightarrow> \<exists>cap. caps_of_state s (aa, b) = Some cap \<and> (a \<noteq> NullCap \<longrightarrow> cap \<noteq> a \<longrightarrow> cap = masked_as_full a a) proof (prove)
goal (2 subgoals):
 1. \<And>slots caps s a aa b cap. \<lbrakk>(a, aa, b) \<in> set caps; valid_reply_caps s; valid_reply_masters s; valid_objs s; valid_mdb s; distinct slots; \<forall>x\<in>set slots. real_cte_at x s \<and> caps_of_state s x = Some NullCap; cap_table_at (length b) aa s; caps_of_state s (aa, b) = Some cap; a \<noteq> NullCap \<longrightarrow> cap = a; s \<turnstile> cap\<rbrakk> \<Longrightarrow> s \<turnstile> a
 2. \<And>slots caps s a aa b. \<lbrakk>(a, aa, b) \<in> set caps; valid_reply_caps s; valid_reply_masters s; valid_objs s; valid_mdb s; distinct slots; \<forall>x\<in>set slots. real_cte_at x s \<and> caps_of_state s x = Some NullCap; \<forall>x\<in>set caps. (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<longrightarrow> cap = fst x)) \<and> real_cte_at (snd x) s\<rbrakk> \<Longrightarrow> \<exists>cap. caps_of_state s (aa, b) = Some cap \<and> (a \<noteq> NullCap \<longrightarrow> cap \<noteq> a \<longrightarrow> cap = masked_as_full a a) proof (prove)
goal (1 subgoal):
 1. \<And>slots caps s a aa b. \<lbrakk>(a, aa, b) \<in> set caps; valid_reply_caps s; valid_reply_masters s; valid_objs s; valid_mdb s; distinct slots; \<forall>x\<in>set slots. real_cte_at x s \<and> caps_of_state s x = Some NullCap; \<forall>x\<in>set caps. (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<longrightarrow> cap = fst x)) \<and> real_cte_at (snd x) s\<rbrakk> \<Longrightarrow> \<exists>cap. caps_of_state s (aa, b) = Some cap \<and> (a \<noteq> NullCap \<longrightarrow> cap \<noteq> a \<longrightarrow> cap = masked_as_full a a) proof (prove)
goal (1 subgoal):
 1. \<And>slots caps s a aa b. \<lbrakk>(a, aa, b) \<in> set caps; valid_reply_caps s; valid_reply_masters s; valid_objs s; valid_mdb s; distinct slots; \<forall>x\<in>set slots. real_cte_at x s \<and> caps_of_state s x = Some NullCap; (\<exists>cap. caps_of_state s (snd (a, aa, b)) = Some cap \<and> (fst (a, aa, b) \<noteq> NullCap \<longrightarrow> cap = fst (a, aa, b))) \<and> real_cte_at (snd (a, aa, b)) s\<rbrakk> \<Longrightarrow> \<exists>cap. caps_of_state s (aa, b) = Some cap \<and> (a \<noteq> NullCap \<longrightarrow> cap \<noteq> a \<longrightarrow> cap = masked_as_full a a) proof (prove)
goal:
No subgoals!