theory ArchArch_IF

lemma cte_wp_at_page_cap_bits :
  "\<lbrakk> cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot s; valid_objs s \<rbrakk>
     \<Longrightarrow> cte_wp_at (\<lambda>c. (\<lambda>x. x && ~~ mask pt_bits) ` set [word, word + 4 .e. word + 2 ^ pt_bits - 1]
                        \<subseteq> obj_refs c \<and> is_pt_cap c) slot s" apply (frule (1) cte_wp_at_valid_objs_valid_cap) apply (clarsimp simp: valid_cap_def cap_aligned_def) apply (erule cte_wp_at_weakenE) apply (unfold is_pt_cap_def) apply (subgoal_tac "is_aligned word pt_bits") prefer 2 apply (simp add: pt_bits_def pageBits_def) apply (auto simp: word_aligned_pt_slots) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot s; valid_objs s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. (\<lambda>x. x && ~~ mask pt_bits) ` set [word , word + 4 .e. word + 2 ^ pt_bits - 1] \<subseteq> obj_refs c \<and> is_pt_cap c) slot s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot s; valid_objs s; \<exists>cap. ArchObjectCap (PageTableCap word option) = cap \<and> s \<turnstile> cap\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. (\<lambda>x. x && ~~ mask pt_bits) ` set [word , word + 4 .e. word + 2 ^ pt_bits - 1] \<subseteq> obj_refs c \<and> is_pt_cap c) slot s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot s; valid_objs s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; case option of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vref < kernel_base \<and> is_aligned vref 20\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. (\<lambda>x. x && ~~ mask pt_bits) ` set [word , word + 4 .e. word + 2 ^ pt_bits - 1] \<subseteq> obj_refs c \<and> is_pt_cap c) slot s proof (prove)
goal (1 subgoal):
 1. \<And>c. \<lbrakk>valid_objs s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; case option of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vref < kernel_base \<and> is_aligned vref 20; ArchObjectCap (PageTableCap word option) = c\<rbrakk> \<Longrightarrow> (\<lambda>x. x && ~~ mask pt_bits) ` set [word , word + 4 .e. word + 2 ^ pt_bits - 1] \<subseteq> obj_refs c \<and> is_pt_cap c proof (prove)
goal (1 subgoal):
 1. \<And>c. \<lbrakk>valid_objs s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; case option of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vref < kernel_base \<and> is_aligned vref 20; ArchObjectCap (PageTableCap word option) = c\<rbrakk> \<Longrightarrow> (\<lambda>x. x && ~~ mask pt_bits) ` set [word , word + 4 .e. word + 2 ^ pt_bits - 1] \<subseteq> obj_refs c \<and> (\<exists>p asid. c = ArchObjectCap (PageTableCap p asid)) proof (prove)
goal (2 subgoals):
 1. \<And>c. \<lbrakk>valid_objs s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; case option of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vref < kernel_base \<and> is_aligned vref 20; ArchObjectCap (PageTableCap word option) = c; is_aligned word pt_bits\<rbrakk> \<Longrightarrow> (\<lambda>x. x && ~~ mask pt_bits) ` set [word , word + 4 .e. word + 2 ^ pt_bits - 1] \<subseteq> obj_refs c \<and> (\<exists>p asid. c = ArchObjectCap (PageTableCap p asid))
 2. \<And>c. \<lbrakk>valid_objs s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; case option of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vref < kernel_base \<and> is_aligned vref 20; ArchObjectCap (PageTableCap word option) = c\<rbrakk> \<Longrightarrow> is_aligned word pt_bits proof (prove)
goal (2 subgoals):
 1. \<And>c. \<lbrakk>valid_objs s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; case option of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vref < kernel_base \<and> is_aligned vref 20; ArchObjectCap (PageTableCap word option) = c\<rbrakk> \<Longrightarrow> is_aligned word pt_bits
 2. \<And>c. \<lbrakk>valid_objs s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; case option of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vref < kernel_base \<and> is_aligned vref 20; ArchObjectCap (PageTableCap word option) = c; is_aligned word pt_bits\<rbrakk> \<Longrightarrow> (\<lambda>x. x && ~~ mask pt_bits) ` set [word , word + 4 .e. word + 2 ^ pt_bits - 1] \<subseteq> obj_refs c \<and> (\<exists>p asid. c = ArchObjectCap (PageTableCap p asid)) proof (prove)
goal (1 subgoal):
 1. \<And>c. \<lbrakk>valid_objs s; is_aligned word 10; 10 < word_bits; typ_at (AArch APageTable) word s; case option of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vref < kernel_base \<and> is_aligned vref 20; ArchObjectCap (PageTableCap word option) = c; is_aligned word pt_bits\<rbrakk> \<Longrightarrow> (\<lambda>x. x && ~~ mask pt_bits) ` set [word , word + 4 .e. word + 2 ^ pt_bits - 1] \<subseteq> obj_refs c \<and> (\<exists>p asid. c = ArchObjectCap (PageTableCap p asid)) proof (prove)
goal:
No subgoals!