theory ArchVSpaceEntries_AI

lemma unmap_page_valid_pdpt[wp]:
  "\<lbrace>valid_pdpt_objs\<rbrace> unmap_page sz asid vptr pptr \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>" apply (simp add: unmap_page_def mapM_discarded
             cong: vmpage_size.case_cong) apply (wp) prefer 2 apply (rule valid_validE[OF find_pd_for_asid_inv]) apply (rule hoare_pre) apply (wp get_object_wp get_pte_wp get_pde_wp lookup_pt_slot_inv_any
              store_invalid_pte_valid_pdpt
              store_invalid_pde_valid_pdpt
              mapM_x_store_invalid_pte_valid_pdpt mapM_x_store_pde_valid_pdpt_objs
                 | simp add: mapM_x_map
                 | wpc | simp add: check_mapping_pptr_def)+ apply (simp add: fun_upd_def[symmetric] is_aligned_mask[symmetric]) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> unmap_page sz asid vptr pptr \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<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);
_ <- mapM_x (swp store_pte 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);
_ <- mapM_x (swp store_pde 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>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>pd. \<lbrace>?B9 pd\<rbrace> 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);
_ <- mapM_x (swp store_pte 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);
_ <- mapM_x (swp store_pde 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 \<lbrace>\<lambda>y s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace>, \<lbrace>\<lambda>x a. \<forall>x\<in>ran (kheap a). obj_valid_pdpt x\<rbrace>
 2. \<lbrace>?Q6\<rbrace> find_pd_for_asid asid \<lbrace>?B9\<rbrace>, \<lbrace>\<lambda>x a. \<forall>x\<in>ran (kheap a). obj_valid_pdpt x\<rbrace>
 3. \<And>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x \<Longrightarrow> ?Q6 s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?Q6\<rbrace> find_pd_for_asid asid \<lbrace>?B9\<rbrace>, \<lbrace>\<lambda>x a. \<forall>x\<in>ran (kheap a). obj_valid_pdpt x\<rbrace>
 2. \<And>pd. \<lbrace>?B9 pd\<rbrace> 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);
_ <- mapM_x (swp store_pte 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);
_ <- mapM_x (swp store_pde 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 \<lbrace>\<lambda>y s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace>, \<lbrace>\<lambda>x a. \<forall>x\<in>ran (kheap a). obj_valid_pdpt x\<rbrace>
 3. \<And>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x \<Longrightarrow> ?Q6 s proof (prove)
goal (2 subgoals):
 1. \<And>pd. \<lbrace>\<lambda>a. \<forall>x\<in>ran (kheap a). obj_valid_pdpt x\<rbrace> 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);
_ <- mapM_x (swp store_pte 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);
_ <- mapM_x (swp store_pde 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 \<lbrace>\<lambda>y s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace>, \<lbrace>\<lambda>x a. \<forall>x\<in>ran (kheap a). obj_valid_pdpt x\<rbrace>
 2. \<And>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x \<Longrightarrow> \<forall>x\<in>ran (kheap s). obj_valid_pdpt x proof (prove)
goal (3 subgoals):
 1. \<And>pd. \<lbrace>?Q15 pd\<rbrace> 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);
_ <- mapM_x (swp store_pte 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);
_ <- mapM_x (swp store_pde 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 \<lbrace>\<lambda>y s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace>, \<lbrace>\<lambda>x a. \<forall>x\<in>ran (kheap a). obj_valid_pdpt x\<rbrace>
 2. \<And>pd s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x \<Longrightarrow> ?Q15 pd s
 3. \<And>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x \<Longrightarrow> \<forall>x\<in>ran (kheap s). obj_valid_pdpt x proof (prove)
goal (2 subgoals):
 1. \<And>pd s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x \<Longrightarrow> (sz = ARMLargePage \<longrightarrow> (\<forall>x pt. ako_at (PageTable pt) (x && ~~ mask pt_bits) s \<longrightarrow> (case pt (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE x xa xb \<Rightarrow> x = addrFromPPtr pptr \<and> ARMLargePage = ARMLargePage | SmallPagePTE x xa xb \<Rightarrow> x = addrFromPPtr pptr \<and> ARMLargePage = ARMSmallPage) \<longrightarrow> x && mask 6 = 0 \<longrightarrow> is_aligned x 6)) \<and> (sz = ARMSuperSection \<longrightarrow> (\<forall>pda. ako_at (PageDirectory pda) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s \<longrightarrow> (case pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) of SectionPDE x xa xb xc \<Rightarrow> x = addrFromPPtr pptr \<and> ARMSuperSection = ARMSection | SuperSectionPDE x xa xb \<Rightarrow> x = addrFromPPtr pptr \<and> ARMSuperSection = ARMSuperSection | _ \<Rightarrow> False) \<longrightarrow> lookup_pd_slot pd vptr && mask 6 = 0 \<longrightarrow> is_aligned (lookup_pd_slot pd vptr) 6))
 2. \<And>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x \<Longrightarrow> \<forall>x\<in>ran (kheap s). obj_valid_pdpt x proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x \<Longrightarrow> \<forall>x\<in>ran (kheap s). obj_valid_pdpt x proof (prove)
goal:
No subgoals!