theory PageTableDuplicates

lemma mapM_x_storePDE_updates:
  "\<lbrace>\<lambda>s. (\<forall>x\<in> set xs. pde_at' x s)
     \<and> Q (\<lambda>x. if (x \<in> set xs) then Some (KOArch (KOPDE pte)) else (ksPSpace s) x) \<rbrace>
     mapM_x (swp storePDE 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: storePDE_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_pde
     split:  Structures_H.kernel_object.split_asm  arch_kernel_object.split_asm if_split) 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. pde_at' x s) \<and> Q (\<lambda>x. if x \<in> set xs then Some (KOArch (KOPDE pte)) else ksPSpace s x)\<rbrace> mapM_x (swp storePDE pte) xs \<lbrace>\<lambda>r s. Q (ksPSpace s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s. (\<forall>x\<in>set []. pde_at' x s) \<and> Q (\<lambda>x. if x \<in> set [] then Some (KOArch (KOPDE pte)) else ksPSpace s x)\<rbrace> mapM_x (swp storePDE pte) [] \<lbrace>\<lambda>r s. Q (ksPSpace s)\<rbrace>
 2. \<And>a xs. \<lbrace>\<lambda>s. (\<forall>x\<in>set xs. pde_at' x s) \<and> Q (\<lambda>x. if x \<in> set xs then Some (KOArch (KOPDE pte)) else ksPSpace s x)\<rbrace> mapM_x (swp storePDE pte) xs \<lbrace>\<lambda>r s. Q (ksPSpace s)\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>x\<in>set (a # xs). pde_at' x s) \<and> Q (\<lambda>x. if x \<in> set (a # xs) then Some (KOArch (KOPDE pte)) else ksPSpace s x)\<rbrace> mapM_x (swp storePDE 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. pde_at' x s) \<and> Q (\<lambda>x. if x \<in> set xs then Some (KOArch (KOPDE pte)) else ksPSpace s x)\<rbrace> mapM_x (swp storePDE pte) xs \<lbrace>\<lambda>r s. Q (ksPSpace s)\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>x\<in>set (a # xs). pde_at' x s) \<and> Q (\<lambda>x. if x \<in> set (a # xs) then Some (KOArch (KOPDE pte)) else ksPSpace s x)\<rbrace> mapM_x (swp storePDE 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. pde_at' x s) \<and> Q (\<lambda>x. if x \<in> set xs then Some (KOArch (KOPDE pte)) else ksPSpace s x)\<rbrace> mapM_x (\<lambda>a. storePDE a pte) xs \<lbrace>\<lambda>r s. Q (ksPSpace s)\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. pde_at' a s \<and> (\<forall>x\<in>set xs. pde_at' x s) \<and> Q (\<lambda>x. if x = a \<or> x \<in> set xs then Some (KOArch (KOPDE pte)) else ksPSpace s x)\<rbrace> do y <- storePDE a pte;
mapM_x (\<lambda>a. storePDE 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. pde_at' x s) \<and> Q (\<lambda>x. if x \<in> set xs then Some (KOArch (KOPDE pte)) else ksPSpace s x)\<rbrace> mapM_x (\<lambda>a. storePDE a pte) xs \<lbrace>\<lambda>r s. Q (ksPSpace s)\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. pde_at' a s \<and> (\<forall>x\<in>set xs. pde_at' x s) \<and> Q (\<lambda>x. if x = a \<or> x \<in> set xs then Some (KOArch (KOPDE pte)) else ksPSpace s x)\<rbrace> storePDE a pte \<lbrace>\<lambda>x s. (\<forall>x\<in>set xs. pde_at' x s) \<and> Q (\<lambda>x. if x \<in> set xs then Some (KOArch (KOPDE pte)) else ksPSpace s x)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrace>\<lambda>s. pde_at' a s \<and> (\<forall>x\<in>set xs. pde_at' x s) \<and> Q (\<lambda>x. if x = a \<or> x \<in> set xs then Some (KOArch (KOPDE pte)) else ksPSpace s x)\<rbrace> storePDE a pte \<lbrace>\<lambda>x s. (\<forall>x\<in>set xs. pde_at' x s) \<and> Q (\<lambda>x. if x \<in> set xs then Some (KOArch (KOPDE pte)) else ksPSpace s x)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrace>\<lambda>s. pde_at' a s \<and> (\<forall>x\<in>set xs. pde_at' x s) \<and> Q (\<lambda>x. if x = a \<or> x \<in> set xs then Some (KOArch (KOPDE 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. pde_at' x s) \<and> Q (\<lambda>x. if x \<in> set xs then Some (KOArch (KOPDE pte)) else ksPSpace s x)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs s. pde_at' a s \<and> (\<forall>x\<in>set xs. pde_at' x s) \<and> Q (\<lambda>x. if x = a \<or> x \<in> set xs then Some (KOArch (KOPDE 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. pde_at' x (s\<lparr>ksPSpace := \<lambda>b. if b = a then Some (KOArch (KOPDE pte)) else ksPSpace s b\<rparr>)) \<and> Q (\<lambda>x. if x \<in> set xs then Some (KOArch (KOPDE pte)) else if x = a then Some (KOArch (KOPDE pte)) else ksPSpace s x) proof (prove)
goal (1 subgoal):
 1. \<And>xs s aa b. \<lbrakk>pde_at' aa s; \<forall>x\<in>set xs. pde_at' x s; Q (\<lambda>x. if x = aa \<or> x \<in> set xs then Some (KOArch (KOPDE pte)) else ksPSpace s x); ksPSpace s aa = Some b\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set xs. pde_at' x (s\<lparr>ksPSpace := \<lambda>a. if a = aa then Some (KOArch (KOPDE pte)) else ksPSpace s a\<rparr>)) \<and> Q (\<lambda>x. if x \<in> set xs then Some (KOArch (KOPDE pte)) else if x = aa then Some (KOArch (KOPDE pte)) else ksPSpace s x) proof (prove)
goal (2 subgoals):
 1. \<And>xs s aa b x. \<lbrakk>pde_at' aa s; \<forall>x\<in>set xs. pde_at' x s; Q (\<lambda>x. if x = aa \<or> x \<in> set xs then Some (KOArch (KOPDE pte)) else ksPSpace s x); ksPSpace s aa = Some b; x \<in> set xs\<rbrakk> \<Longrightarrow> pde_at' x (s\<lparr>ksPSpace := \<lambda>a. if a = aa then Some (KOArch (KOPDE pte)) else ksPSpace s a\<rparr>)
 2. \<And>xs s aa b. \<lbrakk>pde_at' aa s; \<forall>x\<in>set xs. pde_at' x s; Q (\<lambda>x. if x = aa \<or> x \<in> set xs then Some (KOArch (KOPDE pte)) else ksPSpace s x); ksPSpace s aa = Some b\<rbrakk> \<Longrightarrow> Q (\<lambda>x. if x \<in> set xs then Some (KOArch (KOPDE pte)) else if x = aa then Some (KOArch (KOPDE pte)) else ksPSpace s x) proof (prove)
goal (2 subgoals):
 1. \<And>xs s aa b x. \<lbrakk>pde_at' aa s; Q (\<lambda>x. if x = aa \<or> x \<in> set xs then Some (KOArch (KOPDE pte)) else ksPSpace s x); ksPSpace s aa = Some b; x \<in> set xs; pde_at' x s\<rbrakk> \<Longrightarrow> pde_at' x (s\<lparr>ksPSpace := \<lambda>a. if a = aa then Some (KOArch (KOPDE pte)) else ksPSpace s a\<rparr>)
 2. \<And>xs s aa b. \<lbrakk>pde_at' aa s; \<forall>x\<in>set xs. pde_at' x s; Q (\<lambda>x. if x = aa \<or> x \<in> set xs then Some (KOArch (KOPDE pte)) else ksPSpace s x); ksPSpace s aa = Some b\<rbrakk> \<Longrightarrow> Q (\<lambda>x. if x \<in> set xs then Some (KOArch (KOPDE pte)) else if x = aa then Some (KOArch (KOPDE pte)) else ksPSpace s x) proof (prove)
goal (2 subgoals):
 1. \<And>xs s aa x x3 x3a. \<lbrakk>ps_clear aa pdeBits s; is_aligned x pdeBits; ps_clear x pdeBits s; Q (\<lambda>x. if x = aa \<or> x \<in> set xs then Some (KOArch (KOPDE pte)) else ksPSpace s x); ksPSpace s aa = Some (KOArch (KOPDE x3a)); x \<in> set xs; ksPSpace s x = Some (KOArch (KOPDE x3)); is_aligned aa pdeBits\<rbrakk> \<Longrightarrow> (x = aa \<longrightarrow> ps_clear aa pdeBits (s\<lparr>ksPSpace := \<lambda>a. if a = aa then Some (KOArch (KOPDE pte)) else ksPSpace s a\<rparr>)) \<and> (x \<noteq> aa \<longrightarrow> ps_clear x pdeBits (s\<lparr>ksPSpace := \<lambda>a. if a = aa then Some (KOArch (KOPDE pte)) else ksPSpace s a\<rparr>))
 2. \<And>xs s aa b. \<lbrakk>pde_at' aa s; \<forall>x\<in>set xs. pde_at' x s; Q (\<lambda>x. if x = aa \<or> x \<in> set xs then Some (KOArch (KOPDE pte)) else ksPSpace s x); ksPSpace s aa = Some b\<rbrakk> \<Longrightarrow> Q (\<lambda>x. if x \<in> set xs then Some (KOArch (KOPDE pte)) else if x = aa then Some (KOArch (KOPDE pte)) else ksPSpace s x) proof (prove)
goal (1 subgoal):
 1. \<And>xs s aa b. \<lbrakk>pde_at' aa s; \<forall>x\<in>set xs. pde_at' x s; Q (\<lambda>x. if x = aa \<or> x \<in> set xs then Some (KOArch (KOPDE pte)) else ksPSpace s x); ksPSpace s aa = Some b\<rbrakk> \<Longrightarrow> Q (\<lambda>x. if x \<in> set xs then Some (KOArch (KOPDE pte)) else if x = aa then Some (KOArch (KOPDE pte)) else ksPSpace s x) proof (prove)
goal (1 subgoal):
 1. \<And>xs s aa b. \<lbrakk>pde_at' aa s; \<forall>x\<in>set xs. pde_at' x s; ksPSpace s aa = Some b\<rbrakk> \<Longrightarrow> (\<lambda>x. if x = aa \<or> x \<in> set xs then Some (KOArch (KOPDE pte)) else ksPSpace s x) = (\<lambda>x. if x \<in> set xs then Some (KOArch (KOPDE pte)) else if x = aa then Some (KOArch (KOPDE pte)) else ksPSpace s x) proof (prove)
goal:
No subgoals!