theory ArchVSpaceEntries_AI

lemma perform_page_valid_pdpt[wp]:
  "\<lbrace>valid_pdpt_objs and valid_page_inv pinv and page_inv_duplicates_valid pinv\<rbrace>
        perform_page_invocation pinv \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>" apply (simp add: perform_page_invocation_def page_inv_duplicates_valid_def) apply (cases pinv,
         simp_all add: mapM_discarded page_inv_entries_safe_def
            split: sum.split arch_cap.split option.split,
         safe intro!: hoare_gen_asm hoare_gen_asm[unfolded K_def],
         simp_all add: mapM_x_Nil mapM_x_Cons mapM_x_map) apply (wp store_pte_valid_pdpt store_pde_valid_pdpt get_master_pte_wp get_master_pde_wp
                      store_pte_non_master_valid_pdpt store_pde_non_master_valid_pdpt
                      mapM_x_wp'[OF store_invalid_pte_valid_pdpt
                        [where pte=pte.InvalidPTE, simplified]]
                      mapM_x_wp'[OF store_invalid_pde_valid_pdpt
                        [where pde=pde.InvalidPDE, simplified]]
                      set_cap_page_inv_entries_safe
                      hoare_vcg_imp_lift[OF set_cap_arch_obj_neg] hoare_vcg_all_lift
                 | clarsimp simp: cte_wp_at_weakenE[OF _ TrueI] obj_at_def
                                  pte_range_sz_def pde_range_sz_def swp_def valid_page_inv_def
                                  valid_slots_def page_inv_entries_safe_def pte_check_if_mapped_def
                                  pde_check_if_mapped_def
                           split: pte.splits pde.splits
                 | wp (once) hoare_drop_imps)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_page_inv pinv and page_inv_duplicates_valid pinv\<rbrace> perform_page_invocation pinv \<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) and valid_page_inv pinv and (case pinv of PageMap asid cap ct_slot entries \<Rightarrow> page_inv_entries_safe entries | _ \<Rightarrow> \<lambda>_. True)\<rbrace> case pinv 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 $ cleanCacheRange_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 $ cleanCacheRange_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 when (start < end) $ do root_switched <- set_vm_root_for_flush pd asid;
do_machine_op $ do_flush typ start end pstart;
when root_switched $ gets cur_thread >>= set_vm_root
od;
return []
od | PageGetAddr ptr \<Rightarrow> return [addrFromPPtr ptr] \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>x11 x12 a b aa sl. pinv = PageMap x11 x12 (a, b) (Inl (aa, [sl])) \<Longrightarrow> \<lbrace>(\<lambda>s. Ball (ran (kheap s)) obj_valid_pdpt) and valid_page_inv (PageMap x11 x12 (a, b) (Inl (aa, [sl]))) and (obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> pte_range_sz (pt (UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2) && ~~ mask 4)) = 0) (sl && ~~ mask pt_bits) and (\<lambda>y. pte_range_sz aa = 0))\<rbrace> do y <- set_cap x12 (a, b);
y <- do flush <- pte_check_if_mapped sl;
y <- store_pte sl aa;
y <- do_machine_op (cleanCacheRange_PoU sl (last_byte_pte sl) (addrFromPPtr sl));
if flush then invalidate_tlb_by_asid x11 else return ()
od;
return []
od \<lbrace>\<lambda>rv s. Ball (ran (kheap s)) obj_valid_pdpt\<rbrace>
 2. \<And>x11 x12 a b aa ba. \<lbrakk>pinv = PageMap x11 x12 (a, b) (Inl (aa, ba)); \<forall>sl. ba \<noteq> [sl]\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. Ball (ran (kheap s)) obj_valid_pdpt) and valid_page_inv (PageMap x11 x12 (a, b) (Inl (aa, ba))) and (\<lambda>s. \<exists>p. is_aligned p 6 \<and> ba = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C] \<and> obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<forall>x\<in>set (tl ba). pt (UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) = InvalidPTE)) (hd ba && ~~ mask pt_bits) s)\<rbrace> do y <- set_cap x12 (a, b);
y <- do flush <- pte_check_if_mapped (hd ba);
y <- store_pte (hd ba) aa;
_ <- mapM_x (swp store_pte InvalidPTE) (tl ba);
y <- do_machine_op (cleanCacheRange_PoU (hd ba) (last_byte_pte (last ba)) (addrFromPPtr (hd ba)));
if flush then invalidate_tlb_by_asid x11 else return ()
od;
return []
od \<lbrace>\<lambda>rv s. Ball (ran (kheap s)) obj_valid_pdpt\<rbrace>
 3. \<And>x11 x12 a b aa sl. pinv = PageMap x11 x12 (a, b) (Inr (aa, [sl])) \<Longrightarrow> \<lbrace>(\<lambda>s. Ball (ran (kheap s)) obj_valid_pdpt) and valid_page_inv (PageMap x11 x12 (a, b) (Inr (aa, [sl]))) and (obj_at (\<lambda>ko. \<exists>pd. ko = ArchObj (PageDirectory pd) \<and> pde_range_sz (pd (UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) && ~~ mask 4)) = 0) (sl && ~~ mask pd_bits) and (\<lambda>y. pde_range_sz aa = 0))\<rbrace> do y <- set_cap x12 (a, b);
y <- do flush <- pde_check_if_mapped sl;
y <- store_pde sl aa;
y <- do_machine_op (cleanCacheRange_PoU sl (last_byte_pde sl) (addrFromPPtr sl));
if flush then invalidate_tlb_by_asid x11 else return ()
od;
return []
od \<lbrace>\<lambda>rv s. Ball (ran (kheap s)) obj_valid_pdpt\<rbrace>
 4. \<And>x11 x12 a b aa ba. \<lbrakk>pinv = PageMap x11 x12 (a, b) (Inr (aa, ba)); \<forall>sl. ba \<noteq> [sl]\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. Ball (ran (kheap s)) obj_valid_pdpt) and valid_page_inv (PageMap x11 x12 (a, b) (Inr (aa, ba))) and (\<lambda>s. \<exists>p. is_aligned p 6 \<and> ba = map (\<lambda>x. x + p) [0 , 4 .e. 0x3C] \<and> obj_at (\<lambda>ko. \<exists>pd. ko = ArchObj (PageDirectory pd) \<and> (\<forall>x\<in>set (tl ba). pd (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = InvalidPDE)) (hd ba && ~~ mask pd_bits) s)\<rbrace> do y <- set_cap x12 (a, b);
y <- do flush <- pde_check_if_mapped (hd ba);
y <- store_pde (hd ba) aa;
_ <- mapM_x (swp store_pde InvalidPDE) (tl ba);
y <- do_machine_op (cleanCacheRange_PoU (hd ba) (last_byte_pde (last ba)) (addrFromPPtr (hd ba)));
if flush then invalidate_tlb_by_asid x11 else return ()
od;
return []
od \<lbrace>\<lambda>rv s. Ball (ran (kheap s)) obj_valid_pdpt\<rbrace>
 5. \<And>a b x31 x32 x33 x34. pinv = PageUnmap (PageCap x31 x32 x33 x34 None) (a, b) \<Longrightarrow> \<lbrace>(\<lambda>s. Ball (ran (kheap s)) obj_valid_pdpt) and valid_page_inv (PageUnmap (PageCap x31 x32 x33 x34 None) (a, b))\<rbrace> do cap <- liftM the_arch_cap (get_cap (a, b));
y <- set_cap (ArchObjectCap (update_map_data cap None)) (a, b);
return []
od \<lbrace>\<lambda>rv s. Ball (ran (kheap s)) obj_valid_pdpt\<rbrace>
 6. \<And>a b x31 x32 x33 x34 aa ba. pinv = PageUnmap (PageCap x31 x32 x33 x34 (Some (aa, ba))) (a, b) \<Longrightarrow> \<lbrace>(\<lambda>s. Ball (ran (kheap s)) obj_valid_pdpt) and valid_page_inv (PageUnmap (PageCap x31 x32 x33 x34 (Some (aa, ba))) (a, b))\<rbrace> do y <- unmap_page x34 aa ba x32;
cap <- liftM the_arch_cap (get_cap (a, b));
y <- set_cap (ArchObjectCap (update_map_data cap None)) (a, b);
return []
od \<lbrace>\<lambda>rv s. Ball (ran (kheap s)) obj_valid_pdpt\<rbrace>
 7. \<And>x31 x32 x33 x34 x35 x36. pinv = PageFlush x31 x32 x33 x34 x35 x36 \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_page_inv (PageFlush x31 x32 x33 x34 x35 x36)\<rbrace> do y <- when (x32 < x33) (do root_switched <- set_vm_root_for_flush x35 x36;
y <- do_machine_op (do_flush x31 x32 x33 x34);
when root_switched (gets cur_thread >>= set_vm_root)
od);
return []
od \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace>
 8. \<And>x4. pinv = PageGetAddr x4 \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_page_inv (PageGetAddr x4)\<rbrace> return [addrFromPPtr x4] \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal:
No subgoals!