theory ArchArch_IF

lemma unmap_page_table_globals_equiv:
  "\<lbrace>pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup
                   and valid_global_refs and valid_arch_state and globals_equiv st\<rbrace>
   unmap_page_table asid vaddr pt
   \<lbrace>\<lambda>rv. globals_equiv st\<rbrace>" unfolding unmap_page_table_def page_table_mapped_def apply (wp store_pde_globals_equiv | wpc | simp add: cleanByVA_PoU_def)+ apply (rule_tac Q="\<lambda>_. globals_equiv st and (\<lambda>sa. lookup_pd_slot pd vaddr &&
                                                    ~~ mask pd_bits \<noteq> arm_global_pd (arch_state sa))"
                  in hoare_strengthen_post) apply (wp find_pd_for_asid_not_arm_global_pd hoare_post_imp_dc2E_actual | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs and valid_arch_state and globals_equiv st\<rbrace> unmap_page_table asid vaddr pt \<lbrace>\<lambda>rv. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs and valid_arch_state and globals_equiv st\<rbrace> do pdOpt <- doE pd <- find_pd_for_asid asid;
pd_slot <- returnOk $ lookup_pd_slot pd vaddr;
pde <- liftE $ get_pde pd_slot;
case pde of PageTablePDE addr x xa \<Rightarrow> returnOk $ if addrFromPPtr pt = addr then Some pd else None | _ \<Rightarrow> returnOk None
odE <catch> (K $ return None);
case pdOpt of None \<Rightarrow> return () | Some pd \<Rightarrow> do pd_slot <- return $ lookup_pd_slot pd vaddr;
store_pde pd_slot InvalidPDE;
do_machine_op $ cleanByVA_PoU pd_slot (addrFromPPtr pd_slot);
flush_table pd asid vaddr pt
od
od \<lbrace>\<lambda>rv. globals_equiv st\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>pd pd_slot. \<lbrace>?P'177 pd pd_slot\<rbrace> get_pde pd_slot \<lbrace>\<lambda>pde s. (pde = InvalidPDE \<longrightarrow> globals_equiv st s) \<and> (\<forall>x. (addrFromPPtr pt = x \<longrightarrow> (\<exists>xa xb. pde = PageTablePDE x xa xb) \<longrightarrow> globals_equiv st s \<and> lookup_pd_slot pd vaddr && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s)) \<and> (addrFromPPtr pt \<noteq> x \<longrightarrow> (\<exists>xa xb. pde = PageTablePDE x xa xb) \<longrightarrow> globals_equiv st s)) \<and> ((\<exists>x xa xb xc. pde = SectionPDE x xa xb xc) \<longrightarrow> globals_equiv st s) \<and> ((\<exists>x xa xb. pde = SuperSectionPDE x xa xb) \<longrightarrow> globals_equiv st s)\<rbrace>
 2. \<And>pd. \<lbrace>?B127 pd\<rbrace> returnOk $ lookup_pd_slot pd vaddr \<lbrace>\<lambda>pd_slot s. True \<and> ?P'177 pd pd_slot s\<rbrace>, \<lbrace>\<lambda>rv s. \<forall>x. None = Some x \<longrightarrow> globals_equiv st s \<and> lookup_pd_slot x vaddr && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s)\<rbrace>
 3. \<lbrace>?P'44\<rbrace> find_pd_for_asid asid \<lbrace>?B127\<rbrace>, \<lbrace>\<lambda>rv s. \<forall>x. None = Some x \<longrightarrow> globals_equiv st s \<and> lookup_pd_slot x vaddr && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s)\<rbrace>
 4. \<And>s. (pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs and valid_arch_state and globals_equiv st) s \<Longrightarrow> (None = None \<longrightarrow> globals_equiv st s \<and> True \<and> True \<and> True) \<and> ?P'44 s proof (prove)
goal (5 subgoals):
 1. \<And>pd pd_slot. \<lbrace>?P'177 pd pd_slot\<rbrace> get_pde pd_slot \<lbrace>\<lambda>_. globals_equiv st and (\<lambda>sa. lookup_pd_slot pd vaddr && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state sa))\<rbrace>
 2. \<And>pd pd_slot rv s. (globals_equiv st and (\<lambda>sa. lookup_pd_slot pd vaddr && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state sa))) s \<Longrightarrow> (rv = InvalidPDE \<longrightarrow> globals_equiv st s) \<and> (\<forall>x. (addrFromPPtr pt = x \<longrightarrow> (\<exists>xa xb. rv = PageTablePDE x xa xb) \<longrightarrow> globals_equiv st s \<and> lookup_pd_slot pd vaddr && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s)) \<and> (addrFromPPtr pt \<noteq> x \<longrightarrow> (\<exists>xa xb. rv = PageTablePDE x xa xb) \<longrightarrow> globals_equiv st s)) \<and> ((\<exists>x xa xb xc. rv = SectionPDE x xa xb xc) \<longrightarrow> globals_equiv st s) \<and> ((\<exists>x xa xb. rv = SuperSectionPDE x xa xb) \<longrightarrow> globals_equiv st s)
 3. \<And>pd. \<lbrace>?B127 pd\<rbrace> returnOk $ lookup_pd_slot pd vaddr \<lbrace>\<lambda>pd_slot s. True \<and> ?P'177 pd pd_slot s\<rbrace>, \<lbrace>\<lambda>rv s. \<forall>x. None = Some x \<longrightarrow> globals_equiv st s \<and> lookup_pd_slot x vaddr && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s)\<rbrace>
 4. \<lbrace>?P'44\<rbrace> find_pd_for_asid asid \<lbrace>?B127\<rbrace>, \<lbrace>\<lambda>rv s. \<forall>x. None = Some x \<longrightarrow> globals_equiv st s \<and> lookup_pd_slot x vaddr && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s)\<rbrace>
 5. \<And>s. (pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs and valid_arch_state and globals_equiv st) s \<Longrightarrow> (None = None \<longrightarrow> globals_equiv st s \<and> True \<and> True \<and> True) \<and> ?P'44 s proof (prove)
goal:
No subgoals!