theory ArchVSpace_AI

lemma mapM_x_swp_store_empty_table:
  "\<lbrace>page_table_at p and pspace_aligned
       and K ((UNIV :: word8 set) \<subseteq> (\<lambda>sl. ucast ((sl && mask pt_bits) >> 2)) ` set slots
                       \<and> (\<forall>x\<in>set slots. x && ~~ mask pt_bits = p))\<rbrace>
     mapM_x (swp store_pte InvalidPTE) slots
   \<lbrace>\<lambda>rv. obj_at (empty_table {}) p\<rbrace>" apply (wp mapM_x_swp_store_empty_table') apply (clarsimp simp: obj_at_def a_type_def) apply (clarsimp split: Structures_A.kernel_object.split_asm
                         arch_kernel_obj.split_asm if_split_asm) apply (frule(1) pspace_alignedD) apply (clarsimp simp: pt_bits_def pageBits_def) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>typ_at (AArch APageTable) p and pspace_aligned and K (UNIV \<subseteq> (\<lambda>sl. UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2)) ` set slots \<and> (\<forall>x\<in>set slots. x && ~~ mask pt_bits = p))\<rbrace> mapM_x (swp store_pte InvalidPTE) slots \<lbrace>\<lambda>rv. obj_at (empty_table {}) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (typ_at (AArch APageTable) p and pspace_aligned and K (UNIV \<subseteq> (\<lambda>sl. UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2)) ` set slots \<and> (\<forall>x\<in>set slots. x && ~~ mask pt_bits = p))) s \<Longrightarrow> (obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<forall>x. x \<in> (\<lambda>sl. UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2)) ` set slots \<or> pt x = InvalidPTE)) p and K (is_aligned p pt_bits \<and> (\<forall>x\<in>set slots. x && ~~ mask pt_bits = p))) s proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>pspace_aligned s; kheap s p = Some ko; (case ko of CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | Endpoint endpoint \<Rightarrow> AEndpoint | Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = AArch APageTable; UNIV \<subseteq> (\<lambda>sl. UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2)) ` set slots; \<forall>x\<in>set slots. x && ~~ mask pt_bits = p\<rbrakk> \<Longrightarrow> (\<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<forall>x. x \<in> (\<lambda>sl. UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2)) ` set slots \<or> pt x = InvalidPTE)) \<and> is_aligned p pt_bits proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<lbrakk>UNIV \<subseteq> (\<lambda>sl. UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2)) ` set slots; \<forall>x\<in>set slots. x && ~~ mask pt_bits = p; pspace_aligned s; kheap s p = Some (ArchObj (PageTable x2))\<rbrakk> \<Longrightarrow> (\<forall>x. x \<in> (\<lambda>sl. UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2)) ` set slots \<or> x2 x = InvalidPTE) \<and> is_aligned p pt_bits proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<lbrakk>UNIV \<subseteq> (\<lambda>sl. UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2)) ` set slots; \<forall>x\<in>set slots. x && ~~ mask pt_bits = p; pspace_aligned s; kheap s p = Some (ArchObj (PageTable x2)); is_aligned p (obj_bits (ArchObj (PageTable x2)))\<rbrakk> \<Longrightarrow> (\<forall>x. x \<in> (\<lambda>sl. UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2)) ` set slots \<or> x2 x = InvalidPTE) \<and> is_aligned p pt_bits proof (prove)
goal (1 subgoal):
 1. \<And>s x2 x. \<lbrakk>UNIV \<subseteq> (\<lambda>x. UCAST(32 \<rightarrow> 8) (x && mask 10 >> 2)) ` set slots; \<forall>x\<in>set slots. x && ~~ mask 10 = p; pspace_aligned s; kheap s p = Some (ArchObj (PageTable x2)); is_aligned p 10; x2 x \<noteq> InvalidPTE\<rbrakk> \<Longrightarrow> x \<in> (\<lambda>x. UCAST(32 \<rightarrow> 8) (x && mask 10 >> 2)) ` set slots proof (prove)
goal:
No subgoals!