theory ArchArch_IF

lemma perform_page_invocation_reads_respects:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows "reads_respects aag l (pas_refined aag and K (authorised_page_inv aag pgi)
                                               and valid_page_inv pgi and valid_vspace_objs
                                               and pspace_aligned and is_subject aag \<circ> cur_thread)
                        (perform_page_invocation pgi)" unfolding perform_page_invocation_def fun_app_def when_def cleanCacheRange_PoU_def apply (rule equiv_valid_guard_imp) apply wpc apply (simp add: mapM_discarded swp_def) apply (wp dmo_mol_reads_respects dmo_cacheRangeOp_reads_respects  mapM_x_ev''
                store_pte_reads_respects set_cap_reads_respects mapM_ev'' store_pde_reads_respects
                unmap_page_reads_respects set_vm_root_reads_respects dmo_mol_2_reads_respects
                set_vm_root_for_flush_reads_respects get_cap_rev  do_flush_reads_respects
                invalidate_tlb_by_asid_reads_respects get_master_pte_reads_respects
                get_master_pde_reads_respects set_mrs_reads_respects set_message_info_reads_respects
             | simp add: cleanByVA_PoU_def pte_check_if_mapped_def pde_check_if_mapped_def
             | wpc | wp (once) hoare_drop_imps[where R="\<lambda>r s. r"])+ apply (clarsimp simp: authorised_page_inv_def valid_page_inv_def) apply (auto simp: cte_wp_at_caps_of_state valid_slots_def cap_auth_conferred_def
                    update_map_data_def is_page_cap_def authorised_slots_def valid_page_inv_def
                    valid_cap_simps cap_links_asid_slot_def label_owns_asid_slot_def
             dest!: bspec[OF _ rev_subsetD[OF _ tl_subseteq]] clas_caps_of_state pas_refined_Control
         | (frule aag_can_read_self, simp)+)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (pas_refined aag and K (authorised_page_inv aag pgi) and valid_page_inv pgi and valid_vspace_objs and pspace_aligned and is_subject aag \<circ> cur_thread) (perform_page_invocation pgi) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (pas_refined aag and K (authorised_page_inv aag pgi) and valid_page_inv pgi and valid_vspace_objs and pspace_aligned and is_subject aag \<circ> cur_thread) (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 if start < end then do root_switched <- set_vm_root_for_flush pd asid;
do_machine_op (do_flush typ start end pstart);
if root_switched then gets cur_thread >>= set_vm_root else return ()
od else return ();
return []
od | PageGetAddr ptr \<Rightarrow> return [addrFromPPtr ptr]) proof (prove)
goal (2 subgoals):
 1. reads_respects aag l ?Q (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 if start < end then do root_switched <- set_vm_root_for_flush pd asid;
do_machine_op (do_flush typ start end pstart);
if root_switched then gets cur_thread >>= set_vm_root else return ()
od else return ();
return []
od | PageGetAddr ptr \<Rightarrow> return [addrFromPPtr ptr])
 2. \<And>s. (pas_refined aag and K (authorised_page_inv aag pgi) and valid_page_inv pgi and valid_vspace_objs and pspace_aligned and is_subject aag \<circ> cur_thread) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>x11 x12 x13 x14. pgi = PageMap x11 x12 x13 x14 \<Longrightarrow> reads_respects aag l (?R27 x11 x12 x13 x14) (do set_cap x12 x13;
case x14 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 x11 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 x11 else return ()
od;
return []
od)
 2. \<And>x21 x22. pgi = PageUnmap x21 x22 \<Longrightarrow> reads_respects aag l (?R28 x21 x22) (case x21 of PageCap dev p R vp_size vp_mapped_addr \<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 x22);
set_cap (ArchObjectCap (update_map_data cap None)) x22;
return []
od | _ \<Rightarrow> fail)
 3. \<And>x31 x32 x33 x34 x35 x36. pgi = PageFlush x31 x32 x33 x34 x35 x36 \<Longrightarrow> reads_respects aag l (?R29 x31 x32 x33 x34 x35 x36) (do if x32 < x33 then do root_switched <- set_vm_root_for_flush x35 x36;
do_machine_op (do_flush x31 x32 x33 x34);
if root_switched then gets cur_thread >>= set_vm_root else return ()
od else return ();
return []
od)
 4. \<And>x4. pgi = PageGetAddr x4 \<Longrightarrow> reads_respects aag l (?R30 x4) (return [addrFromPPtr x4])
 5. \<And>s. (pas_refined aag and K (authorised_page_inv aag pgi) and valid_page_inv pgi and valid_vspace_objs and pspace_aligned and is_subject aag \<circ> cur_thread) s \<Longrightarrow> (\<forall>x xa xb xc. pgi = PageMap x xa xb xc \<longrightarrow> ?R27 x xa xb xc s) \<and> (\<forall>x xa. pgi = PageUnmap x xa \<longrightarrow> ?R28 x xa s) \<and> (\<forall>x xa xb xc xd xe. pgi = PageFlush x xa xb xc xd xe \<longrightarrow> ?R29 x xa xb xc xd xe s) \<and> (\<forall>x. pgi = PageGetAddr x \<longrightarrow> ?R30 x s) proof (prove)
goal (5 subgoals):
 1. \<And>x11 x12 x13 x14. pgi = PageMap x11 x12 x13 x14 \<Longrightarrow> reads_respects aag l (?R27 x11 x12 x13 x14) (do y <- set_cap x12 x13;
y <- case x14 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 x11 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 x11 else return ()
od;
return []
od)
 2. \<And>x21 x22. pgi = PageUnmap x21 x22 \<Longrightarrow> reads_respects aag l (?R28 x21 x22) (case x21 of PageCap dev p R vp_size vp_mapped_addr \<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 x22);
set_cap (ArchObjectCap (update_map_data cap None)) x22;
return []
od | _ \<Rightarrow> fail)
 3. \<And>x31 x32 x33 x34 x35 x36. pgi = PageFlush x31 x32 x33 x34 x35 x36 \<Longrightarrow> reads_respects aag l (?R29 x31 x32 x33 x34 x35 x36) (do if x32 < x33 then do root_switched <- set_vm_root_for_flush x35 x36;
do_machine_op (do_flush x31 x32 x33 x34);
if root_switched then gets cur_thread >>= set_vm_root else return ()
od else return ();
return []
od)
 4. \<And>x4. pgi = PageGetAddr x4 \<Longrightarrow> reads_respects aag l (?R30 x4) (return [addrFromPPtr x4])
 5. \<And>s. (pas_refined aag and K (authorised_page_inv aag pgi) and valid_page_inv pgi and valid_vspace_objs and pspace_aligned and is_subject aag \<circ> cur_thread) s \<Longrightarrow> (\<forall>x xa xb xc. pgi = PageMap x xa xb xc \<longrightarrow> ?R27 x xa xb xc s) \<and> (\<forall>x xa. pgi = PageUnmap x xa \<longrightarrow> ?R28 x xa s) \<and> (\<forall>x xa xb xc xd xe. pgi = PageFlush x xa xb xc xd xe \<longrightarrow> ?R29 x xa xb xc xd xe s) \<and> (\<forall>x. pgi = PageGetAddr x \<longrightarrow> ?R30 x s) proof (prove)
goal (1 subgoal):
 1. \<And>s. pas_refined aag s \<and> authorised_page_inv aag pgi \<and> valid_page_inv pgi s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> is_subject aag (cur_thread s) \<Longrightarrow> (\<forall>x xa a b xb. pgi = PageMap x xa (a, b) xb \<longrightarrow> aag_can_read aag a \<and> (\<forall>a b. xb = Inl (a, b) \<longrightarrow> is_subject aag (hd b && ~~ mask pt_bits) \<and> (\<forall>x\<in>set (tl b). is_subject aag (x && ~~ mask pt_bits))) \<and> (\<forall>a b. xb = Inr (a, b) \<longrightarrow> is_subject aag (hd b && ~~ mask pd_bits) \<and> (\<forall>x\<in>set (tl b). is_subject aag (x && ~~ mask pd_bits)))) \<and> (\<forall>x a. (\<exists>b. pgi = PageUnmap x (a, b)) \<longrightarrow> (\<forall>xa xb xc xd xe. x = PageCap xa xb xc xd xe \<longrightarrow> (\<forall>a b. xe = Some (a, b) \<longrightarrow> is_subject_asid aag a \<and> b < kernel_base) \<and> aag_can_read aag a)) \<and> (\<forall>x xa xb. (\<exists>xc xd xe. pgi = PageFlush x xa xb xc xd xe) \<longrightarrow> xa < xb \<longrightarrow> (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> cur_thread s = cur_thread t)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pas_refined aag s; case pgi of PageMap asid cap ptr slots \<Rightarrow> pas_cap_cur_auth aag cap \<and> is_subject aag (fst ptr) \<and> authorised_slots aag slots | PageUnmap cap ptr \<Rightarrow> pas_cap_cur_auth aag (ArchObjectCap cap) \<and> is_subject aag (fst ptr) | _ \<Rightarrow> True; (case pgi of PageMap asid cap ptr m \<Rightarrow> cte_wp_at (is_arch_update cap) ptr and (cte_wp_at (\<lambda>c. vs_cap_ref c = None) ptr or (\<lambda>s. cte_wp_at (\<lambda>c. same_refs m c s) ptr s)) and cte_wp_at is_pg_cap ptr and same_refs m cap and valid_slots m and valid_cap cap and K (is_pg_cap cap \<and> empty_refs m \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. \<exists>slot. cte_wp_at (parent_for_refs m) slot s) and (\<lambda>s. \<exists>pd. vspace_at_asid asid pd s) | PageUnmap cap ptr \<Rightarrow> \<lambda>s. \<exists>dev r R sz m. cap = PageCap dev r R sz m \<and> (case m of None \<Rightarrow> True | Some x \<Rightarrow> valid_unmap sz x) \<and> cte_wp_at ((=) (ArchObjectCap cap)) ptr s \<and> s \<turnstile> ArchObjectCap cap | PageFlush typ start end pstart pd asid \<Rightarrow> vspace_at_asid asid pd and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) | PageGetAddr ptr \<Rightarrow> \<lambda>_. True) s; valid_vspace_objs s; pspace_aligned s; is_subject aag (cur_thread s)\<rbrakk> \<Longrightarrow> (\<forall>x xa a b xb. pgi = PageMap x xa (a, b) xb \<longrightarrow> aag_can_read aag a \<and> (\<forall>a b. xb = Inl (a, b) \<longrightarrow> is_subject aag (hd b && ~~ mask pt_bits) \<and> (\<forall>x\<in>set (tl b). is_subject aag (x && ~~ mask pt_bits))) \<and> (\<forall>a b. xb = Inr (a, b) \<longrightarrow> is_subject aag (hd b && ~~ mask pd_bits) \<and> (\<forall>x\<in>set (tl b). is_subject aag (x && ~~ mask pd_bits)))) \<and> (\<forall>x a. (\<exists>b. pgi = PageUnmap x (a, b)) \<longrightarrow> (\<forall>xa xb xc xd xe. x = PageCap xa xb xc xd xe \<longrightarrow> (\<forall>a b. xe = Some (a, b) \<longrightarrow> is_subject_asid aag a \<and> b < kernel_base) \<and> aag_can_read aag a)) \<and> (\<forall>x xa xb. (\<exists>xc xd xe. pgi = PageFlush x xa xb xc xd xe) \<longrightarrow> xa < xb \<longrightarrow> (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> cur_thread s = cur_thread t)) proof (prove)
goal:
No subgoals!