theory ArchFinalCaps

lemma set_pd_silc_inv[wp]:
  "set_pd ptr pd \<lbrace>silc_inv aag st\<rbrace>" unfolding set_pd_def apply (rule silc_inv_pres) apply (wpsimp wp: set_object_wp_strong simp: a_type_def split: kernel_object.splits) apply (fastforce simp: silc_inv_def obj_at_def is_cap_table_def) apply (wp set_object_wp get_object_wp | simp)+ apply (case_tac "ptr = fst slot") apply (clarsimp split: kernel_object.splits) apply (fastforce elim: cte_wp_atE simp: obj_at_def) apply (fastforce elim: cte_wp_atE intro: cte_wp_at_cteI cte_wp_at_tcbI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st\<rbrace> set_pd ptr pd \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st\<rbrace> set_object ptr (ArchObj (PageDirectory pd)) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ptra P. \<lbrace>silc_inv aag st and (\<lambda>s. P (kheap s ptra)) and K (pasObjectAbs aag ptra = SilcLabel)\<rbrace> set_object ptr (ArchObj (PageDirectory pd)) \<lbrace>\<lambda>_ s. P (kheap s ptra)\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (cdt s)\<rbrace> set_object ptr (ArchObj (PageDirectory pd)) \<lbrace>\<lambda>_ s. P (cdt s)\<rbrace>
 3. \<And>P slot. \<lbrace>\<lambda>s. \<not> cte_wp_at P slot s\<rbrace> set_object ptr (ArchObj (PageDirectory pd)) \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>P s x5. \<lbrakk>silc_inv aag st s; P (kheap s ptr); pasObjectAbs aag ptr = SilcLabel; ako_at x5 ptr s; APageDirectory = (case x5 of ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)\<rbrakk> \<Longrightarrow> P (Some (ArchObj (PageDirectory pd)))
 2. \<And>P. \<lbrace>\<lambda>s. P (cdt s)\<rbrace> set_object ptr (ArchObj (PageDirectory pd)) \<lbrace>\<lambda>_ s. P (cdt s)\<rbrace>
 3. \<And>P slot. \<lbrace>\<lambda>s. \<not> cte_wp_at P slot s\<rbrace> set_object ptr (ArchObj (PageDirectory pd)) \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>P. \<lbrace>\<lambda>s. P (cdt s)\<rbrace> set_object ptr (ArchObj (PageDirectory pd)) \<lbrace>\<lambda>_ s. P (cdt s)\<rbrace>
 2. \<And>P slot. \<lbrace>\<lambda>s. \<not> cte_wp_at P slot s\<rbrace> set_object ptr (ArchObj (PageDirectory pd)) \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P slot s. \<not> cte_wp_at P slot s \<Longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(ptr \<mapsto> ArchObj (PageDirectory pd))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>P slot s. \<lbrakk>\<not> cte_wp_at P slot s; ptr = fst slot\<rbrakk> \<Longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(ptr \<mapsto> ArchObj (PageDirectory pd))\<rparr>)
 2. \<And>P slot s. \<lbrakk>\<not> cte_wp_at P slot s; ptr \<noteq> fst slot\<rbrakk> \<Longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(ptr \<mapsto> ArchObj (PageDirectory pd))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>P b s. \<lbrakk>\<not> cte_wp_at P (ptr, b) s; cte_wp_at P (ptr, b) (s\<lparr>kheap := (kheap s)(ptr \<mapsto> ArchObj (PageDirectory pd))\<rparr>)\<rbrakk> \<Longrightarrow> False
 2. \<And>P slot s. \<lbrakk>\<not> cte_wp_at P slot s; ptr \<noteq> fst slot\<rbrakk> \<Longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(ptr \<mapsto> ArchObj (PageDirectory pd))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>P slot s. \<lbrakk>\<not> cte_wp_at P slot s; ptr \<noteq> fst slot\<rbrakk> \<Longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(ptr \<mapsto> ArchObj (PageDirectory pd))\<rparr>) proof (prove)
goal:
No subgoals!