theory Invocation_DP

lemma tcb_has_error_set_cap:
  "\<lbrace> (\<lambda>s. P (tcb_has_error p s)) and K (snd slot \<noteq> tcb_ipcbuffer_slot) \<rbrace> set_cap slot cap
  \<lbrace>\<lambda>ya s. P (tcb_has_error p s)\<rbrace>" apply (rule hoare_name_pre_state) apply clarsimp apply (rule_tac Q = "\<lambda>r s'. tcb_has_error p s' = tcb_has_error p s" in
    hoare_strengthen_post) apply (simp add:set_cap_def
    gets_the_def set_object_def
    split_def) apply (wp|wpc|simp)+ apply (clarsimp simp:tcb_has_error_def
    object_at_def,simp split:cdl_object.split_asm) apply (intro conjI impI) apply (simp add:update_slots_def
     has_slots_def
     object_slots_def
     split:cdl_object.splits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. P (tcb_has_error p s)) and K (snd slot \<noteq> tcb_ipcbuffer_slot)\<rbrace> set_cap slot cap \<lbrace>\<lambda>ya s. P (tcb_has_error p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. P (tcb_has_error p s)) and K (snd slot \<noteq> tcb_ipcbuffer_slot)) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> set_cap slot cap \<lbrace>\<lambda>ya s. P (tcb_has_error p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>P (tcb_has_error p s); snd slot \<noteq> tcb_ipcbuffer_slot\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> set_cap slot cap \<lbrace>\<lambda>ya s. P (tcb_has_error p s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>P (tcb_has_error p s); snd slot \<noteq> tcb_ipcbuffer_slot\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> set_cap slot cap \<lbrace>\<lambda>r s'. tcb_has_error p s' = tcb_has_error p s\<rbrace>
 2. \<And>s rv sa. \<lbrakk>P (tcb_has_error p s); snd slot \<noteq> tcb_ipcbuffer_slot; tcb_has_error p sa = tcb_has_error p s\<rbrakk> \<Longrightarrow> P (tcb_has_error p sa) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>P (tcb_has_error p s); snd slot \<noteq> tcb_ipcbuffer_slot\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do obj <- gets (\<lambda>s. cdl_objects s (fst slot)) >>= assert_opt;
y <- assert (has_slots obj);
obj'' <- case update_slots ((object_slots obj)(snd slot \<mapsto> cap)) obj of Tcb t \<Rightarrow> if snd slot = tcb_ipcbuffer_slot \<and> object_slots obj (snd 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)(snd slot \<mapsto> cap)) obj) | _ \<Rightarrow> return (update_slots ((object_slots obj)(snd slot \<mapsto> cap)) obj);
modify (\<lambda>s. s\<lparr>cdl_objects := (cdl_objects s)(fst slot \<mapsto> obj'')\<rparr>)
od \<lbrace>\<lambda>r s'. tcb_has_error p s' = tcb_has_error p s\<rbrace>
 2. \<And>s rv sa. \<lbrakk>P (tcb_has_error p s); snd slot \<noteq> tcb_ipcbuffer_slot; tcb_has_error p sa = tcb_has_error p s\<rbrakk> \<Longrightarrow> P (tcb_has_error p sa) proof (prove)
goal (2 subgoals):
 1. \<And>s sa. \<lbrakk>P (tcb_has_error p sa); snd slot \<noteq> tcb_ipcbuffer_slot; s = sa\<rbrakk> \<Longrightarrow> (\<exists>y. cdl_objects sa (fst slot) = Some y) \<longrightarrow> has_slots (the (cdl_objects sa (fst slot))) \<longrightarrow> (update_slots ((object_slots (the (cdl_objects sa (fst slot))))(snd slot \<mapsto> cap)) (the (cdl_objects sa (fst slot))) = Endpoint \<longrightarrow> tcb_has_error p (sa\<lparr>cdl_objects := \<lambda>a. if a = fst slot then Some (update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (the (cdl_objects sa (fst slot)))) else cdl_objects sa a\<rparr>) = tcb_has_error p sa) \<and> (update_slots ((object_slots (the (cdl_objects sa (fst slot))))(snd slot \<mapsto> cap)) (the (cdl_objects sa (fst slot))) = Notification \<longrightarrow> tcb_has_error p (sa\<lparr>cdl_objects := \<lambda>a. if a = fst slot then Some (update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (the (cdl_objects sa (fst slot)))) else cdl_objects sa a\<rparr>) = tcb_has_error p sa) \<and> ((\<exists>x. update_slots ((object_slots (the (cdl_objects sa (fst slot))))(snd slot \<mapsto> cap)) (the (cdl_objects sa (fst slot))) = Tcb x) \<longrightarrow> tcb_has_error p (sa\<lparr>cdl_objects := \<lambda>a. if a = fst slot then Some (update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (the (cdl_objects sa (fst slot)))) else cdl_objects sa a\<rparr>) = tcb_has_error p sa) \<and> ((\<exists>x. update_slots ((object_slots (the (cdl_objects sa (fst slot))))(snd slot \<mapsto> cap)) (the (cdl_objects sa (fst slot))) = CNode x) \<longrightarrow> tcb_has_error p (sa\<lparr>cdl_objects := \<lambda>a. if a = fst slot then Some (update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (the (cdl_objects sa (fst slot)))) else cdl_objects sa a\<rparr>) = tcb_has_error p sa) \<and> ((\<exists>x. update_slots ((object_slots (the (cdl_objects sa (fst slot))))(snd slot \<mapsto> cap)) (the (cdl_objects sa (fst slot))) = AsidPool x) \<longrightarrow> tcb_has_error p (sa\<lparr>cdl_objects := \<lambda>a. if a = fst slot then Some (update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (the (cdl_objects sa (fst slot)))) else cdl_objects sa a\<rparr>) = tcb_has_error p sa) \<and> ((\<exists>x. update_slots ((object_slots (the (cdl_objects sa (fst slot))))(snd slot \<mapsto> cap)) (the (cdl_objects sa (fst slot))) = PageTable x) \<longrightarrow> tcb_has_error p (sa\<lparr>cdl_objects := \<lambda>a. if a = fst slot then Some (update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (the (cdl_objects sa (fst slot)))) else cdl_objects sa a\<rparr>) = tcb_has_error p sa) \<and> ((\<exists>x. update_slots ((object_slots (the (cdl_objects sa (fst slot))))(snd slot \<mapsto> cap)) (the (cdl_objects sa (fst slot))) = PageDirectory x) \<longrightarrow> tcb_has_error p (sa\<lparr>cdl_objects := \<lambda>a. if a = fst slot then Some (update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (the (cdl_objects sa (fst slot)))) else cdl_objects sa a\<rparr>) = tcb_has_error p sa) \<and> ((\<exists>x. update_slots ((object_slots (the (cdl_objects sa (fst slot))))(snd slot \<mapsto> cap)) (the (cdl_objects sa (fst slot))) = Frame x) \<longrightarrow> tcb_has_error p (sa\<lparr>cdl_objects := \<lambda>a. if a = fst slot then Some (update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (the (cdl_objects sa (fst slot)))) else cdl_objects sa a\<rparr>) = tcb_has_error p sa) \<and> (update_slots ((object_slots (the (cdl_objects sa (fst slot))))(snd slot \<mapsto> cap)) (the (cdl_objects sa (fst slot))) = Untyped \<longrightarrow> tcb_has_error p (sa\<lparr>cdl_objects := \<lambda>a. if a = fst slot then Some (update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (the (cdl_objects sa (fst slot)))) else cdl_objects sa a\<rparr>) = tcb_has_error p sa) \<and> ((\<exists>x. update_slots ((object_slots (the (cdl_objects sa (fst slot))))(snd slot \<mapsto> cap)) (the (cdl_objects sa (fst slot))) = IRQNode x) \<longrightarrow> tcb_has_error p (sa\<lparr>cdl_objects := \<lambda>a. if a = fst slot then Some (update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (the (cdl_objects sa (fst slot)))) else cdl_objects sa a\<rparr>) = tcb_has_error p sa)
 2. \<And>s rv sa. \<lbrakk>P (tcb_has_error p s); snd slot \<noteq> tcb_ipcbuffer_slot; tcb_has_error p sa = tcb_has_error p s\<rbrakk> \<Longrightarrow> P (tcb_has_error p sa) proof (prove)
goal (11 subgoals):
 1. \<And>sa y. \<lbrakk>snd slot \<noteq> tcb_ipcbuffer_slot; p = fst slot; cdl_objects sa (fst slot) = Some Endpoint; has_slots Endpoint; y = Endpoint; P False\<rbrakk> \<Longrightarrow> (update_slots ((object_slots Endpoint)(snd slot \<mapsto> cap)) Endpoint = Endpoint \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) Endpoint of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> (update_slots ((object_slots Endpoint)(snd slot \<mapsto> cap)) Endpoint = Notification \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) Endpoint of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots Endpoint)(snd slot \<mapsto> cap)) Endpoint = Tcb x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) Endpoint of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots Endpoint)(snd slot \<mapsto> cap)) Endpoint = CNode x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) Endpoint of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots Endpoint)(snd slot \<mapsto> cap)) Endpoint = AsidPool x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) Endpoint of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots Endpoint)(snd slot \<mapsto> cap)) Endpoint = PageTable x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) Endpoint of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots Endpoint)(snd slot \<mapsto> cap)) Endpoint = PageDirectory x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) Endpoint of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots Endpoint)(snd slot \<mapsto> cap)) Endpoint = Frame x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) Endpoint of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> (update_slots ((object_slots Endpoint)(snd slot \<mapsto> cap)) Endpoint = Untyped \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) Endpoint of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots Endpoint)(snd slot \<mapsto> cap)) Endpoint = IRQNode x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) Endpoint of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False))
 2. \<And>sa y. \<lbrakk>snd slot \<noteq> tcb_ipcbuffer_slot; p = fst slot; cdl_objects sa (fst slot) = Some Notification; has_slots Notification; y = Notification; P False\<rbrakk> \<Longrightarrow> (update_slots ((object_slots Notification)(snd slot \<mapsto> cap)) Notification = Endpoint \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) Notification of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> (update_slots ((object_slots Notification)(snd slot \<mapsto> cap)) Notification = Notification \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) Notification of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots Notification)(snd slot \<mapsto> cap)) Notification = Tcb x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) Notification of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots Notification)(snd slot \<mapsto> cap)) Notification = CNode x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) Notification of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots Notification)(snd slot \<mapsto> cap)) Notification = AsidPool x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) Notification of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots Notification)(snd slot \<mapsto> cap)) Notification = PageTable x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) Notification of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots Notification)(snd slot \<mapsto> cap)) Notification = PageDirectory x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) Notification of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots Notification)(snd slot \<mapsto> cap)) Notification = Frame x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) Notification of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> (update_slots ((object_slots Notification)(snd slot \<mapsto> cap)) Notification = Untyped \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) Notification of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots Notification)(snd slot \<mapsto> cap)) Notification = IRQNode x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) Notification of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False))
 3. \<And>sa y x3. \<lbrakk>snd slot \<noteq> tcb_ipcbuffer_slot; p = fst slot; cdl_objects sa (fst slot) = Some (Tcb x3); has_slots (Tcb x3); y = Tcb x3; P (cdl_intent_error (cdl_tcb_intent x3))\<rbrakk> \<Longrightarrow> (update_slots ((object_slots (Tcb x3))(snd slot \<mapsto> cap)) (Tcb x3) = Endpoint \<longrightarrow> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (Tcb x3) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False) = cdl_intent_error (cdl_tcb_intent x3)) \<and> (update_slots ((object_slots (Tcb x3))(snd slot \<mapsto> cap)) (Tcb x3) = Notification \<longrightarrow> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (Tcb x3) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False) = cdl_intent_error (cdl_tcb_intent x3)) \<and> ((\<exists>x. update_slots ((object_slots (Tcb x3))(snd slot \<mapsto> cap)) (Tcb x3) = Tcb x) \<longrightarrow> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (Tcb x3) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False) = cdl_intent_error (cdl_tcb_intent x3)) \<and> ((\<exists>x. update_slots ((object_slots (Tcb x3))(snd slot \<mapsto> cap)) (Tcb x3) = CNode x) \<longrightarrow> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (Tcb x3) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False) = cdl_intent_error (cdl_tcb_intent x3)) \<and> ((\<exists>x. update_slots ((object_slots (Tcb x3))(snd slot \<mapsto> cap)) (Tcb x3) = AsidPool x) \<longrightarrow> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (Tcb x3) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False) = cdl_intent_error (cdl_tcb_intent x3)) \<and> ((\<exists>x. update_slots ((object_slots (Tcb x3))(snd slot \<mapsto> cap)) (Tcb x3) = PageTable x) \<longrightarrow> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (Tcb x3) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False) = cdl_intent_error (cdl_tcb_intent x3)) \<and> ((\<exists>x. update_slots ((object_slots (Tcb x3))(snd slot \<mapsto> cap)) (Tcb x3) = PageDirectory x) \<longrightarrow> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (Tcb x3) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False) = cdl_intent_error (cdl_tcb_intent x3)) \<and> ((\<exists>x. update_slots ((object_slots (Tcb x3))(snd slot \<mapsto> cap)) (Tcb x3) = Frame x) \<longrightarrow> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (Tcb x3) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False) = cdl_intent_error (cdl_tcb_intent x3)) \<and> (update_slots ((object_slots (Tcb x3))(snd slot \<mapsto> cap)) (Tcb x3) = Untyped \<longrightarrow> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (Tcb x3) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False) = cdl_intent_error (cdl_tcb_intent x3)) \<and> ((\<exists>x. update_slots ((object_slots (Tcb x3))(snd slot \<mapsto> cap)) (Tcb x3) = IRQNode x) \<longrightarrow> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (Tcb x3) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False) = cdl_intent_error (cdl_tcb_intent x3))
 4. \<And>sa y x4. \<lbrakk>snd slot \<noteq> tcb_ipcbuffer_slot; p = fst slot; cdl_objects sa (fst slot) = Some (CNode x4); has_slots (CNode x4); y = CNode x4; P False\<rbrakk> \<Longrightarrow> (update_slots ((object_slots (CNode x4))(snd slot \<mapsto> cap)) (CNode x4) = Endpoint \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (CNode x4) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> (update_slots ((object_slots (CNode x4))(snd slot \<mapsto> cap)) (CNode x4) = Notification \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (CNode x4) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots (CNode x4))(snd slot \<mapsto> cap)) (CNode x4) = Tcb x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (CNode x4) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots (CNode x4))(snd slot \<mapsto> cap)) (CNode x4) = CNode x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (CNode x4) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots (CNode x4))(snd slot \<mapsto> cap)) (CNode x4) = AsidPool x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (CNode x4) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots (CNode x4))(snd slot \<mapsto> cap)) (CNode x4) = PageTable x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (CNode x4) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots (CNode x4))(snd slot \<mapsto> cap)) (CNode x4) = PageDirectory x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (CNode x4) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots (CNode x4))(snd slot \<mapsto> cap)) (CNode x4) = Frame x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (CNode x4) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> (update_slots ((object_slots (CNode x4))(snd slot \<mapsto> cap)) (CNode x4) = Untyped \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (CNode x4) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots (CNode x4))(snd slot \<mapsto> cap)) (CNode x4) = IRQNode x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (CNode x4) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False))
 5. \<And>sa y x5. \<lbrakk>snd slot \<noteq> tcb_ipcbuffer_slot; p = fst slot; cdl_objects sa (fst slot) = Some (AsidPool x5); has_slots (AsidPool x5); y = AsidPool x5; P False\<rbrakk> \<Longrightarrow> (update_slots ((object_slots (AsidPool x5))(snd slot \<mapsto> cap)) (AsidPool x5) = Endpoint \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (AsidPool x5) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> (update_slots ((object_slots (AsidPool x5))(snd slot \<mapsto> cap)) (AsidPool x5) = Notification \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (AsidPool x5) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots (AsidPool x5))(snd slot \<mapsto> cap)) (AsidPool x5) = Tcb x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (AsidPool x5) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots (AsidPool x5))(snd slot \<mapsto> cap)) (AsidPool x5) = CNode x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (AsidPool x5) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots (AsidPool x5))(snd slot \<mapsto> cap)) (AsidPool x5) = AsidPool x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (AsidPool x5) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots (AsidPool x5))(snd slot \<mapsto> cap)) (AsidPool x5) = PageTable x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (AsidPool x5) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots (AsidPool x5))(snd slot \<mapsto> cap)) (AsidPool x5) = PageDirectory x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (AsidPool x5) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots (AsidPool x5))(snd slot \<mapsto> cap)) (AsidPool x5) = Frame x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (AsidPool x5) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> (update_slots ((object_slots (AsidPool x5))(snd slot \<mapsto> cap)) (AsidPool x5) = Untyped \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (AsidPool x5) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots (AsidPool x5))(snd slot \<mapsto> cap)) (AsidPool x5) = IRQNode x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (AsidPool x5) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False))
 6. \<And>sa y x6. \<lbrakk>snd slot \<noteq> tcb_ipcbuffer_slot; p = fst slot; cdl_objects sa (fst slot) = Some (PageTable x6); has_slots (PageTable x6); y = PageTable x6; P False\<rbrakk> \<Longrightarrow> (update_slots ((object_slots (PageTable x6))(snd slot \<mapsto> cap)) (PageTable x6) = Endpoint \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (PageTable x6) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> (update_slots ((object_slots (PageTable x6))(snd slot \<mapsto> cap)) (PageTable x6) = Notification \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (PageTable x6) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots (PageTable x6))(snd slot \<mapsto> cap)) (PageTable x6) = Tcb x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (PageTable x6) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots (PageTable x6))(snd slot \<mapsto> cap)) (PageTable x6) = CNode x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (PageTable x6) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots (PageTable x6))(snd slot \<mapsto> cap)) (PageTable x6) = AsidPool x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (PageTable x6) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots (PageTable x6))(snd slot \<mapsto> cap)) (PageTable x6) = PageTable x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (PageTable x6) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots (PageTable x6))(snd slot \<mapsto> cap)) (PageTable x6) = PageDirectory x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (PageTable x6) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots (PageTable x6))(snd slot \<mapsto> cap)) (PageTable x6) = Frame x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (PageTable x6) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> (update_slots ((object_slots (PageTable x6))(snd slot \<mapsto> cap)) (PageTable x6) = Untyped \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (PageTable x6) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots (PageTable x6))(snd slot \<mapsto> cap)) (PageTable x6) = IRQNode x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (PageTable x6) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False))
 7. \<And>sa y x7. \<lbrakk>snd slot \<noteq> tcb_ipcbuffer_slot; p = fst slot; cdl_objects sa (fst slot) = Some (PageDirectory x7); has_slots (PageDirectory x7); y = PageDirectory x7; P False\<rbrakk> \<Longrightarrow> (update_slots ((object_slots (PageDirectory x7))(snd slot \<mapsto> cap)) (PageDirectory x7) = Endpoint \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (PageDirectory x7) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> (update_slots ((object_slots (PageDirectory x7))(snd slot \<mapsto> cap)) (PageDirectory x7) = Notification \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (PageDirectory x7) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots (PageDirectory x7))(snd slot \<mapsto> cap)) (PageDirectory x7) = Tcb x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (PageDirectory x7) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots (PageDirectory x7))(snd slot \<mapsto> cap)) (PageDirectory x7) = CNode x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (PageDirectory x7) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots (PageDirectory x7))(snd slot \<mapsto> cap)) (PageDirectory x7) = AsidPool x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (PageDirectory x7) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots (PageDirectory x7))(snd slot \<mapsto> cap)) (PageDirectory x7) = PageTable x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (PageDirectory x7) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots (PageDirectory x7))(snd slot \<mapsto> cap)) (PageDirectory x7) = PageDirectory x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (PageDirectory x7) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots (PageDirectory x7))(snd slot \<mapsto> cap)) (PageDirectory x7) = Frame x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (PageDirectory x7) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> (update_slots ((object_slots (PageDirectory x7))(snd slot \<mapsto> cap)) (PageDirectory x7) = Untyped \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (PageDirectory x7) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots (PageDirectory x7))(snd slot \<mapsto> cap)) (PageDirectory x7) = IRQNode x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (PageDirectory x7) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False))
 8. \<And>sa y x8. \<lbrakk>snd slot \<noteq> tcb_ipcbuffer_slot; p = fst slot; cdl_objects sa (fst slot) = Some (Frame x8); has_slots (Frame x8); y = Frame x8; P False\<rbrakk> \<Longrightarrow> (update_slots ((object_slots (Frame x8))(snd slot \<mapsto> cap)) (Frame x8) = Endpoint \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (Frame x8) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> (update_slots ((object_slots (Frame x8))(snd slot \<mapsto> cap)) (Frame x8) = Notification \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (Frame x8) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots (Frame x8))(snd slot \<mapsto> cap)) (Frame x8) = Tcb x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (Frame x8) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots (Frame x8))(snd slot \<mapsto> cap)) (Frame x8) = CNode x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (Frame x8) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots (Frame x8))(snd slot \<mapsto> cap)) (Frame x8) = AsidPool x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (Frame x8) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots (Frame x8))(snd slot \<mapsto> cap)) (Frame x8) = PageTable x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (Frame x8) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots (Frame x8))(snd slot \<mapsto> cap)) (Frame x8) = PageDirectory x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (Frame x8) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots (Frame x8))(snd slot \<mapsto> cap)) (Frame x8) = Frame x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (Frame x8) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> (update_slots ((object_slots (Frame x8))(snd slot \<mapsto> cap)) (Frame x8) = Untyped \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (Frame x8) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots (Frame x8))(snd slot \<mapsto> cap)) (Frame x8) = IRQNode x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (Frame x8) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False))
 9. \<And>sa y. \<lbrakk>snd slot \<noteq> tcb_ipcbuffer_slot; p = fst slot; cdl_objects sa (fst slot) = Some Untyped; has_slots Untyped; y = Untyped; P False\<rbrakk> \<Longrightarrow> (update_slots ((object_slots Untyped)(snd slot \<mapsto> cap)) Untyped = Endpoint \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) Untyped of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> (update_slots ((object_slots Untyped)(snd slot \<mapsto> cap)) Untyped = Notification \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) Untyped of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots Untyped)(snd slot \<mapsto> cap)) Untyped = Tcb x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) Untyped of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots Untyped)(snd slot \<mapsto> cap)) Untyped = CNode x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) Untyped of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots Untyped)(snd slot \<mapsto> cap)) Untyped = AsidPool x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) Untyped of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots Untyped)(snd slot \<mapsto> cap)) Untyped = PageTable x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) Untyped of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots Untyped)(snd slot \<mapsto> cap)) Untyped = PageDirectory x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) Untyped of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots Untyped)(snd slot \<mapsto> cap)) Untyped = Frame x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) Untyped of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> (update_slots ((object_slots Untyped)(snd slot \<mapsto> cap)) Untyped = Untyped \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) Untyped of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots Untyped)(snd slot \<mapsto> cap)) Untyped = IRQNode x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) Untyped of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False))
 10. \<And>sa y x10. \<lbrakk>snd slot \<noteq> tcb_ipcbuffer_slot; p = fst slot; cdl_objects sa (fst slot) = Some (IRQNode x10); has_slots (IRQNode x10); y = IRQNode x10; P False\<rbrakk> \<Longrightarrow> (update_slots ((object_slots (IRQNode x10))(snd slot \<mapsto> cap)) (IRQNode x10) = Endpoint \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (IRQNode x10) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> (update_slots ((object_slots (IRQNode x10))(snd slot \<mapsto> cap)) (IRQNode x10) = Notification \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (IRQNode x10) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots (IRQNode x10))(snd slot \<mapsto> cap)) (IRQNode x10) = Tcb x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (IRQNode x10) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots (IRQNode x10))(snd slot \<mapsto> cap)) (IRQNode x10) = CNode x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (IRQNode x10) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots (IRQNode x10))(snd slot \<mapsto> cap)) (IRQNode x10) = AsidPool x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (IRQNode x10) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots (IRQNode x10))(snd slot \<mapsto> cap)) (IRQNode x10) = PageTable x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (IRQNode x10) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots (IRQNode x10))(snd slot \<mapsto> cap)) (IRQNode x10) = PageDirectory x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (IRQNode x10) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots (IRQNode x10))(snd slot \<mapsto> cap)) (IRQNode x10) = Frame x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (IRQNode x10) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> (update_slots ((object_slots (IRQNode x10))(snd slot \<mapsto> cap)) (IRQNode x10) = Untyped \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (IRQNode x10) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)) \<and> ((\<exists>x. update_slots ((object_slots (IRQNode x10))(snd slot \<mapsto> cap)) (IRQNode x10) = IRQNode x) \<longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) (IRQNode x10) of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False))
A total of 11 subgoals... proof (prove)
goal (20 subgoals):
 1. \<And>sa y. \<lbrakk>snd slot \<noteq> tcb_ipcbuffer_slot; p = fst slot; cdl_objects sa (fst slot) = Some Endpoint; has_slots Endpoint; y = Endpoint; P False; update_slots ((object_slots Endpoint)(snd slot \<mapsto> cap)) Endpoint = Endpoint\<rbrakk> \<Longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) Endpoint of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)
 2. \<And>sa y. \<lbrakk>snd slot \<noteq> tcb_ipcbuffer_slot; p = fst slot; cdl_objects sa (fst slot) = Some Endpoint; has_slots Endpoint; y = Endpoint; P False; update_slots ((object_slots Endpoint)(snd slot \<mapsto> cap)) Endpoint = Notification\<rbrakk> \<Longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) Endpoint of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)
 3. \<And>sa y. \<lbrakk>snd slot \<noteq> tcb_ipcbuffer_slot; p = fst slot; cdl_objects sa (fst slot) = Some Endpoint; has_slots Endpoint; y = Endpoint; P False; \<exists>x. update_slots ((object_slots Endpoint)(snd slot \<mapsto> cap)) Endpoint = Tcb x\<rbrakk> \<Longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) Endpoint of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)
 4. \<And>sa y. \<lbrakk>snd slot \<noteq> tcb_ipcbuffer_slot; p = fst slot; cdl_objects sa (fst slot) = Some Endpoint; has_slots Endpoint; y = Endpoint; P False; \<exists>x. update_slots ((object_slots Endpoint)(snd slot \<mapsto> cap)) Endpoint = CNode x\<rbrakk> \<Longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) Endpoint of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)
 5. \<And>sa y. \<lbrakk>snd slot \<noteq> tcb_ipcbuffer_slot; p = fst slot; cdl_objects sa (fst slot) = Some Endpoint; has_slots Endpoint; y = Endpoint; P False; \<exists>x. update_slots ((object_slots Endpoint)(snd slot \<mapsto> cap)) Endpoint = AsidPool x\<rbrakk> \<Longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) Endpoint of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)
 6. \<And>sa y. \<lbrakk>snd slot \<noteq> tcb_ipcbuffer_slot; p = fst slot; cdl_objects sa (fst slot) = Some Endpoint; has_slots Endpoint; y = Endpoint; P False; \<exists>x. update_slots ((object_slots Endpoint)(snd slot \<mapsto> cap)) Endpoint = PageTable x\<rbrakk> \<Longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) Endpoint of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)
 7. \<And>sa y. \<lbrakk>snd slot \<noteq> tcb_ipcbuffer_slot; p = fst slot; cdl_objects sa (fst slot) = Some Endpoint; has_slots Endpoint; y = Endpoint; P False; \<exists>x. update_slots ((object_slots Endpoint)(snd slot \<mapsto> cap)) Endpoint = PageDirectory x\<rbrakk> \<Longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) Endpoint of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)
 8. \<And>sa y. \<lbrakk>snd slot \<noteq> tcb_ipcbuffer_slot; p = fst slot; cdl_objects sa (fst slot) = Some Endpoint; has_slots Endpoint; y = Endpoint; P False; \<exists>x. update_slots ((object_slots Endpoint)(snd slot \<mapsto> cap)) Endpoint = Frame x\<rbrakk> \<Longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) Endpoint of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)
 9. \<And>sa y. \<lbrakk>snd slot \<noteq> tcb_ipcbuffer_slot; p = fst slot; cdl_objects sa (fst slot) = Some Endpoint; has_slots Endpoint; y = Endpoint; P False; update_slots ((object_slots Endpoint)(snd slot \<mapsto> cap)) Endpoint = Untyped\<rbrakk> \<Longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) Endpoint of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)
 10. \<And>sa y. \<lbrakk>snd slot \<noteq> tcb_ipcbuffer_slot; p = fst slot; cdl_objects sa (fst slot) = Some Endpoint; has_slots Endpoint; y = Endpoint; P False; \<exists>x. update_slots ((object_slots Endpoint)(snd slot \<mapsto> cap)) Endpoint = IRQNode x\<rbrakk> \<Longrightarrow> \<not> (case update_slots (\<lambda>a. if a = snd slot then Some cap else object_slots (the (cdl_objects sa (fst slot))) a) Endpoint of Tcb x \<Rightarrow> cdl_intent_error (cdl_tcb_intent x) = True | _ \<Rightarrow> False)
A total of 20 subgoals... proof (prove)
goal:
No subgoals!