theory ArchVSpaceEntries_AI

lemma perform_page_table_valid_pdpt[wp]:
  "\<lbrace>valid_pdpt_objs and valid_pti pinv and pti_duplicates_valid pinv\<rbrace>
      perform_page_table_invocation pinv \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>" apply (simp add: perform_page_table_invocation_def split_def
             cong: page_table_invocation.case_cong
                   option.case_cong cap.case_cong arch_cap.case_cong) apply (rule hoare_pre) apply (wp store_pde_non_master_valid_pdpt hoare_vcg_ex_lift
             set_cap_arch_obj mapM_x_store_pte_valid_pdpt2
              | wpc
              | simp add: swp_def
              | strengthen all_imp_ko_at_from_ex_strg)+ apply (clarsimp simp: pti_duplicates_valid_def valid_pti_def) apply (auto simp: obj_at_def cte_wp_at_caps_of_state valid_cap_simps
                    cap_aligned_def pt_bits_def pageBits_def
            intro!: inj_onI) 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_pti pinv and pti_duplicates_valid pinv\<rbrace> perform_page_table_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_pti pinv and pti_duplicates_valid pinv\<rbrace> case pinv of PageTableMap cap ct_slot pde pd_slot \<Rightarrow> do y <- set_cap cap ct_slot;
y <- 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 y <- case mapped_address of None \<Rightarrow> return () | Some a \<Rightarrow> do y <- unmap_page_table (fst a) (snd a) p;
y <- mapM_x (swp store_pte InvalidPTE) [p , p + 4 .e. p + 2 ^ pt_bits - 1];
do_machine_op (cleanCacheRange_PoU p (p + 2 ^ 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 \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q16\<rbrace> case pinv of PageTableMap cap ct_slot pde pd_slot \<Rightarrow> do y <- set_cap cap ct_slot;
y <- 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 y <- case mapped_address of None \<Rightarrow> return () | Some a \<Rightarrow> do y <- unmap_page_table (fst a) (snd a) p;
y <- mapM_x (swp store_pte InvalidPTE) [p , p + 4 .e. p + 2 ^ pt_bits - 1];
do_machine_op (cleanCacheRange_PoU p (p + 2 ^ 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 \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace>
 2. \<And>s. ((\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_pti pinv and pti_duplicates_valid pinv) s \<Longrightarrow> ?Q16 s proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>x\<in>ran (kheap s). obj_valid_pdpt x) \<and> valid_pti pinv s \<and> pti_duplicates_valid pinv s \<Longrightarrow> (\<forall>x a b xa xb. pinv = PageTableMap x (a, b) xa xb \<longrightarrow> (\<exists>x. ako_at (PageDirectory x) (xb && ~~ mask pd_bits) s \<and> cte_wp_at (\<lambda>_. True) (a, b) s \<and> pde_range_sz (x (UCAST(32 \<rightarrow> 12) (xb && mask pd_bits >> 2) && ~~ mask 4)) = 0 \<and> pde_range_sz xa = 0) \<and> inj (\<lambda>v. ArchObj (PageDirectory v))) \<and> (\<forall>x. (\<exists>a b. pinv = PageTableUnmap x (a, b)) \<longrightarrow> (\<forall>xa. x = ArchObjectCap xa \<longrightarrow> (\<forall>x xb. xa = PageTableCap x xb \<longrightarrow> (\<exists>a b. xb = Some (a, b)) \<longrightarrow> is_aligned x pt_bits))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; (case pinv of PageTableMap cap ptr pde p \<Rightarrow> pde_at p and (\<lambda>s. wellformed_pde pde) and valid_pde pde and valid_cap cap and cte_wp_at (\<lambda>c. is_arch_update cap c \<and> cap_asid c = None) ptr and empty_pde_at p and (\<lambda>s. \<exists>p' ref. vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # ref) \<and> (ref \<rhd> (p && ~~ mask pd_bits)) s \<and> pde_ref pde = Some p' \<and> p' \<in> obj_refs cap \<and> (\<exists>ao. ako_at ao p' s \<and> valid_vspace_obj ao s) \<and> hd (the (vs_cap_ref cap)) \<notin> kernel_vsrefs) and K (is_pt_cap cap \<and> cap_asid cap \<noteq> None) | PageTableUnmap cap ptr \<Rightarrow> cte_wp_at ((=) cap) ptr and valid_cap cap and is_final_cap' cap and K (is_pt_cap cap)) s; (case pinv of PageTableMap cap ct_slot pde pd_slot \<Rightarrow> obj_at (\<lambda>ko. \<exists>pd pde. ko = ArchObj (PageDirectory pd) \<and> pd (UCAST(32 \<rightarrow> 12) (pd_slot && mask pd_bits >> 2) && ~~ mask 4) = pde \<and> pde_range_sz pde = 0) (pd_slot && ~~ mask pd_bits) and K (pde_range_sz pde = 0) | PageTableUnmap capa prod \<Rightarrow> \<lambda>_. True) s\<rbrakk> \<Longrightarrow> (\<forall>x a b xa xb. pinv = PageTableMap x (a, b) xa xb \<longrightarrow> (\<exists>x. ako_at (PageDirectory x) (xb && ~~ mask pd_bits) s \<and> cte_wp_at (\<lambda>_. True) (a, b) s \<and> pde_range_sz (x (UCAST(32 \<rightarrow> 12) (xb && mask pd_bits >> 2) && ~~ mask 4)) = 0 \<and> pde_range_sz xa = 0) \<and> inj (\<lambda>v. ArchObj (PageDirectory v))) \<and> (\<forall>x. (\<exists>a b. pinv = PageTableUnmap x (a, b)) \<longrightarrow> (\<forall>xa. x = ArchObjectCap xa \<longrightarrow> (\<forall>x xb. xa = PageTableCap x xb \<longrightarrow> (\<exists>a b. xb = Some (a, b)) \<longrightarrow> is_aligned x pt_bits))) proof (prove)
goal:
No subgoals!