theory Ipc_AI

lemma (in Ipc_AI) tcl_zombies[wp]:
  "\<And>slots caps ep buffer n mi.
    \<lbrace>zombies_final and valid_objs and valid_mdb and K (distinct slots)
          and (\<lambda>s::'state_ext state. \<forall>slot \<in> set slots. real_cte_at slot s
                                     \<and> cte_wp_at (\<lambda>cap. cap = NullCap) slot s )
          and transfer_caps_srcs caps\<rbrace>
      transfer_caps_loop ep buffer n caps slots mi
    \<lbrace>\<lambda>rv. zombies_final\<rbrace>" apply (rule hoare_pre) apply (rule transfer_caps_loop_presM[where vo=True and em=False and ex=False]) apply (wp cap_insert_zombies) apply clarsimp apply (case_tac "(a, b) = (ab, bb)") apply (clarsimp simp: cte_wp_at_caps_of_state is_derived_def) apply (simp split: if_split_asm) apply ((clarsimp simp: is_cap_simps cap_master_cap_def
                     split: cap.split_asm)+)[2] apply (frule (3) zombies_finalD3) apply (clarsimp simp: is_derived_def is_cap_simps cap_master_cap_simps
                     split: if_split_asm dest!:cap_master_cap_eqDs) apply (drule_tac a=r in equals0D) apply (drule master_cap_obj_refs, simp) apply (fastforce simp: cte_wp_at_caps_of_state is_derived_def
                           is_cap_simps cap_master_cap_def
                    split: if_split_asm cap.split_asm) apply wp apply (clarsimp simp:cte_wp_at_caps_of_state) apply (drule(1) bspec,clarsimp) apply (fastforce dest!:caps_of_state_valid) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>slots caps ep buffer n mi. \<lbrace>zombies_final and valid_objs and valid_mdb and K (distinct slots) and (\<lambda>s. \<forall>slot\<in>set slots. real_cte_at slot s \<and> cte_wp_at (\<lambda>cap. cap = NullCap) slot 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. zombies_final\<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. zombies_final\<rbrace>
 2. \<And>slots caps ep buffer n mi s. (zombies_final and valid_objs and valid_mdb and K (distinct slots) and (\<lambda>s. \<forall>slot\<in>set slots. real_cte_at slot s \<and> cte_wp_at (\<lambda>cap. cap = NullCap) slot 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. zombies_final 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. zombies_final\<rbrace>
 2. \<And>slots caps ep buffer n mi b na. \<lbrace>zombies_final\<rbrace> set_extra_badge buffer b na \<lbrace>\<lambda>_. zombies_final\<rbrace>
 3. \<And>slots caps ep buffer n mi s. (zombies_final and valid_objs and valid_mdb and K (distinct slots) and (\<lambda>s. \<forall>slot\<in>set slots. real_cte_at slot s \<and> cte_wp_at (\<lambda>cap. cap = NullCap) slot 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> zombies_final 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. zombies_final 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> (zombies_final and (\<lambda>s. \<forall>r\<in>obj_refs cap. \<forall>p'. cte_wp_at (\<lambda>c. r \<in> obj_refs c) p' s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) p' s \<and> \<not> is_zombie cap)) s
 2. \<And>slots caps ep buffer n mi b na. \<lbrace>zombies_final\<rbrace> set_extra_badge buffer b na \<lbrace>\<lambda>_. zombies_final\<rbrace>
 3. \<And>slots caps ep buffer n mi s. (zombies_final and valid_objs and valid_mdb and K (distinct slots) and (\<lambda>s. \<forall>slot\<in>set slots. real_cte_at slot s \<and> cte_wp_at (\<lambda>cap. cap = NullCap) slot 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> zombies_final 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 r ab bb. \<lbrakk>r \<in> obj_refs cap; zombies_final 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; cte_wp_at (\<lambda>c. r \<in> obj_refs c) (ab, bb) s\<rbrakk> \<Longrightarrow> cte_wp_at (Not \<circ> is_zombie) (ab, bb) s \<and> \<not> is_zombie cap
 2. \<And>slots caps ep buffer n mi b na. \<lbrace>zombies_final\<rbrace> set_extra_badge buffer b na \<lbrace>\<lambda>_. zombies_final\<rbrace>
 3. \<And>slots caps ep buffer n mi s. (zombies_final and valid_objs and valid_mdb and K (distinct slots) and (\<lambda>s. \<forall>slot\<in>set slots. real_cte_at slot s \<and> cte_wp_at (\<lambda>cap. cap = NullCap) slot 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> zombies_final 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 (4 subgoals):
 1. \<And>cap a b aa ba s r ab bb. \<lbrakk>r \<in> obj_refs cap; zombies_final 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; cte_wp_at (\<lambda>c. r \<in> obj_refs c) (ab, bb) s; (a, b) = (ab, bb)\<rbrakk> \<Longrightarrow> cte_wp_at (Not \<circ> is_zombie) (ab, bb) s \<and> \<not> is_zombie cap
 2. \<And>cap a b aa ba s r ab bb. \<lbrakk>r \<in> obj_refs cap; zombies_final 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; cte_wp_at (\<lambda>c. r \<in> obj_refs c) (ab, bb) s; (a, b) \<noteq> (ab, bb)\<rbrakk> \<Longrightarrow> cte_wp_at (Not \<circ> is_zombie) (ab, bb) s \<and> \<not> is_zombie cap
 3. \<And>slots caps ep buffer n mi b na. \<lbrace>zombies_final\<rbrace> set_extra_badge buffer b na \<lbrace>\<lambda>_. zombies_final\<rbrace>
 4. \<And>slots caps ep buffer n mi s. (zombies_final and valid_objs and valid_mdb and K (distinct slots) and (\<lambda>s. \<forall>slot\<in>set slots. real_cte_at slot s \<and> cte_wp_at (\<lambda>cap. cap = NullCap) slot 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> zombies_final 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 (4 subgoals):
 1. \<And>cap b aa ba s r ab capa. \<lbrakk>r \<in> obj_refs cap; zombies_final 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) ab s; cap \<noteq> NullCap; caps_of_state s (ab, b) = Some capa; r \<in> obj_refs capa; \<not> is_zombie capa; cap \<noteq> IRQControlCap; if is_untyped_cap capa then cap_master_cap capa = cap_master_cap cap \<and> descendants_of (ab, b) (cdt s) = {} else cap_master_cap capa = cap_master_cap cap \<and> (cap_badge capa, cap_badge cap) \<in> capBadge_ordering False; is_master_reply_cap capa = is_reply_cap cap; is_derived_arch cap capa; \<not> is_reply_cap capa; \<not> is_master_reply_cap cap; is_zombie cap\<rbrakk> \<Longrightarrow> False
 2. \<And>cap a b aa ba s r ab bb. \<lbrakk>r \<in> obj_refs cap; zombies_final 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; cte_wp_at (\<lambda>c. r \<in> obj_refs c) (ab, bb) s; (a, b) \<noteq> (ab, bb)\<rbrakk> \<Longrightarrow> cte_wp_at (Not \<circ> is_zombie) (ab, bb) s \<and> \<not> is_zombie cap
 3. \<And>slots caps ep buffer n mi b na. \<lbrace>zombies_final\<rbrace> set_extra_badge buffer b na \<lbrace>\<lambda>_. zombies_final\<rbrace>
 4. \<And>slots caps ep buffer n mi s. (zombies_final and valid_objs and valid_mdb and K (distinct slots) and (\<lambda>s. \<forall>slot\<in>set slots. real_cte_at slot s \<and> cte_wp_at (\<lambda>cap. cap = NullCap) slot 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> zombies_final 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 (5 subgoals):
 1. \<And>cap b aa ba s r ab capa. \<lbrakk>is_master_reply_cap capa = is_reply_cap cap; is_derived_arch cap capa; \<not> is_reply_cap capa; \<not> is_master_reply_cap cap; is_zombie cap; r \<in> obj_refs cap; zombies_final 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) ab s; cap \<noteq> NullCap; caps_of_state s (ab, b) = Some capa; r \<in> obj_refs capa; \<not> is_zombie capa; cap \<noteq> IRQControlCap; is_untyped_cap capa; cap_master_cap capa = cap_master_cap cap \<and> descendants_of (ab, b) (cdt s) = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>cap b aa ba s r ab capa. \<lbrakk>is_master_reply_cap capa = is_reply_cap cap; is_derived_arch cap capa; \<not> is_reply_cap capa; \<not> is_master_reply_cap cap; is_zombie cap; r \<in> obj_refs cap; zombies_final 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) ab s; cap \<noteq> NullCap; caps_of_state s (ab, b) = Some capa; r \<in> obj_refs capa; \<not> is_zombie capa; cap \<noteq> IRQControlCap; \<not> is_untyped_cap capa; cap_master_cap capa = cap_master_cap cap \<and> (cap_badge capa, cap_badge cap) \<in> capBadge_ordering False\<rbrakk> \<Longrightarrow> False
 3. \<And>cap a b aa ba s r ab bb. \<lbrakk>r \<in> obj_refs cap; zombies_final 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; cte_wp_at (\<lambda>c. r \<in> obj_refs c) (ab, bb) s; (a, b) \<noteq> (ab, bb)\<rbrakk> \<Longrightarrow> cte_wp_at (Not \<circ> is_zombie) (ab, bb) s \<and> \<not> is_zombie cap
 4. \<And>slots caps ep buffer n mi b na. \<lbrace>zombies_final\<rbrace> set_extra_badge buffer b na \<lbrace>\<lambda>_. zombies_final\<rbrace>
 5. \<And>slots caps ep buffer n mi s. (zombies_final and valid_objs and valid_mdb and K (distinct slots) and (\<lambda>s. \<forall>slot\<in>set slots. real_cte_at slot s \<and> cte_wp_at (\<lambda>cap. cap = NullCap) slot 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> zombies_final 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 r ab bb. \<lbrakk>r \<in> obj_refs cap; zombies_final 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; cte_wp_at (\<lambda>c. r \<in> obj_refs c) (ab, bb) s; (a, b) \<noteq> (ab, bb)\<rbrakk> \<Longrightarrow> cte_wp_at (Not \<circ> is_zombie) (ab, bb) s \<and> \<not> is_zombie cap
 2. \<And>slots caps ep buffer n mi b na. \<lbrace>zombies_final\<rbrace> set_extra_badge buffer b na \<lbrace>\<lambda>_. zombies_final\<rbrace>
 3. \<And>slots caps ep buffer n mi s. (zombies_final and valid_objs and valid_mdb and K (distinct slots) and (\<lambda>s. \<forall>slot\<in>set slots. real_cte_at slot s \<and> cte_wp_at (\<lambda>cap. cap = NullCap) slot 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> zombies_final 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 (4 subgoals):
 1. \<And>cap a b aa ba s r ab bb capa cap'. \<lbrakk>r \<in> obj_refs cap; zombies_final 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; cte_wp_at (\<lambda>c. r \<in> obj_refs c) (ab, bb) s; (a, b) \<noteq> (ab, bb); is_derived (cdt s) (a, b) cap capa; r \<in> obj_refs cap'\<rbrakk> \<Longrightarrow> obj_refs capa \<inter> obj_refs cap' \<noteq> {}
 2. \<And>cap a b aa ba s r ab bb. \<lbrakk>r \<in> obj_refs cap; zombies_final 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; cte_wp_at (\<lambda>c. r \<in> obj_refs c) (ab, bb) s; (a, b) \<noteq> (ab, bb); cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> cte_wp_at (Not \<circ> is_zombie) (ab, bb) s\<rbrakk> \<Longrightarrow> cte_wp_at (Not \<circ> is_zombie) (ab, bb) s \<and> \<not> is_zombie cap
 3. \<And>slots caps ep buffer n mi b na. \<lbrace>zombies_final\<rbrace> set_extra_badge buffer b na \<lbrace>\<lambda>_. zombies_final\<rbrace>
 4. \<And>slots caps ep buffer n mi s. (zombies_final and valid_objs and valid_mdb and K (distinct slots) and (\<lambda>s. \<forall>slot\<in>set slots. real_cte_at slot s \<and> cte_wp_at (\<lambda>cap. cap = NullCap) slot 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> zombies_final 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 (4 subgoals):
 1. \<And>cap a b aa ba s r ab bb capa cap'. \<lbrakk>r \<in> obj_refs cap'; r \<in> obj_refs cap; zombies_final 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; cte_wp_at (\<lambda>c. r \<in> obj_refs c) (ab, bb) s; a = ab \<longrightarrow> b \<noteq> bb; \<forall>dev r bits f. capa \<noteq> UntypedCap dev r bits f; \<forall>r b n. capa \<noteq> Zombie r b n; cap \<noteq> IRQControlCap; cap_master_cap capa = cap_master_cap cap; (cap_badge capa, cap_badge cap) \<in> capBadge_ordering False; (\<exists>x R. capa = ReplyCap x True R) = (\<exists>x R. cap = ReplyCap x False R); is_derived_arch cap capa; \<forall>x R. capa \<noteq> ReplyCap x False R; \<forall>x R. cap \<noteq> ReplyCap x True R; obj_refs capa \<inter> obj_refs cap' = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>cap a b aa ba s r ab bb. \<lbrakk>r \<in> obj_refs cap; zombies_final 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; cte_wp_at (\<lambda>c. r \<in> obj_refs c) (ab, bb) s; (a, b) \<noteq> (ab, bb); cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> cte_wp_at (Not \<circ> is_zombie) (ab, bb) s\<rbrakk> \<Longrightarrow> cte_wp_at (Not \<circ> is_zombie) (ab, bb) s \<and> \<not> is_zombie cap
 3. \<And>slots caps ep buffer n mi b na. \<lbrace>zombies_final\<rbrace> set_extra_badge buffer b na \<lbrace>\<lambda>_. zombies_final\<rbrace>
 4. \<And>slots caps ep buffer n mi s. (zombies_final and valid_objs and valid_mdb and K (distinct slots) and (\<lambda>s. \<forall>slot\<in>set slots. real_cte_at slot s \<and> cte_wp_at (\<lambda>cap. cap = NullCap) slot 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> zombies_final 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 (4 subgoals):
 1. \<And>cap a b aa ba s r ab bb capa cap'. \<lbrakk>r \<in> obj_refs cap'; r \<in> obj_refs cap; zombies_final 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; cte_wp_at (\<lambda>c. r \<in> obj_refs c) (ab, bb) s; a = ab \<longrightarrow> b \<noteq> bb; \<forall>dev r bits f. capa \<noteq> UntypedCap dev r bits f; \<forall>r b n. capa \<noteq> Zombie r b n; cap \<noteq> IRQControlCap; cap_master_cap capa = cap_master_cap cap; (cap_badge capa, cap_badge cap) \<in> capBadge_ordering False; (\<exists>x R. capa = ReplyCap x True R) = (\<exists>x R. cap = ReplyCap x False R); is_derived_arch cap capa; \<forall>x R. capa \<noteq> ReplyCap x False R; \<forall>x R. cap \<noteq> ReplyCap x True R; r \<notin> obj_refs capa \<inter> obj_refs cap'\<rbrakk> \<Longrightarrow> False
 2. \<And>cap a b aa ba s r ab bb. \<lbrakk>r \<in> obj_refs cap; zombies_final 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; cte_wp_at (\<lambda>c. r \<in> obj_refs c) (ab, bb) s; (a, b) \<noteq> (ab, bb); cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> cte_wp_at (Not \<circ> is_zombie) (ab, bb) s\<rbrakk> \<Longrightarrow> cte_wp_at (Not \<circ> is_zombie) (ab, bb) s \<and> \<not> is_zombie cap
 3. \<And>slots caps ep buffer n mi b na. \<lbrace>zombies_final\<rbrace> set_extra_badge buffer b na \<lbrace>\<lambda>_. zombies_final\<rbrace>
 4. \<And>slots caps ep buffer n mi s. (zombies_final and valid_objs and valid_mdb and K (distinct slots) and (\<lambda>s. \<forall>slot\<in>set slots. real_cte_at slot s \<and> cte_wp_at (\<lambda>cap. cap = NullCap) slot 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> zombies_final 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 r ab bb. \<lbrakk>r \<in> obj_refs cap; zombies_final 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; cte_wp_at (\<lambda>c. r \<in> obj_refs c) (ab, bb) s; (a, b) \<noteq> (ab, bb); cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> cte_wp_at (Not \<circ> is_zombie) (ab, bb) s\<rbrakk> \<Longrightarrow> cte_wp_at (Not \<circ> is_zombie) (ab, bb) s \<and> \<not> is_zombie cap
 2. \<And>slots caps ep buffer n mi b na. \<lbrace>zombies_final\<rbrace> set_extra_badge buffer b na \<lbrace>\<lambda>_. zombies_final\<rbrace>
 3. \<And>slots caps ep buffer n mi s. (zombies_final and valid_objs and valid_mdb and K (distinct slots) and (\<lambda>s. \<forall>slot\<in>set slots. real_cte_at slot s \<and> cte_wp_at (\<lambda>cap. cap = NullCap) slot 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> zombies_final 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>zombies_final\<rbrace> set_extra_badge buffer b na \<lbrace>\<lambda>_. zombies_final\<rbrace>
 2. \<And>slots caps ep buffer n mi s. (zombies_final and valid_objs and valid_mdb and K (distinct slots) and (\<lambda>s. \<forall>slot\<in>set slots. real_cte_at slot s \<and> cte_wp_at (\<lambda>cap. cap = NullCap) slot 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> zombies_final 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. (zombies_final and valid_objs and valid_mdb and K (distinct slots) and (\<lambda>s. \<forall>slot\<in>set slots. real_cte_at slot s \<and> cte_wp_at (\<lambda>cap. cap = NullCap) slot 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> zombies_final 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 s a aa b. \<lbrakk>(a, aa, b) \<in> set caps; zombies_final s; valid_objs s; valid_mdb s; distinct slots; \<forall>slot\<in>set slots. real_cte_at slot s \<and> caps_of_state s slot = 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 \<and> (\<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 cap. \<lbrakk>(a, aa, b) \<in> set caps; zombies_final s; valid_objs s; valid_mdb s; distinct slots; \<forall>slot\<in>set slots. real_cte_at slot s \<and> caps_of_state s slot = 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 proof (prove)
goal:
No subgoals!