theory ArchArch_IF

lemma unmap_page_reads_respects:
  "reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs
                                         and K (is_subject_asid aag asid \<and> vptr < kernel_base))
                  (unmap_page pgsz asid vptr pptr)" unfolding unmap_page_def catch_def fun_app_def cleanCacheRange_PoU_def apply (simp add: unmap_page_def swp_def cong: vmpage_size.case_cong) by (wp dmo_mol_reads_respects dmo_cacheRangeOp_reads_respects store_pte_reads_respects[simplified]
         check_mapping_pptr_reads_respects throw_on_false_reads_respects
         lookup_pt_slot_reads_respects lookup_pt_slot_authorised lookup_pt_slot_authorised2
         store_pde_reads_respects[simplified] flush_page_reads_respects
         find_pd_for_asid_reads_respects find_pd_for_asid_pd_slot_authorised
         mapM_ev''[where m="(\<lambda>a. store_pte a InvalidPTE)"
                     and P="\<lambda>x s. is_subject aag (x && ~~ mask pt_bits)"]
         mapM_ev''[where m="(\<lambda>a. store_pde a InvalidPDE)"
                     and P="\<lambda>x s. is_subject aag (x && ~~ mask pd_bits)"]
      | wpc | wp (once) hoare_drop_imps
      | simp add: is_aligned_6_masks is_aligned_mask[symmetric] cleanByVA_PoU_def)+

(* 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 (is_subject_asid aag asid \<and> vptr < kernel_base)) (unmap_page pgsz asid vptr pptr) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and K (is_subject_asid aag asid \<and> vptr < kernel_base)) (do x <- doE pd <- find_pd_for_asid asid;
case pgsz of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined (check_mapping_pptr pptr pgsz (Inl p));
liftE (do store_pte p InvalidPTE;
do_machine_op (cleanByVA_PoU p (addrFromPPtr p))
od)
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
throw_on_false undefined (check_mapping_pptr pptr pgsz (Inl p));
liftE (do assert (p && mask 6 = 0);
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pte InvalidPTE) slots;
do_machine_op (cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pte (last slots)) (addrFromPPtr (hd slots)))
od)
odE | ARMSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined (check_mapping_pptr pptr pgsz (Inr p));
liftE (do store_pde p InvalidPDE;
do_machine_op (cleanByVA_PoU p (addrFromPPtr p))
od)
odE | ARMSuperSection \<Rightarrow> doE p <- returnOk (lookup_pd_slot pd vptr);
throw_on_false undefined (check_mapping_pptr pptr pgsz (Inr p));
liftE (do assert (p && mask 6 = 0);
slots <- return (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
mapM (swp store_pde InvalidPDE) slots;
do_machine_op (cacheRangeOp cleanByVA_PoU (hd slots) (last_byte_pde (last slots)) (addrFromPPtr (hd slots)))
od)
odE;
liftE (flush_page pgsz pd asid vptr)
odE;
case x of Inl e \<Rightarrow> K (return ()) e | Inr b \<Rightarrow> return b
od) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and (\<lambda>y. is_subject_asid aag asid \<and> vptr < kernel_base)) (do x <- doE pd <- find_pd_for_asid asid;
y <- case pgsz of ARMSmallPage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
y <- throw_on_false undefined (check_mapping_pptr pptr ARMSmallPage (Inl p));
liftE (do y <- store_pte p InvalidPTE;
do_machine_op (cleanByVA_PoU p (addrFromPPtr p))
od)
odE | ARMLargePage \<Rightarrow> doE p <- lookup_pt_slot pd vptr;
y <- throw_on_false undefined (check_mapping_pptr pptr ARMLargePage (Inl p));
liftE (do y <- assert (p && mask 6 = 0);
y <- mapM (\<lambda>y. store_pte y InvalidPTE) (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]);
do_machine_op (cacheRangeOp cleanByVA_PoU (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C])) (last_byte_pte (last (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]))) (addrFromPPtr (hd (map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]))))
od)
odE | ARMSection \<Rightarrow> doE y <- throw_on_false undefined (check_mapping_pptr pptr ARMSection (Inr (lookup_pd_slot pd vptr)));
liftE (do y <- store_pde (lookup_pd_slot pd vptr) InvalidPDE;
do_machine_op (cleanByVA_PoU (lookup_pd_slot pd vptr) (addrFromPPtr (lookup_pd_slot pd vptr)))
od)
odE | ARMSuperSection \<Rightarrow> doE y <- throw_on_false undefined (check_mapping_pptr pptr ARMSuperSection (Inr (lookup_pd_slot pd vptr)));
liftE (do y <- assert (lookup_pd_slot pd vptr && mask 6 = 0);
y <- mapM (\<lambda>y. store_pde y InvalidPDE) (map (\<lambda>x. x + lookup_pd_slot pd vptr) [0 , 4 .e. 0x3C]);
do_machine_op (cacheRangeOp cleanByVA_PoU (hd (map (\<lambda>x. x + lookup_pd_slot pd vptr) [0 , 4 .e. 0x3C])) (last_byte_pde (last (map (\<lambda>x. x + lookup_pd_slot pd vptr) [0 , 4 .e. 0x3C]))) (addrFromPPtr (hd (map (\<lambda>x. x + lookup_pd_slot pd vptr) [0 , 4 .e. 0x3C]))))
od)
odE;
liftE (flush_page pgsz pd asid vptr)
odE;
case x of Inl e \<Rightarrow> K (return ()) e | Inr b \<Rightarrow> return b
od)