theory ArchUserOp_IF

lemma requiv_get_page_info_eq:
  "\<lbrakk> reads_equiv aag s s'; pas_refined aag s; is_subject aag pd; x \<notin> kernel_mappings \<rbrakk>
     \<Longrightarrow> get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) pd x =
         get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) pd x" apply (simp add: get_page_info_def) apply (subst requiv_get_pd_entry_eq[symmetric], simp+) apply (clarsimp split: option.splits pde.splits) apply (frule pt_in_pd_same_agent, fastforce+) apply (rule requiv_get_pt_info_eq, simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; is_subject aag pd; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) pd x = get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) pd x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; is_subject aag pd; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> (case get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) pd x of None \<Rightarrow> None | Some InvalidPDE \<Rightarrow> None | Some (PageTablePDE p xa xaa) \<Rightarrow> get_pt_info (\<lambda>obj. get_arch_obj (kheap s obj)) (ptrFromPAddr p) x | Some (SectionPDE base attrs x rights) \<Rightarrow> Some (base, 20, attrs, rights) | Some (SuperSectionPDE base attrs rights) \<Rightarrow> Some (base, 24, attrs, rights)) = (case get_pd_entry (\<lambda>obj. get_arch_obj (kheap s' obj)) pd x of None \<Rightarrow> None | Some InvalidPDE \<Rightarrow> None | Some (PageTablePDE p xa xaa) \<Rightarrow> get_pt_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (ptrFromPAddr p) x | Some (SectionPDE base attrs x rights) \<Rightarrow> Some (base, 20, attrs, rights) | Some (SuperSectionPDE base attrs rights) \<Rightarrow> Some (base, 24, attrs, rights)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; is_subject aag pd; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> (case get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) pd x of None \<Rightarrow> None | Some InvalidPDE \<Rightarrow> None | Some (PageTablePDE p xa xaa) \<Rightarrow> get_pt_info (\<lambda>obj. get_arch_obj (kheap s obj)) (ptrFromPAddr p) x | Some (SectionPDE base attrs x rights) \<Rightarrow> Some (base, 20, attrs, rights) | Some (SuperSectionPDE base attrs rights) \<Rightarrow> Some (base, 24, attrs, rights)) = (case get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) pd x of None \<Rightarrow> None | Some InvalidPDE \<Rightarrow> None | Some (PageTablePDE p xa xaa) \<Rightarrow> get_pt_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (ptrFromPAddr p) x | Some (SectionPDE base attrs x rights) \<Rightarrow> Some (base, 20, attrs, rights) | Some (SuperSectionPDE base attrs rights) \<Rightarrow> Some (base, 24, attrs, rights)) proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22 x23. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; is_subject aag pd; x \<notin> kernel_mappings; get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) pd x = Some (PageTablePDE x21 x22 x23)\<rbrakk> \<Longrightarrow> get_pt_info (\<lambda>obj. get_arch_obj (kheap s obj)) (ptrFromPAddr x21) x = get_pt_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (ptrFromPAddr x21) x proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22 x23. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; is_subject aag pd; x \<notin> kernel_mappings; get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) pd x = Some (PageTablePDE x21 x22 x23); pasObjectAbs aag pd = pasObjectAbs aag (ptrFromPAddr x21)\<rbrakk> \<Longrightarrow> get_pt_info (\<lambda>obj. get_arch_obj (kheap s obj)) (ptrFromPAddr x21) x = get_pt_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (ptrFromPAddr x21) x proof (prove)
goal:
No subgoals!