theory Retype_DP

lemma set_cap_no_pending[wp]:
  "snd slot = tcb_pending_op_slot \<longrightarrow> \<not> is_pending_cap cap \<Longrightarrow>
  \<lbrace>no_pending\<rbrace> set_cap slot cap \<lbrace>\<lambda>rv s. no_pending s\<rbrace>" apply (simp add: set_cap_def) apply (cases slot, simp) apply (wp set_object_no_pending | wpc | simp add: no_pending_def)+ apply (drule_tac x = a in spec) apply (rule conjI) apply (clarsimp simp: tcb_pending_op_slot_def tcb_ipcbuffer_slot_def) apply clarsimp apply (intro conjI impI allI) apply (clarsimp simp: opt_cap_def slots_of_def)+ apply (case_tac y, (fastforce simp: object_slots_def update_slots_def)+) apply (clarsimp simp: opt_cap_def slots_of_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. snd slot = tcb_pending_op_slot \<longrightarrow> \<not> is_pending_cap cap \<Longrightarrow> \<lbrace>no_pending\<rbrace> set_cap slot cap \<lbrace>\<lambda>rv. no_pending\<rbrace> proof (prove)
goal (1 subgoal):
 1. snd slot = tcb_pending_op_slot \<longrightarrow> \<not> is_pending_cap cap \<Longrightarrow> \<lbrace>no_pending\<rbrace> (case slot 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. no_pending\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>b = tcb_pending_op_slot \<longrightarrow> \<not> is_pending_cap cap; slot = (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>no_pending\<rbrace> do obj <- get_object a;
y <- assert (has_slots obj);
(case update_slots ((object_slots obj)(b \<mapsto> cap)) obj of Tcb t \<Rightarrow> if b = tcb_ipcbuffer_slot \<and> object_slots obj b \<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)(b \<mapsto> cap)) obj) | _ \<Rightarrow> return (update_slots ((object_slots obj)(b \<mapsto> cap)) obj)) >>= set_object a
od \<lbrace>\<lambda>rv. no_pending\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a b s. \<lbrakk>b = tcb_pending_op_slot \<longrightarrow> \<not> is_pending_cap cap; slot = (a, b); \<forall>oid cap. opt_cap (oid, tcb_pending_op_slot) s = Some cap \<longrightarrow> \<not> is_pending_cap cap\<rbrakk> \<Longrightarrow> (tcb_pending_op_slot = b \<longrightarrow> (\<exists>y. cdl_objects s a = Some y) \<longrightarrow> has_slots (the (cdl_objects s a)) \<longrightarrow> (\<forall>x. update_slots ((object_slots (the (cdl_objects s a)))(tcb_pending_op_slot \<mapsto> cap)) (the (cdl_objects s a)) = Tcb x \<longrightarrow> tcb_pending_op_slot = tcb_ipcbuffer_slot \<and> object_slots (the (cdl_objects s a)) tcb_pending_op_slot \<noteq> Some cap \<longrightarrow> (\<forall>cap. object_slots (Tcb x) tcb_ipcbuffer_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap))) \<and> (tcb_pending_op_slot \<noteq> b \<longrightarrow> (\<exists>y. cdl_objects s a = Some y) \<longrightarrow> has_slots (the (cdl_objects s a)) \<longrightarrow> (update_slots ((object_slots (the (cdl_objects s a)))(b \<mapsto> cap)) (the (cdl_objects s a)) = Endpoint \<longrightarrow> (\<forall>cap. object_slots (the (cdl_objects s a)) tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap)) \<and> (update_slots ((object_slots (the (cdl_objects s a)))(b \<mapsto> cap)) (the (cdl_objects s a)) = Notification \<longrightarrow> (\<forall>cap. object_slots (the (cdl_objects s a)) tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap)) \<and> (\<forall>x. update_slots ((object_slots (the (cdl_objects s a)))(b \<mapsto> cap)) (the (cdl_objects s a)) = Tcb x \<longrightarrow> (b = tcb_ipcbuffer_slot \<and> object_slots (the (cdl_objects s a)) b \<noteq> Some cap \<longrightarrow> (\<forall>cap. object_slots (Tcb x) tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap)) \<and> ((b = tcb_ipcbuffer_slot \<longrightarrow> object_slots (the (cdl_objects s a)) tcb_ipcbuffer_slot = Some cap) \<longrightarrow> (\<forall>cap. object_slots (the (cdl_objects s a)) tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap))) \<and> ((\<exists>x. update_slots ((object_slots (the (cdl_objects s a)))(b \<mapsto> cap)) (the (cdl_objects s a)) = CNode x) \<longrightarrow> (\<forall>cap. object_slots (the (cdl_objects s a)) tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap)) \<and> ((\<exists>x. update_slots ((object_slots (the (cdl_objects s a)))(b \<mapsto> cap)) (the (cdl_objects s a)) = AsidPool x) \<longrightarrow> (\<forall>cap. object_slots (the (cdl_objects s a)) tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap)) \<and> ((\<exists>x. update_slots ((object_slots (the (cdl_objects s a)))(b \<mapsto> cap)) (the (cdl_objects s a)) = PageTable x) \<longrightarrow> (\<forall>cap. object_slots (the (cdl_objects s a)) tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap)) \<and> ((\<exists>x. update_slots ((object_slots (the (cdl_objects s a)))(b \<mapsto> cap)) (the (cdl_objects s a)) = PageDirectory x) \<longrightarrow> (\<forall>cap. object_slots (the (cdl_objects s a)) tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap)) \<and> ((\<exists>x. update_slots ((object_slots (the (cdl_objects s a)))(b \<mapsto> cap)) (the (cdl_objects s a)) = Frame x) \<longrightarrow> (\<forall>cap. object_slots (the (cdl_objects s a)) tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap)) \<and> (update_slots ((object_slots (the (cdl_objects s a)))(b \<mapsto> cap)) (the (cdl_objects s a)) = Untyped \<longrightarrow> (\<forall>cap. object_slots (the (cdl_objects s a)) tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap)) \<and> ((\<exists>x. update_slots ((object_slots (the (cdl_objects s a)))(b \<mapsto> cap)) (the (cdl_objects s a)) = IRQNode x) \<longrightarrow> (\<forall>cap. object_slots (the (cdl_objects s a)) tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap))) proof (prove)
goal (1 subgoal):
 1. \<And>a b s. \<lbrakk>b = tcb_pending_op_slot \<longrightarrow> \<not> is_pending_cap cap; slot = (a, b); \<forall>cap. opt_cap (a, tcb_pending_op_slot) s = Some cap \<longrightarrow> \<not> is_pending_cap cap\<rbrakk> \<Longrightarrow> (tcb_pending_op_slot = b \<longrightarrow> (\<exists>y. cdl_objects s a = Some y) \<longrightarrow> has_slots (the (cdl_objects s a)) \<longrightarrow> (\<forall>x. update_slots ((object_slots (the (cdl_objects s a)))(tcb_pending_op_slot \<mapsto> cap)) (the (cdl_objects s a)) = Tcb x \<longrightarrow> tcb_pending_op_slot = tcb_ipcbuffer_slot \<and> object_slots (the (cdl_objects s a)) tcb_pending_op_slot \<noteq> Some cap \<longrightarrow> (\<forall>cap. object_slots (Tcb x) tcb_ipcbuffer_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap))) \<and> (tcb_pending_op_slot \<noteq> b \<longrightarrow> (\<exists>y. cdl_objects s a = Some y) \<longrightarrow> has_slots (the (cdl_objects s a)) \<longrightarrow> (update_slots ((object_slots (the (cdl_objects s a)))(b \<mapsto> cap)) (the (cdl_objects s a)) = Endpoint \<longrightarrow> (\<forall>cap. object_slots (the (cdl_objects s a)) tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap)) \<and> (update_slots ((object_slots (the (cdl_objects s a)))(b \<mapsto> cap)) (the (cdl_objects s a)) = Notification \<longrightarrow> (\<forall>cap. object_slots (the (cdl_objects s a)) tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap)) \<and> (\<forall>x. update_slots ((object_slots (the (cdl_objects s a)))(b \<mapsto> cap)) (the (cdl_objects s a)) = Tcb x \<longrightarrow> (b = tcb_ipcbuffer_slot \<and> object_slots (the (cdl_objects s a)) b \<noteq> Some cap \<longrightarrow> (\<forall>cap. object_slots (Tcb x) tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap)) \<and> ((b = tcb_ipcbuffer_slot \<longrightarrow> object_slots (the (cdl_objects s a)) tcb_ipcbuffer_slot = Some cap) \<longrightarrow> (\<forall>cap. object_slots (the (cdl_objects s a)) tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap))) \<and> ((\<exists>x. update_slots ((object_slots (the (cdl_objects s a)))(b \<mapsto> cap)) (the (cdl_objects s a)) = CNode x) \<longrightarrow> (\<forall>cap. object_slots (the (cdl_objects s a)) tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap)) \<and> ((\<exists>x. update_slots ((object_slots (the (cdl_objects s a)))(b \<mapsto> cap)) (the (cdl_objects s a)) = AsidPool x) \<longrightarrow> (\<forall>cap. object_slots (the (cdl_objects s a)) tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap)) \<and> ((\<exists>x. update_slots ((object_slots (the (cdl_objects s a)))(b \<mapsto> cap)) (the (cdl_objects s a)) = PageTable x) \<longrightarrow> (\<forall>cap. object_slots (the (cdl_objects s a)) tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap)) \<and> ((\<exists>x. update_slots ((object_slots (the (cdl_objects s a)))(b \<mapsto> cap)) (the (cdl_objects s a)) = PageDirectory x) \<longrightarrow> (\<forall>cap. object_slots (the (cdl_objects s a)) tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap)) \<and> ((\<exists>x. update_slots ((object_slots (the (cdl_objects s a)))(b \<mapsto> cap)) (the (cdl_objects s a)) = Frame x) \<longrightarrow> (\<forall>cap. object_slots (the (cdl_objects s a)) tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap)) \<and> (update_slots ((object_slots (the (cdl_objects s a)))(b \<mapsto> cap)) (the (cdl_objects s a)) = Untyped \<longrightarrow> (\<forall>cap. object_slots (the (cdl_objects s a)) tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap)) \<and> ((\<exists>x. update_slots ((object_slots (the (cdl_objects s a)))(b \<mapsto> cap)) (the (cdl_objects s a)) = IRQNode x) \<longrightarrow> (\<forall>cap. object_slots (the (cdl_objects s a)) tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap))) proof (prove)
goal (2 subgoals):
 1. \<And>a b s. \<lbrakk>b = tcb_pending_op_slot \<longrightarrow> \<not> is_pending_cap cap; slot = (a, b); \<forall>cap. opt_cap (a, tcb_pending_op_slot) s = Some cap \<longrightarrow> \<not> is_pending_cap cap\<rbrakk> \<Longrightarrow> tcb_pending_op_slot = b \<longrightarrow> (\<exists>y. cdl_objects s a = Some y) \<longrightarrow> has_slots (the (cdl_objects s a)) \<longrightarrow> (\<forall>x. update_slots ((object_slots (the (cdl_objects s a)))(tcb_pending_op_slot \<mapsto> cap)) (the (cdl_objects s a)) = Tcb x \<longrightarrow> tcb_pending_op_slot = tcb_ipcbuffer_slot \<and> object_slots (the (cdl_objects s a)) tcb_pending_op_slot \<noteq> Some cap \<longrightarrow> (\<forall>cap. object_slots (Tcb x) tcb_ipcbuffer_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap))
 2. \<And>a b s. \<lbrakk>b = tcb_pending_op_slot \<longrightarrow> \<not> is_pending_cap cap; slot = (a, b); \<forall>cap. opt_cap (a, tcb_pending_op_slot) s = Some cap \<longrightarrow> \<not> is_pending_cap cap\<rbrakk> \<Longrightarrow> tcb_pending_op_slot \<noteq> b \<longrightarrow> (\<exists>y. cdl_objects s a = Some y) \<longrightarrow> has_slots (the (cdl_objects s a)) \<longrightarrow> (update_slots ((object_slots (the (cdl_objects s a)))(b \<mapsto> cap)) (the (cdl_objects s a)) = Endpoint \<longrightarrow> (\<forall>cap. object_slots (the (cdl_objects s a)) tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap)) \<and> (update_slots ((object_slots (the (cdl_objects s a)))(b \<mapsto> cap)) (the (cdl_objects s a)) = Notification \<longrightarrow> (\<forall>cap. object_slots (the (cdl_objects s a)) tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap)) \<and> (\<forall>x. update_slots ((object_slots (the (cdl_objects s a)))(b \<mapsto> cap)) (the (cdl_objects s a)) = Tcb x \<longrightarrow> (b = tcb_ipcbuffer_slot \<and> object_slots (the (cdl_objects s a)) b \<noteq> Some cap \<longrightarrow> (\<forall>cap. object_slots (Tcb x) tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap)) \<and> ((b = tcb_ipcbuffer_slot \<longrightarrow> object_slots (the (cdl_objects s a)) tcb_ipcbuffer_slot = Some cap) \<longrightarrow> (\<forall>cap. object_slots (the (cdl_objects s a)) tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap))) \<and> ((\<exists>x. update_slots ((object_slots (the (cdl_objects s a)))(b \<mapsto> cap)) (the (cdl_objects s a)) = CNode x) \<longrightarrow> (\<forall>cap. object_slots (the (cdl_objects s a)) tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap)) \<and> ((\<exists>x. update_slots ((object_slots (the (cdl_objects s a)))(b \<mapsto> cap)) (the (cdl_objects s a)) = AsidPool x) \<longrightarrow> (\<forall>cap. object_slots (the (cdl_objects s a)) tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap)) \<and> ((\<exists>x. update_slots ((object_slots (the (cdl_objects s a)))(b \<mapsto> cap)) (the (cdl_objects s a)) = PageTable x) \<longrightarrow> (\<forall>cap. object_slots (the (cdl_objects s a)) tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap)) \<and> ((\<exists>x. update_slots ((object_slots (the (cdl_objects s a)))(b \<mapsto> cap)) (the (cdl_objects s a)) = PageDirectory x) \<longrightarrow> (\<forall>cap. object_slots (the (cdl_objects s a)) tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap)) \<and> ((\<exists>x. update_slots ((object_slots (the (cdl_objects s a)))(b \<mapsto> cap)) (the (cdl_objects s a)) = Frame x) \<longrightarrow> (\<forall>cap. object_slots (the (cdl_objects s a)) tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap)) \<and> (update_slots ((object_slots (the (cdl_objects s a)))(b \<mapsto> cap)) (the (cdl_objects s a)) = Untyped \<longrightarrow> (\<forall>cap. object_slots (the (cdl_objects s a)) tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap)) \<and> ((\<exists>x. update_slots ((object_slots (the (cdl_objects s a)))(b \<mapsto> cap)) (the (cdl_objects s a)) = IRQNode x) \<longrightarrow> (\<forall>cap. object_slots (the (cdl_objects s a)) tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap)) proof (prove)
goal (1 subgoal):
 1. \<And>a b s. \<lbrakk>b = tcb_pending_op_slot \<longrightarrow> \<not> is_pending_cap cap; slot = (a, b); \<forall>cap. opt_cap (a, tcb_pending_op_slot) s = Some cap \<longrightarrow> \<not> is_pending_cap cap\<rbrakk> \<Longrightarrow> tcb_pending_op_slot \<noteq> b \<longrightarrow> (\<exists>y. cdl_objects s a = Some y) \<longrightarrow> has_slots (the (cdl_objects s a)) \<longrightarrow> (update_slots ((object_slots (the (cdl_objects s a)))(b \<mapsto> cap)) (the (cdl_objects s a)) = Endpoint \<longrightarrow> (\<forall>cap. object_slots (the (cdl_objects s a)) tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap)) \<and> (update_slots ((object_slots (the (cdl_objects s a)))(b \<mapsto> cap)) (the (cdl_objects s a)) = Notification \<longrightarrow> (\<forall>cap. object_slots (the (cdl_objects s a)) tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap)) \<and> (\<forall>x. update_slots ((object_slots (the (cdl_objects s a)))(b \<mapsto> cap)) (the (cdl_objects s a)) = Tcb x \<longrightarrow> (b = tcb_ipcbuffer_slot \<and> object_slots (the (cdl_objects s a)) b \<noteq> Some cap \<longrightarrow> (\<forall>cap. object_slots (Tcb x) tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap)) \<and> ((b = tcb_ipcbuffer_slot \<longrightarrow> object_slots (the (cdl_objects s a)) tcb_ipcbuffer_slot = Some cap) \<longrightarrow> (\<forall>cap. object_slots (the (cdl_objects s a)) tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap))) \<and> ((\<exists>x. update_slots ((object_slots (the (cdl_objects s a)))(b \<mapsto> cap)) (the (cdl_objects s a)) = CNode x) \<longrightarrow> (\<forall>cap. object_slots (the (cdl_objects s a)) tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap)) \<and> ((\<exists>x. update_slots ((object_slots (the (cdl_objects s a)))(b \<mapsto> cap)) (the (cdl_objects s a)) = AsidPool x) \<longrightarrow> (\<forall>cap. object_slots (the (cdl_objects s a)) tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap)) \<and> ((\<exists>x. update_slots ((object_slots (the (cdl_objects s a)))(b \<mapsto> cap)) (the (cdl_objects s a)) = PageTable x) \<longrightarrow> (\<forall>cap. object_slots (the (cdl_objects s a)) tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap)) \<and> ((\<exists>x. update_slots ((object_slots (the (cdl_objects s a)))(b \<mapsto> cap)) (the (cdl_objects s a)) = PageDirectory x) \<longrightarrow> (\<forall>cap. object_slots (the (cdl_objects s a)) tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap)) \<and> ((\<exists>x. update_slots ((object_slots (the (cdl_objects s a)))(b \<mapsto> cap)) (the (cdl_objects s a)) = Frame x) \<longrightarrow> (\<forall>cap. object_slots (the (cdl_objects s a)) tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap)) \<and> (update_slots ((object_slots (the (cdl_objects s a)))(b \<mapsto> cap)) (the (cdl_objects s a)) = Untyped \<longrightarrow> (\<forall>cap. object_slots (the (cdl_objects s a)) tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap)) \<and> ((\<exists>x. update_slots ((object_slots (the (cdl_objects s a)))(b \<mapsto> cap)) (the (cdl_objects s a)) = IRQNode x) \<longrightarrow> (\<forall>cap. object_slots (the (cdl_objects s a)) tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap)) proof (prove)
goal (1 subgoal):
 1. \<And>a b s y. \<lbrakk>slot = (a, b); \<forall>cap. opt_cap (a, tcb_pending_op_slot) s = Some cap \<longrightarrow> \<not> is_pending_cap cap; tcb_pending_op_slot \<noteq> b; cdl_objects s a = Some y; has_slots y\<rbrakk> \<Longrightarrow> (update_slots ((object_slots y)(b \<mapsto> cap)) y = Endpoint \<longrightarrow> (\<forall>cap. object_slots y tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap)) \<and> (update_slots ((object_slots y)(b \<mapsto> cap)) y = Notification \<longrightarrow> (\<forall>cap. object_slots y tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap)) \<and> (\<forall>x. update_slots ((object_slots y)(b \<mapsto> cap)) y = Tcb x \<longrightarrow> (b = tcb_ipcbuffer_slot \<and> object_slots y b \<noteq> Some cap \<longrightarrow> (\<forall>cap. object_slots (Tcb x) tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap)) \<and> ((b = tcb_ipcbuffer_slot \<longrightarrow> object_slots y tcb_ipcbuffer_slot = Some cap) \<longrightarrow> (\<forall>cap. object_slots y tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap))) \<and> ((\<exists>x. update_slots ((object_slots y)(b \<mapsto> cap)) y = CNode x) \<longrightarrow> (\<forall>cap. object_slots y tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap)) \<and> ((\<exists>x. update_slots ((object_slots y)(b \<mapsto> cap)) y = AsidPool x) \<longrightarrow> (\<forall>cap. object_slots y tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap)) \<and> ((\<exists>x. update_slots ((object_slots y)(b \<mapsto> cap)) y = PageTable x) \<longrightarrow> (\<forall>cap. object_slots y tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap)) \<and> ((\<exists>x. update_slots ((object_slots y)(b \<mapsto> cap)) y = PageDirectory x) \<longrightarrow> (\<forall>cap. object_slots y tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap)) \<and> ((\<exists>x. update_slots ((object_slots y)(b \<mapsto> cap)) y = Frame x) \<longrightarrow> (\<forall>cap. object_slots y tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap)) \<and> (update_slots ((object_slots y)(b \<mapsto> cap)) y = Untyped \<longrightarrow> (\<forall>cap. object_slots y tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap)) \<and> ((\<exists>x. update_slots ((object_slots y)(b \<mapsto> cap)) y = IRQNode x) \<longrightarrow> (\<forall>cap. object_slots y tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap)) proof (prove)
goal (11 subgoals):
 1. \<And>a b s y capa. \<lbrakk>slot = (a, b); \<forall>cap. opt_cap (a, tcb_pending_op_slot) s = Some cap \<longrightarrow> \<not> is_pending_cap cap; tcb_pending_op_slot \<noteq> b; cdl_objects s a = Some y; has_slots y; update_slots ((object_slots y)(b \<mapsto> cap)) y = Endpoint; object_slots y tcb_pending_op_slot = Some capa\<rbrakk> \<Longrightarrow> \<not> is_pending_cap capa
 2. \<And>a b s y capa. \<lbrakk>slot = (a, b); \<forall>cap. opt_cap (a, tcb_pending_op_slot) s = Some cap \<longrightarrow> \<not> is_pending_cap cap; tcb_pending_op_slot \<noteq> b; cdl_objects s a = Some y; has_slots y; update_slots ((object_slots y)(b \<mapsto> cap)) y = Notification; object_slots y tcb_pending_op_slot = Some capa\<rbrakk> \<Longrightarrow> \<not> is_pending_cap capa
 3. \<And>a b s y x capa. \<lbrakk>slot = (a, b); \<forall>cap. opt_cap (a, tcb_pending_op_slot) s = Some cap \<longrightarrow> \<not> is_pending_cap cap; tcb_pending_op_slot \<noteq> b; cdl_objects s a = Some y; has_slots y; update_slots ((object_slots y)(b \<mapsto> cap)) y = Tcb x; b = tcb_ipcbuffer_slot \<and> object_slots y b \<noteq> Some cap; object_slots (Tcb x) tcb_pending_op_slot = Some capa\<rbrakk> \<Longrightarrow> \<not> is_pending_cap capa
 4. \<And>a b s y x capa. \<lbrakk>slot = (a, b); \<forall>cap. opt_cap (a, tcb_pending_op_slot) s = Some cap \<longrightarrow> \<not> is_pending_cap cap; tcb_pending_op_slot \<noteq> b; cdl_objects s a = Some y; has_slots y; update_slots ((object_slots y)(b \<mapsto> cap)) y = Tcb x; b = tcb_ipcbuffer_slot \<longrightarrow> object_slots y tcb_ipcbuffer_slot = Some cap; object_slots y tcb_pending_op_slot = Some capa\<rbrakk> \<Longrightarrow> \<not> is_pending_cap capa
 5. \<And>a b s y capa. \<lbrakk>slot = (a, b); \<forall>cap. opt_cap (a, tcb_pending_op_slot) s = Some cap \<longrightarrow> \<not> is_pending_cap cap; tcb_pending_op_slot \<noteq> b; cdl_objects s a = Some y; has_slots y; \<exists>x. update_slots ((object_slots y)(b \<mapsto> cap)) y = CNode x; object_slots y tcb_pending_op_slot = Some capa\<rbrakk> \<Longrightarrow> \<not> is_pending_cap capa
 6. \<And>a b s y capa. \<lbrakk>slot = (a, b); \<forall>cap. opt_cap (a, tcb_pending_op_slot) s = Some cap \<longrightarrow> \<not> is_pending_cap cap; tcb_pending_op_slot \<noteq> b; cdl_objects s a = Some y; has_slots y; \<exists>x. update_slots ((object_slots y)(b \<mapsto> cap)) y = AsidPool x; object_slots y tcb_pending_op_slot = Some capa\<rbrakk> \<Longrightarrow> \<not> is_pending_cap capa
 7. \<And>a b s y capa. \<lbrakk>slot = (a, b); \<forall>cap. opt_cap (a, tcb_pending_op_slot) s = Some cap \<longrightarrow> \<not> is_pending_cap cap; tcb_pending_op_slot \<noteq> b; cdl_objects s a = Some y; has_slots y; \<exists>x. update_slots ((object_slots y)(b \<mapsto> cap)) y = PageTable x; object_slots y tcb_pending_op_slot = Some capa\<rbrakk> \<Longrightarrow> \<not> is_pending_cap capa
 8. \<And>a b s y capa. \<lbrakk>slot = (a, b); \<forall>cap. opt_cap (a, tcb_pending_op_slot) s = Some cap \<longrightarrow> \<not> is_pending_cap cap; tcb_pending_op_slot \<noteq> b; cdl_objects s a = Some y; has_slots y; \<exists>x. update_slots ((object_slots y)(b \<mapsto> cap)) y = PageDirectory x; object_slots y tcb_pending_op_slot = Some capa\<rbrakk> \<Longrightarrow> \<not> is_pending_cap capa
 9. \<And>a b s y capa. \<lbrakk>slot = (a, b); \<forall>cap. opt_cap (a, tcb_pending_op_slot) s = Some cap \<longrightarrow> \<not> is_pending_cap cap; tcb_pending_op_slot \<noteq> b; cdl_objects s a = Some y; has_slots y; \<exists>x. update_slots ((object_slots y)(b \<mapsto> cap)) y = Frame x; object_slots y tcb_pending_op_slot = Some capa\<rbrakk> \<Longrightarrow> \<not> is_pending_cap capa
 10. \<And>a b s y capa. \<lbrakk>slot = (a, b); \<forall>cap. opt_cap (a, tcb_pending_op_slot) s = Some cap \<longrightarrow> \<not> is_pending_cap cap; tcb_pending_op_slot \<noteq> b; cdl_objects s a = Some y; has_slots y; update_slots ((object_slots y)(b \<mapsto> cap)) y = Untyped; object_slots y tcb_pending_op_slot = Some capa\<rbrakk> \<Longrightarrow> \<not> is_pending_cap capa
A total of 11 subgoals... proof (prove)
goal (9 subgoals):
 1. \<And>a s y x capa. \<lbrakk>slot = (a, tcb_ipcbuffer_slot); \<forall>cap. object_slots y tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap; tcb_pending_op_slot \<noteq> tcb_ipcbuffer_slot; cdl_objects s a = Some y; has_slots y; update_slots ((object_slots y)(tcb_ipcbuffer_slot \<mapsto> cap)) y = Tcb x; object_slots y tcb_ipcbuffer_slot \<noteq> Some cap; object_slots (Tcb x) tcb_pending_op_slot = Some capa; is_pending_cap capa\<rbrakk> \<Longrightarrow> False
 2. \<And>a b s y x capa. \<lbrakk>slot = (a, b); \<forall>cap. opt_cap (a, tcb_pending_op_slot) s = Some cap \<longrightarrow> \<not> is_pending_cap cap; tcb_pending_op_slot \<noteq> b; cdl_objects s a = Some y; has_slots y; update_slots ((object_slots y)(b \<mapsto> cap)) y = Tcb x; b = tcb_ipcbuffer_slot \<longrightarrow> object_slots y tcb_ipcbuffer_slot = Some cap; object_slots y tcb_pending_op_slot = Some capa\<rbrakk> \<Longrightarrow> \<not> is_pending_cap capa
 3. \<And>a b s y capa. \<lbrakk>slot = (a, b); \<forall>cap. opt_cap (a, tcb_pending_op_slot) s = Some cap \<longrightarrow> \<not> is_pending_cap cap; tcb_pending_op_slot \<noteq> b; cdl_objects s a = Some y; has_slots y; \<exists>x. update_slots ((object_slots y)(b \<mapsto> cap)) y = CNode x; object_slots y tcb_pending_op_slot = Some capa\<rbrakk> \<Longrightarrow> \<not> is_pending_cap capa
 4. \<And>a b s y capa. \<lbrakk>slot = (a, b); \<forall>cap. opt_cap (a, tcb_pending_op_slot) s = Some cap \<longrightarrow> \<not> is_pending_cap cap; tcb_pending_op_slot \<noteq> b; cdl_objects s a = Some y; has_slots y; \<exists>x. update_slots ((object_slots y)(b \<mapsto> cap)) y = AsidPool x; object_slots y tcb_pending_op_slot = Some capa\<rbrakk> \<Longrightarrow> \<not> is_pending_cap capa
 5. \<And>a b s y capa. \<lbrakk>slot = (a, b); \<forall>cap. opt_cap (a, tcb_pending_op_slot) s = Some cap \<longrightarrow> \<not> is_pending_cap cap; tcb_pending_op_slot \<noteq> b; cdl_objects s a = Some y; has_slots y; \<exists>x. update_slots ((object_slots y)(b \<mapsto> cap)) y = PageTable x; object_slots y tcb_pending_op_slot = Some capa\<rbrakk> \<Longrightarrow> \<not> is_pending_cap capa
 6. \<And>a b s y capa. \<lbrakk>slot = (a, b); \<forall>cap. opt_cap (a, tcb_pending_op_slot) s = Some cap \<longrightarrow> \<not> is_pending_cap cap; tcb_pending_op_slot \<noteq> b; cdl_objects s a = Some y; has_slots y; \<exists>x. update_slots ((object_slots y)(b \<mapsto> cap)) y = PageDirectory x; object_slots y tcb_pending_op_slot = Some capa\<rbrakk> \<Longrightarrow> \<not> is_pending_cap capa
 7. \<And>a b s y capa. \<lbrakk>slot = (a, b); \<forall>cap. opt_cap (a, tcb_pending_op_slot) s = Some cap \<longrightarrow> \<not> is_pending_cap cap; tcb_pending_op_slot \<noteq> b; cdl_objects s a = Some y; has_slots y; \<exists>x. update_slots ((object_slots y)(b \<mapsto> cap)) y = Frame x; object_slots y tcb_pending_op_slot = Some capa\<rbrakk> \<Longrightarrow> \<not> is_pending_cap capa
 8. \<And>a b s y capa. \<lbrakk>slot = (a, b); \<forall>cap. opt_cap (a, tcb_pending_op_slot) s = Some cap \<longrightarrow> \<not> is_pending_cap cap; tcb_pending_op_slot \<noteq> b; cdl_objects s a = Some y; has_slots y; update_slots ((object_slots y)(b \<mapsto> cap)) y = Untyped; object_slots y tcb_pending_op_slot = Some capa\<rbrakk> \<Longrightarrow> \<not> is_pending_cap capa
 9. \<And>a b s y capa. \<lbrakk>slot = (a, b); \<forall>cap. opt_cap (a, tcb_pending_op_slot) s = Some cap \<longrightarrow> \<not> is_pending_cap cap; tcb_pending_op_slot \<noteq> b; cdl_objects s a = Some y; has_slots y; \<exists>x. update_slots ((object_slots y)(b \<mapsto> cap)) y = IRQNode x; object_slots y tcb_pending_op_slot = Some capa\<rbrakk> \<Longrightarrow> \<not> is_pending_cap capa proof (prove)
goal (8 subgoals):
 1. \<And>a b s y x capa. \<lbrakk>slot = (a, b); \<forall>cap. opt_cap (a, tcb_pending_op_slot) s = Some cap \<longrightarrow> \<not> is_pending_cap cap; tcb_pending_op_slot \<noteq> b; cdl_objects s a = Some y; has_slots y; update_slots ((object_slots y)(b \<mapsto> cap)) y = Tcb x; b = tcb_ipcbuffer_slot \<longrightarrow> object_slots y tcb_ipcbuffer_slot = Some cap; object_slots y tcb_pending_op_slot = Some capa\<rbrakk> \<Longrightarrow> \<not> is_pending_cap capa
 2. \<And>a b s y capa. \<lbrakk>slot = (a, b); \<forall>cap. opt_cap (a, tcb_pending_op_slot) s = Some cap \<longrightarrow> \<not> is_pending_cap cap; tcb_pending_op_slot \<noteq> b; cdl_objects s a = Some y; has_slots y; \<exists>x. update_slots ((object_slots y)(b \<mapsto> cap)) y = CNode x; object_slots y tcb_pending_op_slot = Some capa\<rbrakk> \<Longrightarrow> \<not> is_pending_cap capa
 3. \<And>a b s y capa. \<lbrakk>slot = (a, b); \<forall>cap. opt_cap (a, tcb_pending_op_slot) s = Some cap \<longrightarrow> \<not> is_pending_cap cap; tcb_pending_op_slot \<noteq> b; cdl_objects s a = Some y; has_slots y; \<exists>x. update_slots ((object_slots y)(b \<mapsto> cap)) y = AsidPool x; object_slots y tcb_pending_op_slot = Some capa\<rbrakk> \<Longrightarrow> \<not> is_pending_cap capa
 4. \<And>a b s y capa. \<lbrakk>slot = (a, b); \<forall>cap. opt_cap (a, tcb_pending_op_slot) s = Some cap \<longrightarrow> \<not> is_pending_cap cap; tcb_pending_op_slot \<noteq> b; cdl_objects s a = Some y; has_slots y; \<exists>x. update_slots ((object_slots y)(b \<mapsto> cap)) y = PageTable x; object_slots y tcb_pending_op_slot = Some capa\<rbrakk> \<Longrightarrow> \<not> is_pending_cap capa
 5. \<And>a b s y capa. \<lbrakk>slot = (a, b); \<forall>cap. opt_cap (a, tcb_pending_op_slot) s = Some cap \<longrightarrow> \<not> is_pending_cap cap; tcb_pending_op_slot \<noteq> b; cdl_objects s a = Some y; has_slots y; \<exists>x. update_slots ((object_slots y)(b \<mapsto> cap)) y = PageDirectory x; object_slots y tcb_pending_op_slot = Some capa\<rbrakk> \<Longrightarrow> \<not> is_pending_cap capa
 6. \<And>a b s y capa. \<lbrakk>slot = (a, b); \<forall>cap. opt_cap (a, tcb_pending_op_slot) s = Some cap \<longrightarrow> \<not> is_pending_cap cap; tcb_pending_op_slot \<noteq> b; cdl_objects s a = Some y; has_slots y; \<exists>x. update_slots ((object_slots y)(b \<mapsto> cap)) y = Frame x; object_slots y tcb_pending_op_slot = Some capa\<rbrakk> \<Longrightarrow> \<not> is_pending_cap capa
 7. \<And>a b s y capa. \<lbrakk>slot = (a, b); \<forall>cap. opt_cap (a, tcb_pending_op_slot) s = Some cap \<longrightarrow> \<not> is_pending_cap cap; tcb_pending_op_slot \<noteq> b; cdl_objects s a = Some y; has_slots y; update_slots ((object_slots y)(b \<mapsto> cap)) y = Untyped; object_slots y tcb_pending_op_slot = Some capa\<rbrakk> \<Longrightarrow> \<not> is_pending_cap capa
 8. \<And>a b s y capa. \<lbrakk>slot = (a, b); \<forall>cap. opt_cap (a, tcb_pending_op_slot) s = Some cap \<longrightarrow> \<not> is_pending_cap cap; tcb_pending_op_slot \<noteq> b; cdl_objects s a = Some y; has_slots y; \<exists>x. update_slots ((object_slots y)(b \<mapsto> cap)) y = IRQNode x; object_slots y tcb_pending_op_slot = Some capa\<rbrakk> \<Longrightarrow> \<not> is_pending_cap capa proof (prove)
goal:
No subgoals!