theory VSpace_R

lemma valid_slots_duplicated_updateCap[wp]:
  "\<lbrace>valid_slots_duplicated' m'\<rbrace> updateCap cap c'
  \<lbrace>\<lambda>rv s. valid_slots_duplicated' m' s\<rbrace>" apply (case_tac m') apply (simp_all add:valid_slots_duplicated'_def) apply (case_tac a,case_tac aa,simp_all) apply (wp hoare_vcg_ex_lift)+ apply (case_tac b,case_tac a,simp_all) apply (wp hoare_vcg_ex_lift)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_slots_duplicated' m'\<rbrace> updateCap cap c' \<lbrace>\<lambda>rv. valid_slots_duplicated' m'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a. m' = Inl a \<Longrightarrow> \<lbrace>valid_slots_duplicated' m'\<rbrace> updateCap cap c' \<lbrace>\<lambda>rv. valid_slots_duplicated' m'\<rbrace>
 2. \<And>b. m' = Inr b \<Longrightarrow> \<lbrace>valid_slots_duplicated' m'\<rbrace> updateCap cap c' \<lbrace>\<lambda>rv. valid_slots_duplicated' m'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a. m' = Inl a \<Longrightarrow> \<lbrace>\<lambda>s. case a of (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 | (_, 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\<rbrace> updateCap cap c' \<lbrace>\<lambda>rv s. case a of (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 | (_, 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\<rbrace>
 2. \<And>b. m' = 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> updateCap cap c' \<lbrace>\<lambda>rv 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>a aa b. \<lbrakk>m' = 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> updateCap cap c' \<lbrace>\<lambda>rv 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>m' = 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> updateCap cap c' \<lbrace>\<lambda>rv 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>m' = 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> updateCap cap c' \<lbrace>\<lambda>rv 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. m' = 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> updateCap cap c' \<lbrace>\<lambda>rv 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. m' = 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> updateCap cap c' \<lbrace>\<lambda>rv 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>m' = Inr (ARM_H.InvalidPDE, ba); b = (ARM_H.InvalidPDE, ba); a = ARM_H.InvalidPDE\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>p. ba = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrace> updateCap cap c' \<lbrace>\<lambda>rv s. \<exists>p. ba = [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>m' = Inr (ARM_H.PageTablePDE x21 x22 x23, ba); b = (ARM_H.PageTablePDE x21 x22 x23, ba); a = ARM_H.PageTablePDE x21 x22 x23\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>p. ba = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrace> updateCap cap c' \<lbrace>\<lambda>rv s. \<exists>p. ba = [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>m' = Inr (ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37, ba); b = (ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37, ba); a = ARM_H.SectionPDE x31 x32 x33 x34 x35 x36 x37\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>p. ba = [p] \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrace> updateCap cap c' \<lbrace>\<lambda>rv s. \<exists>p. ba = [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>m' = Inr (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46, ba); b = (ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46, ba); a = ARM_H.SuperSectionPDE x41 x42 x43 x44 x45 x46\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>p. ba = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrace> updateCap cap c' \<lbrace>\<lambda>rv s. \<exists>p. ba = [p , p + 4 .e. p + mask 6] \<and> is_aligned p 6 \<and> page_directory_at' (p && ~~ mask pdBits) s\<rbrace> proof (prove)
goal:
No subgoals!