kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchAcc_AI

lemma set_asid_pool_valid_global_vspace_mappings[wp]:
  "\<lbrace>valid_global_vspace_mappings\<rbrace>
      set_asid_pool p ap \<lbrace>\<lambda>rv. valid_global_vspace_mappings\<rbrace>" apply (simp add: set_asid_pool_def) apply (wp set_object_global_vspace_mappings[THEN hoare_set_object_weaken_pre]) including unfold_objects by (clarsimp simp: a_type_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_vspace_mappings\<rbrace> set_asid_pool p ap \<lbrace>\<lambda>rv. valid_global_vspace_mappings\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_vspace_mappings\<rbrace> set_object p (ArchObj (ASIDPool ap)) \<lbrace>\<lambda>rv. valid_global_vspace_mappings\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_global_vspace_mappings s \<Longrightarrow> \<forall>ko. ko_at ko p s \<longrightarrow> a_type (ArchObj (ASIDPool ap)) = a_type ko \<longrightarrow> (valid_global_vspace_mappings and (\<lambda>s. typ_at (AArch APageDirectory) p s \<or> typ_at (AArch APageTable) p s \<longrightarrow> valid_global_objs s \<and> p \<notin> global_refs s)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_global_vspace_mappings s \<Longrightarrow> \<forall>ko. ko_at ko p s \<longrightarrow> a_type (ArchObj (ASIDPool ap)) = a_type ko \<longrightarrow> (valid_global_vspace_mappings and (\<lambda>s. typ_at (AArch APageDirectory) p s \<or> typ_at (AArch APageTable) p s \<longrightarrow> valid_global_objs s \<and> p \<notin> global_refs s)) s
theory ArchAcc_AI

lemma set_asid_pool_kernel_window[wp]:
  "\<lbrace>pspace_in_kernel_window\<rbrace> set_asid_pool p ap \<lbrace>\<lambda>rv. pspace_in_kernel_window\<rbrace>" unfolding set_asid_pool_def including unfold_objects by (wpsimp wp: set_object_pspace_in_kernel_window[THEN hoare_set_object_weaken_pre])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_in_kernel_window\<rbrace> set_asid_pool p ap \<lbrace>\<lambda>rv. pspace_in_kernel_window\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_in_kernel_window\<rbrace> set_object p (ArchObj (ASIDPool ap)) \<lbrace>\<lambda>rv. pspace_in_kernel_window\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_in_kernel_window\<rbrace> set_object p (ArchObj (ASIDPool ap)) \<lbrace>\<lambda>rv. pspace_in_kernel_window\<rbrace>
theory ArchAcc_AI

lemma set_asid_pool_pspace_respects_device_region[wp]:
  "\<lbrace>pspace_respects_device_region\<rbrace> set_asid_pool p ap \<lbrace>\<lambda>rv. pspace_respects_device_region\<rbrace>" unfolding set_asid_pool_def including unfold_objects by (wpsimp wp: set_object_pspace_respects_device_region[THEN hoare_set_object_weaken_pre])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_respects_device_region\<rbrace> set_asid_pool p ap \<lbrace>\<lambda>rv. pspace_respects_device_region\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_respects_device_region\<rbrace> set_object p (ArchObj (ASIDPool ap)) \<lbrace>\<lambda>rv. pspace_respects_device_region\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_respects_device_region\<rbrace> set_object p (ArchObj (ASIDPool ap)) \<lbrace>\<lambda>rv. pspace_respects_device_region\<rbrace>
theory ArchAcc_AI

lemma set_asid_pool_caps_kernel_window[wp]:
  "\<lbrace>cap_refs_in_kernel_window\<rbrace> set_asid_pool p ap \<lbrace>\<lambda>rv. cap_refs_in_kernel_window\<rbrace>" unfolding set_asid_pool_def including unfold_objects by (wpsimp wp: set_object_cap_refs_in_kernel_window[THEN hoare_set_object_weaken_pre]
           simp: a_type_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cap_refs_in_kernel_window\<rbrace> set_asid_pool p ap \<lbrace>\<lambda>rv. cap_refs_in_kernel_window\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cap_refs_in_kernel_window\<rbrace> set_object p (ArchObj (ASIDPool ap)) \<lbrace>\<lambda>rv. cap_refs_in_kernel_window\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cap_refs_in_kernel_window\<rbrace> set_object p (ArchObj (ASIDPool ap)) \<lbrace>\<lambda>rv. cap_refs_in_kernel_window\<rbrace>
theory ArchAcc_AI

lemma set_asid_pool_caps_respects_device_region[wp]:
  "\<lbrace>cap_refs_respects_device_region\<rbrace> set_asid_pool p ap \<lbrace>\<lambda>rv. cap_refs_respects_device_region\<rbrace>" apply (simp add: set_asid_pool_def) apply (wp set_object_cap_refs_respects_device_region[THEN hoare_set_object_weaken_pre]) including unfold_objects by (simp add: a_type_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cap_refs_respects_device_region\<rbrace> set_asid_pool p ap \<lbrace>\<lambda>rv. cap_refs_respects_device_region\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cap_refs_respects_device_region\<rbrace> set_object p (ArchObj (ASIDPool ap)) \<lbrace>\<lambda>rv. cap_refs_respects_device_region\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cap_refs_respects_device_region s \<Longrightarrow> \<forall>ko. ko_at ko p s \<longrightarrow> a_type (ArchObj (ASIDPool ap)) = a_type ko \<longrightarrow> (cap_refs_respects_device_region and obj_at (same_caps (ArchObj (ASIDPool ap))) p) s proof (prove)
goal (1 subgoal):
 1. \<And>s. cap_refs_respects_device_region s \<Longrightarrow> \<forall>ko. ko_at ko p s \<longrightarrow> a_type (ArchObj (ASIDPool ap)) = a_type ko \<longrightarrow> (cap_refs_respects_device_region and obj_at (same_caps (ArchObj (ASIDPool ap))) p) s
theory ArchAcc_AI

lemma set_asid_pool_valid_ioc[wp]:
  "\<lbrace>valid_ioc\<rbrace> set_asid_pool p ap \<lbrace>\<lambda>_. valid_ioc\<rbrace>" apply (simp add: set_asid_pool_def) apply (wp set_object_valid_ioc_no_caps[THEN hoare_set_object_weaken_pre]) including unfold_objects by (clarsimp simp: valid_def get_object_def simpler_gets_def assert_def
          return_def fail_def bind_def
          a_type_simps is_tcb is_cap_table)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_ioc\<rbrace> set_asid_pool p ap \<lbrace>\<lambda>_. valid_ioc\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_ioc\<rbrace> set_object p (ArchObj (ASIDPool ap)) \<lbrace>\<lambda>_. valid_ioc\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_ioc s \<Longrightarrow> \<forall>ko. ko_at ko p s \<longrightarrow> a_type (ArchObj (ASIDPool ap)) = a_type ko \<longrightarrow> valid_ioc s \<and> typ_at (a_type (ArchObj (ASIDPool ap))) p s \<and> \<not> is_tcb (ArchObj (ASIDPool ap)) \<and> (\<forall>n. \<not> is_cap_table n (ArchObj (ASIDPool ap))) proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_ioc s \<Longrightarrow> \<forall>ko. ko_at ko p s \<longrightarrow> a_type (ArchObj (ASIDPool ap)) = a_type ko \<longrightarrow> valid_ioc s \<and> typ_at (a_type (ArchObj (ASIDPool ap))) p s \<and> \<not> is_tcb (ArchObj (ASIDPool ap)) \<and> (\<forall>n. \<not> is_cap_table n (ArchObj (ASIDPool ap)))
theory ArchAcc_AI

lemma set_asid_pool_vms[wp]:
  "\<lbrace>valid_machine_state\<rbrace> set_asid_pool p S \<lbrace>\<lambda>_. valid_machine_state\<rbrace>" apply (simp add: set_asid_pool_def set_object_def) apply (wp get_object_wp) apply clarify apply (erule valid_machine_state_heap_updI) apply (fastforce simp: a_type_def obj_at_def
                  split: kernel_object.splits arch_kernel_obj.splits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_machine_state\<rbrace> set_asid_pool p S \<lbrace>\<lambda>_. valid_machine_state\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_machine_state\<rbrace> do kobj <- get_object p;
y <- assert (a_type kobj = a_type (ArchObj (ASIDPool S)));
s <- get;
put (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool S))\<rparr>)
od \<lbrace>\<lambda>_. valid_machine_state\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_machine_state s \<Longrightarrow> \<forall>ko. ko_at ko p s \<longrightarrow> a_type ko = a_type (ArchObj (ASIDPool S)) \<longrightarrow> valid_machine_state (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool S))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>valid_machine_state s; ko_at ko p s; a_type ko = a_type (ArchObj (ASIDPool S))\<rbrakk> \<Longrightarrow> valid_machine_state (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool S))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s ko. \<lbrakk>ko_at ko p s; a_type ko = a_type (ArchObj (ASIDPool S))\<rbrakk> \<Longrightarrow> typ_at (?type11 s ko) p s
 2. \<And>s ko. \<lbrakk>ko_at ko p s; a_type ko = a_type (ArchObj (ASIDPool S))\<rbrakk> \<Longrightarrow> a_type (ArchObj (ASIDPool S)) = ?type11 s ko proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma mdb_cte_at_set_asid_pool[wp]:
  "\<lbrace>\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrace>
   set_asid_pool y pool
   \<lbrace>\<lambda>r s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrace>" apply (clarsimp simp:mdb_cte_at_def) apply (simp only: imp_conv_disj) apply (wp hoare_vcg_disj_lift hoare_vcg_all_lift) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s)\<rbrace> set_asid_pool y pool \<lbrace>\<lambda>r s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> cte_wp_at ((\<noteq>) NullCap) (a, b) s \<and> cte_wp_at ((\<noteq>) NullCap) (aa, ba) s\<rbrace> set_asid_pool y pool \<lbrace>\<lambda>r s. \<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> cte_wp_at ((\<noteq>) NullCap) (a, b) s \<and> cte_wp_at ((\<noteq>) NullCap) (aa, ba) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>a b aa ba. cdt s (aa, ba) \<noteq> Some (a, b) \<or> cte_wp_at ((\<noteq>) NullCap) (a, b) s \<and> cte_wp_at ((\<noteq>) NullCap) (aa, ba) s\<rbrace> set_asid_pool y pool \<lbrace>\<lambda>r s. \<forall>a b aa ba. cdt s (aa, ba) \<noteq> Some (a, b) \<or> cte_wp_at ((\<noteq>) NullCap) (a, b) s \<and> cte_wp_at ((\<noteq>) NullCap) (aa, ba) s\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma set_asid_pool_invs_unmap:
  "\<lbrace>invs and ko_at (ArchObj (ASIDPool ap)) p and
    (\<lambda>s. \<forall>asid. asid \<le> mask asid_bits \<longrightarrow> ucast asid = x \<longrightarrow>
                arm_asid_table (arch_state s) (asid_high_bits_of asid) = Some p \<longrightarrow>
                arm_asid_map (arch_state s) asid = None)\<rbrace>
       set_asid_pool p (ap(x := None)) \<lbrace>\<lambda>_. invs\<rbrace>" using set_asid_pool_invs_restrict[where S="- {x}"] by (simp add: restrict_map_def fun_upd_def if_flip)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and ako_at (ASIDPool ap) p and (\<lambda>s. \<forall>asid\<le>mask local.asid_bits. UCAST(32 \<rightarrow> 10) asid = x \<longrightarrow> asid_table s (asid_high_bits_of asid) = Some p \<longrightarrow> arm_asid_map (arch_state s) asid = None)\<rbrace> set_asid_pool p (ap(x := None)) \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
using this:
\<lbrace>invs and ako_at (ASIDPool ?ap) ?p and (\<lambda>s. \<forall>asid\<le>mask local.asid_bits. UCAST(32 \<rightarrow> 10) asid \<notin> - {x} \<longrightarrow> asid_table s (asid_high_bits_of asid) = Some ?p \<longrightarrow> arm_asid_map (arch_state s) asid = None)\<rbrace> set_asid_pool ?p (?ap |` (- {x})) \<lbrace>\<lambda>_. invs\<rbrace>

goal (1 subgoal):
 1. \<lbrace>invs and ako_at (ASIDPool ap) p and (\<lambda>s. \<forall>asid\<le>mask local.asid_bits. UCAST(32 \<rightarrow> 10) asid = x \<longrightarrow> asid_table s (asid_high_bits_of asid) = Some p \<longrightarrow> arm_asid_map (arch_state s) asid = None)\<rbrace> set_asid_pool p (ap(x := None)) \<lbrace>\<lambda>_. invs\<rbrace>
theory ArchAcc_AI

lemma valid_slots_typ_at:
  assumes x: "\<And>T p. \<lbrace>typ_at (AArch T) p\<rbrace> f \<lbrace>\<lambda>rv. typ_at (AArch T) p\<rbrace>"
  assumes y: "\<And>p. \<lbrace>\<exists>\<rhd> p\<rbrace> f \<lbrace>\<lambda>rv. \<exists>\<rhd> p\<rbrace>"
  shows "\<lbrace>valid_slots m\<rbrace> f \<lbrace>\<lambda>rv. valid_slots m\<rbrace>" unfolding valid_slots_def by (cases m; clarsimp; wp x y hoare_vcg_const_Ball_lift valid_pte_lift
                            valid_pde_lift pte_at_atyp pde_at_atyp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_slots m\<rbrace> f \<lbrace>\<lambda>rv. valid_slots m\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>case m of Inl (pte, xs) \<Rightarrow> \<lambda>s. xs \<noteq> [] \<and> (\<forall>p\<in>set xs. ((\<lambda>s. \<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) and pte_at p) s) \<and> wellformed_pte pte \<and> valid_pte pte s | Inr (pde, xs) \<Rightarrow> \<lambda>s. xs \<noteq> [] \<and> (\<forall>p\<in>set xs. ((\<lambda>s. \<exists>ref. (ref \<rhd> (p && ~~ mask pd_bits)) s) and pde_at p) s \<and> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots) \<and> wellformed_pde pde \<and> valid_pde pde s\<rbrace> f \<lbrace>\<lambda>rv. case m of Inl (pte, xs) \<Rightarrow> \<lambda>s. xs \<noteq> [] \<and> (\<forall>p\<in>set xs. ((\<lambda>s. \<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) and pte_at p) s) \<and> wellformed_pte pte \<and> valid_pte pte s | Inr (pde, xs) \<Rightarrow> \<lambda>s. xs \<noteq> [] \<and> (\<forall>p\<in>set xs. ((\<lambda>s. \<exists>ref. (ref \<rhd> (p && ~~ mask pd_bits)) s) and pde_at p) s \<and> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots) \<and> wellformed_pde pde \<and> valid_pde pde s\<rbrace>
theory ArchAcc_AI

lemma kernel_base_kernel_mapping_slots:
  "x < kernel_base \<Longrightarrow> ucast (x >> 20) \<notin> kernel_mapping_slots" apply (simp add: kernel_mapping_slots_def kernel_base_def) apply (subst ucast_le_ucast[symmetric, where 'a=12 and 'b=32]) apply simp apply (subst ucast_ucast_mask) apply (simp add: ucast_def) apply (subst less_mask_eq) apply (rule vptr_shiftr_le_2p[unfolded pageBits_def]) apply (subst word_not_le) apply word_bitwise done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x < kernel_base \<Longrightarrow> UCAST(32 \<rightarrow> 12) (x >> 20) \<notin> kernel_mapping_slots proof (prove)
goal (1 subgoal):
 1. x < 0xE0000000 \<Longrightarrow> \<not> 0xE00 \<le> UCAST(32 \<rightarrow> 12) (x >> 20) proof (prove)
goal (2 subgoals):
 1. x < 0xE0000000 \<Longrightarrow> LENGTH(12) \<le> LENGTH(32)
 2. x < 0xE0000000 \<Longrightarrow> \<not> UCAST(12 \<rightarrow> 32) 0xE00 \<le> UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (x >> 20)) proof (prove)
goal (1 subgoal):
 1. x < 0xE0000000 \<Longrightarrow> \<not> UCAST(12 \<rightarrow> 32) 0xE00 \<le> UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (x >> 20)) proof (prove)
goal (1 subgoal):
 1. x < 0xE0000000 \<Longrightarrow> \<not> UCAST(12 \<rightarrow> 32) 0xE00 \<le> (x >> 20) && mask LENGTH(12) proof (prove)
goal (1 subgoal):
 1. x < 0xE0000000 \<Longrightarrow> \<not> 0xE00 \<le> (x >> 20) && mask 12 proof (prove)
goal (2 subgoals):
 1. x < 0xE0000000 \<Longrightarrow> x >> 20 < 2 ^ 12
 2. x < 0xE0000000 \<Longrightarrow> \<not> 0xE00 \<le> x >> 20 proof (prove)
goal (1 subgoal):
 1. x < 0xE0000000 \<Longrightarrow> \<not> 0xE00 \<le> x >> 20 proof (prove)
goal (1 subgoal):
 1. x < 0xE0000000 \<Longrightarrow> x >> 20 < 0xE00 proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma pd_aligned:
  "\<lbrakk>pspace_aligned s; page_directory_at pd s\<rbrakk> \<Longrightarrow> is_aligned pd 14" apply (clarsimp simp: pspace_aligned_def obj_at_def) apply (drule bspec, blast) apply (clarsimp simp: a_type_def split: kernel_object.splits arch_kernel_obj.splits if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_aligned s; typ_at (AArch APageDirectory) pd s\<rbrakk> \<Longrightarrow> is_aligned pd 14 proof (prove)
goal (1 subgoal):
 1. \<And>pda. \<lbrakk>\<forall>x\<in>dom (kheap s). is_aligned x (obj_bits (the (kheap s x))); kheap s pd = Some (ArchObj (PageDirectory pda))\<rbrakk> \<Longrightarrow> is_aligned pd 14 proof (prove)
goal (1 subgoal):
 1. \<And>pda. \<lbrakk>kheap s pd = Some (ArchObj (PageDirectory pda)); is_aligned pd (obj_bits (the (kheap s pd)))\<rbrakk> \<Longrightarrow> is_aligned pd 14 proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma shiftr_shiftl_mask_pd_bits:
  "(((vptr :: word32) >> 20) << 2) && mask pd_bits = (vptr >> 20) << 2" apply (rule iffD2 [OF mask_eq_iff_w2p]) apply (simp add: pd_bits_def pageBits_def word_size) apply (rule shiftl_less_t2n) apply (rule shiftr_less_t2n3,
          simp_all add: pd_bits_def word_bits_def pageBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (vptr >> 20 << 2) && mask pd_bits = vptr >> 20 << 2 proof (prove)
goal (2 subgoals):
 1. pd_bits < size (vptr >> 20 << 2)
 2. vptr >> 20 << 2 < 2 ^ pd_bits proof (prove)
goal (1 subgoal):
 1. vptr >> 20 << 2 < 2 ^ pd_bits proof (prove)
goal (2 subgoals):
 1. vptr >> 20 < 2 ^ (pd_bits - 2)
 2. pd_bits < LENGTH(32) proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma triple_shift_fun:
  "x >> 20 << 2 >> 2 = (x :: ('a :: len) word) >> 20" apply (rule word_eqI) apply (simp add: word_size nth_shiftr nth_shiftl) apply safe apply (drule test_bit_size) apply (simp add: word_size) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x >> 20 << 2 >> 2 = x >> 20 proof (prove)
goal (1 subgoal):
 1. \<And>n. n < size (x >> 20 << 2 >> 2) \<longrightarrow> (x >> 20 << 2 >> 2) !! n = (x >> 20) !! n proof (prove)
goal (1 subgoal):
 1. \<And>n. n < LENGTH('a) \<longrightarrow> (Suc (Suc n) < LENGTH('a) \<and> x !! (20 + n)) = x !! (20 + n) proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>n < LENGTH('a); x !! (20 + n)\<rbrakk> \<Longrightarrow> Suc (Suc n) < LENGTH('a) proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>n < LENGTH('a); 20 + n < size x\<rbrakk> \<Longrightarrow> Suc (Suc n) < LENGTH('a) proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma shiftr_20_unat_ucast:
  "unat (ucast (x >> 20 :: word32) :: 12 word) = unat (x >> 20)" using vptr_shiftr_le_2p[where vptr=x] apply (simp only: unat_ucast) apply (rule mod_less) apply (rule unat_less_power) apply (simp add: word_bits_def) apply (simp add: pageBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat (UCAST(32 \<rightarrow> 12) (x >> 20)) = unat (x >> 20) proof (prove)
using this:
x >> 20 < 2 ^ pageBits

goal (1 subgoal):
 1. unat (UCAST(32 \<rightarrow> 12) (x >> 20)) = unat (x >> 20) proof (prove)
goal (1 subgoal):
 1. x >> 20 < 2 ^ pageBits \<Longrightarrow> unat (x >> 20) mod 2 ^ LENGTH(12) = unat (x >> 20) proof (prove)
goal (1 subgoal):
 1. x >> 20 < 2 ^ pageBits \<Longrightarrow> unat (x >> 20) < 2 ^ LENGTH(12) proof (prove)
goal (2 subgoals):
 1. x >> 20 < 2 ^ pageBits \<Longrightarrow> LENGTH(12) < LENGTH(32)
 2. x >> 20 < 2 ^ pageBits \<Longrightarrow> x >> 20 < 2 ^ LENGTH(12) proof (prove)
goal (1 subgoal):
 1. x >> 20 < 2 ^ pageBits \<Longrightarrow> x >> 20 < 2 ^ LENGTH(12) proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma shiftr_20_less:
  "((ucast (x >> 20) :: 12 word) < ucast (y >> 20)) = ((x >> 20 :: word32) < y >> 20)"
  "((ucast (x >> 20) :: 12 word) \<le> ucast (y >> 20)) = ((x >> 20 :: word32) \<le> y >> 20)" by (simp add: word_less_nat_alt word_le_nat_alt shiftr_20_unat_ucast)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (UCAST(32 \<rightarrow> 12) (x >> 20) < UCAST(32 \<rightarrow> 12) (y >> 20)) = (x >> 20 < y >> 20) &&& (UCAST(32 \<rightarrow> 12) (x >> 20) \<le> UCAST(32 \<rightarrow> 12) (y >> 20)) = (x >> 20 \<le> y >> 20)
theory ArchAcc_AI

lemma kernel_base_aligned_pageBits:
  "is_aligned kernel_base pageBits" by (simp add: is_aligned_def kernel_base_def pageBits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned kernel_base pageBits
theory ArchAcc_AI

lemma kernel_base_ge_observation:
  "(kernel_base \<le> x) = (x && ~~ mask 29 = kernel_base)" apply (subst mask_in_range) apply (simp add: kernel_base_def is_aligned_def) apply (simp add: kernel_base_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (kernel_base \<le> x) = (x && ~~ mask 29 = kernel_base) proof (prove)
goal (2 subgoals):
 1. is_aligned kernel_base 29
 2. (kernel_base \<le> x) = (x \<in> {kernel_base..kernel_base + 2 ^ 29 - 1}) proof (prove)
goal (1 subgoal):
 1. (kernel_base \<le> x) = (x \<in> {kernel_base..kernel_base + 2 ^ 29 - 1}) proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma kernel_base_less_observation:
  "(x < kernel_base) = (x && ~~ mask 29 \<noteq> kernel_base)" apply (simp add: linorder_not_le[symmetric] kernel_base_ge_observation) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x < kernel_base) = (x && ~~ mask 29 \<noteq> kernel_base) proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma is_aligned_lookup_pd_slot:
  "\<lbrakk>is_aligned vptr 24; is_aligned pd 6\<rbrakk>
   \<Longrightarrow> is_aligned (lookup_pd_slot pd vptr) 6" apply (clarsimp simp: lookup_pd_slot_def) apply (erule aligned_add_aligned) apply (rule is_aligned_shiftl) apply (rule is_aligned_shiftr) apply simp apply (simp add: word_bits_conv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned vptr 24; is_aligned pd 6\<rbrakk> \<Longrightarrow> is_aligned (lookup_pd_slot pd vptr) 6 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned vptr 24; is_aligned pd 6\<rbrakk> \<Longrightarrow> is_aligned (pd + (vptr >> 20 << 2)) 6 proof (prove)
goal (2 subgoals):
 1. is_aligned vptr 24 \<Longrightarrow> is_aligned (vptr >> 20 << 2) 6
 2. is_aligned vptr 24 \<Longrightarrow> 6 \<le> 6 proof (prove)
goal (2 subgoals):
 1. is_aligned vptr 24 \<Longrightarrow> is_aligned (vptr >> 20) (6 - 2)
 2. is_aligned vptr 24 \<Longrightarrow> 6 \<le> 6 proof (prove)
goal (2 subgoals):
 1. is_aligned vptr 24 \<Longrightarrow> is_aligned vptr (6 - 2 + 20)
 2. is_aligned vptr 24 \<Longrightarrow> 6 \<le> 6 proof (prove)
goal (1 subgoal):
 1. is_aligned vptr 24 \<Longrightarrow> 6 \<le> 6 proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma lookup_pd_slot_eq:
  "is_aligned pd pd_bits \<Longrightarrow>
   (lookup_pd_slot pd vptr && ~~ mask pd_bits) = pd" apply (clarsimp simp: lookup_pd_slot_def) apply (erule conjunct2[OF is_aligned_add_helper]) apply (rule shiftl_less_t2n) apply (rule shiftr_less_t2n3) apply (simp_all add: pd_bits_def pageBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned pd pd_bits \<Longrightarrow> lookup_pd_slot pd vptr && ~~ mask pd_bits = pd proof (prove)
goal (1 subgoal):
 1. is_aligned pd pd_bits \<Longrightarrow> pd + (vptr >> 20 << 2) && ~~ mask pd_bits = pd proof (prove)
goal (1 subgoal):
 1. vptr >> 20 << 2 < 2 ^ pd_bits proof (prove)
goal (2 subgoals):
 1. vptr >> 20 < 2 ^ (pd_bits - 2)
 2. pd_bits < LENGTH(32) proof (prove)
goal (3 subgoals):
 1. 2 ^ (20 + (pd_bits - 2)) = 0
 2. pd_bits - 2 < LENGTH(32)
 3. pd_bits < LENGTH(32) proof (prove)
goal:
No subgoals!