kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchUntyped_AI

lemma nonempty_default[simp, Untyped_AI_assms]:
  "tp \<noteq> Untyped \<Longrightarrow> \<not> nonempty_table S (default_object tp dev us)" apply (case_tac tp, simp_all add: default_object_def nonempty_table_def
                                    a_type_def) apply (rename_tac aobject_type) apply (case_tac aobject_type, simp_all add: default_arch_object_def) apply (simp_all add: empty_table_def pde_ref_def valid_pde_mappings_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tp \<noteq> Untyped \<Longrightarrow> \<not> nonempty_table S (default_object tp dev us) proof (prove)
goal (1 subgoal):
 1. \<And>x6. tp = ArchObject x6 \<Longrightarrow> (case default_arch_object x6 dev us of ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz) \<noteq> APageTable \<and> (case default_arch_object x6 dev us of ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz) \<noteq> APageDirectory \<or> empty_table S (ArchObj (default_arch_object x6 dev us)) proof (prove)
goal (1 subgoal):
 1. \<And>aobject_type. tp = ArchObject aobject_type \<Longrightarrow> (case default_arch_object aobject_type dev us of ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz) \<noteq> APageTable \<and> (case default_arch_object aobject_type dev us of ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz) \<noteq> APageDirectory \<or> empty_table S (ArchObj (default_arch_object aobject_type dev us)) proof (prove)
goal (2 subgoals):
 1. \<And>aobject_type. \<lbrakk>tp = ArchObject PageTableObj; aobject_type = PageTableObj\<rbrakk> \<Longrightarrow> empty_table S (ArchObj (PageTable (\<lambda>x. InvalidPTE)))
 2. \<And>aobject_type. \<lbrakk>tp = ArchObject PageDirectoryObj; aobject_type = PageDirectoryObj\<rbrakk> \<Longrightarrow> empty_table S (ArchObj (PageDirectory (\<lambda>x. InvalidPDE))) proof (prove)
goal:
No subgoals!
theory ArchUntyped_AI

lemma set_pd_cte_wp_at_iin[wp]:
  "\<lbrace>\<lambda>s. P (cte_wp_at (P' (interrupt_irq_node s)) p s)\<rbrace>
   set_pd q pd
   \<lbrace>\<lambda>_ s. P (cte_wp_at (P' (interrupt_irq_node s)) p s)\<rbrace>" apply (simp add: set_pd_def) including unfold_objects apply (wpsimp wp: set_object_wp_strong
              simp: a_type_def cte_wp_at_after_update') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cte_wp_at (P' (interrupt_irq_node s)) p s)\<rbrace> set_pd q pd \<lbrace>\<lambda>_ s. P (cte_wp_at (P' (interrupt_irq_node s)) p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cte_wp_at (P' (interrupt_irq_node s)) p s)\<rbrace> set_object q (ArchObj (PageDirectory pd)) \<lbrace>\<lambda>_ s. P (cte_wp_at (P' (interrupt_irq_node s)) p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cte_wp_at (P' (interrupt_irq_node s)) p s)\<rbrace> set_object q (ArchObj (PageDirectory pd)) \<lbrace>\<lambda>_ s. P (cte_wp_at (P' (interrupt_irq_node s)) p s)\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchUntyped_AI

lemma create_cap_ioports[wp, Untyped_AI_assms]:
  "\<lbrace>valid_ioports and cte_wp_at (\<lambda>_. True) cref\<rbrace> create_cap tp sz p dev (cref,oref) \<lbrace>\<lambda>rv. valid_ioports\<rbrace>" by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_ioports and cte_wp_at (\<lambda>_. True) cref\<rbrace> create_cap tp sz p dev (cref, oref) \<lbrace>\<lambda>rv. valid_ioports\<rbrace>
theory Arch_AI

lemma invs_strgs:
  "invs s \<longrightarrow> valid_pspace s"
  "invs s \<longrightarrow> valid_mdb s"
  "invs s \<longrightarrow> valid_objs s"
  "invs s \<longrightarrow> pspace_aligned s" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (invs s \<longrightarrow> valid_pspace s &&& invs s \<longrightarrow> valid_mdb s) &&& invs s \<longrightarrow> valid_objs s &&& invs s \<longrightarrow> pspace_aligned s
theory Arch_AI

lemma assocs_empty_dom_comp:
  "(- dom f \<inter> Collect P = {}) = null (filter (\<lambda>(x, y). P x \<and> y = None) (assocs f))" apply (subst assocs_dom_comp [symmetric]) apply (subst empty_set_is_null) apply (simp add: null_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (- dom f \<inter> Collect P = {}) = null (filter (\<lambda>(x, y). P x \<and> y = None) (assocs f)) proof (prove)
goal (1 subgoal):
 1. (set (map fst (filter (\<lambda>(x, y). P x \<and> y = None) (assocs f))) = {}) = null (filter (\<lambda>(x, y). P x \<and> y = None) (assocs f)) proof (prove)
goal (1 subgoal):
 1. null (map fst (filter (\<lambda>(x, y). P x \<and> y = None) (assocs f))) = null (filter (\<lambda>(x, y). P x \<and> y = None) (assocs f)) proof (prove)
goal:
No subgoals!
theory Arch_AI

lemma dom_hd_assocsD:
  fixes P
  defines "filter_assocs f \<equiv> filter (\<lambda>(x,y). P x \<and> y = None) (assocs f)"
  assumes d: "- dom f \<inter> Collect P \<noteq> {}"
  shows "fst (hd (filter_assocs f)) \<notin> dom f \<and> P (fst (hd (filter_assocs f)))" proof - from d have "\<not>null (filter_assocs f)" unfolding filter_assocs_def by (simp add: assocs_empty_dom_comp) hence "hd (filter_assocs f) \<in> set (filter_assocs f)" by (clarsimp simp: null_def neq_Nil_conv) thus ?thesis unfolding filter_assocs_def by (clarsimp simp: in_assocs_is_fun) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fst (hd (filter_assocs f)) \<notin> dom f \<and> P (fst (hd (filter_assocs f))) proof (state)
goal (1 subgoal):
 1. fst (hd (filter_assocs f)) \<notin> dom f \<and> P (fst (hd (filter_assocs f))) proof (chain)
picking this:
- dom f \<inter> Collect P \<noteq> {} proof (prove)
using this:
- dom f \<inter> Collect P \<noteq> {}

goal (1 subgoal):
 1. \<not> null (filter_assocs f) proof (prove)
using this:
- dom f \<inter> Collect P \<noteq> {}

goal (1 subgoal):
 1. \<not> null (filter (\<lambda>(x, y). P x \<and> y = None) (assocs f)) proof (state)
this:
\<not> null (filter_assocs f)

goal (1 subgoal):
 1. fst (hd (filter_assocs f)) \<notin> dom f \<and> P (fst (hd (filter_assocs f))) proof (prove)
using this:
\<not> null (filter_assocs f)

goal (1 subgoal):
 1. hd (filter_assocs f) \<in> set (filter_assocs f) proof (state)
this:
hd (filter_assocs f) \<in> set (filter_assocs f)

goal (1 subgoal):
 1. fst (hd (filter_assocs f)) \<notin> dom f \<and> P (fst (hd (filter_assocs f))) proof (prove)
using this:
hd (filter_assocs f) \<in> set (filter_assocs f)

goal (1 subgoal):
 1. fst (hd (filter_assocs f)) \<notin> dom f \<and> P (fst (hd (filter_assocs f))) proof (prove)
using this:
hd (filter (\<lambda>(x, y). P x \<and> y = None) (assocs f)) \<in> set (filter (\<lambda>(x, y). P x \<and> y = None) (assocs f))

goal (1 subgoal):
 1. fst (hd (filter (\<lambda>(x, y). P x \<and> y = None) (assocs f))) \<notin> dom f \<and> P (fst (hd (filter (\<lambda>(x, y). P x \<and> y = None) (assocs f)))) proof (state)
this:
fst (hd (filter_assocs f)) \<notin> dom f \<and> P (fst (hd (filter_assocs f)))

goal:
No subgoals!
theory Arch_AI

lemma ucast_le_migrate:
  "\<lbrakk> y < 2 ^ size x; size x < size y \<rbrakk> \<Longrightarrow> (ucast x \<le> y) = (x \<le> ucast y)"
  for x :: "'a :: len word" and y :: "'b :: len word" apply (simp add: word_le_def ucast_def del: Word.of_int_uint) apply (subst word_uint.Abs_inverse) apply (simp add: uints_num word_size) apply (rule order_less_le_trans, rule uint_lt2p) apply simp apply (subst word_uint.Abs_inverse) apply (simp add: uints_num word_size word_less_alt uint_2p_alt) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y < 2 ^ size x; size x < size y\<rbrakk> \<Longrightarrow> (UCAST('a \<rightarrow> 'b) x \<le> y) = (x \<le> UCAST('b \<rightarrow> 'a) y) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y < 2 ^ size x; size x < size y\<rbrakk> \<Longrightarrow> (uint (word_of_int (uint x)) \<le> uint y) = (uint x \<le> uint (word_of_int (uint y))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>y < 2 ^ size x; size x < size y\<rbrakk> \<Longrightarrow> uint x \<in> uints LENGTH('b)
 2. \<lbrakk>y < 2 ^ size x; size x < size y\<rbrakk> \<Longrightarrow> (uint x \<le> uint y) = (uint x \<le> uint (word_of_int (uint y))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>y < 2 ^ LENGTH('a); LENGTH('a) < LENGTH('b)\<rbrakk> \<Longrightarrow> uint x < 2 ^ LENGTH('b)
 2. \<lbrakk>y < 2 ^ size x; size x < size y\<rbrakk> \<Longrightarrow> (uint x \<le> uint y) = (uint x \<le> uint (word_of_int (uint y))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>y < 2 ^ LENGTH('a); LENGTH('a) < LENGTH('b)\<rbrakk> \<Longrightarrow> 2 ^ LENGTH('a) \<le> 2 ^ LENGTH('b)
 2. \<lbrakk>y < 2 ^ size x; size x < size y\<rbrakk> \<Longrightarrow> (uint x \<le> uint y) = (uint x \<le> uint (word_of_int (uint y))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y < 2 ^ size x; size x < size y\<rbrakk> \<Longrightarrow> (uint x \<le> uint y) = (uint x \<le> uint (word_of_int (uint y))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>y < 2 ^ size x; size x < size y\<rbrakk> \<Longrightarrow> uint y \<in> uints LENGTH('a)
 2. \<lbrakk>y < 2 ^ size x; size x < size y\<rbrakk> \<Longrightarrow> (uint x \<le> uint y) = (uint x \<le> uint y) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y < 2 ^ size x; size x < size y\<rbrakk> \<Longrightarrow> (uint x \<le> uint y) = (uint x \<le> uint y) proof (prove)
goal:
No subgoals!
theory Arch_AI

lemma obj_at_delete_objects:
  "\<lbrace>\<lambda>s. Q (obj_at (P (interrupt_irq_node s) (arch_state s)) r s) \<and>
        r \<notin> {ptr..ptr + 2 ^ bits - 1}\<rbrace>
   delete_objects ptr bits
   \<lbrace>\<lambda>_ s. Q (obj_at (P (interrupt_irq_node s) (arch_state s)) r s)\<rbrace>" apply (simp add: delete_objects_def do_machine_op_def split_def) apply wp apply (simp add: detype_machine_state_update_comm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Q (obj_at (P (interrupt_irq_node s) (arch_state s)) r s) \<and> r \<notin> {ptr..ptr + 2 ^ bits - 1}\<rbrace> delete_objects ptr bits \<lbrace>\<lambda>_ s. Q (obj_at (P (interrupt_irq_node s) (arch_state s)) r s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Q (obj_at (P (interrupt_irq_node s) (arch_state s)) r s) \<and> (ptr \<le> r \<longrightarrow> \<not> r \<le> ptr + 2 ^ bits - 1)\<rbrace> do y <- do ms <- gets machine_state;
p <- select_f (freeMemory ptr bits ms);
modify (machine_state_update (\<lambda>_. snd p))
od;
modify (detype {ptr..ptr + 2 ^ bits - 1})
od \<lbrace>\<lambda>_ s. Q (obj_at (P (interrupt_irq_node s) (arch_state s)) r s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. Q (obj_at (P (interrupt_irq_node s) (arch_state s)) r s) \<and> (ptr \<le> r \<longrightarrow> \<not> r \<le> ptr + 2 ^ bits - 1) \<Longrightarrow> \<forall>x\<in>fst (freeMemory ptr bits (machine_state s)). Q (obj_at (P (interrupt_irq_node (detype {ptr..ptr + 2 ^ bits - 1} (s\<lparr>machine_state := snd x\<rparr>))) (arch_state (detype {ptr..ptr + 2 ^ bits - 1} (s\<lparr>machine_state := snd x\<rparr>)))) r (detype {ptr..ptr + 2 ^ bits - 1} (s\<lparr>machine_state := snd x\<rparr>))) proof (prove)
goal:
No subgoals!
theory Arch_AI

lemma set_cap_orth:
  "\<lbrace>\<lambda>s. P s \<and> Q cap' s\<rbrace> set_cap cap src \<lbrace>\<lambda>rv s. Q cap' s\<rbrace> \<Longrightarrow>
   \<lbrace>\<lambda>s. P s \<and> src\<noteq> dest \<and> (cte_wp_at ((=) cap') dest s \<longrightarrow> Q cap' s)\<rbrace>
   set_cap cap src
   \<lbrace>\<lambda>rv s. cte_wp_at ((=) cap') dest s \<longrightarrow> Q cap' s\<rbrace>" apply (clarsimp simp:valid_def cte_wp_at_caps_of_state) apply (drule_tac x = s in spec) apply (frule set_cap_caps_of_state_monad) apply clarsimp apply (drule(1) bspec) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P s \<and> Q cap' s\<rbrace> set_cap cap src \<lbrace>\<lambda>rv. Q cap'\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> src \<noteq> dest \<and> (cte_wp_at ((=) cap') dest s \<longrightarrow> Q cap' s)\<rbrace> set_cap cap src \<lbrace>\<lambda>rv s. cte_wp_at ((=) cap') dest s \<longrightarrow> Q cap' s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>\<forall>s. P s \<and> Q cap' s \<longrightarrow> (\<forall>x\<in>fst (set_cap cap src s). case x of (r, x) \<Rightarrow> Q cap' x); ((), b) \<in> fst (set_cap cap src s); P s; src \<noteq> dest; caps_of_state s dest = Some cap' \<longrightarrow> Q cap' s; caps_of_state b dest = Some cap'\<rbrakk> \<Longrightarrow> Q cap' b proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>((), b) \<in> fst (set_cap cap src s); P s; src \<noteq> dest; caps_of_state s dest = Some cap' \<longrightarrow> Q cap' s; caps_of_state b dest = Some cap'; P s \<and> Q cap' s \<longrightarrow> (\<forall>x\<in>fst (set_cap cap src s). case x of (r, x) \<Rightarrow> Q cap' x)\<rbrakk> \<Longrightarrow> Q cap' b proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>((), b) \<in> fst (set_cap cap src s); P s; src \<noteq> dest; caps_of_state s dest = Some cap' \<longrightarrow> Q cap' s; caps_of_state b dest = Some cap'; P s \<and> Q cap' s \<longrightarrow> (\<forall>x\<in>fst (set_cap cap src s). case x of (r, x) \<Rightarrow> Q cap' x); caps_of_state b = (caps_of_state s)(src \<mapsto> cap)\<rbrakk> \<Longrightarrow> Q cap' b proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>((), b) \<in> fst (set_cap cap src s); P s; src \<noteq> dest; Q cap' s; caps_of_state s dest = Some cap'; \<forall>x\<in>fst (set_cap cap src s). case x of (r, x) \<Rightarrow> Q cap' x; caps_of_state b = (caps_of_state s)(src \<mapsto> cap)\<rbrakk> \<Longrightarrow> Q cap' b proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>((), b) \<in> fst (set_cap cap src s); P s; src \<noteq> dest; Q cap' s; caps_of_state s dest = Some cap'; caps_of_state b = (caps_of_state s)(src \<mapsto> cap); case ((), b) of (r, x) \<Rightarrow> Q cap' x\<rbrakk> \<Longrightarrow> Q cap' b proof (prove)
goal:
No subgoals!
theory Arch_AI

lemma set_cap_empty_tables[wp]:
  "\<lbrace>\<lambda>s. P (obj_at (empty_table (set (second_level_tables (arch_state s)))) p s)\<rbrace>
     set_cap cap cref
   \<lbrace>\<lambda>rv s. P (obj_at (empty_table (set (second_level_tables (arch_state s)))) p s)\<rbrace>" apply (rule hoare_pre) apply (rule hoare_use_eq [where f=arch_state, OF set_cap_arch]) apply (wp set_cap_obj_at_impossible) apply (clarsimp simp: empty_table_caps_of) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (obj_at (empty_table (set (second_level_tables (arch_state s)))) p s)\<rbrace> set_cap cap cref \<lbrace>\<lambda>rv s. P (obj_at (empty_table (set (second_level_tables (arch_state s)))) p s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> set_cap cap cref \<lbrace>\<lambda>rv s. P (obj_at (empty_table (set (second_level_tables (arch_state s)))) p s)\<rbrace>
 2. \<And>s. P (obj_at (empty_table (set (second_level_tables (arch_state s)))) p s) \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>f. \<lbrace>?P3 f\<rbrace> set_cap cap cref \<lbrace>\<lambda>rv s. P (obj_at (empty_table (set (second_level_tables f))) p s)\<rbrace>
 2. \<And>s. P (obj_at (empty_table (set (second_level_tables (arch_state s)))) p s) \<Longrightarrow> ?P3 (arch_state s) s proof (prove)
goal (1 subgoal):
 1. \<And>s. P (obj_at (empty_table (set (second_level_tables (arch_state s)))) p s) \<Longrightarrow> P (obj_at (empty_table (set (second_level_tables (arch_state s)))) p s) \<and> (\<forall>ko. empty_table (set (second_level_tables (arch_state s))) ko \<longrightarrow> caps_of ko = {}) proof (prove)
goal:
No subgoals!
theory Arch_AI

lemma cte_wp_at_eq_to_op_eq:
  "cte_wp_at (\<lambda>c. c = cap) = cte_wp_at ((=) cap)" by (simp add: cte_wp_at_caps_of_state fun_eq_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at (\<lambda>c. c = cap) = cte_wp_at ((=) cap)
theory Arch_AI

lemma max_index_upd_caps_overlap_reserved:
  "\<lbrace>\<lambda>s. invs s \<and> S \<subseteq> untyped_range cap \<and>
       descendants_range_in S slot s \<and> cte_wp_at ((=) cap) slot s \<and> is_untyped_cap cap\<rbrace>
  set_cap (max_free_index_update cap) slot
  \<lbrace>\<lambda>rv. caps_overlap_reserved S\<rbrace>" apply (rule hoare_name_pre_state) apply (clarsimp simp:is_cap_simps) apply (wp set_untyped_cap_caps_overlap_reserved) apply (auto simp:cte_wp_at_caps_of_state max_free_index_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. invs s \<and> S \<subseteq> untyped_range cap \<and> descendants_range_in S slot s \<and> cte_wp_at ((=) cap) slot s \<and> is_untyped_cap cap\<rbrace> set_cap (max_free_index_update cap) slot \<lbrace>\<lambda>rv. caps_overlap_reserved S\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. invs s \<and> S \<subseteq> untyped_range cap \<and> descendants_range_in S slot s \<and> cte_wp_at ((=) cap) slot s \<and> is_untyped_cap cap \<Longrightarrow> \<lbrace>(=) s\<rbrace> set_cap (max_free_index_update cap) slot \<lbrace>\<lambda>rv. caps_overlap_reserved S\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s dev r bits f. \<lbrakk>invs s; S \<subseteq> {r..r + 2 ^ bits - 1}; descendants_range_in S slot s; cte_wp_at ((=) (UntypedCap dev r bits f)) slot s; cap = UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> set_cap (UntypedCap dev r bits (max_free_index bits)) slot \<lbrace>\<lambda>rv. caps_overlap_reserved S\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s dev r bits f sa. \<lbrakk>invs s; S \<subseteq> {r..r + 2 ^ bits - 1}; descendants_range_in S slot s; cte_wp_at ((=) (UntypedCap dev r bits f)) slot s; cap = UntypedCap dev r bits f; s = sa\<rbrakk> \<Longrightarrow> invs sa \<and> S \<subseteq> {r..r + 2 ^ bits - 1} \<and> usable_untyped_range (UntypedCap dev r bits (max_free_index bits)) \<inter> S = {} \<and> descendants_range_in S slot sa \<and> cte_wp_at ((=) (UntypedCap dev r bits (?idx13 s dev r bits f))) slot sa proof (prove)
goal:
No subgoals!
theory Arch_AI

lemma max_index_upd_invs_simple:
  "\<lbrace>\<lambda>s. descendants_range_in (untyped_range cap) cref s \<and>
         pspace_no_overlap_range_cover (obj_ref_of cap) (cap_bits cap) s \<and>
         invs s \<and> cte_wp_at ((=) cap) cref s \<and>  is_untyped_cap cap\<rbrace>
   set_cap  (max_free_index_update cap) cref \<lbrace>\<lambda>rv. invs\<rbrace>" apply (rule hoare_name_pre_state) apply (clarsimp simp:is_cap_simps) apply (wp set_untyped_cap_invs_simple) apply (auto simp:cte_wp_at_caps_of_state max_free_index_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. descendants_range_in (untyped_range cap) cref s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> invs s \<and> cte_wp_at ((=) cap) cref s \<and> is_untyped_cap cap\<rbrace> set_cap (max_free_index_update cap) cref \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. descendants_range_in (untyped_range cap) cref s \<and> pspace_no_overlap (up_aligned_area (obj_ref_of cap) (cap_bits cap)) s \<and> invs s \<and> cte_wp_at ((=) cap) cref s \<and> is_untyped_cap cap \<Longrightarrow> \<lbrace>(=) s\<rbrace> set_cap (max_free_index_update cap) cref \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s dev r bits f. \<lbrakk>descendants_range_in {r..r + 2 ^ bits - 1} cref s; pspace_no_overlap (up_aligned_area r bits) s; invs s; cte_wp_at ((=) (UntypedCap dev r bits f)) cref s; cap = UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> set_cap (UntypedCap dev r bits (max_free_index bits)) cref \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s dev r bits f sa. \<lbrakk>descendants_range_in {r..r + 2 ^ bits - 1} cref s; pspace_no_overlap (up_aligned_area r bits) s; invs s; cte_wp_at ((=) (UntypedCap dev r bits f)) cref s; cap = UntypedCap dev r bits f; s = sa\<rbrakk> \<Longrightarrow> descendants_range_in {r..r + 2 ^ bits - 1} cref sa \<and> pspace_no_overlap (up_aligned_area r bits) sa \<and> invs sa \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = bits \<and> cap_is_device c = dev \<and> obj_ref_of c = r) cref sa \<and> max_free_index bits \<le> 2 ^ bits proof (prove)
goal:
No subgoals!
theory Arch_AI

lemma sts_pspace_no_overlap [wp]:
  "\<lbrace>pspace_no_overlap S\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. pspace_no_overlap S\<rbrace>" by (wp pspace_no_overlap_typ_at_lift)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_no_overlap S\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. pspace_no_overlap S\<rbrace>
theory ArchArch_AI

lemma safe_parent_strg:
  "cte_wp_at (\<lambda>cap. cap = UntypedCap False frame pageBits idx) p s \<and>
   descendants_of p (cdt s) = {} \<and>
   valid_objs s
  \<longrightarrow>
  cte_wp_at (safe_parent_for (cdt s) p
             (ArchObjectCap (ASIDPoolCap frame base)))
             p s" apply (clarsimp simp: cte_wp_at_caps_of_state safe_parent_for_def is_physical_def arch_is_physical_def) apply (rule is_aligned_no_overflow) apply (drule (1) caps_of_state_valid_cap) apply (clarsimp simp: valid_cap_def cap_aligned_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at (\<lambda>cap. cap = UntypedCap False frame pageBits idx) p s \<and> descendants_of p (cdt s) = {} \<and> valid_objs s \<longrightarrow> cte_wp_at (safe_parent_for (cdt s) p (ArchObjectCap (ASIDPoolCap frame base))) p s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some (UntypedCap False frame pageBits idx); descendants_of p (cdt s) = {}; valid_objs s\<rbrakk> \<Longrightarrow> frame \<le> frame + 2 ^ pageBits - 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some (UntypedCap False frame pageBits idx); descendants_of p (cdt s) = {}; valid_objs s\<rbrakk> \<Longrightarrow> is_aligned frame pageBits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>descendants_of p (cdt s) = {}; valid_objs s; s \<turnstile> UntypedCap False frame pageBits idx\<rbrakk> \<Longrightarrow> is_aligned frame pageBits proof (prove)
goal:
No subgoals!
theory ArchArch_AI

lemma range_cover_full:
  "\<lbrakk>is_aligned ptr sz;sz<word_bits\<rbrakk> \<Longrightarrow> range_cover (ptr::word32) sz sz (Suc 0)" by (clarsimp simp:range_cover_def unat_eq_0 le_mask_iff[symmetric] word_and_le1 word_bits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr sz; sz < word_bits\<rbrakk> \<Longrightarrow> range_cover ptr sz sz (Suc 0)
theory ArchArch_AI

lemma check_vp_wpR [wp]:
  "\<lbrace>\<lambda>s. vmsz_aligned w sz \<longrightarrow> P () s\<rbrace>
  check_vp_alignment sz w \<lbrace>P\<rbrace>, -" apply (simp add: check_vp_alignment_def unlessE_whenE cong: vmpage_size.case_cong) apply (rule hoare_pre) apply (wp whenE_wp|wpc)+ apply (simp add: vmsz_aligned_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. vmsz_aligned w sz \<longrightarrow> P () s\<rbrace> check_vp_alignment sz w \<lbrace>P\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. vmsz_aligned w sz \<longrightarrow> P () s\<rbrace> whenE (\<not> is_aligned w (pageBitsForSize sz)) (throwError AlignmentError) \<lbrace>P\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> whenE (\<not> is_aligned w (pageBitsForSize sz)) (throwError AlignmentError) \<lbrace>P\<rbrace>, -
 2. \<And>s. vmsz_aligned w sz \<longrightarrow> P () s \<Longrightarrow> ?P' s proof (prove)
goal (1 subgoal):
 1. \<And>s. vmsz_aligned w sz \<longrightarrow> P () s \<Longrightarrow> (if \<not> is_aligned w (pageBitsForSize sz) then \<lambda>s. True \<and> True else P ()) s proof (prove)
goal:
No subgoals!