kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchArch_AI

lemma check_vp_inv: "\<lbrace>P\<rbrace> check_vp_alignment sz w \<lbrace>\<lambda>_. 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 done

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

lemma p2_low_bits_max:
  "(2 ^ asid_low_bits - 1) = (max_word :: 10 word)" by (simp add: asid_low_bits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 2 ^ local.asid_low_bits - 1 = - 1
theory ArchArch_AI

lemma asid_high_bits_max_word:
  "(2 ^ asid_high_bits - 1 :: 7 word) = max_word" by (simp add: asid_high_bits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 2 ^ local.asid_high_bits - 1 = - 1
theory ArchArch_AI

lemma ucast_asid_high_btis_of_le [simp]:
  "ucast (asid_high_bits_of w) \<le> (2 ^ asid_high_bits - 1 :: word32)" apply (simp add: asid_high_bits_of_def) apply (rule word_less_sub_1) apply (rule order_less_le_trans) apply (rule ucast_less) apply simp apply (simp add: asid_high_bits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. UCAST(7 \<rightarrow> 32) (asid_high_bits_of w) \<le> 2 ^ local.asid_high_bits - 1 proof (prove)
goal (1 subgoal):
 1. UCAST(7 \<rightarrow> 32) (UCAST(32 \<rightarrow> 7) (w >> local.asid_low_bits)) \<le> 2 ^ local.asid_high_bits - 1 proof (prove)
goal (1 subgoal):
 1. UCAST(7 \<rightarrow> 32) (UCAST(32 \<rightarrow> 7) (w >> local.asid_low_bits)) < 2 ^ local.asid_high_bits proof (prove)
goal (2 subgoals):
 1. UCAST(7 \<rightarrow> 32) (UCAST(32 \<rightarrow> 7) (w >> local.asid_low_bits)) < ?y2
 2. ?y2 \<le> 2 ^ local.asid_high_bits proof (prove)
goal (2 subgoals):
 1. LENGTH(7) < LENGTH(32)
 2. 2 ^ LENGTH(7) \<le> 2 ^ local.asid_high_bits proof (prove)
goal (1 subgoal):
 1. 2 ^ LENGTH(7) \<le> 2 ^ local.asid_high_bits proof (prove)
goal:
No subgoals!
theory ArchArch_AI

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

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

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

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

lemma vs_asid_refs' [simp]:
  "vs_asid_refs (arm_asid_table (arch_state s')) =
  vs_asid_refs (asid_table s) \<union> {([VSRef (ucast asid) None], ap)}" apply (simp add: s'_def) apply (rule set_eqI) apply (rule iffI) apply (auto simp: vs_asid_refs_def split: if_split_asm)[1] apply clarsimp apply (erule disjE) apply (auto simp: vs_asid_refs_def)[1] apply (subst (asm) vs_asid_refs_def) apply (clarsimp dest!: graph_ofD) apply (rule vs_asid_refsI) apply (clarsimp simp: empty) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. vs_asid_refs (asid_table s') = vs_asid_refs (asid_table s) \<union> {([VSRef (UCAST(7 \<rightarrow> 32) asid) None], ap)} proof (prove)
goal (1 subgoal):
 1. vs_asid_refs ((asid_table s)(asid \<mapsto> ap)) = insert ([VSRef (UCAST(7 \<rightarrow> 32) asid) None], ap) (vs_asid_refs (asid_table s)) proof (prove)
goal (1 subgoal):
 1. \<And>x. (x \<in> vs_asid_refs ((asid_table s)(asid \<mapsto> ap))) = (x \<in> insert ([VSRef (UCAST(7 \<rightarrow> 32) asid) None], ap) (vs_asid_refs (asid_table s))) proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> vs_asid_refs ((asid_table s)(asid \<mapsto> ap)) \<Longrightarrow> x \<in> insert ([VSRef (UCAST(7 \<rightarrow> 32) asid) None], ap) (vs_asid_refs (asid_table s))
 2. \<And>x. x \<in> insert ([VSRef (UCAST(7 \<rightarrow> 32) asid) None], ap) (vs_asid_refs (asid_table s)) \<Longrightarrow> x \<in> vs_asid_refs ((asid_table s)(asid \<mapsto> ap)) proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> insert ([VSRef (UCAST(7 \<rightarrow> 32) asid) None], ap) (vs_asid_refs (asid_table s)) \<Longrightarrow> x \<in> vs_asid_refs ((asid_table s)(asid \<mapsto> ap)) proof (prove)
goal (1 subgoal):
 1. \<And>a b. a = [VSRef (UCAST(7 \<rightarrow> 32) asid) None] \<and> b = ap \<or> (a, b) \<in> vs_asid_refs (asid_table s) \<Longrightarrow> (a, b) \<in> vs_asid_refs ((asid_table s)(asid \<mapsto> ap)) proof (prove)
goal (2 subgoals):
 1. \<And>a b. a = [VSRef (UCAST(7 \<rightarrow> 32) asid) None] \<and> b = ap \<Longrightarrow> (a, b) \<in> vs_asid_refs ((asid_table s)(asid \<mapsto> ap))
 2. \<And>a b. (a, b) \<in> vs_asid_refs (asid_table s) \<Longrightarrow> (a, b) \<in> vs_asid_refs ((asid_table s)(asid \<mapsto> ap)) proof (prove)
goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> vs_asid_refs (asid_table s) \<Longrightarrow> (a, b) \<in> vs_asid_refs ((asid_table s)(asid \<mapsto> ap)) proof (prove)
goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> (\<lambda>(r, y). ([VSRef (UCAST(7 \<rightarrow> 32) r) None], y)) ` graph_of (asid_table s) \<Longrightarrow> (a, b) \<in> vs_asid_refs ((asid_table s)(asid \<mapsto> ap)) proof (prove)
goal (1 subgoal):
 1. \<And>aa ba. asid_table s aa = Some ba \<Longrightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba) \<in> vs_asid_refs ((asid_table s)(asid \<mapsto> ap)) proof (prove)
goal (1 subgoal):
 1. \<And>aa ba. asid_table s aa = Some ba \<Longrightarrow> ((asid_table s)(asid \<mapsto> ap)) aa = Some ba proof (prove)
goal:
No subgoals!
theory ArchArch_AI

lemma vs_lookup':
  "vs_lookup s' = vs_lookup s \<union> {([VSRef (ucast asid) None], ap)}" using ko apply (simp add: vs_lookup_def) apply (rule rtrancl_insert) apply (clarsimp simp: vs_lookup1_def obj_at_def vs_refs_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. vs_lookup s' = vs_lookup s \<union> {([VSRef (UCAST(7 \<rightarrow> 32) asid) None], ap)} proof (prove)
using this:
ako_at (ASIDPool (\<lambda>x. None)) ap s

goal (1 subgoal):
 1. vs_lookup s' = vs_lookup s \<union> {([VSRef (UCAST(7 \<rightarrow> 32) asid) None], ap)} proof (prove)
goal (1 subgoal):
 1. ako_at (ASIDPool (\<lambda>x. None)) ap s \<Longrightarrow> (vs_lookup1 s)\<^sup>* `` insert ([VSRef (UCAST(7 \<rightarrow> 32) asid) None], ap) (vs_asid_refs (asid_table s)) = insert ([VSRef (UCAST(7 \<rightarrow> 32) asid) None], ap) ((vs_lookup1 s)\<^sup>* `` vs_asid_refs (asid_table s)) proof (prove)
goal (1 subgoal):
 1. \<And>y. ako_at (ASIDPool (\<lambda>x. None)) ap s \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) asid) None], ap), y) \<notin> vs_lookup1 s proof (prove)
goal:
No subgoals!
theory ArchArch_AI

lemma vs_lookup_pages':
  "vs_lookup_pages s' = vs_lookup_pages s \<union> {([VSRef (ucast asid) None], ap)}" using ko apply (simp add: vs_lookup_pages_def) apply (rule rtrancl_insert) apply (clarsimp simp: vs_lookup_pages1_def obj_at_def vs_refs_pages_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. vs_lookup_pages s' = vs_lookup_pages s \<union> {([VSRef (UCAST(7 \<rightarrow> 32) asid) None], ap)} proof (prove)
using this:
ako_at (ASIDPool (\<lambda>x. None)) ap s

goal (1 subgoal):
 1. vs_lookup_pages s' = vs_lookup_pages s \<union> {([VSRef (UCAST(7 \<rightarrow> 32) asid) None], ap)} proof (prove)
goal (1 subgoal):
 1. ako_at (ASIDPool (\<lambda>x. None)) ap s \<Longrightarrow> (vs_lookup_pages1 s)\<^sup>* `` insert ([VSRef (UCAST(7 \<rightarrow> 32) asid) None], ap) (vs_asid_refs (asid_table s)) = insert ([VSRef (UCAST(7 \<rightarrow> 32) asid) None], ap) ((vs_lookup_pages1 s)\<^sup>* `` vs_asid_refs (asid_table s)) proof (prove)
goal (1 subgoal):
 1. \<And>y. ako_at (ASIDPool (\<lambda>x. None)) ap s \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) asid) None], ap), y) \<notin> vs_lookup_pages1 s proof (prove)
goal:
No subgoals!
theory ArchArch_AI

lemma obj_at [simp]:
  "obj_at P p s' = obj_at P p s" by (simp add: s'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_at P p s' = obj_at P p s
theory ArchArch_AI

lemma vs_lookup_neq: "\<lbrakk>(rs \<rhd> p) s' ; p \<noteq> ap\<rbrakk> \<Longrightarrow>  (rs \<rhd> p) s" by (clarsimp simp: vs_lookup')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(rs \<rhd> p) s'; p \<noteq> ap\<rbrakk> \<Longrightarrow> (rs \<rhd> p) s
theory ArchArch_AI

lemma global_objs':
  "valid_global_objs s \<Longrightarrow> valid_global_objs s'" apply (clarsimp simp: valid_global_objs_def valid_ao_at_def second_level_tables_def) apply (auto simp: s'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_global_objs s \<Longrightarrow> valid_global_objs s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_vso_at (arm_global_pd (arch_state s)) s; obj_at (empty_table (set (arm_global_pts (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x))\<rbrakk> \<Longrightarrow> valid_vso_at (arm_global_pd (arch_state s')) s' \<and> obj_at (empty_table (set (arm_global_pts (arch_state s')))) (arm_global_pd (arch_state s')) s \<and> (\<forall>p\<in>set (arm_global_pts (arch_state s')). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x))) proof (prove)
goal:
No subgoals!
theory ArchArch_AI

lemma caps_of_state_s':
  "caps_of_state s' = caps_of_state s" by (rule caps_of_state_pspace, simp add: s'_def)

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

lemma valid_vs_lookup':
  "\<lbrakk> valid_vs_lookup s;
     \<exists>ptr cap. caps_of_state s ptr = Some cap
     \<and> ap \<in> obj_refs cap \<and> vs_cap_ref cap = Some [VSRef (ucast asid) None] \<rbrakk>
  \<Longrightarrow> valid_vs_lookup s'" by (clarsimp simp: valid_vs_lookup_def caps_of_state_s' vs_lookup_pages')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_vs_lookup s; \<exists>ptr cap. caps_of_state s ptr = Some cap \<and> ap \<in> obj_refs cap \<and> vs_cap_ref cap = Some [VSRef (UCAST(7 \<rightarrow> 32) asid) None]\<rbrakk> \<Longrightarrow> valid_vs_lookup s'
theory ArchArch_AI

lemma valid_table_caps':
  "\<lbrakk> valid_table_caps s \<rbrakk>
        \<Longrightarrow> valid_table_caps s'" apply (simp add: valid_table_caps_def caps_of_state_s' second_level_tables_def) apply (simp add: s'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_table_caps s \<Longrightarrow> valid_table_caps s' proof (prove)
goal (1 subgoal):
 1. \<forall>r a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s) \<and> (is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) r s) \<Longrightarrow> \<forall>r a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s')))) r s) \<and> (is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s')))) r s) proof (prove)
goal:
No subgoals!
theory ArchArch_AI

lemma valid_arch_caps:
  "\<lbrakk> valid_arch_caps s;
     \<exists>ptr cap. caps_of_state s ptr = Some cap
     \<and> ap \<in> obj_refs cap \<and> vs_cap_ref cap = Some [VSRef (ucast asid) None] \<rbrakk>
  \<Longrightarrow> valid_arch_caps s'" by (simp add: valid_arch_caps_def caps_of_state_s'
                valid_table_caps' valid_vs_lookup')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_arch_caps s; \<exists>ptr cap. caps_of_state s ptr = Some cap \<and> ap \<in> obj_refs cap \<and> vs_cap_ref cap = Some [VSRef (UCAST(7 \<rightarrow> 32) asid) None]\<rbrakk> \<Longrightarrow> valid_arch_caps s'
theory ArchArch_AI

lemma valid_arch_state_strg:
  "valid_arch_state s \<and> ap \<notin> ran (asid_table s) \<and> asid_pool_at ap s \<longrightarrow>
   valid_arch_state (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid \<mapsto> ap)\<rparr>\<rparr>)" apply (clarsimp simp: valid_arch_state_def) apply (clarsimp simp: valid_asid_table_def ran_def) apply (fastforce intro!: inj_on_fun_updI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_arch_state s \<and> ap \<notin> ran (asid_table s) \<and> typ_at (AArch AASIDPool) ap s \<longrightarrow> valid_arch_state (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid \<mapsto> ap)\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_asid_table (asid_table s) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); ap \<notin> ran (asid_table s); typ_at (AArch AASIDPool) ap s\<rbrakk> \<Longrightarrow> valid_asid_table ((asid_table s)(asid \<mapsto> ap)) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); \<forall>a. asid_table s a \<noteq> Some ap; typ_at (AArch AASIDPool) ap s; \<forall>p. (\<exists>a. asid_table s a = Some p) \<longrightarrow> typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s))\<rbrakk> \<Longrightarrow> (\<forall>p. (\<exists>a. (a = asid \<longrightarrow> ap = p) \<and> (a \<noteq> asid \<longrightarrow> asid_table s a = Some p)) \<longrightarrow> typ_at (AArch AASIDPool) p s) \<and> inj_on ((asid_table s)(asid \<mapsto> ap)) (dom (asid_table s)) \<and> Some ap \<notin> asid_table s ` (dom (asid_table s) - {asid}) proof (prove)
goal:
No subgoals!
theory ArchArch_AI

lemma retype_region_ap:
  "\<lbrace>\<top>\<rbrace>
  retype_region ap 1 0 (ArchObject ASIDPoolObj) dev
  \<lbrace>\<lambda>_. ko_at (ArchObj (ASIDPool Map.empty)) ap\<rbrace>" apply (rule hoare_post_imp) prefer 2 apply (rule retype_region_obj_at) apply simp apply simp apply (clarsimp simp: retype_addrs_def obj_bits_api_def default_arch_object_def) apply (clarsimp simp: obj_at_def default_object_def default_arch_object_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> retype_region ap 1 0 (ArchObject ASIDPoolObj) dev \<lbrace>\<lambda>_. ako_at (ASIDPool (\<lambda>x. None)) ap\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s. ?Q rv s \<Longrightarrow> ako_at (ASIDPool (\<lambda>x. None)) ap s
 2. \<lbrace>\<lambda>_. True\<rbrace> retype_region ap 1 0 (ArchObject ASIDPoolObj) dev \<lbrace>?Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>_. True\<rbrace> retype_region ap 1 0 (ArchObject ASIDPoolObj) dev \<lbrace>?Q\<rbrace>
 2. \<And>rv s. ?Q rv s \<Longrightarrow> ako_at (ASIDPool (\<lambda>x. None)) ap s proof (prove)
goal (2 subgoals):
 1. ArchObject ASIDPoolObj \<noteq> Untyped
 2. \<And>rv s. \<forall>x\<in>set (retype_addrs ap (ArchObject ASIDPoolObj) 1 0). obj_at (\<lambda>ko. ko = default_object (ArchObject ASIDPoolObj) dev 0) x s \<Longrightarrow> ako_at (ASIDPool (\<lambda>x. None)) ap s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<forall>x\<in>set (retype_addrs ap (ArchObject ASIDPoolObj) 1 0). obj_at (\<lambda>ko. ko = default_object (ArchObject ASIDPoolObj) dev 0) x s \<Longrightarrow> ako_at (ASIDPool (\<lambda>x. None)) ap s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>x\<in>set (retype_addrs ap (ArchObject ASIDPoolObj) (Suc 0) 0). obj_at (\<lambda>ko. ko = default_object (ArchObject ASIDPoolObj) dev 0) x s \<Longrightarrow> ako_at (ASIDPool (\<lambda>x. None)) ap s proof (prove)
goal (1 subgoal):
 1. \<And>s. obj_at (\<lambda>ko. ko = default_object (ArchObject ASIDPoolObj) dev 0) ap s \<Longrightarrow> ako_at (ASIDPool (\<lambda>x. None)) ap s proof (prove)
goal:
No subgoals!
theory ArchArch_AI

lemma retype_region_ap':
  "\<lbrace>\<top>\<rbrace> retype_region ap 1 0 (ArchObject ASIDPoolObj) dev \<lbrace>\<lambda>rv. asid_pool_at ap\<rbrace>" apply (rule hoare_strengthen_post, rule retype_region_ap) apply (clarsimp simp: a_type_def elim!: obj_at_weakenE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> retype_region ap 1 0 (ArchObject ASIDPoolObj) dev \<lbrace>\<lambda>rv. typ_at (AArch AASIDPool) ap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>rv s. ako_at (ASIDPool (\<lambda>x. None)) ap s \<Longrightarrow> typ_at (AArch AASIDPool) ap s proof (prove)
goal:
No subgoals!
theory ArchArch_AI

lemma no_cap_to_obj_with_diff_ref_null_filter:
  "no_cap_to_obj_with_diff_ref cap S
     = (\<lambda>s. \<forall>c \<in> ran (null_filter (caps_of_state s) |` (- S)).
             obj_refs c = obj_refs cap
                 \<longrightarrow> table_cap_ref c = table_cap_ref cap)" apply (simp add: no_cap_to_obj_with_diff_ref_def
                   ball_ran_eq cte_wp_at_caps_of_state) apply (simp add: Ball_def) apply (intro iff_allI ext) apply (simp add: restrict_map_def null_filter_def) apply (auto dest!: obj_ref_none_no_asid[rule_format]
               simp: table_cap_ref_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_cap_to_obj_with_diff_ref cap S = (\<lambda>s. \<forall>c\<in>ran (null_filter (caps_of_state s) |` (- S)). obj_refs c = obj_refs cap \<longrightarrow> table_cap_ref c = table_cap_ref cap) proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. \<forall>p\<in>UNIV - S. \<forall>capa. obj_refs capa = obj_refs cap \<longrightarrow> caps_of_state s p = Some capa \<longrightarrow> table_cap_ref capa = table_cap_ref cap) = (\<lambda>s. \<forall>a b c. (null_filter (caps_of_state s) |` (- S)) (a, b) = Some c \<longrightarrow> obj_refs c = obj_refs cap \<longrightarrow> table_cap_ref c = table_cap_ref cap) proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. \<forall>a b. (a, b) \<notin> S \<longrightarrow> (\<forall>capa. obj_refs capa = obj_refs cap \<longrightarrow> caps_of_state s (a, b) = Some capa \<longrightarrow> table_cap_ref capa = table_cap_ref cap)) = (\<lambda>s. \<forall>a b c. (null_filter (caps_of_state s) |` (- S)) (a, b) = Some c \<longrightarrow> obj_refs c = obj_refs cap \<longrightarrow> table_cap_ref c = table_cap_ref cap) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. ((a, b) \<notin> S \<longrightarrow> (\<forall>capa. obj_refs capa = obj_refs cap \<longrightarrow> caps_of_state s (a, b) = Some capa \<longrightarrow> table_cap_ref capa = table_cap_ref cap)) = (\<forall>c. (null_filter (caps_of_state s) |` (- S)) (a, b) = Some c \<longrightarrow> obj_refs c = obj_refs cap \<longrightarrow> table_cap_ref c = table_cap_ref cap) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. (caps_of_state s (a, b) = Some NullCap \<longrightarrow> (a, b) \<notin> S \<longrightarrow> {} = obj_refs cap \<longrightarrow> table_cap_ref NullCap = table_cap_ref cap) \<and> (caps_of_state s (a, b) \<noteq> Some NullCap \<longrightarrow> (a, b) \<notin> S \<longrightarrow> (\<forall>capa. obj_refs capa = obj_refs cap \<longrightarrow> caps_of_state s (a, b) = Some capa \<longrightarrow> table_cap_ref capa = table_cap_ref cap) = (\<forall>c. caps_of_state s (a, b) = Some c \<longrightarrow> obj_refs c = obj_refs cap \<longrightarrow> table_cap_ref c = table_cap_ref cap)) proof (prove)
goal:
No subgoals!
theory ArchArch_AI

lemma valid_table_caps_asid_upd [iff]:
  "valid_table_caps (s\<lparr>arch_state := (arm_asid_table_update f (arch_state s))\<rparr>) =
   valid_table_caps s" by (simp add: valid_table_caps_def second_level_tables_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_table_caps (s\<lparr>arch_state := arm_asid_table_update f (arch_state s)\<rparr>) = valid_table_caps s
theory ArchArch_AI

lemma vs_asid_ref_upd:
  "([VSRef (ucast (asid_high_bits_of asid')) None] \<rhd> ap')
    (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of asid \<mapsto> ap)\<rparr>\<rparr>)
  = (if asid_high_bits_of asid' = asid_high_bits_of asid
    then ap' = ap
    else ([VSRef (ucast (asid_high_bits_of asid')) None] \<rhd> ap') s)" by (fastforce intro: vs_lookup_atI elim: vs_lookup_atE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid')) None] \<rhd> ap') (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of asid \<mapsto> ap)\<rparr>\<rparr>) = (if asid_high_bits_of asid' = asid_high_bits_of asid then ap' = ap else ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid')) None] \<rhd> ap') s)
theory ArchArch_AI

lemma vs_asid_ref_eq:
  "([VSRef (ucast asid) None] \<rhd> ap) s
  = (asid_table s asid = Some ap)" by (fastforce elim: vs_lookup_atE intro: vs_lookup_atI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ([VSRef (UCAST(7 \<rightarrow> 32) asid) None] \<rhd> ap) s = (asid_table s asid = Some ap)
theory ArchArch_AI

lemma set_cap_reachable_pg_cap:
  "\<lbrace>\<lambda>s. P (reachable_pg_cap cap s)\<rbrace> set_cap x y \<lbrace>\<lambda>_ s. P (reachable_pg_cap cap s)\<rbrace>" by (unfold reachable_pg_cap_def, wp hoare_vcg_ex_lift set_cap.vs_lookup_pages)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (reachable_pg_cap cap s)\<rbrace> set_cap x y \<lbrace>\<lambda>_ s. P (reachable_pg_cap cap s)\<rbrace>