theory PageTableDuplicates

lemma mapM_x_storePTE_updates:
  "\<lbrace>\<lambda>s. (\<forall>x\<in> set xs. pte_at' x s)
     \<and> Q (\<lambda>x. if (x \<in> set xs) then Some (KOArch (KOPTE pte)) else (ksPSpace s) x) \<rbrace>
     mapM_x (swp storePTE pte) xs
   \<lbrace>\<lambda>r s. Q (ksPSpace s)\<rbrace>" apply (induct xs) apply (simp add: mapM_x_Nil) apply (simp add: mapM_x_Cons) apply (rule hoare_seq_ext, assumption) apply (thin_tac "valid P f Q" for P f Q) apply (simp add: storePTE_def setObject_def) apply (wp | simp add:split_def updateObject_default_def)+ apply clarsimp apply (intro conjI ballI) apply (drule(1) bspec) apply (clarsimp simp:typ_at'_def ko_wp_at'_def
     objBits_simps archObjSize_def dest!:koTypeOf_pte
     split:  Structures_H.kernel_object.split_asm) apply (simp add:ps_clear_def dom_fun_upd2[unfolded fun_upd_def]) apply (erule rsubst[where P=Q]) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>x\<in>set xs. pte_at' x s) \<and> Q (\<lambda>x. if x \<in> set xs then Some (KOArch (KOPTE pte)) else ksPSpace s x)\<rbrace> mapM_x (swp storePTE pte) xs \<lbrace>\<lambda>r s. Q (ksPSpace s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s. (\<forall>x\<in>set []. pte_at' x s) \<and> Q (\<lambda>x. if x \<in> set [] then Some (KOArch (KOPTE pte)) else ksPSpace s x)\<rbrace> mapM_x (swp storePTE pte) [] \<lbrace>\<lambda>r s. Q (ksPSpace s)\<rbrace>
 2. \<And>a xs. \<lbrace>\<lambda>s. (\<forall>x\<in>set xs. pte_at' x s) \<and> Q (\<lambda>x. if x \<in> set xs then Some (KOArch (KOPTE pte)) else ksPSpace s x)\<rbrace> mapM_x (swp storePTE pte) xs \<lbrace>\<lambda>r s. Q (ksPSpace s)\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>x\<in>set (a # xs). pte_at' x s) \<and> Q (\<lambda>x. if x \<in> set (a # xs) then Some (KOArch (KOPTE pte)) else ksPSpace s x)\<rbrace> mapM_x (swp storePTE pte) (a # xs) \<lbrace>\<lambda>r s. Q (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrace>\<lambda>s. (\<forall>x\<in>set xs. pte_at' x s) \<and> Q (\<lambda>x. if x \<in> set xs then Some (KOArch (KOPTE pte)) else ksPSpace s x)\<rbrace> mapM_x (swp storePTE pte) xs \<lbrace>\<lambda>r s. Q (ksPSpace s)\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>x\<in>set (a # xs). pte_at' x s) \<and> Q (\<lambda>x. if x \<in> set (a # xs) then Some (KOArch (KOPTE pte)) else ksPSpace s x)\<rbrace> mapM_x (swp storePTE pte) (a # xs) \<lbrace>\<lambda>r s. Q (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrace>\<lambda>s. (\<forall>x\<in>set xs. pte_at' x s) \<and> Q (\<lambda>x. if x \<in> set xs then Some (KOArch (KOPTE pte)) else ksPSpace s x)\<rbrace> mapM_x (\<lambda>a. storePTE a pte) xs \<lbrace>\<lambda>r s. Q (ksPSpace s)\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. pte_at' a s \<and> (\<forall>x\<in>set xs. pte_at' x s) \<and> Q (\<lambda>x. if x = a \<or> x \<in> set xs then Some (KOArch (KOPTE pte)) else ksPSpace s x)\<rbrace> do y <- storePTE a pte;
mapM_x (\<lambda>a. storePTE a pte) xs
od \<lbrace>\<lambda>r s. Q (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrace>\<lambda>s. (\<forall>x\<in>set xs. pte_at' x s) \<and> Q (\<lambda>x. if x \<in> set xs then Some (KOArch (KOPTE pte)) else ksPSpace s x)\<rbrace> mapM_x (\<lambda>a. storePTE a pte) xs \<lbrace>\<lambda>r s. Q (ksPSpace s)\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. pte_at' a s \<and> (\<forall>x\<in>set xs. pte_at' x s) \<and> Q (\<lambda>x. if x = a \<or> x \<in> set xs then Some (KOArch (KOPTE pte)) else ksPSpace s x)\<rbrace> storePTE a pte \<lbrace>\<lambda>x s. (\<forall>x\<in>set xs. pte_at' x s) \<and> Q (\<lambda>x. if x \<in> set xs then Some (KOArch (KOPTE pte)) else ksPSpace s x)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrace>\<lambda>s. pte_at' a s \<and> (\<forall>x\<in>set xs. pte_at' x s) \<and> Q (\<lambda>x. if x = a \<or> x \<in> set xs then Some (KOArch (KOPTE pte)) else ksPSpace s x)\<rbrace> storePTE a pte \<lbrace>\<lambda>x s. (\<forall>x\<in>set xs. pte_at' x s) \<and> Q (\<lambda>x. if x \<in> set xs then Some (KOArch (KOPTE pte)) else ksPSpace s x)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrace>\<lambda>s. pte_at' a s \<and> (\<forall>x\<in>set xs. pte_at' x s) \<and> Q (\<lambda>x. if x = a \<or> x \<in> set xs then Some (KOArch (KOPTE pte)) else ksPSpace s x)\<rbrace> do ps <- gets ksPSpace;
case lookupAround2 a ps of (before, after) \<Rightarrow> do (ptr', obj) <- assert_opt before;
obj' <- updateObject_default pte obj a ptr' after;
modify (ksPSpace_update (\<lambda>_. ps(ptr' \<mapsto> obj')))
od
od \<lbrace>\<lambda>x s. (\<forall>x\<in>set xs. pte_at' x s) \<and> Q (\<lambda>x. if x \<in> set xs then Some (KOArch (KOPTE pte)) else ksPSpace s x)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs s. pte_at' a s \<and> (\<forall>x\<in>set xs. pte_at' x s) \<and> Q (\<lambda>x. if x = a \<or> x \<in> set xs then Some (KOArch (KOPTE pte)) else ksPSpace s x) \<Longrightarrow> (\<exists>aa b. fst (lookupAround2 a (ksPSpace s)) = Some (aa, b)) \<longrightarrow> a = fst (the (fst (lookupAround2 a (ksPSpace s)))) \<longrightarrow> (\<forall>x\<in>set xs. pte_at' x (s\<lparr>ksPSpace := \<lambda>b. if b = a then Some (KOArch (KOPTE pte)) else ksPSpace s b\<rparr>)) \<and> Q (\<lambda>x. if x \<in> set xs then Some (KOArch (KOPTE pte)) else if x = a then Some (KOArch (KOPTE pte)) else ksPSpace s x) proof (prove)
goal (1 subgoal):
 1. \<And>xs s aa b. \<lbrakk>pte_at' aa s; \<forall>x\<in>set xs. pte_at' x s; Q (\<lambda>x. if x = aa \<or> x \<in> set xs then Some (KOArch (KOPTE pte)) else ksPSpace s x); ksPSpace s aa = Some b\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set xs. pte_at' x (s\<lparr>ksPSpace := \<lambda>a. if a = aa then Some (KOArch (KOPTE pte)) else ksPSpace s a\<rparr>)) \<and> Q (\<lambda>x. if x \<in> set xs then Some (KOArch (KOPTE pte)) else if x = aa then Some (KOArch (KOPTE pte)) else ksPSpace s x) proof (prove)
goal (2 subgoals):
 1. \<And>xs s aa b x. \<lbrakk>pte_at' aa s; \<forall>x\<in>set xs. pte_at' x s; Q (\<lambda>x. if x = aa \<or> x \<in> set xs then Some (KOArch (KOPTE pte)) else ksPSpace s x); ksPSpace s aa = Some b; x \<in> set xs\<rbrakk> \<Longrightarrow> pte_at' x (s\<lparr>ksPSpace := \<lambda>a. if a = aa then Some (KOArch (KOPTE pte)) else ksPSpace s a\<rparr>)
 2. \<And>xs s aa b. \<lbrakk>pte_at' aa s; \<forall>x\<in>set xs. pte_at' x s; Q (\<lambda>x. if x = aa \<or> x \<in> set xs then Some (KOArch (KOPTE pte)) else ksPSpace s x); ksPSpace s aa = Some b\<rbrakk> \<Longrightarrow> Q (\<lambda>x. if x \<in> set xs then Some (KOArch (KOPTE pte)) else if x = aa then Some (KOArch (KOPTE pte)) else ksPSpace s x) proof (prove)
goal (2 subgoals):
 1. \<And>xs s aa b x. \<lbrakk>pte_at' aa s; Q (\<lambda>x. if x = aa \<or> x \<in> set xs then Some (KOArch (KOPTE pte)) else ksPSpace s x); ksPSpace s aa = Some b; x \<in> set xs; pte_at' x s\<rbrakk> \<Longrightarrow> pte_at' x (s\<lparr>ksPSpace := \<lambda>a. if a = aa then Some (KOArch (KOPTE pte)) else ksPSpace s a\<rparr>)
 2. \<And>xs s aa b. \<lbrakk>pte_at' aa s; \<forall>x\<in>set xs. pte_at' x s; Q (\<lambda>x. if x = aa \<or> x \<in> set xs then Some (KOArch (KOPTE pte)) else ksPSpace s x); ksPSpace s aa = Some b\<rbrakk> \<Longrightarrow> Q (\<lambda>x. if x \<in> set xs then Some (KOArch (KOPTE pte)) else if x = aa then Some (KOArch (KOPTE pte)) else ksPSpace s x) proof (prove)
goal (2 subgoals):
 1. \<And>xs s aa x ptea pteaa. \<lbrakk>ps_clear x pteBits s; Q (\<lambda>x. if x = aa \<or> x \<in> set xs then Some (KOArch (KOPTE pte)) else ksPSpace s x); ksPSpace s aa = Some (KOArch (KOPTE pteaa)); x \<in> set xs; ksPSpace s x = Some (KOArch (KOPTE ptea)); is_aligned aa pteBits; ps_clear aa pteBits s; is_aligned x pteBits\<rbrakk> \<Longrightarrow> (x = aa \<longrightarrow> ps_clear aa pteBits (s\<lparr>ksPSpace := \<lambda>a. if a = aa then Some (KOArch (KOPTE pte)) else ksPSpace s a\<rparr>)) \<and> (x \<noteq> aa \<longrightarrow> ps_clear x pteBits (s\<lparr>ksPSpace := \<lambda>a. if a = aa then Some (KOArch (KOPTE pte)) else ksPSpace s a\<rparr>))
 2. \<And>xs s aa b. \<lbrakk>pte_at' aa s; \<forall>x\<in>set xs. pte_at' x s; Q (\<lambda>x. if x = aa \<or> x \<in> set xs then Some (KOArch (KOPTE pte)) else ksPSpace s x); ksPSpace s aa = Some b\<rbrakk> \<Longrightarrow> Q (\<lambda>x. if x \<in> set xs then Some (KOArch (KOPTE pte)) else if x = aa then Some (KOArch (KOPTE pte)) else ksPSpace s x) proof (prove)
goal (1 subgoal):
 1. \<And>xs s aa b. \<lbrakk>pte_at' aa s; \<forall>x\<in>set xs. pte_at' x s; Q (\<lambda>x. if x = aa \<or> x \<in> set xs then Some (KOArch (KOPTE pte)) else ksPSpace s x); ksPSpace s aa = Some b\<rbrakk> \<Longrightarrow> Q (\<lambda>x. if x \<in> set xs then Some (KOArch (KOPTE pte)) else if x = aa then Some (KOArch (KOPTE pte)) else ksPSpace s x) proof (prove)
goal (1 subgoal):
 1. \<And>xs s aa b. \<lbrakk>pte_at' aa s; \<forall>x\<in>set xs. pte_at' x s; ksPSpace s aa = Some b\<rbrakk> \<Longrightarrow> (\<lambda>x. if x = aa \<or> x \<in> set xs then Some (KOArch (KOPTE pte)) else ksPSpace s x) = (\<lambda>x. if x \<in> set xs then Some (KOArch (KOPTE pte)) else if x = aa then Some (KOArch (KOPTE pte)) else ksPSpace s x) proof (prove)
goal:
No subgoals!