kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchVSpace_AI

lemma new_lookups_trans:
  "new_lookups^* = (new_lookups \<union> Id)" apply (rule set_eqI, clarsimp, rule iffI) apply (erule rtranclE) apply simp apply (erule rtranclE) apply simp apply (drule(1) double_new_lookup) apply simp apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. new_lookups\<^sup>* = new_lookups\<^sup>= proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. ((a, b), aa, ba) \<in> new_lookups\<^sup>* \<Longrightarrow> ((a, b), aa, ba) \<in> new_lookups \<or> a = aa \<and> b = ba
 2. \<And>a b aa ba. ((a, b), aa, ba) \<in> new_lookups \<or> a = aa \<and> b = ba \<Longrightarrow> ((a, b), aa, ba) \<in> new_lookups\<^sup>* proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba. (a, b) = (aa, ba) \<Longrightarrow> ((a, b), aa, ba) \<in> new_lookups \<or> a = aa \<and> b = ba
 2. \<And>a b aa ba y. \<lbrakk>((a, b), y) \<in> new_lookups\<^sup>*; (y, aa, ba) \<in> new_lookups\<rbrakk> \<Longrightarrow> ((a, b), aa, ba) \<in> new_lookups \<or> a = aa \<and> b = ba
 3. \<And>a b aa ba. ((a, b), aa, ba) \<in> new_lookups \<or> a = aa \<and> b = ba \<Longrightarrow> ((a, b), aa, ba) \<in> new_lookups\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba y. \<lbrakk>((a, b), y) \<in> new_lookups\<^sup>*; (y, aa, ba) \<in> new_lookups\<rbrakk> \<Longrightarrow> ((a, b), aa, ba) \<in> new_lookups \<or> a = aa \<and> b = ba
 2. \<And>a b aa ba. ((a, b), aa, ba) \<in> new_lookups \<or> a = aa \<and> b = ba \<Longrightarrow> ((a, b), aa, ba) \<in> new_lookups\<^sup>* proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba y. \<lbrakk>(y, aa, ba) \<in> new_lookups; (a, b) = y\<rbrakk> \<Longrightarrow> ((a, b), aa, ba) \<in> new_lookups \<or> a = aa \<and> b = ba
 2. \<And>a b aa ba y ya. \<lbrakk>(y, aa, ba) \<in> new_lookups; ((a, b), ya) \<in> new_lookups\<^sup>*; (ya, y) \<in> new_lookups\<rbrakk> \<Longrightarrow> ((a, b), aa, ba) \<in> new_lookups \<or> a = aa \<and> b = ba
 3. \<And>a b aa ba. ((a, b), aa, ba) \<in> new_lookups \<or> a = aa \<and> b = ba \<Longrightarrow> ((a, b), aa, ba) \<in> new_lookups\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba y ya. \<lbrakk>(y, aa, ba) \<in> new_lookups; ((a, b), ya) \<in> new_lookups\<^sup>*; (ya, y) \<in> new_lookups\<rbrakk> \<Longrightarrow> ((a, b), aa, ba) \<in> new_lookups \<or> a = aa \<and> b = ba
 2. \<And>a b aa ba. ((a, b), aa, ba) \<in> new_lookups \<or> a = aa \<and> b = ba \<Longrightarrow> ((a, b), aa, ba) \<in> new_lookups\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba y ya. \<lbrakk>(y, aa, ba) \<in> new_lookups; ((a, b), ya) \<in> new_lookups\<^sup>*; False\<rbrakk> \<Longrightarrow> ((a, b), aa, ba) \<in> new_lookups \<or> a = aa \<and> b = ba
 2. \<And>a b aa ba. ((a, b), aa, ba) \<in> new_lookups \<or> a = aa \<and> b = ba \<Longrightarrow> ((a, b), aa, ba) \<in> new_lookups\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. ((a, b), aa, ba) \<in> new_lookups \<or> a = aa \<and> b = ba \<Longrightarrow> ((a, b), aa, ba) \<in> new_lookups\<^sup>* proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma arch_state [simp]:
  "arch_state s' = arch_state s" by (simp add: s'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arch_state s' = arch_state s
theory ArchVSpace_AI

lemma vs_lookup:
  "vs_lookup s' \<subseteq> vs_lookup s \<union> new_lookups^* `` vs_lookup s" unfolding vs_lookup_def apply (rule order_trans) apply (rule Image_mono [OF _ order_refl]) apply (rule vs_lookup_trans) apply (clarsimp simp: relcomp_Image Un_Image) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. vs_lookup s' \<subseteq> vs_lookup s \<union> new_lookups\<^sup>* `` vs_lookup s proof (prove)
goal (1 subgoal):
 1. (vs_lookup1 s')\<^sup>* `` vs_asid_refs (asid_table s') \<subseteq> (vs_lookup1 s)\<^sup>* `` vs_asid_refs (asid_table s) \<union> new_lookups\<^sup>* `` (vs_lookup1 s)\<^sup>* `` vs_asid_refs (asid_table s) proof (prove)
goal (2 subgoals):
 1. (vs_lookup1 s')\<^sup>* `` vs_asid_refs (asid_table s') \<subseteq> ?y
 2. ?y \<subseteq> (vs_lookup1 s)\<^sup>* `` vs_asid_refs (asid_table s) \<union> new_lookups\<^sup>* `` (vs_lookup1 s)\<^sup>* `` vs_asid_refs (asid_table s) proof (prove)
goal (2 subgoals):
 1. (vs_lookup1 s')\<^sup>* \<subseteq> ?r3
 2. ?r3 `` vs_asid_refs (asid_table s') \<subseteq> (vs_lookup1 s)\<^sup>* `` vs_asid_refs (asid_table s) \<union> new_lookups\<^sup>* `` (vs_lookup1 s)\<^sup>* `` vs_asid_refs (asid_table s) proof (prove)
goal (1 subgoal):
 1. ((vs_lookup1 s)\<^sup>* \<union> (vs_lookup1 s)\<^sup>* O new_lookups\<^sup>*) `` vs_asid_refs (asid_table s') \<subseteq> (vs_lookup1 s)\<^sup>* `` vs_asid_refs (asid_table s) \<union> new_lookups\<^sup>* `` (vs_lookup1 s)\<^sup>* `` vs_asid_refs (asid_table s) proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma vs_lookup2:
  "vs_lookup s' \<subseteq> vs_lookup s \<union> (new_lookups `` vs_lookup s)" apply (rule order_trans, rule vs_lookup) apply (auto simp add: vs_lookup new_lookups_trans) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. vs_lookup s' \<subseteq> vs_lookup s \<union> new_lookups `` vs_lookup s proof (prove)
goal (1 subgoal):
 1. vs_lookup s \<union> new_lookups\<^sup>* `` vs_lookup s \<subseteq> vs_lookup s \<union> new_lookups `` vs_lookup s proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma global_pde_graph_ofI:
 " \<lbrakk>pd x = pde; pde_ref pde = Some v\<rbrakk>
  \<Longrightarrow> (x, v) \<in> graph_of (pde_ref o pd)" by (clarsimp simp: graph_of_def pde_ref_def comp_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pd x = pde; pde_ref pde = Some v\<rbrakk> \<Longrightarrow> (x, v) \<in> graph_of (pde_ref \<circ> pd)
theory ArchVSpace_AI

lemma glob_vs_refs_subset:
  " vs_refs x \<subseteq> glob_vs_refs x" apply (clarsimp simp: glob_vs_refs_def vs_refs_def) apply (clarsimp split: Structures_A.kernel_object.splits arch_kernel_obj.splits) apply (rule pair_imageI) apply (simp add: graph_of_def split:if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. vs_refs x \<subseteq> glob_vs_refs x proof (prove)
goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> (case x of ArchObj (ASIDPool pool) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | ArchObj (PageDirectory pd) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) | ArchObj _ \<Rightarrow> {} | _ \<Rightarrow> {}) \<Longrightarrow> (a, b) \<in> (case x of ArchObj (ASIDPool pool) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | ArchObj (PageDirectory pd) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (pde_ref \<circ> pd) | ArchObj _ \<Rightarrow> {} | _ \<Rightarrow> {}) proof (prove)
goal (1 subgoal):
 1. \<And>x3 aa ba. \<lbrakk>x = ArchObj (PageDirectory x3); (aa, ba) \<in> graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (x3 x))\<rbrakk> \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) aa) (Some APageDirectory), ba) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (pde_ref \<circ> x3) proof (prove)
goal (1 subgoal):
 1. \<And>x3 aa ba. \<lbrakk>x = ArchObj (PageDirectory x3); (aa, ba) \<in> graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (x3 x))\<rbrakk> \<Longrightarrow> (aa, ba) \<in> graph_of (pde_ref \<circ> x3) proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma vs_refs_pages_pdI:
  "\<lbrakk>pde_ref_pages (pd x) = Some a; x \<notin> kernel_mapping_slots\<rbrakk>
    \<Longrightarrow> (VSRef (ucast x) (Some APageDirectory), a) \<in> vs_refs_pages (ArchObj (PageDirectory pd))" by (auto simp: pde_ref_pages_def vs_refs_pages_def graph_of_def image_def split: pde.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pde_ref_pages (pd x) = Some a; x \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) x) (Some APageDirectory), a) \<in> vs_refs_pages (ArchObj (PageDirectory pd))
theory ArchVSpace_AI

lemma pde_ref_pde_ref_pagesI[elim!]:
  "pde_ref (pd x) = Some a \<Longrightarrow> pde_ref_pages (pd x) = Some a" by (auto simp: pde_ref_def pde_ref_pages_def split: pde.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pde_ref (pd x) = Some a \<Longrightarrow> pde_ref_pages (pd x) = Some a
theory ArchVSpace_AI

lemma vs_refs_pdI2:
  "\<lbrakk>pd r = PageTablePDE x a b; r \<notin> kernel_mapping_slots\<rbrakk>
   \<Longrightarrow> (VSRef (ucast r) (Some APageDirectory), ptrFromPAddr x) \<in> vs_refs (ArchObj (PageDirectory pd))" by (auto simp: vs_refs_def pde_ref_def graph_of_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pd r = PageTablePDE x a b; r \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), ptrFromPAddr x) \<in> vs_refs (ArchObj (PageDirectory pd))
theory ArchVSpace_AI

lemma vs_refs_add_one:
  "\<lbrakk>pde_ref (pd p) = None; p \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow>
   vs_refs (ArchObj (PageDirectory (pd (p := pde)))) =
   vs_refs (ArchObj (PageDirectory pd))
       \<union> Pair (VSRef (ucast p) (Some APageDirectory)) ` set_option (pde_ref pde)" by (simp add: vs_refs_add_one')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pde_ref (pd p) = None; p \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> vs_refs (ArchObj (PageDirectory (pd(p := pde)))) = vs_refs (ArchObj (PageDirectory pd)) \<union> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref pde)
theory ArchVSpace_AI

lemma vs_refs_pages_add_one:
  "\<lbrakk>pde_ref_pages (pd p) = None; p \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow>
   vs_refs_pages (ArchObj (PageDirectory (pd (p := pde)))) =
   vs_refs_pages (ArchObj (PageDirectory pd))
       \<union> Pair (VSRef (ucast p) (Some APageDirectory)) ` set_option (pde_ref_pages pde)" by (simp add: vs_refs_pages_add_one')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pde_ref_pages (pd p) = None; p \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> vs_refs_pages (ArchObj (PageDirectory (pd(p := pde)))) = vs_refs_pages (ArchObj (PageDirectory pd)) \<union> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref_pages pde)
theory ArchVSpace_AI

lemma valid_cap_to_pt_cap:
  "\<lbrakk>valid_cap c s; obj_refs c = {p}; page_table_at p s\<rbrakk> \<Longrightarrow> is_pt_cap c" by (clarsimp simp: valid_cap_def obj_at_def is_obj_defs is_pt_cap_def
              split: cap.splits option.splits arch_cap.splits if_splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<turnstile> c; obj_refs c = {p}; typ_at (AArch APageTable) p s\<rbrakk> \<Longrightarrow> is_pt_cap c
theory ArchVSpace_AI

lemma mask_shift_mask_helper:
  "(p && mask pd_bits >> 2) && mask 12 = (p && mask pd_bits >> 2)" apply (rule word_eqI) apply (simp add: word_size pd_bits_def pageBits_def nth_shiftr conj_comms) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (p && mask pd_bits >> 2) && mask 12 = p && mask pd_bits >> 2 proof (prove)
goal (1 subgoal):
 1. \<And>n. n < size ((p && mask pd_bits >> 2) && mask 12) \<longrightarrow> ((p && mask pd_bits >> 2) && mask 12) !! n = (p && mask pd_bits >> 2) !! n proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma ucast_ucast_mask_shift_helper:
  "ucast (ucast (p && mask pd_bits >> 2 :: word32) :: 12 word)
        = (p && mask pd_bits >> 2 :: word32)" apply (rule ucast_ucast_len) apply (rule shiftr_less_t2n) apply (simp add: pd_bits_def pageBits_def) apply (rule order_less_le_trans, rule and_mask_less_size) apply (simp add: word_size)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)) = p && mask pd_bits >> 2 proof (prove)
goal (1 subgoal):
 1. p && mask pd_bits >> 2 < 2 ^ LENGTH(12) proof (prove)
goal (1 subgoal):
 1. p && mask pd_bits < 2 ^ (2 + LENGTH(12)) proof (prove)
goal (1 subgoal):
 1. p && mask 14 < 0x4000 proof (prove)
goal (2 subgoals):
 1. 14 < size p
 2. 2 ^ 14 \<le> 0x4000 proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma unat_ucast_pd_bits_shift:
  "unat (ucast ((p :: word32) && mask pd_bits >> 2) :: 12 word)
       = unat (p && mask pd_bits >> 2)" apply (simp only: unat_ucast) apply (rule mod_less) apply (rule unat_less_power) apply (simp add: word_bits_def) apply (rule shiftr_less_t2n) apply (rule order_le_less_trans [OF word_and_le1]) apply (simp add: pd_bits_def pageBits_def mask_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)) = unat (p && mask pd_bits >> 2) proof (prove)
goal (1 subgoal):
 1. unat (p && mask pd_bits >> 2) mod 2 ^ LENGTH(12) = unat (p && mask pd_bits >> 2) proof (prove)
goal (1 subgoal):
 1. unat (p && mask pd_bits >> 2) < 2 ^ LENGTH(12) proof (prove)
goal (2 subgoals):
 1. LENGTH(12) < LENGTH(32)
 2. p && mask pd_bits >> 2 < 2 ^ LENGTH(12) proof (prove)
goal (1 subgoal):
 1. p && mask pd_bits >> 2 < 2 ^ LENGTH(12) proof (prove)
goal (1 subgoal):
 1. p && mask pd_bits < 2 ^ (2 + LENGTH(12)) proof (prove)
goal (1 subgoal):
 1. mask pd_bits < 2 ^ (2 + LENGTH(12)) proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma kernel_vsrefs_kernel_mapping_slots:
  "(ucast (p && mask pd_bits >> 2) \<in> kernel_mapping_slots) =
    (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) \<in> kernel_vsrefs)" by (clarsimp simp: kernel_mapping_slots_def kernel_vsrefs_def
                     word_le_nat_alt unat_ucast_pd_bits_shift
                     kernel_base_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<in> kernel_mapping_slots) = (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) \<in> kernel_vsrefs)
theory ArchVSpace_AI

lemma vs_lookup_vs_lookup_pagesI:
  "\<lbrakk>(r \<rhd> p) s; (r' \<unrhd> p) s; valid_vspace_objs s; valid_asid_table (arm_asid_table (arch_state s)) s\<rbrakk>
   \<Longrightarrow> (r' \<rhd> p) s" by (erule (5) vs_lookup_vs_lookup_pagesI'[OF _ vs_lookup_typI])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(r \<rhd> p) s; (r' \<unrhd> p) s; valid_vspace_objs s; valid_asid_table (asid_table s) s\<rbrakk> \<Longrightarrow> (r' \<rhd> p) s
theory ArchVSpace_AI

lemma set_cap_empty_pde:
  "\<lbrace>empty_pde_at p and cte_at p'\<rbrace> set_cap cap p' \<lbrace>\<lambda>_. empty_pde_at p\<rbrace>" apply (simp add: empty_pde_at_def) apply (rule hoare_pre) apply (wp set_cap_obj_at_other hoare_vcg_ex_lift) apply clarsimp apply (rule exI, rule conjI, assumption) apply (erule conjI) apply (clarsimp simp: cte_wp_at_cases obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>empty_pde_at p and cte_wp_at (\<lambda>_. True) p'\<rbrace> set_cap cap p' \<lbrace>\<lambda>_. empty_pde_at p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<exists>pd. ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s \<and> pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)) = InvalidPDE) and cte_wp_at (\<lambda>_. True) p'\<rbrace> set_cap cap p' \<lbrace>\<lambda>_ s. \<exists>pd. ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s \<and> pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)) = InvalidPDE\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> set_cap cap p' \<lbrace>\<lambda>_ s. \<exists>pd. ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s \<and> pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)) = InvalidPDE\<rbrace>
 2. \<And>s. ((\<lambda>s. \<exists>pd. ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s \<and> pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)) = InvalidPDE) and cte_wp_at (\<lambda>_. True) p') s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. \<exists>pd. ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s \<and> pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)) = InvalidPDE) and cte_wp_at (\<lambda>_. True) p') s \<Longrightarrow> \<exists>x. (ako_at (PageDirectory x) (p && ~~ mask pd_bits) s \<and> x (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)) = InvalidPDE) \<and> p && ~~ mask pd_bits \<noteq> fst p' proof (prove)
goal (1 subgoal):
 1. \<And>s pd. \<lbrakk>cte_wp_at (\<lambda>_. True) p' s; ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s; pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)) = InvalidPDE\<rbrakk> \<Longrightarrow> \<exists>x. ako_at (PageDirectory x) (p && ~~ mask pd_bits) s \<and> x (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)) = InvalidPDE \<and> p && ~~ mask pd_bits \<noteq> fst p' proof (prove)
goal (1 subgoal):
 1. \<And>s pd. \<lbrakk>cte_wp_at (\<lambda>_. True) p' s; ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s; pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)) = InvalidPDE\<rbrakk> \<Longrightarrow> pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)) = InvalidPDE \<and> p && ~~ mask pd_bits \<noteq> fst p' proof (prove)
goal (1 subgoal):
 1. \<And>s pd. \<lbrakk>cte_wp_at (\<lambda>_. True) p' s; ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> p && ~~ mask pd_bits \<noteq> fst p' proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma valid_cap_obj_ref_pt_pd:
  "\<lbrakk> s \<turnstile> cap; s \<turnstile> cap'; obj_refs cap = obj_refs cap' \<rbrakk>
       \<Longrightarrow> (is_pt_cap cap \<longrightarrow> is_pt_cap cap')
         \<and> (is_pd_cap cap \<longrightarrow> is_pd_cap cap')" by (auto simp: is_cap_simps valid_cap_def
                 obj_at_def is_ep is_ntfn is_cap_table
                 is_tcb a_type_def
          split: cap.split_asm if_split_asm
                 arch_cap.split_asm option.split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<turnstile> cap; s \<turnstile> cap'; obj_refs cap = obj_refs cap'\<rbrakk> \<Longrightarrow> (is_pt_cap cap \<longrightarrow> is_pt_cap cap') \<and> (is_pd_cap cap \<longrightarrow> is_pd_cap cap')
theory ArchVSpace_AI

lemma is_pt_pd_cap_asid_None_table_ref:
  "is_pt_cap cap \<or> is_pd_cap cap
     \<Longrightarrow> ((table_cap_ref cap = None) = (cap_asid cap = None))" by (auto simp: is_cap_simps table_cap_ref_def cap_asid_def
          split: option.split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_pt_cap cap \<or> is_pd_cap cap \<Longrightarrow> (table_cap_ref cap = None) = (cap_asid cap = None)
theory ArchVSpace_AI

lemma valid_idle_store_pte[wp]:
  "\<lbrace>valid_idle\<rbrace> store_pte y pte \<lbrace>\<lambda>rv. valid_idle\<rbrace>" apply (simp add: store_pte_def set_pt_def) including unfold_objects apply (wpsimp wp: set_pt_valid_idle) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle\<rbrace> store_pte y pte \<lbrace>\<lambda>rv. valid_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle\<rbrace> do pt <- get_pt (y && ~~ mask pt_bits);
set_object (y && ~~ mask pt_bits) (ArchObj (PageTable (pt(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := pte))))
od \<lbrace>\<lambda>rv. valid_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle\<rbrace> do pt <- get_pt (y && ~~ mask pt_bits);
set_object (y && ~~ mask pt_bits) (ArchObj (PageTable (pt(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := pte))))
od \<lbrace>\<lambda>rv. valid_idle\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma vs_refs_pdI3:
  "\<lbrakk>pde_ref (pd x) = Some p; x \<notin> kernel_mapping_slots\<rbrakk>
   \<Longrightarrow> (VSRef (ucast x) (Some APageDirectory), p) \<in> vs_refs (ArchObj (PageDirectory pd))" by (auto simp: pde_ref_def vs_refs_def graph_of_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pde_ref (pd x) = Some p; x \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) x) (Some APageDirectory), p) \<in> vs_refs (ArchObj (PageDirectory pd))
theory ArchVSpace_AI

lemma same_refs_lD:
  "\<lbrakk>same_refs (Inl(pte,p # slots)) cap s\<rbrakk>
 \<Longrightarrow> (\<exists>p. pte_ref_pages pte = Some p \<and> p \<in> obj_refs cap) \<and>
  (\<forall>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s \<longrightarrow>
  vs_cap_ref cap = Some (VSRef (p && mask pt_bits >> 2) (Some APageTable) # ref))" by (clarsimp simp:same_refs_def split:list.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. same_refs (Inl (pte, p # slots)) cap s \<Longrightarrow> (\<exists>p. pte_ref_pages pte = Some p \<and> p \<in> obj_refs cap) \<and> (\<forall>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s \<longrightarrow> vs_cap_ref cap = Some (VSRef (p && mask pt_bits >> 2) (Some APageTable) # ref))
theory ArchVSpace_AI

lemma same_refs_rD:
  "\<lbrakk>same_refs (Inr(pde,p # slots)) cap s\<rbrakk>
 \<Longrightarrow>  (\<exists>p. pde_ref_pages pde = Some p \<and> p \<in> obj_refs cap) \<and>
         (\<forall>ref. (ref \<rhd> (p && ~~ mask pd_bits)) s \<longrightarrow>
               vs_cap_ref cap =
               Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # ref))" by (clarsimp simp:same_refs_def split:list.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. same_refs (Inr (pde, p # slots)) cap s \<Longrightarrow> (\<exists>p. pde_ref_pages pde = Some p \<and> p \<in> obj_refs cap) \<and> (\<forall>ref. (ref \<rhd> (p && ~~ mask pd_bits)) s \<longrightarrow> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # ref))
theory ArchVSpace_AI

lemma simpler_store_pde_def:
  "store_pde p pde s =
    (case kheap s (p && ~~ mask pd_bits) of
          Some (ArchObj (PageDirectory pd)) =>
            ({((), s\<lparr>kheap := (kheap s)(p && ~~ mask pd_bits \<mapsto>
                                        ArchObj (PageDirectory (pd(ucast (p && mask pd_bits >> 2) := pde))))\<rparr>)}, False)
        | _ => ({}, True))" by (auto simp: store_pde_def simpler_set_pd_def get_object_def simpler_gets_def assert_def
                 return_def fail_def set_object_def get_def put_def bind_def get_pd_def
           split: Structures_A.kernel_object.splits option.splits arch_kernel_obj.splits if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. store_pde p pde s = (case kheap s (p && ~~ mask pd_bits) of None \<Rightarrow> ({}, True) | Some (ArchObj (PageDirectory pd)) \<Rightarrow> ({((), s\<lparr>kheap := (kheap s)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))\<rparr>)}, False) | Some (ArchObj _) \<Rightarrow> ({}, True) | Some _ \<Rightarrow> ({}, True))