theory ArchArch_IF

lemma perform_page_table_invocation_reads_respects:
  "reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs
                                         and K (authorised_page_table_inv aag pti))
                  (perform_page_table_invocation pti)" unfolding perform_page_table_invocation_def fun_app_def cleanCacheRange_PoU_def apply (rule equiv_valid_guard_imp) apply (wp dmo_cacheRangeOp_reads_respects dmo_mol_reads_respects store_pde_reads_respects
             set_cap_reads_respects mapM_x_ev'' store_pte_reads_respects
             unmap_page_table_reads_respects get_cap_rev
          | wpc | simp add: cleanByVA_PoU_def)+ apply (case_tac pti; clarsimp simp: authorised_page_table_inv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and K (authorised_page_table_inv aag pti)) (perform_page_table_invocation pti) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and K (authorised_page_table_inv aag pti)) (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) proof (prove)
goal (2 subgoals):
 1. reads_respects aag l ?Q (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)
 2. \<And>s. (pas_refined aag and pspace_aligned and valid_vspace_objs and K (authorised_page_table_inv aag pti)) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> authorised_page_table_inv aag pti \<Longrightarrow> (\<forall>x a b xa xb. pti = PageTableMap x (a, b) xa xb \<longrightarrow> aag_can_read aag a \<and> is_subject aag (xb && ~~ mask pd_bits)) \<and> (\<forall>x a. (\<exists>b. pti = PageTableUnmap x (a, b)) \<longrightarrow> (\<forall>xa. x = ArchObjectCap xa \<longrightarrow> (\<forall>x xb. xa = PageTableCap x xb \<longrightarrow> (\<forall>a. (\<exists>b. xb = Some (a, b)) \<longrightarrow> is_subject_asid aag a \<and> (\<forall>x\<in>set [x , x + 4 .e. x + 2 ^ pt_bits - 1]. is_subject aag (x && ~~ mask pt_bits))) \<and> aag_can_read aag a))) proof (prove)
goal:
No subgoals!