theory ArchArch_IF

lemma perform_page_invocation_globals_equiv:
  "\<lbrace>authorised_for_globals_page_inv pgi and valid_page_inv pgi and globals_equiv st and
    valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and
    valid_vs_lookup and valid_global_refs and ct_active and valid_idle\<rbrace>
   perform_page_invocation pgi
   \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" unfolding perform_page_invocation_def cleanCacheRange_PoU_def apply (rule hoare_weaken_pre) apply (wp mapM_swp_store_pte_globals_equiv hoare_vcg_all_lift dmo_cacheRangeOp_lift
            mapM_swp_store_pde_globals_equiv mapM_x_swp_store_pte_globals_equiv
            mapM_x_swp_store_pde_globals_equiv set_cap_globals_equiv''
            unmap_page_globals_equiv store_pte_globals_equiv store_pde_globals_equiv hoare_weak_lift_imp
            do_flush_globals_equiv set_mrs_globals_equiv set_message_info_globals_equiv
         | wpc | simp add: do_machine_op_bind cleanByVA_PoU_def)+ by (auto simp: cte_wp_parent_not_global_pd authorised_for_globals_page_inv_def valid_page_inv_def
                 valid_slots_def valid_idle_def st_tcb_def2 ct_in_state_def pred_tcb_at_def obj_at_def
          dest!: rev_subsetD[OF _ tl_subseteq])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>authorised_for_globals_page_inv pgi and valid_page_inv pgi and globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs and ct_active and valid_idle\<rbrace> perform_page_invocation pgi \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>authorised_for_globals_page_inv pgi and valid_page_inv pgi and globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs and ct_active and valid_idle\<rbrace> case pgi of PageMap asid cap ct_slot entries \<Rightarrow> do set_cap cap ct_slot;
case entries of Inl (pte, slots) \<Rightarrow> do flush <- pte_check_if_mapped (hd slots);
store_pte (hd slots) pte;
mapM (swp store_pte InvalidPTE) (tl slots);
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots));
if flush then invalidate_tlb_by_asid asid else return ()
od | Inr (pde, slots) \<Rightarrow> do flush <- pde_check_if_mapped (hd slots);
store_pde (hd slots) pde;
mapM (swp store_pde InvalidPDE) (tl slots);
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots));
if flush then invalidate_tlb_by_asid asid else return ()
od;
return []
od | PageUnmap (PageCap dev p R vp_size vp_mapped_addr) ct_slot \<Rightarrow> do case vp_mapped_addr of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmap_page vp_size asid vaddr p;
cap <- liftM the_arch_cap $ get_cap ct_slot;
set_cap (ArchObjectCap $ update_map_data cap None) ct_slot;
return []
od | PageUnmap _ ct_slot \<Rightarrow> fail | PageFlush typ start end pstart pd asid \<Rightarrow> do when (start < end) $ do root_switched <- set_vm_root_for_flush pd asid;
do_machine_op $ do_flush typ start end pstart;
when root_switched $ gets cur_thread >>= set_vm_root
od;
return []
od | PageGetAddr ptr \<Rightarrow> return [addrFromPPtr ptr] \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> case pgi of PageMap asid cap ct_slot entries \<Rightarrow> do set_cap cap ct_slot;
case entries of Inl (pte, slots) \<Rightarrow> do flush <- pte_check_if_mapped (hd slots);
store_pte (hd slots) pte;
mapM (swp store_pte InvalidPTE) (tl slots);
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots));
if flush then invalidate_tlb_by_asid asid else return ()
od | Inr (pde, slots) \<Rightarrow> do flush <- pde_check_if_mapped (hd slots);
store_pde (hd slots) pde;
mapM (swp store_pde InvalidPDE) (tl slots);
do_machine_op $ cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots));
if flush then invalidate_tlb_by_asid asid else return ()
od;
return []
od | PageUnmap (PageCap dev p R vp_size vp_mapped_addr) ct_slot \<Rightarrow> do case vp_mapped_addr of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> unmap_page vp_size asid vaddr p;
cap <- liftM the_arch_cap $ get_cap ct_slot;
set_cap (ArchObjectCap $ update_map_data cap None) ct_slot;
return []
od | PageUnmap _ ct_slot \<Rightarrow> fail | PageFlush typ start end pstart pd asid \<Rightarrow> do when (start < end) $ do root_switched <- set_vm_root_for_flush pd asid;
do_machine_op $ do_flush typ start end pstart;
when root_switched $ gets cur_thread >>= set_vm_root
od;
return []
od | PageGetAddr ptr \<Rightarrow> return [addrFromPPtr ptr] \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<And>s. (authorised_for_globals_page_inv pgi and valid_page_inv pgi and globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs and ct_active and valid_idle) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. authorised_for_globals_page_inv pgi s \<and> valid_page_inv pgi s \<and> globals_equiv st s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_global_objs s \<and> valid_vs_lookup s \<and> valid_global_refs s \<and> ct_active s \<and> valid_idle s \<Longrightarrow> \<forall>x xa a b xb. pgi = PageMap x xa (a, b) xb \<longrightarrow> (\<forall>a b. xb = Inr (a, b) \<longrightarrow> hd b && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) \<and> (\<forall>x\<in>set (tl b). x && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s)))