theory ArchVSpace_AI

lemma unmap_page_table_invs[wp]:
  "\<lbrace>invs and K (asid \<le> mask asid_bits \<and> vaddr < kernel_base
                     \<and> vmsz_aligned vaddr ARMSection)\<rbrace>
     unmap_page_table asid vaddr pt
   \<lbrace>\<lambda>rv. invs\<rbrace>" apply (simp add: unmap_page_table_def) apply (rule hoare_pre) apply (wp dmo_invs | wpc | simp)+ apply (rule_tac Q="\<lambda>_. invs and K (asid \<le> mask asid_bits)" in hoare_post_imp) apply safe apply (drule_tac Q="\<lambda>_ m'. underlying_memory m' p =
                                   underlying_memory m p" in use_valid) apply ((wp | simp)+)[3] apply(erule use_valid, wp no_irq_cleanByVA_PoU no_irq, assumption) apply (wp store_pde_invs_unmap page_table_mapped_wp | wpc | simp)+ apply (simp add: lookup_pd_slot_pd pde_ref_def) apply (strengthen lookup_pd_slot_kernel_mappings_strg
                    not_in_global_refs_vs_lookup) apply (auto simp: vspace_at_asid_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and K (asid \<le> mask local.asid_bits \<and> vaddr < kernel_base \<and> vmsz_aligned vaddr ARMSection)\<rbrace> unmap_page_table asid vaddr pt \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>y. asid \<le> mask local.asid_bits \<and> vaddr < kernel_base \<and> vmsz_aligned vaddr ARMSection)\<rbrace> do pdOpt <- page_table_mapped asid vaddr pt;
case pdOpt of None \<Rightarrow> return () | Some pd \<Rightarrow> do pd_slot <- return $ lookup_pd_slot pd vaddr;
store_pde pd_slot InvalidPDE;
do_machine_op $ cleanByVA_PoU pd_slot (addrFromPPtr pd_slot);
flush_table pd asid vaddr pt
od
od \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do pdOpt <- page_table_mapped asid vaddr pt;
case pdOpt of None \<Rightarrow> return () | Some pd \<Rightarrow> do pd_slot <- return $ lookup_pd_slot pd vaddr;
store_pde pd_slot InvalidPDE;
do_machine_op $ cleanByVA_PoU pd_slot (addrFromPPtr pd_slot);
flush_table pd asid vaddr pt
od
od \<lbrace>\<lambda>rv. invs\<rbrace>
 2. \<And>s. (invs and (\<lambda>y. asid \<le> mask local.asid_bits \<and> vaddr < kernel_base \<and> vmsz_aligned vaddr ARMSection)) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>pdOpt x2 pd_slot. pdOpt = Some x2 \<Longrightarrow> \<lbrace>?B21 (Some x2) x2 pd_slot\<rbrace> store_pde pd_slot InvalidPDE \<lbrace>\<lambda>x s. (\<forall>m. \<forall>x\<in>fst (cleanByVA_PoU pd_slot (addrFromPPtr pd_slot) m). case x of (r, m') \<Rightarrow> (\<forall>p. in_user_frame p s \<or> underlying_memory m' p = underlying_memory m p) \<and> (m = machine_state s \<longrightarrow> (\<forall>irq. interrupt_states s irq = IRQInactive \<longrightarrow> irq_masks m' irq \<or> irq_masks m' irq = irq_masks (machine_state s) irq)) \<and> invs s) \<and> asid \<le> mask local.asid_bits\<rbrace>
 2. \<And>pdOpt x2. pdOpt = Some x2 \<Longrightarrow> \<lbrace>?R15 pdOpt x2\<rbrace> return $ lookup_pd_slot x2 vaddr \<lbrace>?B21 pdOpt x2\<rbrace>
 3. \<lbrace>?Q\<rbrace> page_table_mapped asid vaddr pt \<lbrace>\<lambda>pdOpt s. (pdOpt = None \<longrightarrow> invs s) \<and> (\<forall>x. pdOpt = Some x \<longrightarrow> ?R15 pdOpt x s)\<rbrace>
 4. \<And>s. (invs and (\<lambda>y. asid \<le> mask local.asid_bits \<and> vaddr < kernel_base \<and> vmsz_aligned vaddr ARMSection)) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>pdOpt x2 pd_slot rv s. \<lbrakk>pdOpt = Some x2; (invs and K (asid \<le> mask local.asid_bits)) s\<rbrakk> \<Longrightarrow> (\<forall>m. \<forall>x\<in>fst (cleanByVA_PoU pd_slot (addrFromPPtr pd_slot) m). case x of (r, m') \<Rightarrow> (\<forall>p. in_user_frame p s \<or> underlying_memory m' p = underlying_memory m p) \<and> (m = machine_state s \<longrightarrow> (\<forall>irq. interrupt_states s irq = IRQInactive \<longrightarrow> irq_masks m' irq \<or> irq_masks m' irq = irq_masks (machine_state s) irq)) \<and> invs s) \<and> asid \<le> mask local.asid_bits
 2. \<And>pdOpt x2 pd_slot. pdOpt = Some x2 \<Longrightarrow> \<lbrace>?B21 (Some x2) x2 pd_slot\<rbrace> store_pde pd_slot InvalidPDE \<lbrace>\<lambda>_. invs and K (asid \<le> mask local.asid_bits)\<rbrace>
 3. \<And>pdOpt x2. pdOpt = Some x2 \<Longrightarrow> \<lbrace>?R15 pdOpt x2\<rbrace> return $ lookup_pd_slot x2 vaddr \<lbrace>?B21 pdOpt x2\<rbrace>
 4. \<lbrace>?Q\<rbrace> page_table_mapped asid vaddr pt \<lbrace>\<lambda>pdOpt s. (pdOpt = None \<longrightarrow> invs s) \<and> (\<forall>x. pdOpt = Some x \<longrightarrow> ?R15 pdOpt x s)\<rbrace>
 5. \<And>s. (invs and (\<lambda>y. asid \<le> mask local.asid_bits \<and> vaddr < kernel_base \<and> vmsz_aligned vaddr ARMSection)) s \<Longrightarrow> ?Q s proof (prove)
goal (7 subgoals):
 1. \<And>pdOpt x2 pd_slot s m b p. \<lbrakk>invs s; K (asid \<le> mask local.asid_bits) s; ((), b) \<in> fst (cleanByVA_PoU pd_slot (addrFromPPtr pd_slot) m); underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> in_user_frame p s
 2. \<And>pdOpt x2 pd_slot s m b irq. \<lbrakk>invs s; K (asid \<le> mask local.asid_bits) s; ((), b) \<in> fst (cleanByVA_PoU pd_slot (addrFromPPtr pd_slot) (machine_state s)); interrupt_states s irq = IRQInactive; \<not> irq_masks b irq; irq_masks (machine_state s) irq\<rbrakk> \<Longrightarrow> irq_masks b irq
 3. \<And>pdOpt x2 pd_slot rv s. \<lbrakk>invs s; K (asid \<le> mask local.asid_bits) s\<rbrakk> \<Longrightarrow> asid \<le> mask local.asid_bits
 4. \<And>pdOpt x2 pd_slot. \<lbrace>?B21 (Some x2) x2 pd_slot\<rbrace> store_pde pd_slot InvalidPDE \<lbrace>\<lambda>_. invs and K (asid \<le> mask local.asid_bits)\<rbrace>
 5. \<And>pdOpt x2. \<lbrace>?R15 (Some x2) x2\<rbrace> return $ lookup_pd_slot x2 vaddr \<lbrace>?B21 (Some x2) x2\<rbrace>
 6. \<lbrace>?Q\<rbrace> page_table_mapped asid vaddr pt \<lbrace>\<lambda>pdOpt s. (pdOpt = None \<longrightarrow> invs s) \<and> (\<forall>x. pdOpt = Some x \<longrightarrow> ?R15 pdOpt x s)\<rbrace>
 7. \<And>s. \<lbrakk>invs s; asid \<le> mask local.asid_bits; vaddr < kernel_base; vmsz_aligned vaddr ARMSection\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (9 subgoals):
 1. \<And>pdOpt x2 pd_slot s m b p. \<lbrakk>invs s; K (asid \<le> mask local.asid_bits) s; underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> \<lbrace>?P61 pdOpt x2 pd_slot s m b p\<rbrace> cleanByVA_PoU pd_slot (addrFromPPtr pd_slot) \<lbrace>\<lambda>_ m'. underlying_memory m' p = underlying_memory m p\<rbrace>
 2. \<And>pdOpt x2 pd_slot s m b p. \<lbrakk>invs s; K (asid \<le> mask local.asid_bits) s; underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> ?P61 pdOpt x2 pd_slot s m b p m
 3. \<And>pdOpt x2 pd_slot s m b p. \<lbrakk>invs s; K (asid \<le> mask local.asid_bits) s; underlying_memory b p \<noteq> underlying_memory m p; underlying_memory b p = underlying_memory m p\<rbrakk> \<Longrightarrow> in_user_frame p s
 4. \<And>pdOpt x2 pd_slot s m b irq. \<lbrakk>invs s; K (asid \<le> mask local.asid_bits) s; ((), b) \<in> fst (cleanByVA_PoU pd_slot (addrFromPPtr pd_slot) (machine_state s)); interrupt_states s irq = IRQInactive; \<not> irq_masks b irq; irq_masks (machine_state s) irq\<rbrakk> \<Longrightarrow> irq_masks b irq
 5. \<And>pdOpt x2 pd_slot rv s. \<lbrakk>invs s; K (asid \<le> mask local.asid_bits) s\<rbrakk> \<Longrightarrow> asid \<le> mask local.asid_bits
 6. \<And>pdOpt x2 pd_slot. \<lbrace>?B21 (Some x2) x2 pd_slot\<rbrace> store_pde pd_slot InvalidPDE \<lbrace>\<lambda>_. invs and K (asid \<le> mask local.asid_bits)\<rbrace>
 7. \<And>pdOpt x2. \<lbrace>?R15 (Some x2) x2\<rbrace> return $ lookup_pd_slot x2 vaddr \<lbrace>?B21 (Some x2) x2\<rbrace>
 8. \<lbrace>?Q\<rbrace> page_table_mapped asid vaddr pt \<lbrace>\<lambda>pdOpt s. (pdOpt = None \<longrightarrow> invs s) \<and> (\<forall>x. pdOpt = Some x \<longrightarrow> ?R15 pdOpt x s)\<rbrace>
 9. \<And>s. \<lbrakk>invs s; asid \<le> mask local.asid_bits; vaddr < kernel_base; vmsz_aligned vaddr ARMSection\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>pdOpt x2 pd_slot s m b irq. \<lbrakk>invs s; K (asid \<le> mask local.asid_bits) s; ((), b) \<in> fst (cleanByVA_PoU pd_slot (addrFromPPtr pd_slot) (machine_state s)); interrupt_states s irq = IRQInactive; \<not> irq_masks b irq; irq_masks (machine_state s) irq\<rbrakk> \<Longrightarrow> irq_masks b irq
 2. \<And>pdOpt x2 pd_slot rv s. \<lbrakk>invs s; K (asid \<le> mask local.asid_bits) s\<rbrakk> \<Longrightarrow> asid \<le> mask local.asid_bits
 3. \<And>pdOpt x2 pd_slot. \<lbrace>?B21 (Some x2) x2 pd_slot\<rbrace> store_pde pd_slot InvalidPDE \<lbrace>\<lambda>_. invs and K (asid \<le> mask local.asid_bits)\<rbrace>
 4. \<And>pdOpt x2. \<lbrace>?R15 (Some x2) x2\<rbrace> return $ lookup_pd_slot x2 vaddr \<lbrace>?B21 (Some x2) x2\<rbrace>
 5. \<lbrace>?Q\<rbrace> page_table_mapped asid vaddr pt \<lbrace>\<lambda>pdOpt s. (pdOpt = None \<longrightarrow> invs s) \<and> (\<forall>x. pdOpt = Some x \<longrightarrow> ?R15 pdOpt x s)\<rbrace>
 6. \<And>s. \<lbrakk>invs s; asid \<le> mask local.asid_bits; vaddr < kernel_base; vmsz_aligned vaddr ARMSection\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>pdOpt x2 pd_slot rv s. \<lbrakk>invs s; K (asid \<le> mask local.asid_bits) s\<rbrakk> \<Longrightarrow> asid \<le> mask local.asid_bits
 2. \<And>pdOpt x2 pd_slot. \<lbrace>?B21 (Some x2) x2 pd_slot\<rbrace> store_pde pd_slot InvalidPDE \<lbrace>\<lambda>_. invs and K (asid \<le> mask local.asid_bits)\<rbrace>
 3. \<And>pdOpt x2. \<lbrace>?R15 (Some x2) x2\<rbrace> return $ lookup_pd_slot x2 vaddr \<lbrace>?B21 (Some x2) x2\<rbrace>
 4. \<lbrace>?Q\<rbrace> page_table_mapped asid vaddr pt \<lbrace>\<lambda>pdOpt s. (pdOpt = None \<longrightarrow> invs s) \<and> (\<forall>x. pdOpt = Some x \<longrightarrow> ?R15 pdOpt x s)\<rbrace>
 5. \<And>s. \<lbrakk>invs s; asid \<le> mask local.asid_bits; vaddr < kernel_base; vmsz_aligned vaddr ARMSection\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>invs s; asid \<le> mask local.asid_bits; vaddr < kernel_base; vmsz_aligned vaddr ARMSection\<rbrakk> \<Longrightarrow> valid_vspace_objs s \<and> pspace_aligned s \<and> (\<forall>pd. vspace_at_asid asid pd s \<and> typ_at (AArch APageDirectory) pd s \<and> is_aligned pd pd_bits \<longrightarrow> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vaddr && mask pd_bits >> 2) \<notin> kernel_mapping_slots \<and> lookup_pd_slot pd vaddr && ~~ mask pd_bits \<notin> global_refs s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>invs s; asid \<le> mask local.asid_bits; vaddr < kernel_base; vmsz_aligned vaddr ARMSection\<rbrakk> \<Longrightarrow> valid_vspace_objs s \<and> pspace_aligned s \<and> (\<forall>pd. vspace_at_asid asid pd s \<and> typ_at (AArch APageDirectory) pd s \<and> is_aligned pd pd_bits \<longrightarrow> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vaddr && mask pd_bits >> 2) \<notin> kernel_mapping_slots \<and> pd \<notin> global_refs s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>invs s; asid \<le> mask local.asid_bits; vaddr < kernel_base; vmsz_aligned vaddr ARMSection\<rbrakk> \<Longrightarrow> valid_vspace_objs s \<and> pspace_aligned s \<and> (\<forall>x. vspace_at_asid asid x s \<and> typ_at (AArch APageDirectory) x s \<and> is_aligned x pd_bits \<longrightarrow> (is_aligned x pd_bits \<and> vaddr < kernel_base \<and> vmsz_aligned vaddr ARMSection) \<and> (\<exists>ref. (ref \<rhd> x) s) \<and> valid_vs_lookup s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_global_objs s \<and> typ_at (AArch APageDirectory) x s) proof (prove)
goal:
No subgoals!