theory ArchArch_AI

lemma create_mapping_entries_same_refs_ex:
  "\<lbrace>valid_arch_state and valid_vspace_objs and valid_vs_lookup and (\<lambda>s. unique_table_refs (caps_of_state s))
    and pspace_aligned and valid_objs and valid_kernel_mappings and \<exists>\<rhd> pd and
    (\<lambda>s. \<exists>dev pd_cap pd_cptr asid rights'. cte_wp_at ((=) pd_cap) pd_cptr s
          \<and> pd_cap = cap.ArchObjectCap (arch_cap.PageDirectoryCap pd (Some asid))
          \<and> page_directory_at pd s \<and> vaddr < kernel_base \<and> (cap = (cap.ArchObjectCap (arch_cap.PageCap dev p rights' pgsz (Some (asid, vaddr))))))\<rbrace>
   create_mapping_entries (addrFromPPtr p) vaddr pgsz rights attribs pd
   \<lbrace>\<lambda>rv s. same_refs rv cap s\<rbrace>,-" apply (clarsimp simp: validE_R_def validE_def valid_def split: sum.split) apply (erule use_validE_R[OF _ create_mapping_entries_same_refs]) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_state and valid_vspace_objs and valid_vs_lookup and (\<lambda>s. unique_table_refs (caps_of_state s)) and pspace_aligned and valid_objs and valid_kernel_mappings and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and (\<lambda>s. \<exists>dev pd_cap pd_cptr asid rights'. cte_wp_at ((=) pd_cap) pd_cptr s \<and> pd_cap = ArchObjectCap (PageDirectoryCap pd (Some asid)) \<and> typ_at (AArch APageDirectory) pd s \<and> vaddr < kernel_base \<and> cap = ArchObjectCap (PageCap dev p rights' pgsz (Some (asid, vaddr))))\<rbrace> create_mapping_entries (addrFromPPtr p) vaddr pgsz rights attribs pd \<lbrace>\<lambda>rv. same_refs rv cap\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s b r ref dev aa asid ba rights'. \<lbrakk>(Inr r, b) \<in> fst (create_mapping_entries (addrFromPPtr p) vaddr pgsz rights attribs pd s); valid_arch_state s; valid_vspace_objs s; valid_vs_lookup s; unique_table_refs (caps_of_state s); pspace_aligned s; valid_objs s; valid_kernel_mappings s; (ref \<rhd> pd) s; cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap pd (Some asid)))) (aa, ba) s; typ_at (AArch APageDirectory) pd s; vaddr < kernel_base; cap = ArchObjectCap (PageCap dev p rights' pgsz (Some (asid, vaddr)))\<rbrakk> \<Longrightarrow> same_refs r (ArchObjectCap (PageCap dev p rights' pgsz (Some (asid, vaddr)))) b proof (prove)
goal (1 subgoal):
 1. \<And>s b r ref dev aa asid ba rights'. \<lbrakk>valid_arch_state s; valid_vspace_objs s; valid_vs_lookup s; unique_table_refs (caps_of_state s); pspace_aligned s; valid_objs s; valid_kernel_mappings s; (ref \<rhd> pd) s; cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap pd (Some asid)))) (aa, ba) s; typ_at (AArch APageDirectory) pd s; vaddr < kernel_base; cap = ArchObjectCap (PageCap dev p rights' pgsz (Some (asid, vaddr)))\<rbrakk> \<Longrightarrow> (valid_arch_state and valid_vspace_objs and valid_vs_lookup and (\<lambda>s. unique_table_refs (caps_of_state s)) and pspace_aligned and valid_objs and valid_kernel_mappings and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and (\<lambda>sa. \<exists>pd_cap pd_cptr. cte_wp_at ((=) pd_cap) pd_cptr sa \<and> pd_cap = ArchObjectCap (PageDirectoryCap pd (Some (?asid35 s b r ref dev aa asid ba rights')))) and typ_at (AArch APageDirectory) pd and K (vaddr < kernel_base \<and> ArchObjectCap (PageCap dev p rights' pgsz (Some (asid, vaddr))) = ArchObjectCap (PageCap (?dev35 s b r ref dev aa asid ba rights') p (?rights'35 s b r ref dev aa asid ba rights') pgsz (Some (?asid35 s b r ref dev aa asid ba rights', vaddr))))) s proof (prove)
goal:
No subgoals!