theory VSpace_R

lemma corres_store_pte_with_invalid_tail:
  "\<forall>slot\<in> set ys. \<not> is_aligned (slot >> 2) (pte_align' aa)
  \<Longrightarrow> corres dc ((\<lambda>s. \<forall>y\<in>set ys. pte_at y s) and pspace_aligned and valid_etcbs)
                (pspace_aligned' and pspace_distinct')
             (mapM (swp store_pte ARM_A.pte.InvalidPTE) ys)
             (mapM (swp storePTE aa) ys)" apply (rule_tac S ="{(x,y). x = y \<and> x \<in> set ys}"
               in corres_mapM[where r = dc and r' = dc]) apply simp apply simp apply clarsimp apply (rule corres_guard_imp) apply (rule storePTE_corres') apply (drule bspec) apply simp apply (simp add:pte_relation_aligned_def) apply auto[1] apply (drule bspec,simp) apply simp apply (wp hoare_vcg_ball_lift | simp)+ apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pte_align' aa) \<Longrightarrow> corres dc ((\<lambda>s. \<forall>y\<in>set ys. pte_at y s) and pspace_aligned and valid_etcbs) (pspace_aligned' and pspace_distinct') (mapM (swp store_pte ARM_A.InvalidPTE) ys) (mapM (swp storePTE aa) ys) proof (prove)
goal (7 subgoals):
 1. \<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pte_align' aa) \<Longrightarrow> dc [] []
 2. \<And>x xs y ysa. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pte_align' aa); dc xs ysa; dc x y\<rbrakk> \<Longrightarrow> dc (x # xs) (y # ysa)
 3. \<And>x y. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pte_align' aa); (x, y) \<in> {(x, y). x = y \<and> x \<in> set ys}\<rbrakk> \<Longrightarrow> corres dc ((\<lambda>s. \<forall>y\<in>set ys. pte_at y s) and pspace_aligned and valid_etcbs) (pspace_aligned' and pspace_distinct') (swp store_pte ARM_A.InvalidPTE x) (swp storePTE aa y)
 4. \<And>x y. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pte_align' aa); (x, y) \<in> {(x, y). x = y \<and> x \<in> set ys}\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>y\<in>set ys. pte_at y s) and pspace_aligned and valid_etcbs\<rbrace> swp store_pte ARM_A.InvalidPTE x \<lbrace>\<lambda>rv. (\<lambda>s. \<forall>y\<in>set ys. pte_at y s) and pspace_aligned and valid_etcbs\<rbrace>
 5. \<And>x y. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pte_align' aa); (x, y) \<in> {(x, y). x = y \<and> x \<in> set ys}\<rbrakk> \<Longrightarrow> \<lbrace>pspace_aligned' and pspace_distinct'\<rbrace> swp storePTE aa y \<lbrace>\<lambda>rv. pspace_aligned' and pspace_distinct'\<rbrace>
 6. \<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pte_align' aa) \<Longrightarrow> length ys = length ys
 7. \<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pte_align' aa) \<Longrightarrow> set (zip ys ys) \<subseteq> {(x, y). x = y \<and> x \<in> set ys} proof (prove)
goal (6 subgoals):
 1. \<And>x xs y ysa. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pte_align' aa); dc xs ysa; dc x y\<rbrakk> \<Longrightarrow> dc (x # xs) (y # ysa)
 2. \<And>x y. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pte_align' aa); (x, y) \<in> {(x, y). x = y \<and> x \<in> set ys}\<rbrakk> \<Longrightarrow> corres dc ((\<lambda>s. \<forall>y\<in>set ys. pte_at y s) and pspace_aligned and valid_etcbs) (pspace_aligned' and pspace_distinct') (swp store_pte ARM_A.InvalidPTE x) (swp storePTE aa y)
 3. \<And>x y. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pte_align' aa); (x, y) \<in> {(x, y). x = y \<and> x \<in> set ys}\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>y\<in>set ys. pte_at y s) and pspace_aligned and valid_etcbs\<rbrace> swp store_pte ARM_A.InvalidPTE x \<lbrace>\<lambda>rv. (\<lambda>s. \<forall>y\<in>set ys. pte_at y s) and pspace_aligned and valid_etcbs\<rbrace>
 4. \<And>x y. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pte_align' aa); (x, y) \<in> {(x, y). x = y \<and> x \<in> set ys}\<rbrakk> \<Longrightarrow> \<lbrace>pspace_aligned' and pspace_distinct'\<rbrace> swp storePTE aa y \<lbrace>\<lambda>rv. pspace_aligned' and pspace_distinct'\<rbrace>
 5. \<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pte_align' aa) \<Longrightarrow> length ys = length ys
 6. \<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pte_align' aa) \<Longrightarrow> set (zip ys ys) \<subseteq> {(x, y). x = y \<and> x \<in> set ys} proof (prove)
goal (5 subgoals):
 1. \<And>x y. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pte_align' aa); (x, y) \<in> {(x, y). x = y \<and> x \<in> set ys}\<rbrakk> \<Longrightarrow> corres dc ((\<lambda>s. \<forall>y\<in>set ys. pte_at y s) and pspace_aligned and valid_etcbs) (pspace_aligned' and pspace_distinct') (swp store_pte ARM_A.InvalidPTE x) (swp storePTE aa y)
 2. \<And>x y. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pte_align' aa); (x, y) \<in> {(x, y). x = y \<and> x \<in> set ys}\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>y\<in>set ys. pte_at y s) and pspace_aligned and valid_etcbs\<rbrace> swp store_pte ARM_A.InvalidPTE x \<lbrace>\<lambda>rv. (\<lambda>s. \<forall>y\<in>set ys. pte_at y s) and pspace_aligned and valid_etcbs\<rbrace>
 3. \<And>x y. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pte_align' aa); (x, y) \<in> {(x, y). x = y \<and> x \<in> set ys}\<rbrakk> \<Longrightarrow> \<lbrace>pspace_aligned' and pspace_distinct'\<rbrace> swp storePTE aa y \<lbrace>\<lambda>rv. pspace_aligned' and pspace_distinct'\<rbrace>
 4. \<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pte_align' aa) \<Longrightarrow> length ys = length ys
 5. \<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pte_align' aa) \<Longrightarrow> set (zip ys ys) \<subseteq> {(x, y). x = y \<and> x \<in> set ys} proof (prove)
goal (5 subgoals):
 1. \<And>x. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (case aa of ARM_H.LargePagePTE x xa xb xc xd \<Rightarrow> 4 | _ \<Rightarrow> 0); x \<in> set ys\<rbrakk> \<Longrightarrow> corres dc ((\<lambda>s. \<forall>y\<in>set ys. pte_at y s) and pspace_aligned and valid_etcbs) (pspace_aligned' and pspace_distinct') (store_pte x ARM_A.InvalidPTE) (storePTE x aa)
 2. \<And>x y. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pte_align' aa); (x, y) \<in> {(x, y). x = y \<and> x \<in> set ys}\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>y\<in>set ys. pte_at y s) and pspace_aligned and valid_etcbs\<rbrace> swp store_pte ARM_A.InvalidPTE x \<lbrace>\<lambda>rv. (\<lambda>s. \<forall>y\<in>set ys. pte_at y s) and pspace_aligned and valid_etcbs\<rbrace>
 3. \<And>x y. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pte_align' aa); (x, y) \<in> {(x, y). x = y \<and> x \<in> set ys}\<rbrakk> \<Longrightarrow> \<lbrace>pspace_aligned' and pspace_distinct'\<rbrace> swp storePTE aa y \<lbrace>\<lambda>rv. pspace_aligned' and pspace_distinct'\<rbrace>
 4. \<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pte_align' aa) \<Longrightarrow> length ys = length ys
 5. \<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pte_align' aa) \<Longrightarrow> set (zip ys ys) \<subseteq> {(x, y). x = y \<and> x \<in> set ys} proof (prove)
goal (7 subgoals):
 1. \<And>x. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (case aa of ARM_H.LargePagePTE x xa xb xc xd \<Rightarrow> 4 | _ \<Rightarrow> 0); x \<in> set ys\<rbrakk> \<Longrightarrow> corres dc (?Q8 x) (?Q'8 x) (store_pte x ARM_A.InvalidPTE) (storePTE x aa)
 2. \<And>x s. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (case aa of ARM_H.LargePagePTE x xa xb xc xd \<Rightarrow> 4 | _ \<Rightarrow> 0); x \<in> set ys; ((\<lambda>s. \<forall>y\<in>set ys. pte_at y s) and pspace_aligned and valid_etcbs) s\<rbrakk> \<Longrightarrow> ?Q8 x s
 3. \<And>x s. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (case aa of ARM_H.LargePagePTE x xa xb xc xd \<Rightarrow> 4 | _ \<Rightarrow> 0); x \<in> set ys; (pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> ?Q'8 x s
 4. \<And>x y. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pte_align' aa); (x, y) \<in> {(x, y). x = y \<and> x \<in> set ys}\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>y\<in>set ys. pte_at y s) and pspace_aligned and valid_etcbs\<rbrace> swp store_pte ARM_A.InvalidPTE x \<lbrace>\<lambda>rv. (\<lambda>s. \<forall>y\<in>set ys. pte_at y s) and pspace_aligned and valid_etcbs\<rbrace>
 5. \<And>x y. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pte_align' aa); (x, y) \<in> {(x, y). x = y \<and> x \<in> set ys}\<rbrakk> \<Longrightarrow> \<lbrace>pspace_aligned' and pspace_distinct'\<rbrace> swp storePTE aa y \<lbrace>\<lambda>rv. pspace_aligned' and pspace_distinct'\<rbrace>
 6. \<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pte_align' aa) \<Longrightarrow> length ys = length ys
 7. \<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pte_align' aa) \<Longrightarrow> set (zip ys ys) \<subseteq> {(x, y). x = y \<and> x \<in> set ys} proof (prove)
goal (7 subgoals):
 1. \<And>x. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (case aa of ARM_H.LargePagePTE x xa xb xc xd \<Rightarrow> 4 | _ \<Rightarrow> 0); x \<in> set ys\<rbrakk> \<Longrightarrow> pte_relation_aligned (x >> 2) ARM_A.InvalidPTE aa
 2. \<And>x s. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (case aa of ARM_H.LargePagePTE x xa xb xc xd \<Rightarrow> 4 | _ \<Rightarrow> 0); x \<in> set ys; ((\<lambda>s. \<forall>y\<in>set ys. pte_at y s) and pspace_aligned and valid_etcbs) s\<rbrakk> \<Longrightarrow> (pte_at x and pspace_aligned and valid_etcbs) s
 3. \<And>x s. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (case aa of ARM_H.LargePagePTE x xa xb xc xd \<Rightarrow> 4 | _ \<Rightarrow> 0); x \<in> set ys; (pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct') s
 4. \<And>x y. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pte_align' aa); (x, y) \<in> {(x, y). x = y \<and> x \<in> set ys}\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>y\<in>set ys. pte_at y s) and pspace_aligned and valid_etcbs\<rbrace> swp store_pte ARM_A.InvalidPTE x \<lbrace>\<lambda>rv. (\<lambda>s. \<forall>y\<in>set ys. pte_at y s) and pspace_aligned and valid_etcbs\<rbrace>
 5. \<And>x y. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pte_align' aa); (x, y) \<in> {(x, y). x = y \<and> x \<in> set ys}\<rbrakk> \<Longrightarrow> \<lbrace>pspace_aligned' and pspace_distinct'\<rbrace> swp storePTE aa y \<lbrace>\<lambda>rv. pspace_aligned' and pspace_distinct'\<rbrace>
 6. \<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pte_align' aa) \<Longrightarrow> length ys = length ys
 7. \<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pte_align' aa) \<Longrightarrow> set (zip ys ys) \<subseteq> {(x, y). x = y \<and> x \<in> set ys} proof (prove)
goal (8 subgoals):
 1. \<And>x. x \<in> set ys \<Longrightarrow> ?slot14 x \<in> set ys
 2. \<And>x. \<lbrakk>x \<in> set ys; \<not> is_aligned (?slot14 x >> 2) (case aa of ARM_H.LargePagePTE x xa xb xc xd \<Rightarrow> 4 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> pte_relation_aligned (x >> 2) ARM_A.InvalidPTE aa
 3. \<And>x s. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (case aa of ARM_H.LargePagePTE x xa xb xc xd \<Rightarrow> 4 | _ \<Rightarrow> 0); x \<in> set ys; ((\<lambda>s. \<forall>y\<in>set ys. pte_at y s) and pspace_aligned and valid_etcbs) s\<rbrakk> \<Longrightarrow> (pte_at x and pspace_aligned and valid_etcbs) s
 4. \<And>x s. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (case aa of ARM_H.LargePagePTE x xa xb xc xd \<Rightarrow> 4 | _ \<Rightarrow> 0); x \<in> set ys; (pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct') s
 5. \<And>x y. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pte_align' aa); (x, y) \<in> {(x, y). x = y \<and> x \<in> set ys}\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>y\<in>set ys. pte_at y s) and pspace_aligned and valid_etcbs\<rbrace> swp store_pte ARM_A.InvalidPTE x \<lbrace>\<lambda>rv. (\<lambda>s. \<forall>y\<in>set ys. pte_at y s) and pspace_aligned and valid_etcbs\<rbrace>
 6. \<And>x y. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pte_align' aa); (x, y) \<in> {(x, y). x = y \<and> x \<in> set ys}\<rbrakk> \<Longrightarrow> \<lbrace>pspace_aligned' and pspace_distinct'\<rbrace> swp storePTE aa y \<lbrace>\<lambda>rv. pspace_aligned' and pspace_distinct'\<rbrace>
 7. \<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pte_align' aa) \<Longrightarrow> length ys = length ys
 8. \<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pte_align' aa) \<Longrightarrow> set (zip ys ys) \<subseteq> {(x, y). x = y \<and> x \<in> set ys} proof (prove)
goal (7 subgoals):
 1. \<And>x. \<lbrakk>x \<in> set ys; \<not> is_aligned (x >> 2) (case aa of ARM_H.LargePagePTE x xa xb xc xd \<Rightarrow> 4 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> pte_relation_aligned (x >> 2) ARM_A.InvalidPTE aa
 2. \<And>x s. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (case aa of ARM_H.LargePagePTE x xa xb xc xd \<Rightarrow> 4 | _ \<Rightarrow> 0); x \<in> set ys; ((\<lambda>s. \<forall>y\<in>set ys. pte_at y s) and pspace_aligned and valid_etcbs) s\<rbrakk> \<Longrightarrow> (pte_at x and pspace_aligned and valid_etcbs) s
 3. \<And>x s. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (case aa of ARM_H.LargePagePTE x xa xb xc xd \<Rightarrow> 4 | _ \<Rightarrow> 0); x \<in> set ys; (pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct') s
 4. \<And>x y. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pte_align' aa); (x, y) \<in> {(x, y). x = y \<and> x \<in> set ys}\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>y\<in>set ys. pte_at y s) and pspace_aligned and valid_etcbs\<rbrace> swp store_pte ARM_A.InvalidPTE x \<lbrace>\<lambda>rv. (\<lambda>s. \<forall>y\<in>set ys. pte_at y s) and pspace_aligned and valid_etcbs\<rbrace>
 5. \<And>x y. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pte_align' aa); (x, y) \<in> {(x, y). x = y \<and> x \<in> set ys}\<rbrakk> \<Longrightarrow> \<lbrace>pspace_aligned' and pspace_distinct'\<rbrace> swp storePTE aa y \<lbrace>\<lambda>rv. pspace_aligned' and pspace_distinct'\<rbrace>
 6. \<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pte_align' aa) \<Longrightarrow> length ys = length ys
 7. \<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pte_align' aa) \<Longrightarrow> set (zip ys ys) \<subseteq> {(x, y). x = y \<and> x \<in> set ys} proof (prove)
goal (6 subgoals):
 1. \<And>x s. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (case aa of ARM_H.LargePagePTE x xa xb xc xd \<Rightarrow> 4 | _ \<Rightarrow> 0); x \<in> set ys; ((\<lambda>s. \<forall>y\<in>set ys. pte_at y s) and pspace_aligned and valid_etcbs) s\<rbrakk> \<Longrightarrow> (pte_at x and pspace_aligned and valid_etcbs) s
 2. \<And>x s. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (case aa of ARM_H.LargePagePTE x xa xb xc xd \<Rightarrow> 4 | _ \<Rightarrow> 0); x \<in> set ys; (pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct') s
 3. \<And>x y. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pte_align' aa); (x, y) \<in> {(x, y). x = y \<and> x \<in> set ys}\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>y\<in>set ys. pte_at y s) and pspace_aligned and valid_etcbs\<rbrace> swp store_pte ARM_A.InvalidPTE x \<lbrace>\<lambda>rv. (\<lambda>s. \<forall>y\<in>set ys. pte_at y s) and pspace_aligned and valid_etcbs\<rbrace>
 4. \<And>x y. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pte_align' aa); (x, y) \<in> {(x, y). x = y \<and> x \<in> set ys}\<rbrakk> \<Longrightarrow> \<lbrace>pspace_aligned' and pspace_distinct'\<rbrace> swp storePTE aa y \<lbrace>\<lambda>rv. pspace_aligned' and pspace_distinct'\<rbrace>
 5. \<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pte_align' aa) \<Longrightarrow> length ys = length ys
 6. \<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pte_align' aa) \<Longrightarrow> set (zip ys ys) \<subseteq> {(x, y). x = y \<and> x \<in> set ys} proof (prove)
goal (5 subgoals):
 1. \<And>x s. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (case aa of ARM_H.LargePagePTE x xa xb xc xd \<Rightarrow> 4 | _ \<Rightarrow> 0); x \<in> set ys; (pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct') s
 2. \<And>x y. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pte_align' aa); (x, y) \<in> {(x, y). x = y \<and> x \<in> set ys}\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>y\<in>set ys. pte_at y s) and pspace_aligned and valid_etcbs\<rbrace> swp store_pte ARM_A.InvalidPTE x \<lbrace>\<lambda>rv. (\<lambda>s. \<forall>y\<in>set ys. pte_at y s) and pspace_aligned and valid_etcbs\<rbrace>
 3. \<And>x y. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pte_align' aa); (x, y) \<in> {(x, y). x = y \<and> x \<in> set ys}\<rbrakk> \<Longrightarrow> \<lbrace>pspace_aligned' and pspace_distinct'\<rbrace> swp storePTE aa y \<lbrace>\<lambda>rv. pspace_aligned' and pspace_distinct'\<rbrace>
 4. \<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pte_align' aa) \<Longrightarrow> length ys = length ys
 5. \<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pte_align' aa) \<Longrightarrow> set (zip ys ys) \<subseteq> {(x, y). x = y \<and> x \<in> set ys} proof (prove)
goal (5 subgoals):
 1. \<And>x s. \<lbrakk>x \<in> set ys; (pspace_aligned' and pspace_distinct') s; \<not> is_aligned (x >> 2) (case aa of ARM_H.LargePagePTE x xa xb xc xd \<Rightarrow> 4 | _ \<Rightarrow> 0)\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct') s
 2. \<And>x y. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pte_align' aa); (x, y) \<in> {(x, y). x = y \<and> x \<in> set ys}\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>y\<in>set ys. pte_at y s) and pspace_aligned and valid_etcbs\<rbrace> swp store_pte ARM_A.InvalidPTE x \<lbrace>\<lambda>rv. (\<lambda>s. \<forall>y\<in>set ys. pte_at y s) and pspace_aligned and valid_etcbs\<rbrace>
 3. \<And>x y. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pte_align' aa); (x, y) \<in> {(x, y). x = y \<and> x \<in> set ys}\<rbrakk> \<Longrightarrow> \<lbrace>pspace_aligned' and pspace_distinct'\<rbrace> swp storePTE aa y \<lbrace>\<lambda>rv. pspace_aligned' and pspace_distinct'\<rbrace>
 4. \<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pte_align' aa) \<Longrightarrow> length ys = length ys
 5. \<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pte_align' aa) \<Longrightarrow> set (zip ys ys) \<subseteq> {(x, y). x = y \<and> x \<in> set ys} proof (prove)
goal (4 subgoals):
 1. \<And>x y. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pte_align' aa); (x, y) \<in> {(x, y). x = y \<and> x \<in> set ys}\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>y\<in>set ys. pte_at y s) and pspace_aligned and valid_etcbs\<rbrace> swp store_pte ARM_A.InvalidPTE x \<lbrace>\<lambda>rv. (\<lambda>s. \<forall>y\<in>set ys. pte_at y s) and pspace_aligned and valid_etcbs\<rbrace>
 2. \<And>x y. \<lbrakk>\<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pte_align' aa); (x, y) \<in> {(x, y). x = y \<and> x \<in> set ys}\<rbrakk> \<Longrightarrow> \<lbrace>pspace_aligned' and pspace_distinct'\<rbrace> swp storePTE aa y \<lbrace>\<lambda>rv. pspace_aligned' and pspace_distinct'\<rbrace>
 3. \<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pte_align' aa) \<Longrightarrow> length ys = length ys
 4. \<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (pte_align' aa) \<Longrightarrow> set (zip ys ys) \<subseteq> {(x, y). x = y \<and> x \<in> set ys} proof (prove)
goal (1 subgoal):
 1. \<forall>slot\<in>set ys. \<not> is_aligned (slot >> 2) (case aa of ARM_H.LargePagePTE x xa xb xc xd \<Rightarrow> 4 | _ \<Rightarrow> 0) \<Longrightarrow> set (zip ys ys) \<subseteq> {(x, y). x = y \<and> x \<in> set ys} proof (prove)
goal:
No subgoals!