theory ArchArch_IF

lemma cte_wp_at_page_directory_not_in_kernel_mappings:
  "\<lbrakk> cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap word optiona))) slot s;
     x \<le> (kernel_base >> 20) - 1; valid_objs s; valid_global_refs s \<rbrakk>
     \<Longrightarrow> ucast ((x << 2) + word && mask pd_bits >> 2) \<notin> kernel_mapping_slots" apply (frule (1) cte_wp_at_valid_objs_valid_cap) apply (simp add: cte_wp_at_caps_of_state) apply (drule (1) valid_global_refsD2) apply (simp add: cap_range_def) apply (frule valid_cap_aligned) apply (simp add: cap_aligned_def) apply (subgoal_tac "is_aligned word pd_bits") apply (rule pd_shifting_kernel_mapping_slots) apply (simp add: pd_bits_def pageBits_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap word optiona))) slot s; x \<le> (kernel_base >> 20) - 1; valid_objs s; valid_global_refs s\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) ((x << 2) + word && mask pd_bits >> 2) \<notin> kernel_mapping_slots proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap word optiona))) slot s; x \<le> (kernel_base >> 20) - 1; valid_objs s; valid_global_refs s; \<exists>cap. ArchObjectCap (PageDirectoryCap word optiona) = cap \<and> s \<turnstile> cap\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) ((x << 2) + word && mask pd_bits >> 2) \<notin> kernel_mapping_slots proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s slot = Some (ArchObjectCap (PageDirectoryCap word optiona)); x \<le> (kernel_base >> 20) - 1; valid_objs s; valid_global_refs s; s \<turnstile> ArchObjectCap (PageDirectoryCap word optiona)\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) ((x << 2) + word && mask pd_bits >> 2) \<notin> kernel_mapping_slots proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<le> (kernel_base >> 20) - 1; valid_objs s; valid_global_refs s; s \<turnstile> ArchObjectCap (PageDirectoryCap word optiona); global_refs s \<inter> cap_range (ArchObjectCap (PageDirectoryCap word optiona)) = {}\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) ((x << 2) + word && mask pd_bits >> 2) \<notin> kernel_mapping_slots proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<le> (kernel_base >> 20) - 1; valid_objs s; valid_global_refs s; s \<turnstile> ArchObjectCap (PageDirectoryCap word optiona); word \<notin> global_refs s\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) ((x << 2) + word && mask pd_bits >> 2) \<notin> kernel_mapping_slots proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<le> (kernel_base >> 20) - 1; valid_objs s; valid_global_refs s; s \<turnstile> ArchObjectCap (PageDirectoryCap word optiona); word \<notin> global_refs s; cap_aligned (ArchObjectCap (PageDirectoryCap word optiona))\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) ((x << 2) + word && mask pd_bits >> 2) \<notin> kernel_mapping_slots proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<le> (kernel_base >> 20) - 1; valid_objs s; valid_global_refs s; s \<turnstile> ArchObjectCap (PageDirectoryCap word optiona); word \<notin> global_refs s; is_aligned word 14 \<and> 14 < word_bits\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) ((x << 2) + word && mask pd_bits >> 2) \<notin> kernel_mapping_slots proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<le> (kernel_base >> 20) - 1; valid_objs s; valid_global_refs s; s \<turnstile> ArchObjectCap (PageDirectoryCap word optiona); word \<notin> global_refs s; is_aligned word 14 \<and> 14 < word_bits; is_aligned word pd_bits\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) ((x << 2) + word && mask pd_bits >> 2) \<notin> kernel_mapping_slots
 2. \<lbrakk>x \<le> (kernel_base >> 20) - 1; valid_objs s; valid_global_refs s; s \<turnstile> ArchObjectCap (PageDirectoryCap word optiona); word \<notin> global_refs s; is_aligned word 14 \<and> 14 < word_bits\<rbrakk> \<Longrightarrow> is_aligned word pd_bits proof (prove)
goal (3 subgoals):
 1. \<lbrakk>x \<le> (kernel_base >> 20) - 1; valid_objs s; valid_global_refs s; s \<turnstile> ArchObjectCap (PageDirectoryCap word optiona); word \<notin> global_refs s; is_aligned word 14 \<and> 14 < word_bits; is_aligned word pd_bits\<rbrakk> \<Longrightarrow> is_aligned word pd_bits
 2. \<lbrakk>x \<le> (kernel_base >> 20) - 1; valid_objs s; valid_global_refs s; s \<turnstile> ArchObjectCap (PageDirectoryCap word optiona); word \<notin> global_refs s; is_aligned word 14 \<and> 14 < word_bits; is_aligned word pd_bits\<rbrakk> \<Longrightarrow> x \<le> (kernel_base >> 20) - 1
 3. \<lbrakk>x \<le> (kernel_base >> 20) - 1; valid_objs s; valid_global_refs s; s \<turnstile> ArchObjectCap (PageDirectoryCap word optiona); word \<notin> global_refs s; is_aligned word 14 \<and> 14 < word_bits\<rbrakk> \<Longrightarrow> is_aligned word pd_bits proof (prove)
goal:
No subgoals!