theory Arch_R

lemma valid_slots_duplicated_lift':
  assumes ko_wp_at':
    "\<And>P p. \<lbrace>ko_wp_at' (\<lambda>ko. P (vs_entry_align ko)) p \<rbrace> f \<lbrace>\<lambda>rv. ko_wp_at' (\<lambda>ko. P (vs_entry_align ko)) p\<rbrace>"
  and pt_at:
  "\<And>p. \<lbrace>page_table_at' p \<rbrace> f \<lbrace>\<lambda>rv. page_table_at' p\<rbrace>"
  and pd_at:
  "\<And>p. \<lbrace>page_directory_at' p\<rbrace> f \<lbrace>\<lambda>rv. page_directory_at' p\<rbrace>"
  shows
  "\<lbrace>valid_slots_duplicated' x\<rbrace> f \<lbrace>\<lambda>r. valid_slots_duplicated' x\<rbrace>" apply (simp add:valid_slots_duplicated'_def) apply (case_tac x) apply (case_tac a) apply (case_tac aa) apply simp_all apply (rule hoare_pre) apply simp apply (wp hoare_vcg_ex_lift ko_wp_at' pt_at pd_at | simp)+ apply (case_tac b) apply (case_tac a) apply (wp hoare_vcg_ex_lift ko_wp_at' pt_at pd_at | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_slots_duplicated' x\<rbrace> f \<lbrace>\<lambda>r. valid_slots_duplicated' x\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. case x of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrace> f \<lbrace>\<lambda>r s. case x of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a. x = Inl a \<Longrightarrow> \<lbrace>\<lambda>s. case x of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrace> f \<lbrace>\<lambda>r s. case x of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrace>
 2. \<And>b. x = Inr b \<Longrightarrow> \<lbrace>\<lambda>s. case x of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrace> f \<lbrace>\<lambda>r s. case x of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a aa b. \<lbrakk>x = Inl a; a = (aa, b)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. case x of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrace> f \<lbrace>\<lambda>r s. case x of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrace>
 2. \<And>b. x = Inr b \<Longrightarrow> \<lbrace>\<lambda>s. case x of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrace> f \<lbrace>\<lambda>r s. case x of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>a aa b. \<lbrakk>x = Inl a; a = (aa, b); aa = ARM_H.InvalidPTE\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. case x of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrace> f \<lbrace>\<lambda>r s. case x of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrace>
 2. \<And>a aa b x21 x22 x23 x24 x25. \<lbrakk>x = Inl a; a = (aa, b); aa = ARM_H.LargePagePTE x21 x22 x23 x24 x25\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. case x of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrace> f \<lbrace>\<lambda>r s. case x of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrace>
 3. \<And>a aa b x31 x32 x33 x34 x35. \<lbrakk>x = Inl a; a = (aa, b); aa = ARM_H.SmallPagePTE x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. case x of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrace> f \<lbrace>\<lambda>r s. case x of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrace>
 4. \<And>b. x = Inr b \<Longrightarrow> \<lbrace>\<lambda>s. case x of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrace> f \<lbrace>\<lambda>r s. case x of Inl (ARM_H.LargePagePTE x xa xb xc xd, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s | Inl (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s | Inr (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | Inr (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>a aa b. \<lbrakk>x = Inl (ARM_H.InvalidPTE, b); a = (ARM_H.InvalidPTE, b); aa = ARM_H.InvalidPTE\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>p. b = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s\<rbrace> f \<lbrace>\<lambda>r s. \<exists>p. b = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s\<rbrace>
 2. \<And>a aa b x21 x22 x23 x24 x25. \<lbrakk>x = Inl (ARM_H.LargePagePTE x21 x22 x23 x24 x25, b); a = (ARM_H.LargePagePTE x21 x22 x23 x24 x25, b); aa = ARM_H.LargePagePTE x21 x22 x23 x24 x25\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>p. b = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s\<rbrace> f \<lbrace>\<lambda>r s. \<exists>p. b = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s\<rbrace>
 3. \<And>a aa b x31 x32 x33 x34 x35. \<lbrakk>x = Inl (ARM_H.SmallPagePTE x31 x32 x33 x34 x35, b); a = (ARM_H.SmallPagePTE x31 x32 x33 x34 x35, b); aa = ARM_H.SmallPagePTE x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>p. b = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s\<rbrace> f \<lbrace>\<lambda>r s. \<exists>p. b = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s\<rbrace>
 4. \<And>b. x = Inr b \<Longrightarrow> \<lbrace>\<lambda>s. case b of (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrace> f \<lbrace>\<lambda>r s. case b of (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>a aa b. \<lbrakk>x = Inl (ARM_H.InvalidPTE, b); a = (ARM_H.InvalidPTE, b); aa = ARM_H.InvalidPTE\<rbrakk> \<Longrightarrow> \<lbrace>?Q3 a aa b\<rbrace> f \<lbrace>\<lambda>r s. \<exists>p. b = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s\<rbrace>
 2. \<And>a aa b s. \<lbrakk>x = Inl (ARM_H.InvalidPTE, b); a = (ARM_H.InvalidPTE, b); aa = ARM_H.InvalidPTE; \<exists>p. b = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s\<rbrakk> \<Longrightarrow> ?Q3 a aa b s
 3. \<And>a aa b x21 x22 x23 x24 x25. \<lbrakk>x = Inl (ARM_H.LargePagePTE x21 x22 x23 x24 x25, b); a = (ARM_H.LargePagePTE x21 x22 x23 x24 x25, b); aa = ARM_H.LargePagePTE x21 x22 x23 x24 x25\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>p. b = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s\<rbrace> f \<lbrace>\<lambda>r s. \<exists>p. b = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s\<rbrace>
 4. \<And>a aa b x31 x32 x33 x34 x35. \<lbrakk>x = Inl (ARM_H.SmallPagePTE x31 x32 x33 x34 x35, b); a = (ARM_H.SmallPagePTE x31 x32 x33 x34 x35, b); aa = ARM_H.SmallPagePTE x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>p. b = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s\<rbrace> f \<lbrace>\<lambda>r s. \<exists>p. b = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s\<rbrace>
 5. \<And>b. x = Inr b \<Longrightarrow> \<lbrace>\<lambda>s. case b of (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrace> f \<lbrace>\<lambda>r s. case b of (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>a aa b. \<lbrakk>x = Inl (ARM_H.InvalidPTE, b); a = (ARM_H.InvalidPTE, b); aa = ARM_H.InvalidPTE\<rbrakk> \<Longrightarrow> \<lbrace>?Q3 (ARM_H.InvalidPTE, b) ARM_H.InvalidPTE b\<rbrace> f \<lbrace>\<lambda>r s. \<exists>p. b = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s\<rbrace>
 2. \<And>a aa b s. \<lbrakk>x = Inl (ARM_H.InvalidPTE, b); a = (ARM_H.InvalidPTE, b); aa = ARM_H.InvalidPTE; \<exists>p. b = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s\<rbrakk> \<Longrightarrow> ?Q3 a aa b s
 3. \<And>a aa b x21 x22 x23 x24 x25. \<lbrakk>x = Inl (ARM_H.LargePagePTE x21 x22 x23 x24 x25, b); a = (ARM_H.LargePagePTE x21 x22 x23 x24 x25, b); aa = ARM_H.LargePagePTE x21 x22 x23 x24 x25\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>p. b = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s\<rbrace> f \<lbrace>\<lambda>r s. \<exists>p. b = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_table_at' (p && ~~ mask ptBits) s\<rbrace>
 4. \<And>a aa b x31 x32 x33 x34 x35. \<lbrakk>x = Inl (ARM_H.SmallPagePTE x31 x32 x33 x34 x35, b); a = (ARM_H.SmallPagePTE x31 x32 x33 x34 x35, b); aa = ARM_H.SmallPagePTE x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>p. b = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s\<rbrace> f \<lbrace>\<lambda>r s. \<exists>p. b = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_table_at' (p && ~~ mask ptBits) s\<rbrace>
 5. \<And>b. x = Inr b \<Longrightarrow> \<lbrace>\<lambda>s. case b of (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrace> f \<lbrace>\<lambda>r s. case b of (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>b. x = Inr b \<Longrightarrow> \<lbrace>\<lambda>s. case b of (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrace> f \<lbrace>\<lambda>r s. case b of (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>b a ba. \<lbrakk>x = Inr b; b = (a, ba)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. case b of (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrace> f \<lbrace>\<lambda>r s. case b of (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>b a ba. \<lbrakk>x = Inr b; b = (a, ba); a = ARM_H.InvalidPDE\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. case b of (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrace> f \<lbrace>\<lambda>r s. case b of (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrace>
 2. \<And>b a ba x21 x22 x23. \<lbrakk>x = Inr b; b = (a, ba); a = ARM_H.PageTablePDE x21 x22 x23\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. case b of (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrace> f \<lbrace>\<lambda>r s. case b of (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrace>
 3. \<And>b a ba x31 x32 x33 x34 x35 x36 x37. \<lbrakk>x = Inr b; b = (a, ba); a = ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. case b of (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrace> f \<lbrace>\<lambda>r s. case b of (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrace>
 4. \<And>b a ba x41 x42 x43 x44 x45 x46. \<lbrakk>x = Inr b; b = (a, ba); a = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. case b of (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrace> f \<lbrace>\<lambda>r s. case b of (ARM_H.SuperSectionPDE x xa xb xc xd xe, xs) \<Rightarrow> \<exists>p. xs = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s | (_, xs) \<Rightarrow> \<exists>p. xs = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrace> proof (prove)
goal:
No subgoals!