theory ArchArch_AC

lemma unmap_page_respects:
  "\<lbrace>integrity aag X st and pspace_aligned and valid_vspace_objs
                       and K (is_subject_asid aag asid) and pas_refined aag
                       and K (vmsz_aligned vptr sz \<and> vptr < kernel_base)\<rbrace>
   unmap_page sz asid vptr pptr
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (rule hoare_gen_asm) apply (simp add: unmap_page_def swp_def cong: vmpage_size.case_cong) apply (rule hoare_pre) apply (wpsimp wp: store_pte_respects store_pde_respects lookup_pt_slot_authorised
                     hoare_drop_imps[where Q="\<lambda>rv. integrity aag X st"]
               simp: is_aligned_6_masks is_aligned_mask[symmetric] cleanByVA_PoU_def
          | wp (once) hoare_drop_imps
                      mapM_set''[where f="(\<lambda>a. store_pte a InvalidPTE)"
                                   and I="\<lambda>x s. is_subject aag (x && ~~ mask pt_bits)"
                                   and Q="integrity aag X st"]
                      mapM_set''[where f="(\<lambda>a. store_pde a InvalidPDE)"
                                   and I="\<lambda>x s. is_subject aag (x && ~~ mask pd_bits)"
                                   and Q="integrity aag X st"]
          | wp (once) hoare_drop_imps[where R="\<lambda>rv s. rv"])+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pspace_aligned and valid_vspace_objs and K (is_subject_asid aag asid) and pas_refined aag and K (vmsz_aligned vptr sz \<and> vptr < kernel_base)\<rbrace> unmap_page sz asid vptr pptr \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. vmsz_aligned vptr sz \<and> vptr < kernel_base \<Longrightarrow> \<lbrace>integrity aag X st and pspace_aligned and valid_vspace_objs and K (is_subject_asid aag asid) and pas_refined aag\<rbrace> unmap_page sz asid vptr pptr \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. vmsz_aligned vptr sz \<and> vptr < kernel_base \<Longrightarrow> \<lbrace>integrity aag X st and pspace_aligned and valid_vspace_objs and (\<lambda>y. is_subject_asid aag asid) and pas_refined aag\<rbrace> doE pd <- find_pd_for_asid asid;
y <- case sz 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 (cleanCacheRange_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 (cleanCacheRange_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 sz pd asid vptr)
odE <catch> (\<lambda>y. return ()) \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (2 subgoals):
 1. vmsz_aligned vptr sz \<and> vptr < kernel_base \<Longrightarrow> \<lbrace>?Q6\<rbrace> doE pd <- find_pd_for_asid asid;
y <- case sz 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 (cleanCacheRange_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 (cleanCacheRange_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 sz pd asid vptr)
odE <catch> (\<lambda>y. return ()) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>s. \<lbrakk>vmsz_aligned vptr sz \<and> vptr < kernel_base; (integrity aag X st and pspace_aligned and valid_vspace_objs and (\<lambda>y. is_subject_asid aag asid) and pas_refined aag) s\<rbrakk> \<Longrightarrow> ?Q6 s proof (prove)
goal:
No subgoals!