theory ArchVSpace_AI

lemma unmap_page_table_unmapped3:
  "\<lbrace>pspace_aligned and valid_vspace_objs and page_table_at pt and
      K (ref = [VSRef (vaddr >> 20) (Some APageDirectory),
               VSRef (asid && mask asid_low_bits) (Some AASIDPool),
               VSRef (ucast (asid_high_bits_of asid)) None]
           \<and> p = pt)\<rbrace>
     unmap_page_table asid vaddr pt
   \<lbrace>\<lambda>rv s. \<not> (ref \<unrhd> p) s\<rbrace>" apply (rule hoare_gen_asm) apply (simp add: unmap_page_table_def lookup_pd_slot_def Let_def
             cong: option.case_cong) apply (rule hoare_pre) apply ((wp store_pde_unmap_page | wpc | simp)+)[1] apply (rule page_table_mapped_wp) apply (clarsimp simp: vspace_at_asid_def pd_aligned pd_bits_def pageBits_def) apply (drule vs_lookup_pages_2ConsD) apply (clarsimp simp: obj_at_def vs_refs_pages_def
                 dest!: vs_lookup_pages1D
                 split: Structures_A.kernel_object.splits
                        arch_kernel_obj.splits) apply (drule vs_lookup_pages_eq_ap[THEN fun_cong, symmetric, THEN iffD1]) apply (erule swap) apply (drule (1) valid_vspace_objsD[rotated 2]) apply (simp add: obj_at_def) apply (erule vs_lookup_step) apply (clarsimp simp: obj_at_def vs_refs_def vs_lookup1_def
                        graph_of_def image_def
                 split: if_split_asm) apply (drule bspec, fastforce) apply (auto simp: obj_at_def data_at_def valid_pde_def pde_ref_def pde_ref_pages_def
                 split: pde.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned and valid_vspace_objs and typ_at (AArch APageTable) pt and K (ref = [VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<and> p = pt)\<rbrace> unmap_page_table asid vaddr pt \<lbrace>\<lambda>rv s. (ref, p) \<notin> vs_lookup_pages s\<rbrace> proof (prove)
goal (1 subgoal):
 1. ref = [VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<and> p = pt \<Longrightarrow> \<lbrace>pspace_aligned and valid_vspace_objs and typ_at (AArch APageTable) pt\<rbrace> unmap_page_table asid vaddr pt \<lbrace>\<lambda>rv s. (ref, p) \<notin> vs_lookup_pages s\<rbrace> proof (prove)
goal (1 subgoal):
 1. ref = [VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<and> p = pt \<Longrightarrow> \<lbrace>pspace_aligned and valid_vspace_objs and typ_at (AArch APageTable) pt\<rbrace> do pdOpt <- page_table_mapped asid vaddr pt;
case pdOpt of None \<Rightarrow> return () | Some pd \<Rightarrow> do y <- store_pde (pd + (vaddr >> 20 << 2)) InvalidPDE;
y <- do_machine_op (cleanByVA_PoU (pd + (vaddr >> 20 << 2)) (addrFromPPtr (pd + (vaddr >> 20 << 2))));
flush_table pd asid vaddr pt
od
od \<lbrace>\<lambda>rv s. ([VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pt) \<notin> vs_lookup_pages s\<rbrace> proof (prove)
goal (2 subgoals):
 1. ref = [VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<and> p = pt \<Longrightarrow> \<lbrace>?Q4\<rbrace> do pdOpt <- page_table_mapped asid vaddr pt;
case pdOpt of None \<Rightarrow> return () | Some pd \<Rightarrow> do y <- store_pde (pd + (vaddr >> 20 << 2)) InvalidPDE;
y <- do_machine_op (cleanByVA_PoU (pd + (vaddr >> 20 << 2)) (addrFromPPtr (pd + (vaddr >> 20 << 2))));
flush_table pd asid vaddr pt
od
od \<lbrace>\<lambda>rv s. ([VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pt) \<notin> vs_lookup_pages s\<rbrace>
 2. \<And>s. \<lbrakk>ref = [VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<and> p = pt; (pspace_aligned and valid_vspace_objs and typ_at (AArch APageTable) pt) s\<rbrakk> \<Longrightarrow> ?Q4 s proof (prove)
goal (2 subgoals):
 1. ref = [VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<and> p = pt \<Longrightarrow> \<lbrace>?Q4\<rbrace> page_table_mapped asid vaddr pt \<lbrace>\<lambda>pdOpt s. (pdOpt = None \<longrightarrow> ([VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pt) \<notin> vs_lookup_pages s) \<and> (\<forall>x. pdOpt = Some x \<longrightarrow> ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> x) s \<and> is_aligned x pd_bits)\<rbrace>
 2. \<And>s. \<lbrakk>ref = [VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<and> p = pt; (pspace_aligned and valid_vspace_objs and typ_at (AArch APageTable) pt) s\<rbrakk> \<Longrightarrow> ?Q4 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>ref = [VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<and> p = pt; (pspace_aligned and valid_vspace_objs and typ_at (AArch APageTable) pt) s\<rbrakk> \<Longrightarrow> valid_vspace_objs s \<and> pspace_aligned s \<and> (([VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pt) \<notin> vs_lookup s \<longrightarrow> (None = None \<longrightarrow> ([VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pt) \<notin> vs_lookup_pages s) \<and> (\<forall>x. None = Some x \<longrightarrow> ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> x) s \<and> is_aligned x pd_bits)) \<and> (\<forall>pd. vspace_at_asid asid pd s \<and> typ_at (AArch APageDirectory) pd s \<and> is_aligned pd pd_bits \<longrightarrow> (Some pd = None \<longrightarrow> ([VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pt) \<notin> vs_lookup_pages s) \<and> (\<forall>x. Some pd = Some x \<longrightarrow> ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> x) s \<and> is_aligned x pd_bits)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>ref = [VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]; p = pt; pspace_aligned s; valid_vspace_objs s; typ_at (AArch APageTable) pt s; ([VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pt) \<notin> vs_lookup s; ([VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> pt) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>ref = [VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]; p = pt; pspace_aligned s; valid_vspace_objs s; typ_at (AArch APageTable) pt s; ([VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pt) \<notin> vs_lookup s; \<exists>p'. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> p') s \<and> (([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p'), [VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pt) \<in> vs_lookup_pages1 s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s pta pa x3 a. \<lbrakk>ref = [VSRef (UCAST(12 \<rightarrow> 32) a) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]; p = pt; pspace_aligned s; valid_vspace_objs s; ([VSRef (UCAST(12 \<rightarrow> 32) a) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pt) \<notin> vs_lookup s; kheap s pt = Some (ArchObj (PageTable pta)); ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<unrhd> pa) s; kheap s pa = Some (ArchObj (PageDirectory x3)); (a, pt) \<in> graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref_pages (x3 x)); vaddr >> 20 = UCAST(12 \<rightarrow> 32) a\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s pta pa x3 a. \<lbrakk>ref = [VSRef (UCAST(12 \<rightarrow> 32) a) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]; p = pt; pspace_aligned s; valid_vspace_objs s; ([VSRef (UCAST(12 \<rightarrow> 32) a) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pt) \<notin> vs_lookup s; kheap s pt = Some (ArchObj (PageTable pta)); kheap s pa = Some (ArchObj (PageDirectory x3)); (a, pt) \<in> graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref_pages (x3 x)); vaddr >> 20 = UCAST(12 \<rightarrow> 32) a; ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pa) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s pta pa x3 a. \<lbrakk>ref = [VSRef (UCAST(12 \<rightarrow> 32) a) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]; p = pt; pspace_aligned s; valid_vspace_objs s; kheap s pt = Some (ArchObj (PageTable pta)); kheap s pa = Some (ArchObj (PageDirectory x3)); (a, pt) \<in> graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref_pages (x3 x)); vaddr >> 20 = UCAST(12 \<rightarrow> 32) a; ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pa) s; \<not> False\<rbrakk> \<Longrightarrow> ([VSRef (UCAST(12 \<rightarrow> 32) a) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pt) s proof (prove)
goal (2 subgoals):
 1. \<And>s pta pa x3 a. \<lbrakk>ref = [VSRef (UCAST(12 \<rightarrow> 32) a) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]; p = pt; pspace_aligned s; kheap s pt = Some (ArchObj (PageTable pta)); kheap s pa = Some (ArchObj (PageDirectory x3)); (a, pt) \<in> graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref_pages (x3 x)); vaddr >> 20 = UCAST(12 \<rightarrow> 32) a; ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pa) s; \<not> False\<rbrakk> \<Longrightarrow> ako_at (?ao146 s pta pa x3 a) pa s
 2. \<And>s pta pa x3 a. \<lbrakk>ref = [VSRef (UCAST(12 \<rightarrow> 32) a) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]; p = pt; pspace_aligned s; kheap s pt = Some (ArchObj (PageTable pta)); kheap s pa = Some (ArchObj (PageDirectory x3)); (a, pt) \<in> graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref_pages (x3 x)); vaddr >> 20 = UCAST(12 \<rightarrow> 32) a; ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pa) s; \<not> False; valid_vspace_obj (?ao146 s pta pa x3 a) s\<rbrakk> \<Longrightarrow> ([VSRef (UCAST(12 \<rightarrow> 32) a) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pt) s proof (prove)
goal (1 subgoal):
 1. \<And>s pta pa x3 a. \<lbrakk>ref = [VSRef (UCAST(12 \<rightarrow> 32) a) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]; p = pt; pspace_aligned s; kheap s pt = Some (ArchObj (PageTable pta)); kheap s pa = Some (ArchObj (PageDirectory x3)); (a, pt) \<in> graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref_pages (x3 x)); vaddr >> 20 = UCAST(12 \<rightarrow> 32) a; ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pa) s; \<not> False; valid_vspace_obj (PageDirectory x3) s\<rbrakk> \<Longrightarrow> ([VSRef (UCAST(12 \<rightarrow> 32) a) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pt) s proof (prove)
goal (1 subgoal):
 1. \<And>s pta pa x3 a. \<lbrakk>ref = [VSRef (UCAST(12 \<rightarrow> 32) a) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]; p = pt; pspace_aligned s; kheap s pt = Some (ArchObj (PageTable pta)); kheap s pa = Some (ArchObj (PageDirectory x3)); (a, pt) \<in> graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref_pages (x3 x)); vaddr >> 20 = UCAST(12 \<rightarrow> 32) a; \<not> False; valid_vspace_obj (PageDirectory x3) s\<rbrakk> \<Longrightarrow> (([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pa), [VSRef (UCAST(12 \<rightarrow> 32) a) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pt) \<in> vs_lookup1 s proof (prove)
goal (1 subgoal):
 1. \<And>s pta pa x3 a. \<lbrakk>vaddr >> 20 = UCAST(12 \<rightarrow> 32) a; \<forall>x\<in>- kernel_mapping_slots. valid_pde (x3 x) s; ref = [VSRef (UCAST(12 \<rightarrow> 32) a) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]; p = pt; pspace_aligned s; kheap s pt = Some (ArchObj (PageTable pta)); kheap s pa = Some (ArchObj (PageDirectory x3)); a \<notin> kernel_mapping_slots; pde_ref_pages (x3 a) = Some pt\<rbrakk> \<Longrightarrow> pde_ref (x3 a) = Some pt proof (prove)
goal (1 subgoal):
 1. \<And>s pta pa x3 a. \<lbrakk>vaddr >> 20 = UCAST(12 \<rightarrow> 32) a; ref = [VSRef (UCAST(12 \<rightarrow> 32) a) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]; p = pt; pspace_aligned s; kheap s pt = Some (ArchObj (PageTable pta)); kheap s pa = Some (ArchObj (PageDirectory x3)); a \<notin> kernel_mapping_slots; pde_ref_pages (x3 a) = Some pt; valid_pde (x3 a) s\<rbrakk> \<Longrightarrow> pde_ref (x3 a) = Some pt proof (prove)
goal:
No subgoals!