theory Arch_DR

lemma set_cap_opt_cap':
  "\<lbrace>\<lambda>s. P ((\<lambda>p. opt_cap p s) (slot \<mapsto> cap))\<rbrace> KHeap_D.set_cap slot cap \<lbrace>\<lambda>rv s. P (\<lambda>p. opt_cap p s)\<rbrace>" apply (cases slot) apply (clarsimp simp add:KHeap_D.set_cap_def split_def) apply (rule hoare_seq_ext [OF _ dget_object_sp]) apply (case_tac obj; simp add: KHeap_D.set_object_def has_slots_def update_slots_def object_slots_def
                            split del: if_split cong: if_cong bind_cong;
                       wpsimp) by (auto elim!:rsubst[where P=P] simp: opt_cap_def slots_of_def object_slots_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P ((\<lambda>p. opt_cap p s)(slot \<mapsto> cap))\<rbrace> KHeap_D.set_cap slot cap \<lbrace>\<lambda>rv s. P (\<lambda>p. opt_cap p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a b. slot = (a, b) \<Longrightarrow> \<lbrace>\<lambda>s. P ((\<lambda>p. opt_cap p s)(slot \<mapsto> cap))\<rbrace> KHeap_D.set_cap slot cap \<lbrace>\<lambda>rv s. P (\<lambda>p. opt_cap p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a b. slot = (a, b) \<Longrightarrow> \<lbrace>\<lambda>s. P ((\<lambda>p. opt_cap p s)((a, b) \<mapsto> cap))\<rbrace> do obj <- KHeap_D.get_object a;
y <- assert (has_slots obj);
(case update_slots ((object_slots obj)(b \<mapsto> cap)) obj of Tcb t \<Rightarrow> if snd (a, b) = tcb_ipcbuffer_slot \<and> object_slots obj (snd (a, b)) \<noteq> Some cap then do intent' <- select UNIV;
return $ Tcb (dupdate_tcb_intent intent' t)
od else return (update_slots ((object_slots obj)(snd (a, b) \<mapsto> cap)) obj) | _ \<Rightarrow> return (update_slots ((object_slots obj)(snd (a, b) \<mapsto> cap)) obj)) >>= KHeap_D.set_object a
od \<lbrace>\<lambda>rv s. P (\<lambda>p. opt_cap p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a b obj. slot = (a, b) \<Longrightarrow> \<lbrace>\<lambda>s. P ((\<lambda>p. opt_cap p s)((a, b) \<mapsto> cap)) \<and> cdl_objects s a = Some obj\<rbrace> do y <- assert (has_slots obj);
(case update_slots ((object_slots obj)(b \<mapsto> cap)) obj of Tcb t \<Rightarrow> if snd (a, b) = tcb_ipcbuffer_slot \<and> object_slots obj (snd (a, b)) \<noteq> Some cap then do intent' <- select UNIV;
return $ Tcb (dupdate_tcb_intent intent' t)
od else return (update_slots ((object_slots obj)(snd (a, b) \<mapsto> cap)) obj) | _ \<Rightarrow> return (update_slots ((object_slots obj)(snd (a, b) \<mapsto> cap)) obj)) >>= KHeap_D.set_object a
od \<lbrace>\<lambda>rv s. P (\<lambda>p. opt_cap p s)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>a b x3 s. \<lbrakk>slot = (a, b); P ((\<lambda>p. opt_cap p s)((a, b) \<mapsto> cap)); cdl_objects s a = Some (Tcb x3)\<rbrakk> \<Longrightarrow> (b = tcb_ipcbuffer_slot \<and> cdl_tcb_caps x3 b \<noteq> Some cap \<longrightarrow> (\<forall>x. P (\<lambda>p. opt_cap p (s\<lparr>cdl_objects := \<lambda>b. if b = a then Some (Tcb (dupdate_tcb_intent x (x3\<lparr>cdl_tcb_caps := \<lambda>a. if a = tcb_ipcbuffer_slot then Some cap else cdl_tcb_caps x3 a\<rparr>))) else cdl_objects s b\<rparr>)))) \<and> ((b = tcb_ipcbuffer_slot \<longrightarrow> cdl_tcb_caps x3 tcb_ipcbuffer_slot = Some cap) \<longrightarrow> P (\<lambda>p. opt_cap p (s\<lparr>cdl_objects := \<lambda>c. if c = a then Some (Tcb (x3\<lparr>cdl_tcb_caps := \<lambda>a. if a = b then Some cap else cdl_tcb_caps x3 a\<rparr>)) else cdl_objects s c\<rparr>)))
 2. \<And>a b x4 s. \<lbrakk>slot = (a, b); P ((\<lambda>p. opt_cap p s)((a, b) \<mapsto> cap)); cdl_objects s a = Some (cdl_object.CNode x4)\<rbrakk> \<Longrightarrow> P (\<lambda>p. opt_cap p (s\<lparr>cdl_objects := \<lambda>c. if c = a then Some (cdl_object.CNode (x4\<lparr>cdl_cnode_caps := \<lambda>a. if a = b then Some cap else cdl_cnode_caps x4 a\<rparr>)) else cdl_objects s c\<rparr>))
 3. \<And>a b x5 s. \<lbrakk>slot = (a, b); P ((\<lambda>p. opt_cap p s)((a, b) \<mapsto> cap)); cdl_objects s a = Some (AsidPool x5)\<rbrakk> \<Longrightarrow> P (\<lambda>p. opt_cap p (s\<lparr>cdl_objects := \<lambda>c. if c = a then Some (AsidPool (x5\<lparr>cdl_asid_pool_caps := \<lambda>a. if a = b then Some cap else cdl_asid_pool_caps x5 a\<rparr>)) else cdl_objects s c\<rparr>))
 4. \<And>a b x6 s. \<lbrakk>slot = (a, b); P ((\<lambda>p. opt_cap p s)((a, b) \<mapsto> cap)); cdl_objects s a = Some (cdl_object.PageTable x6)\<rbrakk> \<Longrightarrow> P (\<lambda>p. opt_cap p (s\<lparr>cdl_objects := \<lambda>c. if c = a then Some (cdl_object.PageTable (x6\<lparr>cdl_page_table_caps := \<lambda>a. if a = b then Some cap else cdl_page_table_caps x6 a\<rparr>)) else cdl_objects s c\<rparr>))
 5. \<And>a b x7 s. \<lbrakk>slot = (a, b); P ((\<lambda>p. opt_cap p s)((a, b) \<mapsto> cap)); cdl_objects s a = Some (cdl_object.PageDirectory x7)\<rbrakk> \<Longrightarrow> P (\<lambda>p. opt_cap p (s\<lparr>cdl_objects := \<lambda>c. if c = a then Some (cdl_object.PageDirectory (x7\<lparr>cdl_page_directory_caps := \<lambda>a. if a = b then Some cap else cdl_page_directory_caps x7 a\<rparr>)) else cdl_objects s c\<rparr>))
 6. \<And>a b x10 s. \<lbrakk>slot = (a, b); P ((\<lambda>p. opt_cap p s)((a, b) \<mapsto> cap)); cdl_objects s a = Some (IRQNode x10)\<rbrakk> \<Longrightarrow> P (\<lambda>p. opt_cap p (s\<lparr>cdl_objects := \<lambda>c. if c = a then Some (IRQNode (x10\<lparr>cdl_irq_node_caps := \<lambda>a. if a = b then Some cap else cdl_irq_node_caps x10 a\<rparr>)) else cdl_objects s c\<rparr>))