theory ArchArch_IF

lemma perform_page_table_invocation_globals_equiv:
  "\<lbrace>valid_global_refs and valid_global_objs and valid_arch_state and globals_equiv st
                      and pspace_aligned and valid_vspace_objs and valid_vs_lookup
                      and valid_kernel_mappings and authorised_for_globals_page_table_inv pti\<rbrace>
   perform_page_table_invocation pti
   \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" unfolding perform_page_table_invocation_def cleanCacheRange_PoU_def apply (rule hoare_weaken_pre) apply (wp store_pde_globals_equiv set_cap_globals_equiv'' dmo_cacheRangeOp_lift
             mapM_x_swp_store_pte_globals_equiv unmap_page_table_globals_equiv
          | wpc | simp add: cleanByVA_PoU_def)+ apply (fastforce simp: authorised_for_globals_page_table_inv_def
                         valid_arch_state_def obj_at_def
                   dest: a_type_pdD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_refs and valid_global_objs and valid_arch_state and globals_equiv st and pspace_aligned and valid_vspace_objs and valid_vs_lookup and valid_kernel_mappings and authorised_for_globals_page_table_inv pti\<rbrace> perform_page_table_invocation pti \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_refs and valid_global_objs and valid_arch_state and globals_equiv st and pspace_aligned and valid_vspace_objs and valid_vs_lookup and valid_kernel_mappings and authorised_for_globals_page_table_inv pti\<rbrace> case pti of PageTableMap cap ct_slot pde pd_slot \<Rightarrow> do set_cap cap ct_slot;
store_pde pd_slot pde;
do_machine_op $ cleanByVA_PoU pd_slot (addrFromPPtr pd_slot)
od | PageTableUnmap (ArchObjectCap (PageTableCap p mapped_address)) ct_slot \<Rightarrow> do case mapped_address of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmap_page_table asid vaddr p;
pte_bits <- return 2;
slots <- return [p , p + (1 << pte_bits) .e. p + (1 << pt_bits) - 1];
mapM_x (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU p (p + (1 << pt_bits) - 1) (addrFromPPtr p)
od;
cap <- liftM the_arch_cap $ get_cap ct_slot;
set_cap (ArchObjectCap $ update_map_data cap None) ct_slot
od | PageTableUnmap (ArchObjectCap _) ct_slot \<Rightarrow> fail | PageTableUnmap _ ct_slot \<Rightarrow> fail \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> case pti of PageTableMap cap ct_slot pde pd_slot \<Rightarrow> do set_cap cap ct_slot;
store_pde pd_slot pde;
do_machine_op $ cleanByVA_PoU pd_slot (addrFromPPtr pd_slot)
od | PageTableUnmap (ArchObjectCap (PageTableCap p mapped_address)) ct_slot \<Rightarrow> do case mapped_address of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmap_page_table asid vaddr p;
pte_bits <- return 2;
slots <- return [p , p + (1 << pte_bits) .e. p + (1 << pt_bits) - 1];
mapM_x (swp store_pte InvalidPTE) slots;
do_machine_op $ cacheRangeOp cleanByVA_PoU p (p + (1 << pt_bits) - 1) (addrFromPPtr p)
od;
cap <- liftM the_arch_cap $ get_cap ct_slot;
set_cap (ArchObjectCap $ update_map_data cap None) ct_slot
od | PageTableUnmap (ArchObjectCap _) ct_slot \<Rightarrow> fail | PageTableUnmap _ ct_slot \<Rightarrow> fail \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<And>s. (valid_global_refs and valid_global_objs and valid_arch_state and globals_equiv st and pspace_aligned and valid_vspace_objs and valid_vs_lookup and valid_kernel_mappings and authorised_for_globals_page_table_inv pti) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_global_refs s \<and> valid_global_objs s \<and> valid_arch_state s \<and> globals_equiv st s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_vs_lookup s \<and> valid_kernel_mappings s \<and> authorised_for_globals_page_table_inv pti s \<Longrightarrow> \<forall>x a b xa xb. pti = PageTableMap x (a, b) xa xb \<longrightarrow> xb && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) proof (prove)
goal:
No subgoals!