theory Frame_SD

lemma set_cap_wp:
  "\<lbrace>\<lambda>s. <ptr \<mapsto>c - \<and>* R> s\<rbrace>
    set_cap ptr cap
   \<lbrace>\<lambda>rv s. <ptr \<mapsto>c cap \<and>* R> s\<rbrace>" apply (clarsimp simp: set_cap_def) apply (case_tac ptr, rename_tac obj_id slot, clarsimp) apply (wp|wpc)+ apply (rule_tac obj = obj in set_object_slot_wp) apply (wp |wpc)+ apply clarsimp apply (clarsimp simp: update_slots_def has_slots_def
                 split: cdl_object.splits) apply (rename_tac tcb) apply (rule conjI, clarsimp) apply (rename_tac intent) apply (rule_tac x = "Tcb (tcb\<lparr>cdl_tcb_intent := intent\<rparr>)" in exI) apply (clarsimp simp: object_clean_def intent_reset_def asid_reset_def
                             update_slots_def object_slots_def) apply clarsimp apply (rule_tac x = "Tcb tcb" in exI) apply (clarsimp simp: fun_eq_iff) apply (fastforce simp: cdl_cnode.splits fun_eq_iff)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift (ptr \<mapsto>c - \<and>* R)\<rbrace> set_cap ptr cap \<lbrace>\<lambda>rv. cdl.lift (ptr \<mapsto>c cap \<and>* R)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift (ptr \<mapsto>c - \<and>* R)\<rbrace> (case ptr of (obj_id, slot) \<Rightarrow> \<lambda>cap. do obj <- get_object obj_id;
y <- assert (has_slots obj);
(case update_slots ((object_slots obj)(slot \<mapsto> cap)) obj of Tcb t \<Rightarrow> if slot = tcb_ipcbuffer_slot \<and> object_slots obj slot \<noteq> Some cap then do intent' <- select UNIV;
return $ Tcb (t\<lparr>cdl_tcb_intent := intent'\<rparr>)
od else return (update_slots ((object_slots obj)(slot \<mapsto> cap)) obj) | _ \<Rightarrow> return (update_slots ((object_slots obj)(slot \<mapsto> cap)) obj)) >>= set_object obj_id
od) cap \<lbrace>\<lambda>rv. cdl.lift (ptr \<mapsto>c cap \<and>* R)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>obj_id slot. ptr = (obj_id, slot) \<Longrightarrow> \<lbrace>cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R)\<rbrace> do obj <- get_object obj_id;
y <- assert (has_slots obj);
(case update_slots ((object_slots obj)(slot \<mapsto> cap)) obj of Tcb t \<Rightarrow> if slot = tcb_ipcbuffer_slot \<and> object_slots obj slot \<noteq> Some cap then do intent' <- select UNIV;
return $ Tcb (t\<lparr>cdl_tcb_intent := intent'\<rparr>)
od else return (update_slots ((object_slots obj)(slot \<mapsto> cap)) obj) | _ \<Rightarrow> return (update_slots ((object_slots obj)(slot \<mapsto> cap)) obj)) >>= set_object obj_id
od \<lbrace>\<lambda>rv. cdl.lift ((obj_id, slot) \<mapsto>c cap \<and>* R)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>obj_id slot obj y x. ptr = (obj_id, slot) \<Longrightarrow> \<lbrace>?B4 obj_id slot obj y x\<rbrace> set_object obj_id x \<lbrace>\<lambda>rv. cdl.lift ((obj_id, slot) \<mapsto>c cap \<and>* R)\<rbrace>
 2. \<And>obj_id slot obj y. ptr = (obj_id, slot) \<Longrightarrow> \<lbrace>?B3 obj_id slot obj y\<rbrace> case update_slots ((object_slots obj)(slot \<mapsto> cap)) obj of Tcb t \<Rightarrow> if slot = tcb_ipcbuffer_slot \<and> object_slots obj slot \<noteq> Some cap then do intent' <- select UNIV;
return $ Tcb (t\<lparr>cdl_tcb_intent := intent'\<rparr>)
od else return (update_slots ((object_slots obj)(slot \<mapsto> cap)) obj) | _ \<Rightarrow> return (update_slots ((object_slots obj)(slot \<mapsto> cap)) obj) \<lbrace>?B4 obj_id slot obj y\<rbrace>
 3. \<And>obj_id slot obj. ptr = (obj_id, slot) \<Longrightarrow> \<lbrace>?B2 obj_id slot obj\<rbrace> assert (has_slots obj) \<lbrace>?B3 obj_id slot obj\<rbrace>
 4. \<And>obj_id slot. ptr = (obj_id, slot) \<Longrightarrow> \<lbrace>?Q1 obj_id slot\<rbrace> get_object obj_id \<lbrace>?B2 obj_id slot\<rbrace>
 5. \<And>obj_id slot s. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s\<rbrakk> \<Longrightarrow> ?Q1 obj_id slot s proof (prove)
goal (4 subgoals):
 1. \<And>obj_id slot obj y. ptr = (obj_id, slot) \<Longrightarrow> \<lbrace>?B3 obj_id slot obj y\<rbrace> case update_slots ((object_slots obj)(slot \<mapsto> cap)) obj of Tcb t \<Rightarrow> if slot = tcb_ipcbuffer_slot \<and> object_slots obj slot \<noteq> Some cap then do intent' <- select UNIV;
return $ Tcb (t\<lparr>cdl_tcb_intent := intent'\<rparr>)
od else return (update_slots ((object_slots obj)(slot \<mapsto> cap)) obj) | _ \<Rightarrow> return (update_slots ((object_slots obj)(slot \<mapsto> cap)) obj) \<lbrace>\<lambda>x s. cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s \<and> cdl_objects s obj_id = Some obj \<and> (\<exists>obj'. object_clean obj = object_clean obj' \<and> x = update_slots ((object_slots obj')(slot \<mapsto> cap)) obj')\<rbrace>
 2. \<And>obj_id slot obj. ptr = (obj_id, slot) \<Longrightarrow> \<lbrace>?B2 obj_id slot obj\<rbrace> assert (has_slots obj) \<lbrace>?B3 obj_id slot obj\<rbrace>
 3. \<And>obj_id slot. ptr = (obj_id, slot) \<Longrightarrow> \<lbrace>?Q1 obj_id slot\<rbrace> get_object obj_id \<lbrace>?B2 obj_id slot\<rbrace>
 4. \<And>obj_id slot s. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s\<rbrakk> \<Longrightarrow> ?Q1 obj_id slot s proof (prove)
goal (1 subgoal):
 1. \<And>obj_id slot s. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s\<rbrakk> \<Longrightarrow> cdl_objects s obj_id \<noteq> None \<longrightarrow> has_slots (the (cdl_objects s obj_id)) \<longrightarrow> (update_slots ((object_slots (the (cdl_objects s obj_id)))(slot \<mapsto> cap)) (the (cdl_objects s obj_id)) = Endpoint \<longrightarrow> cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s \<and> cdl_objects s obj_id = Some (the (cdl_objects s obj_id)) \<and> (\<exists>obj'. object_clean (the (cdl_objects s obj_id)) = object_clean obj' \<and> update_slots ((object_slots (the (cdl_objects s obj_id)))(slot \<mapsto> cap)) (the (cdl_objects s obj_id)) = update_slots ((object_slots obj')(slot \<mapsto> cap)) obj')) \<and> (update_slots ((object_slots (the (cdl_objects s obj_id)))(slot \<mapsto> cap)) (the (cdl_objects s obj_id)) = Notification \<longrightarrow> cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s \<and> cdl_objects s obj_id = Some (the (cdl_objects s obj_id)) \<and> (\<exists>obj'. object_clean (the (cdl_objects s obj_id)) = object_clean obj' \<and> update_slots ((object_slots (the (cdl_objects s obj_id)))(slot \<mapsto> cap)) (the (cdl_objects s obj_id)) = update_slots ((object_slots obj')(slot \<mapsto> cap)) obj')) \<and> (\<forall>x. update_slots ((object_slots (the (cdl_objects s obj_id)))(slot \<mapsto> cap)) (the (cdl_objects s obj_id)) = Tcb x \<longrightarrow> (slot = tcb_ipcbuffer_slot \<and> object_slots (the (cdl_objects s obj_id)) slot \<noteq> Some cap \<longrightarrow> (\<forall>xa\<in>UNIV. cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s \<and> cdl_objects s obj_id = Some (the (cdl_objects s obj_id)) \<and> (\<exists>obj'. object_clean (the (cdl_objects s obj_id)) = object_clean obj' \<and> Tcb (x\<lparr>cdl_tcb_intent := xa\<rparr>) = update_slots ((object_slots obj')(slot \<mapsto> cap)) obj'))) \<and> (\<not> (slot = tcb_ipcbuffer_slot \<and> object_slots (the (cdl_objects s obj_id)) slot \<noteq> Some cap) \<longrightarrow> cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s \<and> cdl_objects s obj_id = Some (the (cdl_objects s obj_id)) \<and> (\<exists>obj'. object_clean (the (cdl_objects s obj_id)) = object_clean obj' \<and> update_slots ((object_slots (the (cdl_objects s obj_id)))(slot \<mapsto> cap)) (the (cdl_objects s obj_id)) = update_slots ((object_slots obj')(slot \<mapsto> cap)) obj'))) \<and> (\<forall>x. update_slots ((object_slots (the (cdl_objects s obj_id)))(slot \<mapsto> cap)) (the (cdl_objects s obj_id)) = CNode x \<longrightarrow> cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s \<and> cdl_objects s obj_id = Some (the (cdl_objects s obj_id)) \<and> (\<exists>obj'. object_clean (the (cdl_objects s obj_id)) = object_clean obj' \<and> update_slots ((object_slots (the (cdl_objects s obj_id)))(slot \<mapsto> cap)) (the (cdl_objects s obj_id)) = update_slots ((object_slots obj')(slot \<mapsto> cap)) obj')) \<and> (\<forall>x. update_slots ((object_slots (the (cdl_objects s obj_id)))(slot \<mapsto> cap)) (the (cdl_objects s obj_id)) = AsidPool x \<longrightarrow> cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s \<and> cdl_objects s obj_id = Some (the (cdl_objects s obj_id)) \<and> (\<exists>obj'. object_clean (the (cdl_objects s obj_id)) = object_clean obj' \<and> update_slots ((object_slots (the (cdl_objects s obj_id)))(slot \<mapsto> cap)) (the (cdl_objects s obj_id)) = update_slots ((object_slots obj')(slot \<mapsto> cap)) obj')) \<and> (\<forall>x. update_slots ((object_slots (the (cdl_objects s obj_id)))(slot \<mapsto> cap)) (the (cdl_objects s obj_id)) = PageTable x \<longrightarrow> cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s \<and> cdl_objects s obj_id = Some (the (cdl_objects s obj_id)) \<and> (\<exists>obj'. object_clean (the (cdl_objects s obj_id)) = object_clean obj' \<and> update_slots ((object_slots (the (cdl_objects s obj_id)))(slot \<mapsto> cap)) (the (cdl_objects s obj_id)) = update_slots ((object_slots obj')(slot \<mapsto> cap)) obj')) \<and> (\<forall>x. update_slots ((object_slots (the (cdl_objects s obj_id)))(slot \<mapsto> cap)) (the (cdl_objects s obj_id)) = PageDirectory x \<longrightarrow> cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s \<and> cdl_objects s obj_id = Some (the (cdl_objects s obj_id)) \<and> (\<exists>obj'. object_clean (the (cdl_objects s obj_id)) = object_clean obj' \<and> update_slots ((object_slots (the (cdl_objects s obj_id)))(slot \<mapsto> cap)) (the (cdl_objects s obj_id)) = update_slots ((object_slots obj')(slot \<mapsto> cap)) obj')) \<and> (\<forall>x. update_slots ((object_slots (the (cdl_objects s obj_id)))(slot \<mapsto> cap)) (the (cdl_objects s obj_id)) = Frame x \<longrightarrow> cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s \<and> cdl_objects s obj_id = Some (the (cdl_objects s obj_id)) \<and> (\<exists>obj'. object_clean (the (cdl_objects s obj_id)) = object_clean obj' \<and> update_slots ((object_slots (the (cdl_objects s obj_id)))(slot \<mapsto> cap)) (the (cdl_objects s obj_id)) = update_slots ((object_slots obj')(slot \<mapsto> cap)) obj')) \<and> (update_slots ((object_slots (the (cdl_objects s obj_id)))(slot \<mapsto> cap)) (the (cdl_objects s obj_id)) = Untyped \<longrightarrow> cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s \<and> cdl_objects s obj_id = Some (the (cdl_objects s obj_id)) \<and> (\<exists>obj'. object_clean (the (cdl_objects s obj_id)) = object_clean obj' \<and> update_slots ((object_slots (the (cdl_objects s obj_id)))(slot \<mapsto> cap)) (the (cdl_objects s obj_id)) = update_slots ((object_slots obj')(slot \<mapsto> cap)) obj')) \<and> (\<forall>x. update_slots ((object_slots (the (cdl_objects s obj_id)))(slot \<mapsto> cap)) (the (cdl_objects s obj_id)) = IRQNode x \<longrightarrow> cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s \<and> cdl_objects s obj_id = Some (the (cdl_objects s obj_id)) \<and> (\<exists>obj'. object_clean (the (cdl_objects s obj_id)) = object_clean obj' \<and> update_slots ((object_slots (the (cdl_objects s obj_id)))(slot \<mapsto> cap)) (the (cdl_objects s obj_id)) = update_slots ((object_slots obj')(slot \<mapsto> cap)) obj')) proof (prove)
goal (1 subgoal):
 1. \<And>obj_id slot s y. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some y; has_slots y\<rbrakk> \<Longrightarrow> (update_slots ((object_slots y)(slot \<mapsto> cap)) y = Endpoint \<longrightarrow> (\<exists>obj'. object_clean y = object_clean obj' \<and> update_slots (\<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a) y = update_slots ((object_slots obj')(slot \<mapsto> cap)) obj')) \<and> (update_slots ((object_slots y)(slot \<mapsto> cap)) y = Notification \<longrightarrow> (\<exists>obj'. object_clean y = object_clean obj' \<and> update_slots (\<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a) y = update_slots ((object_slots obj')(slot \<mapsto> cap)) obj')) \<and> (\<forall>x. update_slots ((object_slots y)(slot \<mapsto> cap)) y = Tcb x \<longrightarrow> (slot = tcb_ipcbuffer_slot \<and> object_slots y slot \<noteq> Some cap \<longrightarrow> cdl.lift ((obj_id, tcb_ipcbuffer_slot) \<mapsto>c - \<and>* R) s \<and> (\<forall>xa. \<exists>obj'. object_clean y = object_clean obj' \<and> Tcb (x\<lparr>cdl_tcb_intent := xa\<rparr>) = update_slots ((object_slots obj')(tcb_ipcbuffer_slot \<mapsto> cap)) obj')) \<and> ((slot = tcb_ipcbuffer_slot \<longrightarrow> object_slots y tcb_ipcbuffer_slot = Some cap) \<longrightarrow> (\<exists>obj'. object_clean y = object_clean obj' \<and> update_slots (\<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a) y = update_slots ((object_slots obj')(slot \<mapsto> cap)) obj'))) \<and> ((\<exists>x. update_slots ((object_slots y)(slot \<mapsto> cap)) y = CNode x) \<longrightarrow> (\<exists>obj'. object_clean y = object_clean obj' \<and> update_slots (\<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a) y = update_slots ((object_slots obj')(slot \<mapsto> cap)) obj')) \<and> ((\<exists>x. update_slots ((object_slots y)(slot \<mapsto> cap)) y = AsidPool x) \<longrightarrow> (\<exists>obj'. object_clean y = object_clean obj' \<and> update_slots (\<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a) y = update_slots ((object_slots obj')(slot \<mapsto> cap)) obj')) \<and> ((\<exists>x. update_slots ((object_slots y)(slot \<mapsto> cap)) y = PageTable x) \<longrightarrow> (\<exists>obj'. object_clean y = object_clean obj' \<and> update_slots (\<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a) y = update_slots ((object_slots obj')(slot \<mapsto> cap)) obj')) \<and> ((\<exists>x. update_slots ((object_slots y)(slot \<mapsto> cap)) y = PageDirectory x) \<longrightarrow> (\<exists>obj'. object_clean y = object_clean obj' \<and> update_slots (\<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a) y = update_slots ((object_slots obj')(slot \<mapsto> cap)) obj')) \<and> ((\<exists>x. update_slots ((object_slots y)(slot \<mapsto> cap)) y = Frame x) \<longrightarrow> (\<exists>obj'. object_clean y = object_clean obj' \<and> update_slots (\<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a) y = update_slots ((object_slots obj')(slot \<mapsto> cap)) obj')) \<and> (update_slots ((object_slots y)(slot \<mapsto> cap)) y = Untyped \<longrightarrow> (\<exists>obj'. object_clean y = object_clean obj' \<and> update_slots (\<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a) y = update_slots ((object_slots obj')(slot \<mapsto> cap)) obj')) \<and> ((\<exists>x. update_slots ((object_slots y)(slot \<mapsto> cap)) y = IRQNode x) \<longrightarrow> (\<exists>obj'. object_clean y = object_clean obj' \<and> update_slots (\<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a) y = update_slots ((object_slots obj')(slot \<mapsto> cap)) obj')) proof (prove)
goal (6 subgoals):
 1. \<And>obj_id slot s x3. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (Tcb x3)\<rbrakk> \<Longrightarrow> (slot = tcb_ipcbuffer_slot \<and> object_slots (Tcb x3) slot \<noteq> Some cap \<longrightarrow> cdl.lift ((obj_id, tcb_ipcbuffer_slot) \<mapsto>c - \<and>* R) s \<and> (\<forall>x. \<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3a. obj' = Tcb x3a \<longrightarrow> object_clean (Tcb x3) = object_clean (Tcb x3a) \<and> x3\<lparr>cdl_tcb_caps := (object_slots (Tcb x3))(tcb_ipcbuffer_slot \<mapsto> cap), cdl_tcb_intent := x\<rparr> = x3a\<lparr>cdl_tcb_caps := (object_slots (Tcb x3a))(tcb_ipcbuffer_slot \<mapsto> cap)\<rparr>) \<and> (\<forall>x4. obj' \<noteq> CNode x4) \<and> (\<forall>x5. obj' \<noteq> AsidPool x5) \<and> (\<forall>x6. obj' \<noteq> PageTable x6) \<and> (\<forall>x7. obj' \<noteq> PageDirectory x7) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10. obj' \<noteq> IRQNode x10))) \<and> ((slot = tcb_ipcbuffer_slot \<longrightarrow> object_slots (Tcb x3) tcb_ipcbuffer_slot = Some cap) \<longrightarrow> (\<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3a. obj' = Tcb x3a \<longrightarrow> object_clean (Tcb x3) = object_clean (Tcb x3a) \<and> x3\<lparr>cdl_tcb_caps := \<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a\<rparr> = x3a\<lparr>cdl_tcb_caps := (object_slots (Tcb x3a))(slot \<mapsto> cap)\<rparr>) \<and> (\<forall>x4. obj' \<noteq> CNode x4) \<and> (\<forall>x5. obj' \<noteq> AsidPool x5) \<and> (\<forall>x6. obj' \<noteq> PageTable x6) \<and> (\<forall>x7. obj' \<noteq> PageDirectory x7) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10. obj' \<noteq> IRQNode x10)))
 2. \<And>obj_id slot s x4. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (CNode x4)\<rbrakk> \<Longrightarrow> \<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3. obj' \<noteq> Tcb x3) \<and> (\<forall>x4a. obj' = CNode x4a \<longrightarrow> object_clean (CNode x4) = object_clean (CNode x4a) \<and> x4\<lparr>cdl_cnode_caps := \<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a\<rparr> = x4a\<lparr>cdl_cnode_caps := (object_slots (CNode x4a))(slot \<mapsto> cap)\<rparr>) \<and> (\<forall>x5. obj' \<noteq> AsidPool x5) \<and> (\<forall>x6. obj' \<noteq> PageTable x6) \<and> (\<forall>x7. obj' \<noteq> PageDirectory x7) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10. obj' \<noteq> IRQNode x10)
 3. \<And>obj_id slot s x5. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (AsidPool x5)\<rbrakk> \<Longrightarrow> \<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3. obj' \<noteq> Tcb x3) \<and> (\<forall>x4. obj' \<noteq> CNode x4) \<and> (\<forall>x5a. obj' = AsidPool x5a \<longrightarrow> object_clean (AsidPool x5) = object_clean (AsidPool x5a) \<and> x5\<lparr>cdl_asid_pool_caps := \<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a\<rparr> = x5a\<lparr>cdl_asid_pool_caps := (object_slots (AsidPool x5a))(slot \<mapsto> cap)\<rparr>) \<and> (\<forall>x6. obj' \<noteq> PageTable x6) \<and> (\<forall>x7. obj' \<noteq> PageDirectory x7) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10. obj' \<noteq> IRQNode x10)
 4. \<And>obj_id slot s x6. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (PageTable x6)\<rbrakk> \<Longrightarrow> \<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3. obj' \<noteq> Tcb x3) \<and> (\<forall>x4. obj' \<noteq> CNode x4) \<and> (\<forall>x5. obj' \<noteq> AsidPool x5) \<and> (\<forall>x6a. obj' = PageTable x6a \<longrightarrow> object_clean (PageTable x6) = object_clean (PageTable x6a) \<and> x6\<lparr>cdl_page_table_caps := \<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a\<rparr> = x6a\<lparr>cdl_page_table_caps := (object_slots (PageTable x6a))(slot \<mapsto> cap)\<rparr>) \<and> (\<forall>x7. obj' \<noteq> PageDirectory x7) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10. obj' \<noteq> IRQNode x10)
 5. \<And>obj_id slot s x7. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (PageDirectory x7)\<rbrakk> \<Longrightarrow> \<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3. obj' \<noteq> Tcb x3) \<and> (\<forall>x4. obj' \<noteq> CNode x4) \<and> (\<forall>x5. obj' \<noteq> AsidPool x5) \<and> (\<forall>x6. obj' \<noteq> PageTable x6) \<and> (\<forall>x7a. obj' = PageDirectory x7a \<longrightarrow> object_clean (PageDirectory x7) = object_clean (PageDirectory x7a) \<and> x7\<lparr>cdl_page_directory_caps := \<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a\<rparr> = x7a\<lparr>cdl_page_directory_caps := (object_slots (PageDirectory x7a))(slot \<mapsto> cap)\<rparr>) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10. obj' \<noteq> IRQNode x10)
 6. \<And>obj_id slot s x10. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (IRQNode x10)\<rbrakk> \<Longrightarrow> \<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3. obj' \<noteq> Tcb x3) \<and> (\<forall>x4. obj' \<noteq> CNode x4) \<and> (\<forall>x5. obj' \<noteq> AsidPool x5) \<and> (\<forall>x6. obj' \<noteq> PageTable x6) \<and> (\<forall>x7. obj' \<noteq> PageDirectory x7) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10a. obj' = IRQNode x10a \<longrightarrow> object_clean (IRQNode x10) = object_clean (IRQNode x10a) \<and> x10\<lparr>cdl_irq_node_caps := \<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a\<rparr> = x10a\<lparr>cdl_irq_node_caps := (object_slots (IRQNode x10a))(slot \<mapsto> cap)\<rparr>) proof (prove)
goal (6 subgoals):
 1. \<And>obj_id slot s tcb. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcb)\<rbrakk> \<Longrightarrow> (slot = tcb_ipcbuffer_slot \<and> object_slots (Tcb tcb) slot \<noteq> Some cap \<longrightarrow> cdl.lift ((obj_id, tcb_ipcbuffer_slot) \<mapsto>c - \<and>* R) s \<and> (\<forall>x. \<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3. obj' = Tcb x3 \<longrightarrow> object_clean (Tcb tcb) = object_clean (Tcb x3) \<and> tcb\<lparr>cdl_tcb_caps := (object_slots (Tcb tcb))(tcb_ipcbuffer_slot \<mapsto> cap), cdl_tcb_intent := x\<rparr> = x3\<lparr>cdl_tcb_caps := (object_slots (Tcb x3))(tcb_ipcbuffer_slot \<mapsto> cap)\<rparr>) \<and> (\<forall>x4. obj' \<noteq> CNode x4) \<and> (\<forall>x5. obj' \<noteq> AsidPool x5) \<and> (\<forall>x6. obj' \<noteq> PageTable x6) \<and> (\<forall>x7. obj' \<noteq> PageDirectory x7) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10. obj' \<noteq> IRQNode x10))) \<and> ((slot = tcb_ipcbuffer_slot \<longrightarrow> object_slots (Tcb tcb) tcb_ipcbuffer_slot = Some cap) \<longrightarrow> (\<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3. obj' = Tcb x3 \<longrightarrow> object_clean (Tcb tcb) = object_clean (Tcb x3) \<and> tcb\<lparr>cdl_tcb_caps := \<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a\<rparr> = x3\<lparr>cdl_tcb_caps := (object_slots (Tcb x3))(slot \<mapsto> cap)\<rparr>) \<and> (\<forall>x4. obj' \<noteq> CNode x4) \<and> (\<forall>x5. obj' \<noteq> AsidPool x5) \<and> (\<forall>x6. obj' \<noteq> PageTable x6) \<and> (\<forall>x7. obj' \<noteq> PageDirectory x7) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10. obj' \<noteq> IRQNode x10)))
 2. \<And>obj_id slot s x4. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (CNode x4)\<rbrakk> \<Longrightarrow> \<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3. obj' \<noteq> Tcb x3) \<and> (\<forall>x4a. obj' = CNode x4a \<longrightarrow> object_clean (CNode x4) = object_clean (CNode x4a) \<and> x4\<lparr>cdl_cnode_caps := \<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a\<rparr> = x4a\<lparr>cdl_cnode_caps := (object_slots (CNode x4a))(slot \<mapsto> cap)\<rparr>) \<and> (\<forall>x5. obj' \<noteq> AsidPool x5) \<and> (\<forall>x6. obj' \<noteq> PageTable x6) \<and> (\<forall>x7. obj' \<noteq> PageDirectory x7) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10. obj' \<noteq> IRQNode x10)
 3. \<And>obj_id slot s x5. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (AsidPool x5)\<rbrakk> \<Longrightarrow> \<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3. obj' \<noteq> Tcb x3) \<and> (\<forall>x4. obj' \<noteq> CNode x4) \<and> (\<forall>x5a. obj' = AsidPool x5a \<longrightarrow> object_clean (AsidPool x5) = object_clean (AsidPool x5a) \<and> x5\<lparr>cdl_asid_pool_caps := \<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a\<rparr> = x5a\<lparr>cdl_asid_pool_caps := (object_slots (AsidPool x5a))(slot \<mapsto> cap)\<rparr>) \<and> (\<forall>x6. obj' \<noteq> PageTable x6) \<and> (\<forall>x7. obj' \<noteq> PageDirectory x7) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10. obj' \<noteq> IRQNode x10)
 4. \<And>obj_id slot s x6. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (PageTable x6)\<rbrakk> \<Longrightarrow> \<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3. obj' \<noteq> Tcb x3) \<and> (\<forall>x4. obj' \<noteq> CNode x4) \<and> (\<forall>x5. obj' \<noteq> AsidPool x5) \<and> (\<forall>x6a. obj' = PageTable x6a \<longrightarrow> object_clean (PageTable x6) = object_clean (PageTable x6a) \<and> x6\<lparr>cdl_page_table_caps := \<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a\<rparr> = x6a\<lparr>cdl_page_table_caps := (object_slots (PageTable x6a))(slot \<mapsto> cap)\<rparr>) \<and> (\<forall>x7. obj' \<noteq> PageDirectory x7) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10. obj' \<noteq> IRQNode x10)
 5. \<And>obj_id slot s x7. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (PageDirectory x7)\<rbrakk> \<Longrightarrow> \<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3. obj' \<noteq> Tcb x3) \<and> (\<forall>x4. obj' \<noteq> CNode x4) \<and> (\<forall>x5. obj' \<noteq> AsidPool x5) \<and> (\<forall>x6. obj' \<noteq> PageTable x6) \<and> (\<forall>x7a. obj' = PageDirectory x7a \<longrightarrow> object_clean (PageDirectory x7) = object_clean (PageDirectory x7a) \<and> x7\<lparr>cdl_page_directory_caps := \<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a\<rparr> = x7a\<lparr>cdl_page_directory_caps := (object_slots (PageDirectory x7a))(slot \<mapsto> cap)\<rparr>) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10. obj' \<noteq> IRQNode x10)
 6. \<And>obj_id slot s x10. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (IRQNode x10)\<rbrakk> \<Longrightarrow> \<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3. obj' \<noteq> Tcb x3) \<and> (\<forall>x4. obj' \<noteq> CNode x4) \<and> (\<forall>x5. obj' \<noteq> AsidPool x5) \<and> (\<forall>x6. obj' \<noteq> PageTable x6) \<and> (\<forall>x7. obj' \<noteq> PageDirectory x7) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10a. obj' = IRQNode x10a \<longrightarrow> object_clean (IRQNode x10) = object_clean (IRQNode x10a) \<and> x10\<lparr>cdl_irq_node_caps := \<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a\<rparr> = x10a\<lparr>cdl_irq_node_caps := (object_slots (IRQNode x10a))(slot \<mapsto> cap)\<rparr>) proof (prove)
goal (7 subgoals):
 1. \<And>obj_id s tcb x. \<lbrakk>ptr = (obj_id, tcb_ipcbuffer_slot); cdl.lift ((obj_id, tcb_ipcbuffer_slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcb); object_slots (Tcb tcb) tcb_ipcbuffer_slot \<noteq> Some cap\<rbrakk> \<Longrightarrow> \<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3. obj' = Tcb x3 \<longrightarrow> object_clean (Tcb tcb) = object_clean (Tcb x3) \<and> tcb\<lparr>cdl_tcb_caps := (object_slots (Tcb tcb))(tcb_ipcbuffer_slot \<mapsto> cap), cdl_tcb_intent := x\<rparr> = x3\<lparr>cdl_tcb_caps := (object_slots (Tcb x3))(tcb_ipcbuffer_slot \<mapsto> cap)\<rparr>) \<and> (\<forall>x4. obj' \<noteq> CNode x4) \<and> (\<forall>x5. obj' \<noteq> AsidPool x5) \<and> (\<forall>x6. obj' \<noteq> PageTable x6) \<and> (\<forall>x7. obj' \<noteq> PageDirectory x7) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10. obj' \<noteq> IRQNode x10)
 2. \<And>obj_id slot s tcb. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcb)\<rbrakk> \<Longrightarrow> (slot = tcb_ipcbuffer_slot \<longrightarrow> object_slots (Tcb tcb) tcb_ipcbuffer_slot = Some cap) \<longrightarrow> (\<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3. obj' = Tcb x3 \<longrightarrow> object_clean (Tcb tcb) = object_clean (Tcb x3) \<and> tcb\<lparr>cdl_tcb_caps := \<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a\<rparr> = x3\<lparr>cdl_tcb_caps := (object_slots (Tcb x3))(slot \<mapsto> cap)\<rparr>) \<and> (\<forall>x4. obj' \<noteq> CNode x4) \<and> (\<forall>x5. obj' \<noteq> AsidPool x5) \<and> (\<forall>x6. obj' \<noteq> PageTable x6) \<and> (\<forall>x7. obj' \<noteq> PageDirectory x7) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10. obj' \<noteq> IRQNode x10))
 3. \<And>obj_id slot s x4. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (CNode x4)\<rbrakk> \<Longrightarrow> \<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3. obj' \<noteq> Tcb x3) \<and> (\<forall>x4a. obj' = CNode x4a \<longrightarrow> object_clean (CNode x4) = object_clean (CNode x4a) \<and> x4\<lparr>cdl_cnode_caps := \<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a\<rparr> = x4a\<lparr>cdl_cnode_caps := (object_slots (CNode x4a))(slot \<mapsto> cap)\<rparr>) \<and> (\<forall>x5. obj' \<noteq> AsidPool x5) \<and> (\<forall>x6. obj' \<noteq> PageTable x6) \<and> (\<forall>x7. obj' \<noteq> PageDirectory x7) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10. obj' \<noteq> IRQNode x10)
 4. \<And>obj_id slot s x5. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (AsidPool x5)\<rbrakk> \<Longrightarrow> \<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3. obj' \<noteq> Tcb x3) \<and> (\<forall>x4. obj' \<noteq> CNode x4) \<and> (\<forall>x5a. obj' = AsidPool x5a \<longrightarrow> object_clean (AsidPool x5) = object_clean (AsidPool x5a) \<and> x5\<lparr>cdl_asid_pool_caps := \<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a\<rparr> = x5a\<lparr>cdl_asid_pool_caps := (object_slots (AsidPool x5a))(slot \<mapsto> cap)\<rparr>) \<and> (\<forall>x6. obj' \<noteq> PageTable x6) \<and> (\<forall>x7. obj' \<noteq> PageDirectory x7) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10. obj' \<noteq> IRQNode x10)
 5. \<And>obj_id slot s x6. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (PageTable x6)\<rbrakk> \<Longrightarrow> \<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3. obj' \<noteq> Tcb x3) \<and> (\<forall>x4. obj' \<noteq> CNode x4) \<and> (\<forall>x5. obj' \<noteq> AsidPool x5) \<and> (\<forall>x6a. obj' = PageTable x6a \<longrightarrow> object_clean (PageTable x6) = object_clean (PageTable x6a) \<and> x6\<lparr>cdl_page_table_caps := \<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a\<rparr> = x6a\<lparr>cdl_page_table_caps := (object_slots (PageTable x6a))(slot \<mapsto> cap)\<rparr>) \<and> (\<forall>x7. obj' \<noteq> PageDirectory x7) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10. obj' \<noteq> IRQNode x10)
 6. \<And>obj_id slot s x7. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (PageDirectory x7)\<rbrakk> \<Longrightarrow> \<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3. obj' \<noteq> Tcb x3) \<and> (\<forall>x4. obj' \<noteq> CNode x4) \<and> (\<forall>x5. obj' \<noteq> AsidPool x5) \<and> (\<forall>x6. obj' \<noteq> PageTable x6) \<and> (\<forall>x7a. obj' = PageDirectory x7a \<longrightarrow> object_clean (PageDirectory x7) = object_clean (PageDirectory x7a) \<and> x7\<lparr>cdl_page_directory_caps := \<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a\<rparr> = x7a\<lparr>cdl_page_directory_caps := (object_slots (PageDirectory x7a))(slot \<mapsto> cap)\<rparr>) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10. obj' \<noteq> IRQNode x10)
 7. \<And>obj_id slot s x10. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (IRQNode x10)\<rbrakk> \<Longrightarrow> \<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3. obj' \<noteq> Tcb x3) \<and> (\<forall>x4. obj' \<noteq> CNode x4) \<and> (\<forall>x5. obj' \<noteq> AsidPool x5) \<and> (\<forall>x6. obj' \<noteq> PageTable x6) \<and> (\<forall>x7. obj' \<noteq> PageDirectory x7) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10a. obj' = IRQNode x10a \<longrightarrow> object_clean (IRQNode x10) = object_clean (IRQNode x10a) \<and> x10\<lparr>cdl_irq_node_caps := \<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a\<rparr> = x10a\<lparr>cdl_irq_node_caps := (object_slots (IRQNode x10a))(slot \<mapsto> cap)\<rparr>) proof (prove)
goal (7 subgoals):
 1. \<And>obj_id s tcb intent. \<lbrakk>ptr = (obj_id, tcb_ipcbuffer_slot); cdl.lift ((obj_id, tcb_ipcbuffer_slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcb); object_slots (Tcb tcb) tcb_ipcbuffer_slot \<noteq> Some cap\<rbrakk> \<Longrightarrow> \<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3. obj' = Tcb x3 \<longrightarrow> object_clean (Tcb tcb) = object_clean (Tcb x3) \<and> tcb\<lparr>cdl_tcb_caps := (object_slots (Tcb tcb))(tcb_ipcbuffer_slot \<mapsto> cap), cdl_tcb_intent := intent\<rparr> = x3\<lparr>cdl_tcb_caps := (object_slots (Tcb x3))(tcb_ipcbuffer_slot \<mapsto> cap)\<rparr>) \<and> (\<forall>x4. obj' \<noteq> CNode x4) \<and> (\<forall>x5. obj' \<noteq> AsidPool x5) \<and> (\<forall>x6. obj' \<noteq> PageTable x6) \<and> (\<forall>x7. obj' \<noteq> PageDirectory x7) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10. obj' \<noteq> IRQNode x10)
 2. \<And>obj_id slot s tcb. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcb)\<rbrakk> \<Longrightarrow> (slot = tcb_ipcbuffer_slot \<longrightarrow> object_slots (Tcb tcb) tcb_ipcbuffer_slot = Some cap) \<longrightarrow> (\<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3. obj' = Tcb x3 \<longrightarrow> object_clean (Tcb tcb) = object_clean (Tcb x3) \<and> tcb\<lparr>cdl_tcb_caps := \<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a\<rparr> = x3\<lparr>cdl_tcb_caps := (object_slots (Tcb x3))(slot \<mapsto> cap)\<rparr>) \<and> (\<forall>x4. obj' \<noteq> CNode x4) \<and> (\<forall>x5. obj' \<noteq> AsidPool x5) \<and> (\<forall>x6. obj' \<noteq> PageTable x6) \<and> (\<forall>x7. obj' \<noteq> PageDirectory x7) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10. obj' \<noteq> IRQNode x10))
 3. \<And>obj_id slot s x4. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (CNode x4)\<rbrakk> \<Longrightarrow> \<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3. obj' \<noteq> Tcb x3) \<and> (\<forall>x4a. obj' = CNode x4a \<longrightarrow> object_clean (CNode x4) = object_clean (CNode x4a) \<and> x4\<lparr>cdl_cnode_caps := \<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a\<rparr> = x4a\<lparr>cdl_cnode_caps := (object_slots (CNode x4a))(slot \<mapsto> cap)\<rparr>) \<and> (\<forall>x5. obj' \<noteq> AsidPool x5) \<and> (\<forall>x6. obj' \<noteq> PageTable x6) \<and> (\<forall>x7. obj' \<noteq> PageDirectory x7) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10. obj' \<noteq> IRQNode x10)
 4. \<And>obj_id slot s x5. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (AsidPool x5)\<rbrakk> \<Longrightarrow> \<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3. obj' \<noteq> Tcb x3) \<and> (\<forall>x4. obj' \<noteq> CNode x4) \<and> (\<forall>x5a. obj' = AsidPool x5a \<longrightarrow> object_clean (AsidPool x5) = object_clean (AsidPool x5a) \<and> x5\<lparr>cdl_asid_pool_caps := \<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a\<rparr> = x5a\<lparr>cdl_asid_pool_caps := (object_slots (AsidPool x5a))(slot \<mapsto> cap)\<rparr>) \<and> (\<forall>x6. obj' \<noteq> PageTable x6) \<and> (\<forall>x7. obj' \<noteq> PageDirectory x7) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10. obj' \<noteq> IRQNode x10)
 5. \<And>obj_id slot s x6. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (PageTable x6)\<rbrakk> \<Longrightarrow> \<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3. obj' \<noteq> Tcb x3) \<and> (\<forall>x4. obj' \<noteq> CNode x4) \<and> (\<forall>x5. obj' \<noteq> AsidPool x5) \<and> (\<forall>x6a. obj' = PageTable x6a \<longrightarrow> object_clean (PageTable x6) = object_clean (PageTable x6a) \<and> x6\<lparr>cdl_page_table_caps := \<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a\<rparr> = x6a\<lparr>cdl_page_table_caps := (object_slots (PageTable x6a))(slot \<mapsto> cap)\<rparr>) \<and> (\<forall>x7. obj' \<noteq> PageDirectory x7) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10. obj' \<noteq> IRQNode x10)
 6. \<And>obj_id slot s x7. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (PageDirectory x7)\<rbrakk> \<Longrightarrow> \<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3. obj' \<noteq> Tcb x3) \<and> (\<forall>x4. obj' \<noteq> CNode x4) \<and> (\<forall>x5. obj' \<noteq> AsidPool x5) \<and> (\<forall>x6. obj' \<noteq> PageTable x6) \<and> (\<forall>x7a. obj' = PageDirectory x7a \<longrightarrow> object_clean (PageDirectory x7) = object_clean (PageDirectory x7a) \<and> x7\<lparr>cdl_page_directory_caps := \<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a\<rparr> = x7a\<lparr>cdl_page_directory_caps := (object_slots (PageDirectory x7a))(slot \<mapsto> cap)\<rparr>) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10. obj' \<noteq> IRQNode x10)
 7. \<And>obj_id slot s x10. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (IRQNode x10)\<rbrakk> \<Longrightarrow> \<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3. obj' \<noteq> Tcb x3) \<and> (\<forall>x4. obj' \<noteq> CNode x4) \<and> (\<forall>x5. obj' \<noteq> AsidPool x5) \<and> (\<forall>x6. obj' \<noteq> PageTable x6) \<and> (\<forall>x7. obj' \<noteq> PageDirectory x7) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10a. obj' = IRQNode x10a \<longrightarrow> object_clean (IRQNode x10) = object_clean (IRQNode x10a) \<and> x10\<lparr>cdl_irq_node_caps := \<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a\<rparr> = x10a\<lparr>cdl_irq_node_caps := (object_slots (IRQNode x10a))(slot \<mapsto> cap)\<rparr>) proof (prove)
goal (7 subgoals):
 1. \<And>obj_id s tcb intent. \<lbrakk>ptr = (obj_id, tcb_ipcbuffer_slot); cdl.lift ((obj_id, tcb_ipcbuffer_slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcb); object_slots (Tcb tcb) tcb_ipcbuffer_slot \<noteq> Some cap\<rbrakk> \<Longrightarrow> Tcb (tcb\<lparr>cdl_tcb_intent := intent\<rparr>) \<noteq> Endpoint \<and> Tcb (tcb\<lparr>cdl_tcb_intent := intent\<rparr>) \<noteq> Notification \<and> (\<forall>x3. Tcb (tcb\<lparr>cdl_tcb_intent := intent\<rparr>) = Tcb x3 \<longrightarrow> object_clean (Tcb tcb) = object_clean (Tcb x3) \<and> tcb\<lparr>cdl_tcb_caps := (object_slots (Tcb tcb))(tcb_ipcbuffer_slot \<mapsto> cap), cdl_tcb_intent := intent\<rparr> = x3\<lparr>cdl_tcb_caps := (object_slots (Tcb x3))(tcb_ipcbuffer_slot \<mapsto> cap)\<rparr>) \<and> (\<forall>x4. Tcb (tcb\<lparr>cdl_tcb_intent := intent\<rparr>) \<noteq> CNode x4) \<and> (\<forall>x5. Tcb (tcb\<lparr>cdl_tcb_intent := intent\<rparr>) \<noteq> AsidPool x5) \<and> (\<forall>x6. Tcb (tcb\<lparr>cdl_tcb_intent := intent\<rparr>) \<noteq> PageTable x6) \<and> (\<forall>x7. Tcb (tcb\<lparr>cdl_tcb_intent := intent\<rparr>) \<noteq> PageDirectory x7) \<and> (\<forall>x8. Tcb (tcb\<lparr>cdl_tcb_intent := intent\<rparr>) \<noteq> Frame x8) \<and> Tcb (tcb\<lparr>cdl_tcb_intent := intent\<rparr>) \<noteq> Untyped \<and> (\<forall>x10. Tcb (tcb\<lparr>cdl_tcb_intent := intent\<rparr>) \<noteq> IRQNode x10)
 2. \<And>obj_id slot s tcb. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcb)\<rbrakk> \<Longrightarrow> (slot = tcb_ipcbuffer_slot \<longrightarrow> object_slots (Tcb tcb) tcb_ipcbuffer_slot = Some cap) \<longrightarrow> (\<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3. obj' = Tcb x3 \<longrightarrow> object_clean (Tcb tcb) = object_clean (Tcb x3) \<and> tcb\<lparr>cdl_tcb_caps := \<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a\<rparr> = x3\<lparr>cdl_tcb_caps := (object_slots (Tcb x3))(slot \<mapsto> cap)\<rparr>) \<and> (\<forall>x4. obj' \<noteq> CNode x4) \<and> (\<forall>x5. obj' \<noteq> AsidPool x5) \<and> (\<forall>x6. obj' \<noteq> PageTable x6) \<and> (\<forall>x7. obj' \<noteq> PageDirectory x7) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10. obj' \<noteq> IRQNode x10))
 3. \<And>obj_id slot s x4. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (CNode x4)\<rbrakk> \<Longrightarrow> \<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3. obj' \<noteq> Tcb x3) \<and> (\<forall>x4a. obj' = CNode x4a \<longrightarrow> object_clean (CNode x4) = object_clean (CNode x4a) \<and> x4\<lparr>cdl_cnode_caps := \<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a\<rparr> = x4a\<lparr>cdl_cnode_caps := (object_slots (CNode x4a))(slot \<mapsto> cap)\<rparr>) \<and> (\<forall>x5. obj' \<noteq> AsidPool x5) \<and> (\<forall>x6. obj' \<noteq> PageTable x6) \<and> (\<forall>x7. obj' \<noteq> PageDirectory x7) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10. obj' \<noteq> IRQNode x10)
 4. \<And>obj_id slot s x5. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (AsidPool x5)\<rbrakk> \<Longrightarrow> \<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3. obj' \<noteq> Tcb x3) \<and> (\<forall>x4. obj' \<noteq> CNode x4) \<and> (\<forall>x5a. obj' = AsidPool x5a \<longrightarrow> object_clean (AsidPool x5) = object_clean (AsidPool x5a) \<and> x5\<lparr>cdl_asid_pool_caps := \<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a\<rparr> = x5a\<lparr>cdl_asid_pool_caps := (object_slots (AsidPool x5a))(slot \<mapsto> cap)\<rparr>) \<and> (\<forall>x6. obj' \<noteq> PageTable x6) \<and> (\<forall>x7. obj' \<noteq> PageDirectory x7) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10. obj' \<noteq> IRQNode x10)
 5. \<And>obj_id slot s x6. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (PageTable x6)\<rbrakk> \<Longrightarrow> \<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3. obj' \<noteq> Tcb x3) \<and> (\<forall>x4. obj' \<noteq> CNode x4) \<and> (\<forall>x5. obj' \<noteq> AsidPool x5) \<and> (\<forall>x6a. obj' = PageTable x6a \<longrightarrow> object_clean (PageTable x6) = object_clean (PageTable x6a) \<and> x6\<lparr>cdl_page_table_caps := \<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a\<rparr> = x6a\<lparr>cdl_page_table_caps := (object_slots (PageTable x6a))(slot \<mapsto> cap)\<rparr>) \<and> (\<forall>x7. obj' \<noteq> PageDirectory x7) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10. obj' \<noteq> IRQNode x10)
 6. \<And>obj_id slot s x7. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (PageDirectory x7)\<rbrakk> \<Longrightarrow> \<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3. obj' \<noteq> Tcb x3) \<and> (\<forall>x4. obj' \<noteq> CNode x4) \<and> (\<forall>x5. obj' \<noteq> AsidPool x5) \<and> (\<forall>x6. obj' \<noteq> PageTable x6) \<and> (\<forall>x7a. obj' = PageDirectory x7a \<longrightarrow> object_clean (PageDirectory x7) = object_clean (PageDirectory x7a) \<and> x7\<lparr>cdl_page_directory_caps := \<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a\<rparr> = x7a\<lparr>cdl_page_directory_caps := (object_slots (PageDirectory x7a))(slot \<mapsto> cap)\<rparr>) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10. obj' \<noteq> IRQNode x10)
 7. \<And>obj_id slot s x10. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (IRQNode x10)\<rbrakk> \<Longrightarrow> \<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3. obj' \<noteq> Tcb x3) \<and> (\<forall>x4. obj' \<noteq> CNode x4) \<and> (\<forall>x5. obj' \<noteq> AsidPool x5) \<and> (\<forall>x6. obj' \<noteq> PageTable x6) \<and> (\<forall>x7. obj' \<noteq> PageDirectory x7) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10a. obj' = IRQNode x10a \<longrightarrow> object_clean (IRQNode x10) = object_clean (IRQNode x10a) \<and> x10\<lparr>cdl_irq_node_caps := \<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a\<rparr> = x10a\<lparr>cdl_irq_node_caps := (object_slots (IRQNode x10a))(slot \<mapsto> cap)\<rparr>) proof (prove)
goal (6 subgoals):
 1. \<And>obj_id slot s tcb. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcb)\<rbrakk> \<Longrightarrow> (slot = tcb_ipcbuffer_slot \<longrightarrow> object_slots (Tcb tcb) tcb_ipcbuffer_slot = Some cap) \<longrightarrow> (\<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3. obj' = Tcb x3 \<longrightarrow> object_clean (Tcb tcb) = object_clean (Tcb x3) \<and> tcb\<lparr>cdl_tcb_caps := \<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a\<rparr> = x3\<lparr>cdl_tcb_caps := (object_slots (Tcb x3))(slot \<mapsto> cap)\<rparr>) \<and> (\<forall>x4. obj' \<noteq> CNode x4) \<and> (\<forall>x5. obj' \<noteq> AsidPool x5) \<and> (\<forall>x6. obj' \<noteq> PageTable x6) \<and> (\<forall>x7. obj' \<noteq> PageDirectory x7) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10. obj' \<noteq> IRQNode x10))
 2. \<And>obj_id slot s x4. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (CNode x4)\<rbrakk> \<Longrightarrow> \<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3. obj' \<noteq> Tcb x3) \<and> (\<forall>x4a. obj' = CNode x4a \<longrightarrow> object_clean (CNode x4) = object_clean (CNode x4a) \<and> x4\<lparr>cdl_cnode_caps := \<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a\<rparr> = x4a\<lparr>cdl_cnode_caps := (object_slots (CNode x4a))(slot \<mapsto> cap)\<rparr>) \<and> (\<forall>x5. obj' \<noteq> AsidPool x5) \<and> (\<forall>x6. obj' \<noteq> PageTable x6) \<and> (\<forall>x7. obj' \<noteq> PageDirectory x7) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10. obj' \<noteq> IRQNode x10)
 3. \<And>obj_id slot s x5. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (AsidPool x5)\<rbrakk> \<Longrightarrow> \<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3. obj' \<noteq> Tcb x3) \<and> (\<forall>x4. obj' \<noteq> CNode x4) \<and> (\<forall>x5a. obj' = AsidPool x5a \<longrightarrow> object_clean (AsidPool x5) = object_clean (AsidPool x5a) \<and> x5\<lparr>cdl_asid_pool_caps := \<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a\<rparr> = x5a\<lparr>cdl_asid_pool_caps := (object_slots (AsidPool x5a))(slot \<mapsto> cap)\<rparr>) \<and> (\<forall>x6. obj' \<noteq> PageTable x6) \<and> (\<forall>x7. obj' \<noteq> PageDirectory x7) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10. obj' \<noteq> IRQNode x10)
 4. \<And>obj_id slot s x6. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (PageTable x6)\<rbrakk> \<Longrightarrow> \<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3. obj' \<noteq> Tcb x3) \<and> (\<forall>x4. obj' \<noteq> CNode x4) \<and> (\<forall>x5. obj' \<noteq> AsidPool x5) \<and> (\<forall>x6a. obj' = PageTable x6a \<longrightarrow> object_clean (PageTable x6) = object_clean (PageTable x6a) \<and> x6\<lparr>cdl_page_table_caps := \<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a\<rparr> = x6a\<lparr>cdl_page_table_caps := (object_slots (PageTable x6a))(slot \<mapsto> cap)\<rparr>) \<and> (\<forall>x7. obj' \<noteq> PageDirectory x7) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10. obj' \<noteq> IRQNode x10)
 5. \<And>obj_id slot s x7. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (PageDirectory x7)\<rbrakk> \<Longrightarrow> \<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3. obj' \<noteq> Tcb x3) \<and> (\<forall>x4. obj' \<noteq> CNode x4) \<and> (\<forall>x5. obj' \<noteq> AsidPool x5) \<and> (\<forall>x6. obj' \<noteq> PageTable x6) \<and> (\<forall>x7a. obj' = PageDirectory x7a \<longrightarrow> object_clean (PageDirectory x7) = object_clean (PageDirectory x7a) \<and> x7\<lparr>cdl_page_directory_caps := \<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a\<rparr> = x7a\<lparr>cdl_page_directory_caps := (object_slots (PageDirectory x7a))(slot \<mapsto> cap)\<rparr>) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10. obj' \<noteq> IRQNode x10)
 6. \<And>obj_id slot s x10. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (IRQNode x10)\<rbrakk> \<Longrightarrow> \<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3. obj' \<noteq> Tcb x3) \<and> (\<forall>x4. obj' \<noteq> CNode x4) \<and> (\<forall>x5. obj' \<noteq> AsidPool x5) \<and> (\<forall>x6. obj' \<noteq> PageTable x6) \<and> (\<forall>x7. obj' \<noteq> PageDirectory x7) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10a. obj' = IRQNode x10a \<longrightarrow> object_clean (IRQNode x10) = object_clean (IRQNode x10a) \<and> x10\<lparr>cdl_irq_node_caps := \<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a\<rparr> = x10a\<lparr>cdl_irq_node_caps := (object_slots (IRQNode x10a))(slot \<mapsto> cap)\<rparr>) proof (prove)
goal (6 subgoals):
 1. \<And>obj_id slot s tcb. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcb); slot = tcb_ipcbuffer_slot \<longrightarrow> object_slots (Tcb tcb) tcb_ipcbuffer_slot = Some cap\<rbrakk> \<Longrightarrow> \<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3. obj' = Tcb x3 \<longrightarrow> object_clean (Tcb tcb) = object_clean (Tcb x3) \<and> tcb\<lparr>cdl_tcb_caps := \<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a\<rparr> = x3\<lparr>cdl_tcb_caps := (object_slots (Tcb x3))(slot \<mapsto> cap)\<rparr>) \<and> (\<forall>x4. obj' \<noteq> CNode x4) \<and> (\<forall>x5. obj' \<noteq> AsidPool x5) \<and> (\<forall>x6. obj' \<noteq> PageTable x6) \<and> (\<forall>x7. obj' \<noteq> PageDirectory x7) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10. obj' \<noteq> IRQNode x10)
 2. \<And>obj_id slot s x4. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (CNode x4)\<rbrakk> \<Longrightarrow> \<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3. obj' \<noteq> Tcb x3) \<and> (\<forall>x4a. obj' = CNode x4a \<longrightarrow> object_clean (CNode x4) = object_clean (CNode x4a) \<and> x4\<lparr>cdl_cnode_caps := \<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a\<rparr> = x4a\<lparr>cdl_cnode_caps := (object_slots (CNode x4a))(slot \<mapsto> cap)\<rparr>) \<and> (\<forall>x5. obj' \<noteq> AsidPool x5) \<and> (\<forall>x6. obj' \<noteq> PageTable x6) \<and> (\<forall>x7. obj' \<noteq> PageDirectory x7) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10. obj' \<noteq> IRQNode x10)
 3. \<And>obj_id slot s x5. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (AsidPool x5)\<rbrakk> \<Longrightarrow> \<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3. obj' \<noteq> Tcb x3) \<and> (\<forall>x4. obj' \<noteq> CNode x4) \<and> (\<forall>x5a. obj' = AsidPool x5a \<longrightarrow> object_clean (AsidPool x5) = object_clean (AsidPool x5a) \<and> x5\<lparr>cdl_asid_pool_caps := \<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a\<rparr> = x5a\<lparr>cdl_asid_pool_caps := (object_slots (AsidPool x5a))(slot \<mapsto> cap)\<rparr>) \<and> (\<forall>x6. obj' \<noteq> PageTable x6) \<and> (\<forall>x7. obj' \<noteq> PageDirectory x7) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10. obj' \<noteq> IRQNode x10)
 4. \<And>obj_id slot s x6. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (PageTable x6)\<rbrakk> \<Longrightarrow> \<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3. obj' \<noteq> Tcb x3) \<and> (\<forall>x4. obj' \<noteq> CNode x4) \<and> (\<forall>x5. obj' \<noteq> AsidPool x5) \<and> (\<forall>x6a. obj' = PageTable x6a \<longrightarrow> object_clean (PageTable x6) = object_clean (PageTable x6a) \<and> x6\<lparr>cdl_page_table_caps := \<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a\<rparr> = x6a\<lparr>cdl_page_table_caps := (object_slots (PageTable x6a))(slot \<mapsto> cap)\<rparr>) \<and> (\<forall>x7. obj' \<noteq> PageDirectory x7) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10. obj' \<noteq> IRQNode x10)
 5. \<And>obj_id slot s x7. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (PageDirectory x7)\<rbrakk> \<Longrightarrow> \<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3. obj' \<noteq> Tcb x3) \<and> (\<forall>x4. obj' \<noteq> CNode x4) \<and> (\<forall>x5. obj' \<noteq> AsidPool x5) \<and> (\<forall>x6. obj' \<noteq> PageTable x6) \<and> (\<forall>x7a. obj' = PageDirectory x7a \<longrightarrow> object_clean (PageDirectory x7) = object_clean (PageDirectory x7a) \<and> x7\<lparr>cdl_page_directory_caps := \<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a\<rparr> = x7a\<lparr>cdl_page_directory_caps := (object_slots (PageDirectory x7a))(slot \<mapsto> cap)\<rparr>) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10. obj' \<noteq> IRQNode x10)
 6. \<And>obj_id slot s x10. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (IRQNode x10)\<rbrakk> \<Longrightarrow> \<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3. obj' \<noteq> Tcb x3) \<and> (\<forall>x4. obj' \<noteq> CNode x4) \<and> (\<forall>x5. obj' \<noteq> AsidPool x5) \<and> (\<forall>x6. obj' \<noteq> PageTable x6) \<and> (\<forall>x7. obj' \<noteq> PageDirectory x7) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10a. obj' = IRQNode x10a \<longrightarrow> object_clean (IRQNode x10) = object_clean (IRQNode x10a) \<and> x10\<lparr>cdl_irq_node_caps := \<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a\<rparr> = x10a\<lparr>cdl_irq_node_caps := (object_slots (IRQNode x10a))(slot \<mapsto> cap)\<rparr>) proof (prove)
goal (6 subgoals):
 1. \<And>obj_id slot s tcb. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (Tcb tcb); slot = tcb_ipcbuffer_slot \<longrightarrow> object_slots (Tcb tcb) tcb_ipcbuffer_slot = Some cap\<rbrakk> \<Longrightarrow> Tcb tcb \<noteq> Endpoint \<and> Tcb tcb \<noteq> Notification \<and> (\<forall>x3. Tcb tcb = Tcb x3 \<longrightarrow> object_clean (Tcb tcb) = object_clean (Tcb x3) \<and> tcb\<lparr>cdl_tcb_caps := \<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a\<rparr> = x3\<lparr>cdl_tcb_caps := (object_slots (Tcb x3))(slot \<mapsto> cap)\<rparr>) \<and> (\<forall>x4. Tcb tcb \<noteq> CNode x4) \<and> (\<forall>x5. Tcb tcb \<noteq> AsidPool x5) \<and> (\<forall>x6. Tcb tcb \<noteq> PageTable x6) \<and> (\<forall>x7. Tcb tcb \<noteq> PageDirectory x7) \<and> (\<forall>x8. Tcb tcb \<noteq> Frame x8) \<and> Tcb tcb \<noteq> Untyped \<and> (\<forall>x10. Tcb tcb \<noteq> IRQNode x10)
 2. \<And>obj_id slot s x4. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (CNode x4)\<rbrakk> \<Longrightarrow> \<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3. obj' \<noteq> Tcb x3) \<and> (\<forall>x4a. obj' = CNode x4a \<longrightarrow> object_clean (CNode x4) = object_clean (CNode x4a) \<and> x4\<lparr>cdl_cnode_caps := \<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a\<rparr> = x4a\<lparr>cdl_cnode_caps := (object_slots (CNode x4a))(slot \<mapsto> cap)\<rparr>) \<and> (\<forall>x5. obj' \<noteq> AsidPool x5) \<and> (\<forall>x6. obj' \<noteq> PageTable x6) \<and> (\<forall>x7. obj' \<noteq> PageDirectory x7) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10. obj' \<noteq> IRQNode x10)
 3. \<And>obj_id slot s x5. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (AsidPool x5)\<rbrakk> \<Longrightarrow> \<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3. obj' \<noteq> Tcb x3) \<and> (\<forall>x4. obj' \<noteq> CNode x4) \<and> (\<forall>x5a. obj' = AsidPool x5a \<longrightarrow> object_clean (AsidPool x5) = object_clean (AsidPool x5a) \<and> x5\<lparr>cdl_asid_pool_caps := \<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a\<rparr> = x5a\<lparr>cdl_asid_pool_caps := (object_slots (AsidPool x5a))(slot \<mapsto> cap)\<rparr>) \<and> (\<forall>x6. obj' \<noteq> PageTable x6) \<and> (\<forall>x7. obj' \<noteq> PageDirectory x7) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10. obj' \<noteq> IRQNode x10)
 4. \<And>obj_id slot s x6. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (PageTable x6)\<rbrakk> \<Longrightarrow> \<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3. obj' \<noteq> Tcb x3) \<and> (\<forall>x4. obj' \<noteq> CNode x4) \<and> (\<forall>x5. obj' \<noteq> AsidPool x5) \<and> (\<forall>x6a. obj' = PageTable x6a \<longrightarrow> object_clean (PageTable x6) = object_clean (PageTable x6a) \<and> x6\<lparr>cdl_page_table_caps := \<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a\<rparr> = x6a\<lparr>cdl_page_table_caps := (object_slots (PageTable x6a))(slot \<mapsto> cap)\<rparr>) \<and> (\<forall>x7. obj' \<noteq> PageDirectory x7) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10. obj' \<noteq> IRQNode x10)
 5. \<And>obj_id slot s x7. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (PageDirectory x7)\<rbrakk> \<Longrightarrow> \<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3. obj' \<noteq> Tcb x3) \<and> (\<forall>x4. obj' \<noteq> CNode x4) \<and> (\<forall>x5. obj' \<noteq> AsidPool x5) \<and> (\<forall>x6. obj' \<noteq> PageTable x6) \<and> (\<forall>x7a. obj' = PageDirectory x7a \<longrightarrow> object_clean (PageDirectory x7) = object_clean (PageDirectory x7a) \<and> x7\<lparr>cdl_page_directory_caps := \<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a\<rparr> = x7a\<lparr>cdl_page_directory_caps := (object_slots (PageDirectory x7a))(slot \<mapsto> cap)\<rparr>) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10. obj' \<noteq> IRQNode x10)
 6. \<And>obj_id slot s x10. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (IRQNode x10)\<rbrakk> \<Longrightarrow> \<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3. obj' \<noteq> Tcb x3) \<and> (\<forall>x4. obj' \<noteq> CNode x4) \<and> (\<forall>x5. obj' \<noteq> AsidPool x5) \<and> (\<forall>x6. obj' \<noteq> PageTable x6) \<and> (\<forall>x7. obj' \<noteq> PageDirectory x7) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10a. obj' = IRQNode x10a \<longrightarrow> object_clean (IRQNode x10) = object_clean (IRQNode x10a) \<and> x10\<lparr>cdl_irq_node_caps := \<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a\<rparr> = x10a\<lparr>cdl_irq_node_caps := (object_slots (IRQNode x10a))(slot \<mapsto> cap)\<rparr>) proof (prove)
goal (5 subgoals):
 1. \<And>obj_id slot s x4. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (CNode x4)\<rbrakk> \<Longrightarrow> \<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3. obj' \<noteq> Tcb x3) \<and> (\<forall>x4a. obj' = CNode x4a \<longrightarrow> object_clean (CNode x4) = object_clean (CNode x4a) \<and> x4\<lparr>cdl_cnode_caps := \<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a\<rparr> = x4a\<lparr>cdl_cnode_caps := (object_slots (CNode x4a))(slot \<mapsto> cap)\<rparr>) \<and> (\<forall>x5. obj' \<noteq> AsidPool x5) \<and> (\<forall>x6. obj' \<noteq> PageTable x6) \<and> (\<forall>x7. obj' \<noteq> PageDirectory x7) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10. obj' \<noteq> IRQNode x10)
 2. \<And>obj_id slot s x5. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (AsidPool x5)\<rbrakk> \<Longrightarrow> \<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3. obj' \<noteq> Tcb x3) \<and> (\<forall>x4. obj' \<noteq> CNode x4) \<and> (\<forall>x5a. obj' = AsidPool x5a \<longrightarrow> object_clean (AsidPool x5) = object_clean (AsidPool x5a) \<and> x5\<lparr>cdl_asid_pool_caps := \<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a\<rparr> = x5a\<lparr>cdl_asid_pool_caps := (object_slots (AsidPool x5a))(slot \<mapsto> cap)\<rparr>) \<and> (\<forall>x6. obj' \<noteq> PageTable x6) \<and> (\<forall>x7. obj' \<noteq> PageDirectory x7) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10. obj' \<noteq> IRQNode x10)
 3. \<And>obj_id slot s x6. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (PageTable x6)\<rbrakk> \<Longrightarrow> \<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3. obj' \<noteq> Tcb x3) \<and> (\<forall>x4. obj' \<noteq> CNode x4) \<and> (\<forall>x5. obj' \<noteq> AsidPool x5) \<and> (\<forall>x6a. obj' = PageTable x6a \<longrightarrow> object_clean (PageTable x6) = object_clean (PageTable x6a) \<and> x6\<lparr>cdl_page_table_caps := \<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a\<rparr> = x6a\<lparr>cdl_page_table_caps := (object_slots (PageTable x6a))(slot \<mapsto> cap)\<rparr>) \<and> (\<forall>x7. obj' \<noteq> PageDirectory x7) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10. obj' \<noteq> IRQNode x10)
 4. \<And>obj_id slot s x7. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (PageDirectory x7)\<rbrakk> \<Longrightarrow> \<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3. obj' \<noteq> Tcb x3) \<and> (\<forall>x4. obj' \<noteq> CNode x4) \<and> (\<forall>x5. obj' \<noteq> AsidPool x5) \<and> (\<forall>x6. obj' \<noteq> PageTable x6) \<and> (\<forall>x7a. obj' = PageDirectory x7a \<longrightarrow> object_clean (PageDirectory x7) = object_clean (PageDirectory x7a) \<and> x7\<lparr>cdl_page_directory_caps := \<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a\<rparr> = x7a\<lparr>cdl_page_directory_caps := (object_slots (PageDirectory x7a))(slot \<mapsto> cap)\<rparr>) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10. obj' \<noteq> IRQNode x10)
 5. \<And>obj_id slot s x10. \<lbrakk>ptr = (obj_id, slot); cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some (IRQNode x10)\<rbrakk> \<Longrightarrow> \<exists>obj'. obj' \<noteq> Endpoint \<and> obj' \<noteq> Notification \<and> (\<forall>x3. obj' \<noteq> Tcb x3) \<and> (\<forall>x4. obj' \<noteq> CNode x4) \<and> (\<forall>x5. obj' \<noteq> AsidPool x5) \<and> (\<forall>x6. obj' \<noteq> PageTable x6) \<and> (\<forall>x7. obj' \<noteq> PageDirectory x7) \<and> (\<forall>x8. obj' \<noteq> Frame x8) \<and> obj' \<noteq> Untyped \<and> (\<forall>x10a. obj' = IRQNode x10a \<longrightarrow> object_clean (IRQNode x10) = object_clean (IRQNode x10a) \<and> x10\<lparr>cdl_irq_node_caps := \<lambda>a. if a = slot then Some cap else object_slots (the (cdl_objects s obj_id)) a\<rparr> = x10a\<lparr>cdl_irq_node_caps := (object_slots (IRQNode x10a))(slot \<mapsto> cap)\<rparr>) proof (prove)
goal:
No subgoals!