kings-crown/FVELER_Isabelle huggingface dataset:
theory CSpaceInv_AI

lemma set_cap_rvk_cdt_ct_ms[wp]:
  "\<lbrace>\<lambda>s. P (is_original_cap s)\<rbrace> set_cap p cap \<lbrace>\<lambda>rv s. P (is_original_cap s)\<rbrace>"
  "\<lbrace>\<lambda>s. Q (cur_thread s)\<rbrace> set_cap p cap \<lbrace>\<lambda>rv s. Q (cur_thread s)\<rbrace>"
  "\<lbrace>\<lambda>s. R (machine_state s)\<rbrace> set_cap p cap \<lbrace>\<lambda>rv s. R (machine_state s)\<rbrace>"
  "\<lbrace>\<lambda>s. S (cdt s)\<rbrace> set_cap p cap \<lbrace>\<lambda>rv s. S (cdt s)\<rbrace>"
  "\<lbrace>\<lambda>s. T (idle_thread s)\<rbrace> set_cap p cap \<lbrace>\<lambda>rv s. T (idle_thread s)\<rbrace>"
  "\<lbrace>\<lambda>s. U (arch_state s)\<rbrace> set_cap p cap \<lbrace>\<lambda>rv s. U (arch_state s)\<rbrace>" by (rule set_cap_pspace | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lbrace>\<lambda>s. P (is_original_cap s)\<rbrace> set_cap p cap \<lbrace>\<lambda>rv s. P (is_original_cap s)\<rbrace> &&& \<lbrace>\<lambda>s. Q (cur_thread s)\<rbrace> set_cap p cap \<lbrace>\<lambda>rv s. Q (cur_thread s)\<rbrace> &&& \<lbrace>\<lambda>s. R (machine_state s)\<rbrace> set_cap p cap \<lbrace>\<lambda>rv s. R (machine_state s)\<rbrace>) &&& \<lbrace>\<lambda>s. S (cdt s)\<rbrace> set_cap p cap \<lbrace>\<lambda>rv s. S (cdt s)\<rbrace> &&& \<lbrace>\<lambda>s. T (idle_thread s)\<rbrace> set_cap p cap \<lbrace>\<lambda>rv s. T (idle_thread s)\<rbrace> &&& \<lbrace>\<lambda>s. U (arch_state s)\<rbrace> set_cap p cap \<lbrace>\<lambda>rv s. U (arch_state s)\<rbrace>
theory CSpaceInv_AI

lemma obvious:
  "\<lbrakk> S = {a}; x \<noteq> y; x \<in> S; y \<in> S \<rbrakk> \<Longrightarrow> P" by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>S = {a}; x \<noteq> y; x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> P
theory CSpaceInv_AI

lemma obvious2:
  "\<lbrakk> x \<in> S; \<And>y. y \<noteq> x \<Longrightarrow> y \<notin> S \<rbrakk> \<Longrightarrow> \<exists>x. S = {x}" by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> S; \<And>y. y \<noteq> x \<Longrightarrow> y \<notin> S\<rbrakk> \<Longrightarrow> \<exists>x. S = {x}
theory CSpaceInv_AI

lemma zombie_has_refs:
  "is_zombie cap \<Longrightarrow> gen_obj_refs cap \<noteq> {}" by (clarsimp simp: is_cap_simps cap_irqs_def cap_irq_opt_def
                     gen_obj_refs_def
              split: sum.split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_zombie cap \<Longrightarrow> gen_obj_refs cap \<noteq> {}
theory CSpaceInv_AI

lemma zombie_cap_irqs:
  "is_zombie cap \<Longrightarrow> cap_irqs cap = {}" by (clarsimp simp: is_cap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_zombie cap \<Longrightarrow> cap_irqs cap = {}
theory CSpaceInv_AI

lemma zombie_cap_arch_gen_obj_refs:
  "is_zombie cap \<Longrightarrow> arch_gen_refs cap = {}" by (clarsimp simp: is_cap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_zombie cap \<Longrightarrow> arch_gen_refs cap = {}
theory CSpaceInv_AI

lemma zombies_finalD2:
  "\<lbrakk> fst (get_cap p s) = {(cap, s)}; fst (get_cap p' s) = {(cap', s)};
     p \<noteq> p'; zombies_final s; obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<rbrakk>
     \<Longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap'" by (simp only: zombies_final_def2 cte_wp_at_def simp_thms conj_comms)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>fst (get_cap p s) = {(cap, s)}; fst (get_cap p' s) = {(cap', s)}; p \<noteq> p'; zombies_final s; obj_refs cap \<inter> obj_refs cap' \<noteq> {}\<rbrakk> \<Longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap'
theory CSpaceInv_AI

lemma zombies_finalD3:
  "\<lbrakk> cte_wp_at P p s; cte_wp_at P' p' s; p \<noteq> p'; zombies_final s;
     \<And>cap cap'. \<lbrakk> P cap; P' cap' \<rbrakk> \<Longrightarrow> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<rbrakk>
     \<Longrightarrow> cte_wp_at (Not \<circ> is_zombie) p s \<and> cte_wp_at (Not \<circ> is_zombie) p' s" apply (clarsimp simp: cte_wp_at_def) apply (erule(3) zombies_finalD2) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at P p s; cte_wp_at P' p' s; p \<noteq> p'; zombies_final s; \<And>cap cap'. \<lbrakk>P cap; P' cap'\<rbrakk> \<Longrightarrow> obj_refs cap \<inter> obj_refs cap' \<noteq> {}\<rbrakk> \<Longrightarrow> cte_wp_at (Not \<circ> is_zombie) p s \<and> cte_wp_at (Not \<circ> is_zombie) p' s proof (prove)
goal (1 subgoal):
 1. \<And>cap capa. \<lbrakk>p \<noteq> p'; zombies_final s; \<And>cap cap'. \<lbrakk>P cap; P' cap'\<rbrakk> \<Longrightarrow> obj_refs cap \<inter> obj_refs cap' \<noteq> {}; fst (get_cap p s) = {(cap, s)}; P cap; fst (get_cap p' s) = {(capa, s)}; P' capa\<rbrakk> \<Longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie capa proof (prove)
goal (1 subgoal):
 1. \<And>cap capa. \<lbrakk>p \<noteq> p'; zombies_final s; \<And>cap cap'. \<lbrakk>P cap; P' cap'\<rbrakk> \<Longrightarrow> obj_refs cap \<inter> obj_refs cap' \<noteq> {}; P cap; fst (get_cap p' s) = {(capa, s)}; P' capa\<rbrakk> \<Longrightarrow> obj_refs cap \<inter> obj_refs capa \<noteq> {} proof (prove)
goal:
No subgoals!
theory CSpaceInv_AI

lemma set_cap_final_cap_at:
  "\<lbrace>\<lambda>s. is_final_cap' cap' s \<and>
     cte_wp_at (\<lambda>cap''. (gen_obj_refs cap'' \<inter> gen_obj_refs cap' \<noteq> {})
                            = (gen_obj_refs cap \<inter> gen_obj_refs cap' \<noteq> {})) p s\<rbrace>
     set_cap cap p
   \<lbrace>\<lambda>rv. is_final_cap' cap'\<rbrace>" apply (simp add: is_final_cap'_def2 cte_wp_at_caps_of_state) apply wp apply (elim conjE exEI allEI) apply (clarsimp simp: Int_commute) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. is_final_cap' cap' s \<and> cte_wp_at (\<lambda>cap''. (gen_obj_refs cap'' \<inter> gen_obj_refs cap' \<noteq> {}) = (gen_obj_refs cap \<inter> gen_obj_refs cap' \<noteq> {})) p s\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. is_final_cap' cap'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<exists>a b. \<forall>aa ba. (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> gen_obj_refs cap' \<inter> gen_obj_refs cap \<noteq> {}) = (aa = a \<and> ba = b)) \<and> (\<exists>capa. caps_of_state s p = Some capa \<and> (gen_obj_refs capa \<inter> gen_obj_refs cap' = {}) = (gen_obj_refs cap \<inter> gen_obj_refs cap' = {}))\<rbrace> set_cap cap p \<lbrace>\<lambda>rv s. \<exists>a b. \<forall>aa ba. (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> gen_obj_refs cap' \<inter> gen_obj_refs cap \<noteq> {}) = (aa = a \<and> ba = b)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<exists>a b. \<forall>aa ba. (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> gen_obj_refs cap' \<inter> gen_obj_refs cap \<noteq> {}) = (aa = a \<and> ba = b)) \<and> (\<exists>capa. caps_of_state s p = Some capa \<and> (gen_obj_refs capa \<inter> gen_obj_refs cap' = {}) = (gen_obj_refs cap \<inter> gen_obj_refs cap' = {})) \<Longrightarrow> \<exists>a b. \<forall>aa ba. (\<exists>capa. ((caps_of_state s)(p \<mapsto> cap)) (aa, ba) = Some capa \<and> gen_obj_refs cap' \<inter> gen_obj_refs capa \<noteq> {}) = (aa = a \<and> ba = b) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa a b. \<lbrakk>\<exists>capa. caps_of_state s p = Some capa \<and> (gen_obj_refs capa \<inter> gen_obj_refs cap' = {}) = (gen_obj_refs cap \<inter> gen_obj_refs cap' = {}); (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> gen_obj_refs cap' \<inter> gen_obj_refs cap \<noteq> {}) = (a = x \<and> b = xa)\<rbrakk> \<Longrightarrow> (\<exists>capa. ((caps_of_state s)(p \<mapsto> cap)) (a, b) = Some capa \<and> gen_obj_refs cap' \<inter> gen_obj_refs capa \<noteq> {}) = (a = x \<and> b = xa) proof (prove)
goal:
No subgoals!
theory CSpaceInv_AI

lemma new_cap_iflive:
  "\<lbrace>cte_wp_at ((=) cap.NullCap) p
      and if_live_then_nonz_cap\<rbrace>
     set_cap cap p \<lbrace>\<lambda>rv s. if_live_then_nonz_cap s\<rbrace>" by (wp set_cap_iflive, clarsimp elim!: cte_wp_at_weakenE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at ((=) NullCap) p and if_live_then_nonz_cap\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. if_live_then_nonz_cap\<rbrace>
theory CSpaceInv_AI

lemma new_cap_ifunsafe:
  "\<lbrace>cte_wp_at ((=) cap.NullCap) p
      and if_unsafe_then_cap and ex_cte_cap_wp_to (appropriate_cte_cap cap) p\<rbrace>
     set_cap cap p \<lbrace>\<lambda>rv s. if_unsafe_then_cap s\<rbrace>" by (wp set_cap_ifunsafe, clarsimp elim!: cte_wp_at_weakenE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at ((=) NullCap) p and if_unsafe_then_cap and ex_cte_cap_wp_to (appropriate_cte_cap cap) p\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace>
theory CSpaceInv_AI

lemma ex_zombie_refs_Null[simp]:
  "ex_zombie_refs (c, cap.NullCap) = obj_refs c" by (simp add: ex_zombie_refs_def2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ex_zombie_refs (c, NullCap) = obj_refs c
theory CSpaceInv_AI

lemma new_cap_zombies:
  "\<lbrace>\<lambda>s. cte_wp_at ((=) cap.NullCap) p s \<and>
        (\<forall>r\<in>obj_refs cap. \<forall>p'. p \<noteq> p' \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') p' s
                                   \<longrightarrow> (cte_wp_at (Not \<circ> is_zombie) p' s \<and> \<not> is_zombie cap))
        \<and> zombies_final s\<rbrace>
     set_cap cap p
   \<lbrace>\<lambda>rv. zombies_final\<rbrace>" apply (wp set_cap_zombies) apply (clarsimp elim!: cte_wp_at_weakenE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at ((=) NullCap) p s \<and> (\<forall>r\<in>obj_refs cap. \<forall>p'. p \<noteq> p' \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') p' s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) p' s \<and> \<not> is_zombie cap) \<and> zombies_final s\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. zombies_final\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cte_wp_at ((=) NullCap) p s \<and> (\<forall>r\<in>obj_refs cap. \<forall>p'. p \<noteq> p' \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') p' s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) p' s \<and> \<not> is_zombie cap) \<and> zombies_final s \<Longrightarrow> zombies_final s \<and> cte_wp_at (\<lambda>cap'. \<forall>r\<in>ex_zombie_refs (cap, cap'). \<forall>p'. p \<noteq> p' \<and> cte_wp_at (\<lambda>cap''. r \<in> obj_refs cap'') p' s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) p' s \<and> \<not> is_zombie cap) p s proof (prove)
goal:
No subgoals!
theory CSpaceInv_AI

lemma new_cap_valid_pspace:
  "\<lbrace>cte_wp_at ((=) cap.NullCap) p and valid_cap cap
      and tcb_cap_valid cap p and valid_pspace
      and (\<lambda>s. \<forall>r\<in>obj_refs cap. \<forall>p'. p \<noteq> p' \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') p' s
                                     \<longrightarrow> (cte_wp_at (Not \<circ> is_zombie) p' s \<and> \<not> is_zombie cap))\<rbrace>
     set_cap cap p
   \<lbrace>\<lambda>rv. valid_pspace\<rbrace>" apply (simp add: valid_pspace_def) apply (wp set_cap_valid_objs new_cap_iflive new_cap_ifunsafe new_cap_zombies) apply (auto simp: cte_wp_at_caps_of_state) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at ((=) NullCap) p and valid_cap cap and tcb_cap_valid cap p and valid_pspace and (\<lambda>s. \<forall>r\<in>obj_refs cap. \<forall>p'. p \<noteq> p' \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') p' s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) p' s \<and> \<not> is_zombie cap)\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. valid_pspace\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at ((=) NullCap) p and valid_cap cap and tcb_cap_valid cap p and (valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s))) and (\<lambda>s. \<forall>r\<in>obj_refs cap. \<forall>a b. p \<noteq> (a, b) \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie cap)\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (cte_wp_at ((=) NullCap) p and valid_cap cap and tcb_cap_valid cap p and (valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s))) and (\<lambda>s. \<forall>r\<in>obj_refs cap. \<forall>a b. p \<noteq> (a, b) \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie cap)) s \<Longrightarrow> (valid_objs and valid_cap cap and tcb_cap_valid cap p) s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (cte_wp_at ((=) NullCap) p and if_live_then_nonz_cap) s \<and> (cte_wp_at ((=) NullCap) p s \<and> (\<forall>r\<in>obj_refs cap. \<forall>p'. p \<noteq> p' \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') p' s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) p' s \<and> \<not> is_zombie cap) \<and> zombies_final s) \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s) proof (prove)
goal:
No subgoals!
theory CSpaceInv_AI

lemma gen_obj_refs_distinct_or_equal_corl:
  "\<lbrakk> x \<in> gen_obj_refs cap; x \<in> gen_obj_refs cap' \<rbrakk>
     \<Longrightarrow> gen_obj_refs cap = gen_obj_refs cap'" by (blast intro!: gen_obj_refs_distinct_or_equal)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> gen_obj_refs cap; x \<in> gen_obj_refs cap'\<rbrakk> \<Longrightarrow> gen_obj_refs cap = gen_obj_refs cap'
theory CSpaceInv_AI

lemma obj_refs_cap_irqs_not_both:
  "obj_refs cap \<noteq> {} \<longrightarrow> cap_irqs cap = {} \<and> arch_gen_refs cap = {}" apply (intro impI conjI) apply (clarsimp simp: cap_irqs_def cap_irq_opt_def split: cap.split sum.split_asm) by (clarsimp simp: ex_in_conv[symmetric] obj_ref_not_arch_gen_ref)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_refs cap \<noteq> {} \<longrightarrow> cap_irqs cap = {} \<and> arch_gen_refs cap = {} proof (prove)
goal (2 subgoals):
 1. obj_refs cap \<noteq> {} \<Longrightarrow> cap_irqs cap = {}
 2. obj_refs cap \<noteq> {} \<Longrightarrow> arch_gen_refs cap = {} proof (prove)
goal (1 subgoal):
 1. obj_refs cap \<noteq> {} \<Longrightarrow> arch_gen_refs cap = {}
theory CSpaceInv_AI

lemma delete_no_untyped:
  "\<lbrakk> ((), s') \<in> fst (set_cap cap.NullCap p s);
     \<not> (\<exists>cref. cte_wp_at (\<lambda>c. p' \<in> untyped_range c) cref s) \<rbrakk> \<Longrightarrow>
     \<not> (\<exists>cref. cte_wp_at (\<lambda>c. p' \<in> untyped_range c) cref s')" apply (simp only: cte_wp_at_caps_of_state) apply (erule use_valid, wp) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((), s') \<in> fst (set_cap NullCap p s); \<nexists>cref. cte_wp_at (\<lambda>c. p' \<in> untyped_range c) cref s\<rbrakk> \<Longrightarrow> \<nexists>cref. cte_wp_at (\<lambda>c. p' \<in> untyped_range c) cref s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((), s') \<in> fst (set_cap NullCap p s); \<nexists>cref cap. caps_of_state s cref = Some cap \<and> p' \<in> untyped_range cap\<rbrakk> \<Longrightarrow> \<nexists>cref cap. caps_of_state s' cref = Some cap \<and> p' \<in> untyped_range cap proof (prove)
goal (1 subgoal):
 1. \<nexists>cref cap. caps_of_state s cref = Some cap \<and> p' \<in> untyped_range cap \<Longrightarrow> \<nexists>cref cap. ((caps_of_state s)(p \<mapsto> NullCap)) cref = Some cap \<and> p' \<in> untyped_range cap proof (prove)
goal:
No subgoals!
theory CSpaceInv_AI

lemma get_cap_caps_of_state:
  "(fst (get_cap p s) = {(cap, s)}) = (Some cap = caps_of_state s p)" by (clarsimp simp: caps_of_state_def eq_commute)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (fst (get_cap p s) = {(cap, s)}) = (Some cap = caps_of_state s p)
theory CSpaceInv_AI

lemma abj_ref_none_no_refs:
  "obj_refs c = {} \<Longrightarrow> table_cap_ref c = None" unfolding table_cap_ref_def apply (cases c; simp) subgoal for ac by (cases ac; simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_refs c = {} \<Longrightarrow> table_cap_ref c = None proof (prove)
goal (1 subgoal):
 1. obj_refs c = {} \<Longrightarrow> arch_cap_fun_lift table_cap_ref_arch None c = None proof (prove)
goal (1 subgoal):
 1. \<And>x12. \<lbrakk>aobj_ref x12 = None; c = ArchObjectCap x12\<rbrakk> \<Longrightarrow> (case x12 of ASIDPoolCap obj_ref asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | PageTableCap obj_ref None \<Rightarrow> None | PageTableCap obj_ref (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | PageDirectoryCap obj_ref None \<Rightarrow> None | PageDirectoryCap obj_ref (Some asid) \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | _ \<Rightarrow> None) = None proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aobj_ref ac = None; c = ArchObjectCap ac\<rbrakk> \<Longrightarrow> (case ac of ASIDPoolCap obj_ref asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | PageTableCap obj_ref None \<Rightarrow> None | PageTableCap obj_ref (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | PageDirectoryCap obj_ref None \<Rightarrow> None | PageDirectoryCap obj_ref (Some asid) \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | _ \<Rightarrow> None) = None proof (prove)
goal:
No subgoals!
theory CSpaceInv_AI

lemma no_cap_to_obj_with_diff_ref_Null:
  "no_cap_to_obj_with_diff_ref NullCap S = \<top>" by (rule ext, clarsimp simp: no_cap_to_obj_with_diff_ref_def
                               cte_wp_at_caps_of_state abj_ref_none_no_refs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_cap_to_obj_with_diff_ref NullCap S = (\<lambda>_. True)
theory CSpaceInv_AI

lemma range_not_empty_is_physical:
  "valid_cap cap s \<Longrightarrow> (cap_class cap = PhysicalClass) = (cap_range cap \<noteq> {})" apply (case_tac cap) by (simp_all add: cap_range_def valid_cap_simps cap_aligned_def is_aligned_no_overflow physical_arch_cap_has_ref)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<turnstile> cap \<Longrightarrow> (cap_class cap = PhysicalClass) = (cap_range cap \<noteq> {}) proof (prove)
goal (12 subgoals):
 1. \<lbrakk>s \<turnstile> cap; cap = NullCap\<rbrakk> \<Longrightarrow> (cap_class cap = PhysicalClass) = (cap_range cap \<noteq> {})
 2. \<And>x21 x22 x23 x24. \<lbrakk>s \<turnstile> cap; cap = UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> (cap_class cap = PhysicalClass) = (cap_range cap \<noteq> {})
 3. \<And>x31 x32 x33. \<lbrakk>s \<turnstile> cap; cap = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> (cap_class cap = PhysicalClass) = (cap_range cap \<noteq> {})
 4. \<And>x41 x42 x43. \<lbrakk>s \<turnstile> cap; cap = NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> (cap_class cap = PhysicalClass) = (cap_range cap \<noteq> {})
 5. \<And>x51 x52 x53. \<lbrakk>s \<turnstile> cap; cap = ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> (cap_class cap = PhysicalClass) = (cap_range cap \<noteq> {})
 6. \<And>x61 x62 x63. \<lbrakk>s \<turnstile> cap; cap = CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> (cap_class cap = PhysicalClass) = (cap_range cap \<noteq> {})
 7. \<And>x7. \<lbrakk>s \<turnstile> cap; cap = ThreadCap x7\<rbrakk> \<Longrightarrow> (cap_class cap = PhysicalClass) = (cap_range cap \<noteq> {})
 8. \<lbrakk>s \<turnstile> cap; cap = DomainCap\<rbrakk> \<Longrightarrow> (cap_class cap = PhysicalClass) = (cap_range cap \<noteq> {})
 9. \<lbrakk>s \<turnstile> cap; cap = IRQControlCap\<rbrakk> \<Longrightarrow> (cap_class cap = PhysicalClass) = (cap_range cap \<noteq> {})
 10. \<And>x10. \<lbrakk>s \<turnstile> cap; cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> (cap_class cap = PhysicalClass) = (cap_range cap \<noteq> {})
A total of 12 subgoals...
theory CSpaceInv_AI

lemma zombies_finalE:
  "\<lbrakk> \<not> is_final_cap' cap s; is_zombie cap; zombies_final s;
     cte_wp_at ((=) cap) p s \<rbrakk>
     \<Longrightarrow> P" apply (frule(1) zombies_finalD) apply simp apply (clarsimp simp: cte_wp_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> is_final_cap' cap s; is_zombie cap; zombies_final s; cte_wp_at ((=) cap) p s\<rbrakk> \<Longrightarrow> P proof (prove)
goal (2 subgoals):
 1. \<And>capa. \<lbrakk>\<not> is_final_cap' cap s; is_zombie cap; zombies_final s; cte_wp_at ((=) cap) p s; cap = capa\<rbrakk> \<Longrightarrow> is_zombie capa
 2. \<lbrakk>\<not> is_final_cap' cap s; is_zombie cap; zombies_final s; cte_wp_at ((=) cap) p s; cte_wp_at (\<lambda>cap. is_final_cap' cap s) p s\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> is_final_cap' cap s; is_zombie cap; zombies_final s; cte_wp_at ((=) cap) p s; cte_wp_at (\<lambda>cap. is_final_cap' cap s) p s\<rbrakk> \<Longrightarrow> P proof (prove)
goal:
No subgoals!
theory CSpaceInv_AI

lemma non_unsafe_set_cap:
  "\<lbrace>\<lambda>s. \<not> cte_wp_at ((\<noteq>) cap.NullCap) p' s\<rbrace>
     set_cap cap.NullCap p''
   \<lbrace>\<lambda>rv s. \<not> cte_wp_at ((\<noteq>) cap.NullCap) p' s\<rbrace>" by (simp add: cte_wp_at_caps_of_state | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> cte_wp_at ((\<noteq>) NullCap) p' s\<rbrace> set_cap NullCap p'' \<lbrace>\<lambda>rv s. \<not> cte_wp_at ((\<noteq>) NullCap) p' s\<rbrace>
theory CSpaceInv_AI

lemma cte_refs_obj_refs_elem:
  "x \<in> cte_refs cap y \<Longrightarrow> fst x \<in> obj_refs cap
                            \<or> (\<exists>irq. cap = cap.IRQHandlerCap irq)" by (cases cap, simp_all split: sum.split, fastforce+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> cte_refs cap y \<Longrightarrow> fst x \<in> obj_refs cap \<or> (\<exists>irq. cap = IRQHandlerCap irq)
theory CSpaceInv_AI

lemma get_cap_valid_objs_valid_cap:
  "\<lbrakk> fst (get_cap p s) = {(cap, s)}; valid_objs s \<rbrakk>
     \<Longrightarrow> valid_cap cap s" apply (rule cte_wp_at_valid_objs_valid_cap[where P="(=) cap", simplified]) apply (simp add: cte_wp_at_def) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>fst (get_cap p s) = {(cap, s)}; valid_objs s\<rbrakk> \<Longrightarrow> s \<turnstile> cap proof (prove)
goal (2 subgoals):
 1. \<lbrakk>fst (get_cap p s) = {(cap, s)}; valid_objs s\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) ?p s
 2. \<lbrakk>fst (get_cap p s) = {(cap, s)}; valid_objs s\<rbrakk> \<Longrightarrow> valid_objs s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>fst (get_cap p s) = {(cap, s)}; valid_objs s\<rbrakk> \<Longrightarrow> valid_objs s proof (prove)
goal:
No subgoals!