theory ArchVSpace_AI

lemma mapM_x_swp_store_empty_table':
  "\<lbrace>obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt)
                 \<and> (\<forall>x. x \<in> (\<lambda>sl. ucast ((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))\<rbrace>
      mapM_x (swp store_pte InvalidPTE) slots
   \<lbrace>\<lambda>rv. obj_at (empty_table {}) p\<rbrace>" apply (rule hoare_gen_asm) apply (induct slots, simp_all add: mapM_x_Nil mapM_x_Cons) apply wp apply (clarsimp simp: obj_at_def empty_table_def fun_eq_iff) apply (rule hoare_seq_ext, assumption) apply (thin_tac "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>" for P f Q) apply (simp add: store_pte_def set_pt_def set_object_def) apply (wp get_object_wp) apply (clarsimp simp: obj_at_def) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>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))\<rbrace> mapM_x (swp store_pte InvalidPTE) slots \<lbrace>\<lambda>rv. obj_at (empty_table {}) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_aligned p pt_bits \<and> (\<forall>x\<in>set slots. x && ~~ mask pt_bits = p) \<Longrightarrow> \<lbrace>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\<rbrace> mapM_x (swp store_pte InvalidPTE) slots \<lbrace>\<lambda>rv. obj_at (empty_table {}) p\<rbrace> proof (prove)
goal (2 subgoals):
 1. is_aligned p pt_bits \<Longrightarrow> \<lbrace>obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<forall>x. pt x = InvalidPTE)) p\<rbrace> return () \<lbrace>\<lambda>rv. obj_at (empty_table {}) p\<rbrace>
 2. \<And>a slots. \<lbrakk>\<lbrace>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\<rbrace> mapM_x (swp store_pte InvalidPTE) slots \<lbrace>\<lambda>rv. obj_at (empty_table {}) p\<rbrace>; is_aligned p pt_bits \<and> a && ~~ mask pt_bits = p \<and> (\<forall>x\<in>set slots. x && ~~ mask pt_bits = p)\<rbrakk> \<Longrightarrow> \<lbrace>obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<forall>x. x = UCAST(32 \<rightarrow> 8) (a && mask pt_bits >> 2) \<or> x \<in> (\<lambda>x. UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) ` set slots \<or> pt x = InvalidPTE)) p\<rbrace> do y <- store_pte a InvalidPTE;
mapM_x (swp store_pte InvalidPTE) slots
od \<lbrace>\<lambda>rv. obj_at (empty_table {}) p\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>is_aligned p pt_bits; obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<forall>x. pt x = InvalidPTE)) p s\<rbrakk> \<Longrightarrow> obj_at (empty_table {}) p s
 2. \<And>a slots. \<lbrakk>\<lbrace>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\<rbrace> mapM_x (swp store_pte InvalidPTE) slots \<lbrace>\<lambda>rv. obj_at (empty_table {}) p\<rbrace>; is_aligned p pt_bits \<and> a && ~~ mask pt_bits = p \<and> (\<forall>x\<in>set slots. x && ~~ mask pt_bits = p)\<rbrakk> \<Longrightarrow> \<lbrace>obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<forall>x. x = UCAST(32 \<rightarrow> 8) (a && mask pt_bits >> 2) \<or> x \<in> (\<lambda>x. UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) ` set slots \<or> pt x = InvalidPTE)) p\<rbrace> do y <- store_pte a InvalidPTE;
mapM_x (swp store_pte InvalidPTE) slots
od \<lbrace>\<lambda>rv. obj_at (empty_table {}) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a slots. \<lbrakk>\<lbrace>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\<rbrace> mapM_x (swp store_pte InvalidPTE) slots \<lbrace>\<lambda>rv. obj_at (empty_table {}) p\<rbrace>; is_aligned p pt_bits \<and> a && ~~ mask pt_bits = p \<and> (\<forall>x\<in>set slots. x && ~~ mask pt_bits = p)\<rbrakk> \<Longrightarrow> \<lbrace>obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<forall>x. x = UCAST(32 \<rightarrow> 8) (a && mask pt_bits >> 2) \<or> x \<in> (\<lambda>x. UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) ` set slots \<or> pt x = InvalidPTE)) p\<rbrace> do y <- store_pte a InvalidPTE;
mapM_x (swp store_pte InvalidPTE) slots
od \<lbrace>\<lambda>rv. obj_at (empty_table {}) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a slots. \<lbrakk>\<lbrace>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\<rbrace> mapM_x (swp store_pte InvalidPTE) slots \<lbrace>\<lambda>rv. obj_at (empty_table {}) p\<rbrace>; is_aligned p pt_bits \<and> a && ~~ mask pt_bits = p \<and> (\<forall>x\<in>set slots. x && ~~ mask pt_bits = p)\<rbrakk> \<Longrightarrow> \<lbrace>obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<forall>x. x = UCAST(32 \<rightarrow> 8) (a && mask pt_bits >> 2) \<or> x \<in> (\<lambda>x. UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) ` set slots \<or> pt x = InvalidPTE)) p\<rbrace> store_pte a InvalidPTE \<lbrace>\<lambda>y. 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\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a slots. is_aligned p pt_bits \<and> a && ~~ mask pt_bits = p \<and> (\<forall>x\<in>set slots. x && ~~ mask pt_bits = p) \<Longrightarrow> \<lbrace>obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<forall>x. x = UCAST(32 \<rightarrow> 8) (a && mask pt_bits >> 2) \<or> x \<in> (\<lambda>x. UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) ` set slots \<or> pt x = InvalidPTE)) p\<rbrace> store_pte a InvalidPTE \<lbrace>\<lambda>y. 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\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a slots. is_aligned p pt_bits \<and> a && ~~ mask pt_bits = p \<and> (\<forall>x\<in>set slots. x && ~~ mask pt_bits = p) \<Longrightarrow> \<lbrace>obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<forall>x. x = UCAST(32 \<rightarrow> 8) (a && mask pt_bits >> 2) \<or> x \<in> (\<lambda>x. UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) ` set slots \<or> pt x = InvalidPTE)) p\<rbrace> do pt <- get_pt p;
kobj <- get_object p;
y <- assert (a_type kobj = a_type (ArchObj (PageTable (pt(UCAST(32 \<rightarrow> 8) (a && mask pt_bits >> 2) := InvalidPTE)))));
s <- get;
put (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable (pt(UCAST(32 \<rightarrow> 8) (a && mask pt_bits >> 2) := InvalidPTE))))\<rparr>)
od \<lbrace>\<lambda>y. 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\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a slots s. \<lbrakk>is_aligned p pt_bits \<and> a && ~~ mask pt_bits = p \<and> (\<forall>x\<in>set slots. x && ~~ mask pt_bits = p); obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> (\<forall>x. x = UCAST(32 \<rightarrow> 8) (a && mask pt_bits >> 2) \<or> x \<in> (\<lambda>x. UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) ` set slots \<or> pt x = InvalidPTE)) p s\<rbrakk> \<Longrightarrow> \<forall>pt. ako_at (PageTable pt) p s \<longrightarrow> (\<forall>ko. ko_at ko p s \<longrightarrow> a_type ko = a_type (ArchObj (PageTable (pt(UCAST(32 \<rightarrow> 8) (a && mask pt_bits >> 2) := InvalidPTE)))) \<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 (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable (pt(UCAST(32 \<rightarrow> 8) (a && mask pt_bits >> 2) := InvalidPTE))))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>a slots s pta x. \<lbrakk>\<forall>x\<in>set slots. x && ~~ mask pt_bits = a && ~~ mask pt_bits; p = a && ~~ mask pt_bits; \<forall>x. x = UCAST(32 \<rightarrow> 8) (a && mask pt_bits >> 2) \<or> x \<in> (\<lambda>x. UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2)) ` set slots \<or> pta x = InvalidPTE; kheap s (a && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); a_type (ArchObj (PageTable pta)) = a_type (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (a && mask pt_bits >> 2) := InvalidPTE)))); x \<noteq> UCAST(32 \<rightarrow> 8) (a && mask pt_bits >> 2); pta x \<noteq> InvalidPTE\<rbrakk> \<Longrightarrow> x \<in> (\<lambda>sl. UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2)) ` set slots proof (prove)
goal:
No subgoals!