theory Finalise_C

lemma doUnbindNotification_ccorres:
  "ccorres dc xfdc (invs' and tcb_at' tcb)
    (UNIV \<inter> {s. ntfnPtr_' s = ntfn_Ptr ntfnptr} \<inter> {s. tcbptr_' s = tcb_ptr_to_ctcb_ptr tcb}) []
   (do ntfn \<leftarrow> getNotification ntfnptr; doUnbindNotification ntfnptr ntfn tcb od)
   (Call doUnbindNotification_'proc)" apply (cinit' lift: ntfnPtr_' tcbptr_') apply (rule ccorres_symb_exec_l [OF _ get_ntfn_inv' _ empty_fail_getNotification]) apply (rule_tac P="invs' and ko_at' ntfn ntfnptr" and P'=UNIV
             in ccorres_split_nothrow_novcg) apply (rule ccorres_from_vcg[where rrel=dc and xf=xfdc]) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: option_to_ptr_def option_to_0_def) apply (frule cmap_relation_ntfn) apply (erule (1) cmap_relation_ko_atE) apply (rule conjI) apply (erule h_t_valid_clift) apply (clarsimp simp: setNotification_def split_def) apply (rule bexI [OF _ setObject_eq]) apply (simp add: rf_sr_def cstate_relation_def Let_def init_def
                             typ_heap_simps'
                             cpspace_relation_def update_ntfn_map_tos) apply (elim conjE) apply (intro conjI)
            \<comment> \<open>tcb relation\<close> apply (rule cpspace_relation_ntfn_update_ntfn, assumption+) apply (clarsimp simp: cnotification_relation_def Let_def
                                     mask_def [where n=2] NtfnState_Waiting_def) apply (case_tac "ntfnObj ntfn", ((simp add: option_to_ctcb_ptr_def)+)[4]) subgoal by (simp add: carch_state_relation_def typ_heap_simps') subgoal by (simp add: cmachine_state_relation_def) subgoal by (simp add: h_t_valid_clift_Some_iff) subgoal by (simp add: objBits_simps') subgoal by (simp add: objBits_simps) apply assumption apply ceqv apply (rule ccorres_move_c_guard_tcb) apply (simp add: setBoundNotification_def) apply (rule_tac P'="\<top>" and P="\<top>"
                   in threadSet_ccorres_lemma3) apply vcg apply simp apply (erule(1) rf_sr_tcb_update_no_queue2) apply (simp add: typ_heap_simps')+ apply (simp add: tcb_cte_cases_def) apply (simp add: ctcb_relation_def option_to_ptr_def option_to_0_def) apply (simp add: invs'_def valid_state'_def) apply (wp get_ntfn_ko' | simp add: guard_is_UNIV_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (invs' and tcb_at' tcb) (UNIV \<inter> \<lbrace>\<acute>ntfnPtr = ntfn_Ptr ntfnptr\<rbrace> \<inter> \<lbrace>\<acute>tcbptr = tcb_ptr_to_ctcb_ptr tcb\<rbrace>) [] (do ntfn <- getNotification ntfnptr;
doUnbindNotification ntfnptr ntfn tcb
od) (Call doUnbindNotification_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>tcbptr ntfnPtr. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q104 tcbptr ntfnPtr) (?Q'104 tcbptr ntfnPtr) [SKIP] (do ntfn <- getNotification ntfnptr;
y <- setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None tcb
od) (CALL notification_ptr_set_ntfnBoundTCB_'proc(ntfnPtr,UCAST(32 \<rightarrow> 32) (SCAST(32 signed \<rightarrow> 32) 0));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcbptr} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcbptr\<rightarrow>[''tcbBoundNotification_C''])) NULL))))
 2. \<And>tcbptr ntfnPtr s s'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; (invs' and tcb_at' tcb) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q104 tcbptr ntfnPtr s \<and> s' \<in> ?Q'104 tcbptr ntfnPtr proof (prove)
goal (3 subgoals):
 1. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q110 tcbptr ntfnPtr ntfn) (?Q'110 tcbptr ntfnPtr ntfn) [SKIP] (do y <- setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None tcb
od) (CALL notification_ptr_set_ntfnBoundTCB_'proc(ntfnPtr,UCAST(32 \<rightarrow> 32) (SCAST(32 signed \<rightarrow> 32) 0));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcbptr} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcbptr\<rightarrow>[''tcbBoundNotification_C''])) NULL))))
 2. \<And>tcbptr ntfnPtr. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q104 tcbptr ntfnPtr\<rbrace> getNotification ntfnptr \<lbrace>?Q110 tcbptr ntfnPtr\<rbrace>
 3. \<And>tcbptr ntfnPtr s s'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; (invs' and tcb_at' tcb) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q104 tcbptr ntfnPtr s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ?Q110 tcbptr ntfnPtr rv s \<longrightarrow> s' \<in> ?Q'110 tcbptr ntfnPtr rv} proof (prove)
goal (7 subgoals):
 1. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> ccorres (?r'117 tcbptr ntfnPtr ntfn) (?xf'117 tcbptr ntfnPtr ntfn) (invs' and ko_at' ntfn ntfnptr) UNIV [] (setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn)) (CALL notification_ptr_set_ntfnBoundTCB_'proc(ntfnPtr,UCAST(32 \<rightarrow> 32) (SCAST(32 signed \<rightarrow> 32) 0)))
 2. \<And>tcbptr ntfnPtr ntfn rv' t t'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> ceqv \<Gamma> (?xf'117 tcbptr ntfnPtr ntfn) rv' t t' (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcbptr} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcbptr\<rightarrow>[''tcbBoundNotification_C''])) NULL)))) (?d'117 tcbptr ntfnPtr ntfn rv')
 3. \<And>tcbptr ntfnPtr ntfn rv rv'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; ?r'117 tcbptr ntfnPtr ntfn rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q117 tcbptr ntfnPtr ntfn rv) (?Q'117 tcbptr ntfnPtr ntfn rv rv') [SKIP] (setBoundNotification None tcb) (?d'117 tcbptr ntfnPtr ntfn rv')
 4. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?R117 tcbptr ntfnPtr ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn) \<lbrace>?Q117 tcbptr ntfnPtr ntfn\<rbrace>
 5. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> guard_is_UNIV (?r'117 tcbptr ntfnPtr ntfn) (?xf'117 tcbptr ntfnPtr ntfn) (?Q'117 tcbptr ntfnPtr ntfn)
 6. \<And>tcbptr ntfnPtr. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q104 tcbptr ntfnPtr\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and ?R117 tcbptr ntfnPtr ntfn\<rbrace>
 7. \<And>tcbptr ntfnPtr s s'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; (invs' and tcb_at' tcb) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q104 tcbptr ntfnPtr s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (invs' and ko_at' rv ntfnptr and ?R117 tcbptr ntfnPtr rv) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (7 subgoals):
 1. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. (invs' and ko_at' ntfn ntfnptr) \<sigma> \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} CALL notification_ptr_set_ntfnBoundTCB_'proc(ntfnPtr,UCAST(32 \<rightarrow> 32) (SCAST(32 signed \<rightarrow> 32) 0)) {s. \<exists>(rv, \<sigma>')\<in>fst (setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)}
 2. \<And>tcbptr ntfnPtr ntfn rv' t t'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcbptr} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcbptr\<rightarrow>[''tcbBoundNotification_C''])) NULL)))) (?d'117 tcbptr ntfnPtr ntfn rv')
 3. \<And>tcbptr ntfnPtr ntfn rv rv'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q117 tcbptr ntfnPtr ntfn rv) (?Q'117 tcbptr ntfnPtr ntfn rv rv') [SKIP] (setBoundNotification None tcb) (?d'117 tcbptr ntfnPtr ntfn rv')
 4. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?R117 tcbptr ntfnPtr ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn) \<lbrace>?Q117 tcbptr ntfnPtr ntfn\<rbrace>
 5. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'117 tcbptr ntfnPtr ntfn)
 6. \<And>tcbptr ntfnPtr. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q104 tcbptr ntfnPtr\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and ?R117 tcbptr ntfnPtr ntfn\<rbrace>
 7. \<And>tcbptr ntfnPtr s s'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; (invs' and tcb_at' tcb) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q104 tcbptr ntfnPtr s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (invs' and ko_at' rv ntfnptr and ?R117 tcbptr ntfnPtr rv) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (7 subgoals):
 1. \<And>tcbptr ntfnPtr ntfn \<sigma>. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> {s. (invs' and ko_at' ntfn ntfnptr) \<sigma> \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. s \<Turnstile>\<^sub>c ntfnPtr \<and> (\<forall>t. (\<exists>notification. notification_lift notification = notification_lift (the (cslift s ntfnPtr))\<lparr>ntfnBoundTCB_CL := UCAST(32 \<rightarrow> 32) (SCAST(32 signed \<rightarrow> 32) 0) && ~~ mask 4\<rparr> \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update ntfnPtr notification) (t_hrs_' (globals s))) \<longrightarrow> (\<exists>(rv, \<sigma>')\<in>fst (setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn) \<sigma>). (\<sigma>', s\<lparr>globals := globals s\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>) \<in> rf_sr \<and> dc rv (xfdc (s\<lparr>globals := globals s\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>))))}
 2. \<And>tcbptr ntfnPtr ntfn rv' t t'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcbptr} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcbptr\<rightarrow>[''tcbBoundNotification_C''])) NULL)))) (?d'117 tcbptr ntfnPtr ntfn rv')
 3. \<And>tcbptr ntfnPtr ntfn rv rv'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q117 tcbptr ntfnPtr ntfn rv) (?Q'117 tcbptr ntfnPtr ntfn rv rv') [SKIP] (setBoundNotification None tcb) (?d'117 tcbptr ntfnPtr ntfn rv')
 4. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?R117 tcbptr ntfnPtr ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn) \<lbrace>?Q117 tcbptr ntfnPtr ntfn\<rbrace>
 5. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'117 tcbptr ntfnPtr ntfn)
 6. \<And>tcbptr ntfnPtr. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q104 tcbptr ntfnPtr\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and ?R117 tcbptr ntfnPtr ntfn\<rbrace>
 7. \<And>tcbptr ntfnPtr s s'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; (invs' and tcb_at' tcb) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q104 tcbptr ntfnPtr s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (invs' and ko_at' rv ntfnptr and ?R117 tcbptr ntfnPtr rv) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (7 subgoals):
 1. \<And>ntfn \<sigma> x. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; (\<sigma>, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> x \<Turnstile>\<^sub>c ntfn_Ptr ntfnptr \<and> (\<forall>t. (\<exists>notification. notification_lift notification = notification_lift (the (cslift x (ntfn_Ptr ntfnptr)))\<lparr>ntfnBoundTCB_CL := 0\<rparr> \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))) \<longrightarrow> (\<exists>xa\<in>fst (setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x\<lparr>globals := globals x\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>) \<in> rf_sr))
 2. \<And>tcbptr ntfnPtr ntfn rv' t t'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcbptr} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcbptr\<rightarrow>[''tcbBoundNotification_C''])) NULL)))) (?d'117 tcbptr ntfnPtr ntfn rv')
 3. \<And>tcbptr ntfnPtr ntfn rv rv'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q117 tcbptr ntfnPtr ntfn rv) (?Q'117 tcbptr ntfnPtr ntfn rv rv') [SKIP] (setBoundNotification None tcb) (?d'117 tcbptr ntfnPtr ntfn rv')
 4. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?R117 tcbptr ntfnPtr ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn) \<lbrace>?Q117 tcbptr ntfnPtr ntfn\<rbrace>
 5. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'117 tcbptr ntfnPtr ntfn)
 6. \<And>tcbptr ntfnPtr. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q104 tcbptr ntfnPtr\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and ?R117 tcbptr ntfnPtr ntfn\<rbrace>
 7. \<And>tcbptr ntfnPtr s s'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; (invs' and tcb_at' tcb) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q104 tcbptr ntfnPtr s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (invs' and ko_at' rv ntfnptr and ?R117 tcbptr ntfnPtr rv) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (7 subgoals):
 1. \<And>ntfn \<sigma> x. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; (\<sigma>, x) \<in> rf_sr; cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x))\<rbrakk> \<Longrightarrow> x \<Turnstile>\<^sub>c ntfn_Ptr ntfnptr \<and> (\<forall>t. (\<exists>notification. notification_lift notification = notification_lift (the (cslift x (ntfn_Ptr ntfnptr)))\<lparr>ntfnBoundTCB_CL := 0\<rparr> \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))) \<longrightarrow> (\<exists>xa\<in>fst (setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x\<lparr>globals := globals x\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>) \<in> rf_sr))
 2. \<And>tcbptr ntfnPtr ntfn rv' t t'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcbptr} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcbptr\<rightarrow>[''tcbBoundNotification_C''])) NULL)))) (?d'117 tcbptr ntfnPtr ntfn rv')
 3. \<And>tcbptr ntfnPtr ntfn rv rv'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q117 tcbptr ntfnPtr ntfn rv) (?Q'117 tcbptr ntfnPtr ntfn rv rv') [SKIP] (setBoundNotification None tcb) (?d'117 tcbptr ntfnPtr ntfn rv')
 4. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?R117 tcbptr ntfnPtr ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn) \<lbrace>?Q117 tcbptr ntfnPtr ntfn\<rbrace>
 5. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'117 tcbptr ntfnPtr ntfn)
 6. \<And>tcbptr ntfnPtr. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q104 tcbptr ntfnPtr\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and ?R117 tcbptr ntfnPtr ntfn\<rbrace>
 7. \<And>tcbptr ntfnPtr s s'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; (invs' and tcb_at' tcb) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q104 tcbptr ntfnPtr s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (invs' and ko_at' rv ntfnptr and ?R117 tcbptr ntfnPtr rv) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (7 subgoals):
 1. \<And>ntfn \<sigma> x ko'. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'\<rbrakk> \<Longrightarrow> x \<Turnstile>\<^sub>c ntfn_Ptr ntfnptr \<and> (\<forall>t. (\<exists>notification. notification_lift notification = notification_lift (the (cslift x (ntfn_Ptr ntfnptr)))\<lparr>ntfnBoundTCB_CL := 0\<rparr> \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))) \<longrightarrow> (\<exists>xa\<in>fst (setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x\<lparr>globals := globals x\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>) \<in> rf_sr))
 2. \<And>tcbptr ntfnPtr ntfn rv' t t'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcbptr} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcbptr\<rightarrow>[''tcbBoundNotification_C''])) NULL)))) (?d'117 tcbptr ntfnPtr ntfn rv')
 3. \<And>tcbptr ntfnPtr ntfn rv rv'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q117 tcbptr ntfnPtr ntfn rv) (?Q'117 tcbptr ntfnPtr ntfn rv rv') [SKIP] (setBoundNotification None tcb) (?d'117 tcbptr ntfnPtr ntfn rv')
 4. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?R117 tcbptr ntfnPtr ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn) \<lbrace>?Q117 tcbptr ntfnPtr ntfn\<rbrace>
 5. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'117 tcbptr ntfnPtr ntfn)
 6. \<And>tcbptr ntfnPtr. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q104 tcbptr ntfnPtr\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and ?R117 tcbptr ntfnPtr ntfn\<rbrace>
 7. \<And>tcbptr ntfnPtr s s'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; (invs' and tcb_at' tcb) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q104 tcbptr ntfnPtr s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (invs' and ko_at' rv ntfnptr and ?R117 tcbptr ntfnPtr rv) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (8 subgoals):
 1. \<And>ntfn \<sigma> x ko'. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'\<rbrakk> \<Longrightarrow> x \<Turnstile>\<^sub>c ntfn_Ptr ntfnptr
 2. \<And>ntfn \<sigma> x ko'. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'\<rbrakk> \<Longrightarrow> \<forall>t. (\<exists>notification. notification_lift notification = notification_lift (the (cslift x (ntfn_Ptr ntfnptr)))\<lparr>ntfnBoundTCB_CL := 0\<rparr> \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))) \<longrightarrow> (\<exists>xa\<in>fst (setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x\<lparr>globals := globals x\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>) \<in> rf_sr)
 3. \<And>tcbptr ntfnPtr ntfn rv' t t'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcbptr} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcbptr\<rightarrow>[''tcbBoundNotification_C''])) NULL)))) (?d'117 tcbptr ntfnPtr ntfn rv')
 4. \<And>tcbptr ntfnPtr ntfn rv rv'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q117 tcbptr ntfnPtr ntfn rv) (?Q'117 tcbptr ntfnPtr ntfn rv rv') [SKIP] (setBoundNotification None tcb) (?d'117 tcbptr ntfnPtr ntfn rv')
 5. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?R117 tcbptr ntfnPtr ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn) \<lbrace>?Q117 tcbptr ntfnPtr ntfn\<rbrace>
 6. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'117 tcbptr ntfnPtr ntfn)
 7. \<And>tcbptr ntfnPtr. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q104 tcbptr ntfnPtr\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and ?R117 tcbptr ntfnPtr ntfn\<rbrace>
 8. \<And>tcbptr ntfnPtr s s'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; (invs' and tcb_at' tcb) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q104 tcbptr ntfnPtr s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (invs' and ko_at' rv ntfnptr and ?R117 tcbptr ntfnPtr rv) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (7 subgoals):
 1. \<And>ntfn \<sigma> x ko'. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'\<rbrakk> \<Longrightarrow> \<forall>t. (\<exists>notification. notification_lift notification = notification_lift (the (cslift x (ntfn_Ptr ntfnptr)))\<lparr>ntfnBoundTCB_CL := 0\<rparr> \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))) \<longrightarrow> (\<exists>xa\<in>fst (setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x\<lparr>globals := globals x\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>) \<in> rf_sr)
 2. \<And>tcbptr ntfnPtr ntfn rv' t t'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcbptr} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcbptr\<rightarrow>[''tcbBoundNotification_C''])) NULL)))) (?d'117 tcbptr ntfnPtr ntfn rv')
 3. \<And>tcbptr ntfnPtr ntfn rv rv'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q117 tcbptr ntfnPtr ntfn rv) (?Q'117 tcbptr ntfnPtr ntfn rv rv') [SKIP] (setBoundNotification None tcb) (?d'117 tcbptr ntfnPtr ntfn rv')
 4. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?R117 tcbptr ntfnPtr ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn) \<lbrace>?Q117 tcbptr ntfnPtr ntfn\<rbrace>
 5. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'117 tcbptr ntfnPtr ntfn)
 6. \<And>tcbptr ntfnPtr. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q104 tcbptr ntfnPtr\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and ?R117 tcbptr ntfnPtr ntfn\<rbrace>
 7. \<And>tcbptr ntfnPtr s s'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; (invs' and tcb_at' tcb) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q104 tcbptr ntfnPtr s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (invs' and ko_at' rv ntfnptr and ?R117 tcbptr ntfnPtr rv) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (7 subgoals):
 1. \<And>ntfn \<sigma> x ko' t notification. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (setObject ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn) \<sigma>). (snd xa, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr
 2. \<And>tcbptr ntfnPtr ntfn rv' t t'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcbptr} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcbptr\<rightarrow>[''tcbBoundNotification_C''])) NULL)))) (?d'117 tcbptr ntfnPtr ntfn rv')
 3. \<And>tcbptr ntfnPtr ntfn rv rv'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q117 tcbptr ntfnPtr ntfn rv) (?Q'117 tcbptr ntfnPtr ntfn rv rv') [SKIP] (setBoundNotification None tcb) (?d'117 tcbptr ntfnPtr ntfn rv')
 4. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?R117 tcbptr ntfnPtr ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn) \<lbrace>?Q117 tcbptr ntfnPtr ntfn\<rbrace>
 5. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'117 tcbptr ntfnPtr ntfn)
 6. \<And>tcbptr ntfnPtr. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q104 tcbptr ntfnPtr\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and ?R117 tcbptr ntfnPtr ntfn\<rbrace>
 7. \<And>tcbptr ntfnPtr s s'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; (invs' and tcb_at' tcb) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q104 tcbptr ntfnPtr s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (invs' and ko_at' rv ntfnptr and ?R117 tcbptr ntfnPtr rv) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (11 subgoals):
 1. \<And>ntfn \<sigma> x ko' t notification. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> (snd ((), \<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(ntfnptr \<mapsto> injectKOS (ntfnBoundTCB_update (\<lambda>_. None) ntfn))\<rparr>), x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr
 2. \<And>ntfn \<sigma> x ko' t notification val old ptr ptr' next. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> updateObject val old ptr ptr' next = updateObject_default val old ptr ptr' next
 3. \<And>ntfn \<sigma> x ko' t notification v. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> 1 < 2 ^ objBits v
 4. \<And>ntfn \<sigma> x ko' t notification v v'. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> objBits v = objBits v'
 5. \<And>ntfn \<sigma> x ko' t notification. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> obj_at' (?P173 ntfn \<sigma> x ko' t notification) ntfnptr \<sigma>
 6. \<And>tcbptr ntfnPtr ntfn rv' t t'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcbptr} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcbptr\<rightarrow>[''tcbBoundNotification_C''])) NULL)))) (?d'117 tcbptr ntfnPtr ntfn rv')
 7. \<And>tcbptr ntfnPtr ntfn rv rv'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q117 tcbptr ntfnPtr ntfn rv) (?Q'117 tcbptr ntfnPtr ntfn rv rv') [SKIP] (setBoundNotification None tcb) (?d'117 tcbptr ntfnPtr ntfn rv')
 8. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?R117 tcbptr ntfnPtr ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn) \<lbrace>?Q117 tcbptr ntfnPtr ntfn\<rbrace>
 9. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'117 tcbptr ntfnPtr ntfn)
 10. \<And>tcbptr ntfnPtr. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q104 tcbptr ntfnPtr\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and ?R117 tcbptr ntfnPtr ntfn\<rbrace>
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>ntfn \<sigma> x ko' t notification. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation \<and> cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation \<and> cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)) \<and> cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)) \<and> cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation \<and> cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation \<and> cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation \<and> cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation \<and> cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation \<and> carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr \<and> carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr \<and> cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>) \<and> zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)) \<and> cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>) \<and> cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>) \<and> ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>) \<and> ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>) \<and> cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)) \<and> cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)) \<and> carch_state_relation (ksArchState \<sigma>) (globals x) \<and> cmachine_state_relation (ksMachineState \<sigma>) (globals x) \<and> cte_array_relation \<sigma> (globals x) \<and> tcb_cte_array_relation \<sigma> (globals x) \<and> apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>) \<and> ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>) \<and> ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma> \<and> x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr \<and> {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs \<and> x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr \<and> {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs \<and> htd_safe domain (hrs_htd (t_hrs_' (globals x))) \<and> - domain \<subseteq> kernel_data_refs \<and> globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list \<and> cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule \<and> ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>) \<and> ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>) \<and> ksDomainTime_' (globals x) = ksDomainTime \<sigma>; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> cmap_relation (map_to_ntfns ((ksPSpace \<sigma>)(ntfnptr \<mapsto> KONotification (ntfnBoundTCB_update (\<lambda>_. None) ntfn)))) ((cslift x)(ntfn_Ptr ntfnptr \<mapsto> notification)) ntfn_Ptr (cnotification_relation (cslift x)) \<and> carch_state_relation (ksArchState \<sigma>) (globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rparr>) \<and> cmachine_state_relation (ksMachineState \<sigma>) (globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rparr>)
 2. \<And>ntfn \<sigma> x ko' t notification val old ptr ptr' next. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> updateObject val old ptr ptr' next = updateObject_default val old ptr ptr' next
 3. \<And>ntfn \<sigma> x ko' t notification v. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> 1 < 2 ^ objBits v
 4. \<And>ntfn \<sigma> x ko' t notification v v'. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> objBits v = objBits v'
 5. \<And>ntfn \<sigma> x ko' t notification. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> obj_at' (?P173 ntfn \<sigma> x ko' t notification) ntfnptr \<sigma>
 6. \<And>tcbptr ntfnPtr ntfn rv' t t'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcbptr} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcbptr\<rightarrow>[''tcbBoundNotification_C''])) NULL)))) (?d'117 tcbptr ntfnPtr ntfn rv')
 7. \<And>tcbptr ntfnPtr ntfn rv rv'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q117 tcbptr ntfnPtr ntfn rv) (?Q'117 tcbptr ntfnPtr ntfn rv rv') [SKIP] (setBoundNotification None tcb) (?d'117 tcbptr ntfnPtr ntfn rv')
 8. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?R117 tcbptr ntfnPtr ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn) \<lbrace>?Q117 tcbptr ntfnPtr ntfn\<rbrace>
 9. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'117 tcbptr ntfnPtr ntfn)
 10. \<And>tcbptr ntfnPtr. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q104 tcbptr ntfnPtr\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and ?R117 tcbptr ntfnPtr ntfn\<rbrace>
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>ntfn \<sigma> x ko' t notification. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x)); cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr; cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); carch_state_relation (ksArchState \<sigma>) (globals x); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> cmap_relation (map_to_ntfns ((ksPSpace \<sigma>)(ntfnptr \<mapsto> KONotification (ntfnBoundTCB_update (\<lambda>_. None) ntfn)))) ((cslift x)(ntfn_Ptr ntfnptr \<mapsto> notification)) ntfn_Ptr (cnotification_relation (cslift x)) \<and> carch_state_relation (ksArchState \<sigma>) (globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rparr>) \<and> cmachine_state_relation (ksMachineState \<sigma>) (globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rparr>)
 2. \<And>ntfn \<sigma> x ko' t notification val old ptr ptr' next. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> updateObject val old ptr ptr' next = updateObject_default val old ptr ptr' next
 3. \<And>ntfn \<sigma> x ko' t notification v. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> 1 < 2 ^ objBits v
 4. \<And>ntfn \<sigma> x ko' t notification v v'. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> objBits v = objBits v'
 5. \<And>ntfn \<sigma> x ko' t notification. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> obj_at' (?P173 ntfn \<sigma> x ko' t notification) ntfnptr \<sigma>
 6. \<And>tcbptr ntfnPtr ntfn rv' t t'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcbptr} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcbptr\<rightarrow>[''tcbBoundNotification_C''])) NULL)))) (?d'117 tcbptr ntfnPtr ntfn rv')
 7. \<And>tcbptr ntfnPtr ntfn rv rv'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q117 tcbptr ntfnPtr ntfn rv) (?Q'117 tcbptr ntfnPtr ntfn rv rv') [SKIP] (setBoundNotification None tcb) (?d'117 tcbptr ntfnPtr ntfn rv')
 8. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?R117 tcbptr ntfnPtr ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn) \<lbrace>?Q117 tcbptr ntfnPtr ntfn\<rbrace>
 9. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'117 tcbptr ntfnPtr ntfn)
 10. \<And>tcbptr ntfnPtr. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q104 tcbptr ntfnPtr\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and ?R117 tcbptr ntfnPtr ntfn\<rbrace>
A total of 11 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>ntfn \<sigma> x ko' t notification. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x)); cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr; cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); carch_state_relation (ksArchState \<sigma>) (globals x); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> cmap_relation (map_to_ntfns ((ksPSpace \<sigma>)(ntfnptr \<mapsto> KONotification (ntfnBoundTCB_update (\<lambda>_. None) ntfn)))) ((cslift x)(ntfn_Ptr ntfnptr \<mapsto> notification)) ntfn_Ptr (cnotification_relation (cslift x))
 2. \<And>ntfn \<sigma> x ko' t notification. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x)); cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr; cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); carch_state_relation (ksArchState \<sigma>) (globals x); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> carch_state_relation (ksArchState \<sigma>) (globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rparr>)
 3. \<And>ntfn \<sigma> x ko' t notification. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x)); cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr; cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); carch_state_relation (ksArchState \<sigma>) (globals x); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> cmachine_state_relation (ksMachineState \<sigma>) (globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rparr>)
 4. \<And>ntfn \<sigma> x ko' t notification val old ptr ptr' next. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> updateObject val old ptr ptr' next = updateObject_default val old ptr ptr' next
 5. \<And>ntfn \<sigma> x ko' t notification v. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> 1 < 2 ^ objBits v
 6. \<And>ntfn \<sigma> x ko' t notification v v'. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> objBits v = objBits v'
 7. \<And>ntfn \<sigma> x ko' t notification. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> obj_at' (?P173 ntfn \<sigma> x ko' t notification) ntfnptr \<sigma>
 8. \<And>tcbptr ntfnPtr ntfn rv' t t'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcbptr} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcbptr\<rightarrow>[''tcbBoundNotification_C''])) NULL)))) (?d'117 tcbptr ntfnPtr ntfn rv')
 9. \<And>tcbptr ntfnPtr ntfn rv rv'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q117 tcbptr ntfnPtr ntfn rv) (?Q'117 tcbptr ntfnPtr ntfn rv rv') [SKIP] (setBoundNotification None tcb) (?d'117 tcbptr ntfnPtr ntfn rv')
 10. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?R117 tcbptr ntfnPtr ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn) \<lbrace>?Q117 tcbptr ntfnPtr ntfn\<rbrace>
A total of 13 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>ntfn \<sigma> x ko' t notification. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x)); cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr; cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); carch_state_relation (ksArchState \<sigma>) (globals x); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> cnotification_relation (cslift x) (ntfnBoundTCB_update (\<lambda>_. None) ntfn) notification
 2. \<And>ntfn \<sigma> x ko' t notification. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x)); cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr; cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); carch_state_relation (ksArchState \<sigma>) (globals x); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> cslift x|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` (if isWaitingNtfn (ntfnObj ntfn) then set (ntfnQueue (ntfnObj ntfn)) else {}))\<^esub> = cslift x|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` (if isWaitingNtfn (ntfnObj ntfn) then set (ntfnQueue (ntfnObj ntfn)) else {}))\<^esub>
 3. \<And>ntfn \<sigma> x ko' t notification. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x)); cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr; cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); carch_state_relation (ksArchState \<sigma>) (globals x); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> carch_state_relation (ksArchState \<sigma>) (globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rparr>)
 4. \<And>ntfn \<sigma> x ko' t notification. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x)); cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr; cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); carch_state_relation (ksArchState \<sigma>) (globals x); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> cmachine_state_relation (ksMachineState \<sigma>) (globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rparr>)
 5. \<And>ntfn \<sigma> x ko' t notification val old ptr ptr' next. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> updateObject val old ptr ptr' next = updateObject_default val old ptr ptr' next
 6. \<And>ntfn \<sigma> x ko' t notification v. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> 1 < 2 ^ objBits v
 7. \<And>ntfn \<sigma> x ko' t notification v v'. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> objBits v = objBits v'
 8. \<And>ntfn \<sigma> x ko' t notification. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> obj_at' (?P173 ntfn \<sigma> x ko' t notification) ntfnptr \<sigma>
 9. \<And>tcbptr ntfnPtr ntfn rv' t t'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcbptr} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcbptr\<rightarrow>[''tcbBoundNotification_C''])) NULL)))) (?d'117 tcbptr ntfnPtr ntfn rv')
 10. \<And>tcbptr ntfnPtr ntfn rv rv'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q117 tcbptr ntfnPtr ntfn rv) (?Q'117 tcbptr ntfnPtr ntfn rv rv') [SKIP] (setBoundNotification None tcb) (?d'117 tcbptr ntfnPtr ntfn rv')
A total of 14 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>ntfn \<sigma> x ko' t notification. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; cslift x (ntfn_Ptr ntfnptr) = Some ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x)); cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr; cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); carch_state_relation (ksArchState \<sigma>) (globals x); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>; case ntfnObj ntfn of Structures_H.ntfn.IdleNtfn \<Rightarrow> notification_CL.state_CL (notification_lift ko') = SCAST(32 signed \<rightarrow> 32) NtfnState_Idle \<and> ep_queue_relation' (cslift x) [] (tcb_Ptr (ntfnQueue_head_CL (notification_lift ko'))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift ko'))) | Structures_H.ntfn.ActiveNtfn msgid \<Rightarrow> notification_CL.state_CL (notification_lift ko') = SCAST(32 signed \<rightarrow> 32) NtfnState_Active \<and> msgid = ntfnMsgIdentifier_CL (notification_lift ko') \<and> ep_queue_relation' (cslift x) [] (tcb_Ptr (ntfnQueue_head_CL (notification_lift ko'))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift ko'))) | Structures_H.ntfn.WaitingNtfn q \<Rightarrow> notification_CL.state_CL (notification_lift ko') = SCAST(32 signed \<rightarrow> 32) NtfnState_Waiting \<and> ep_queue_relation' (cslift x) q (tcb_Ptr (ntfnQueue_head_CL (notification_lift ko'))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift ko'))); option_to_ctcb_ptr (ntfnBoundTCB ntfn) = tcb_Ptr (ntfnBoundTCB_CL (notification_lift ko'))\<rbrakk> \<Longrightarrow> (case ntfnObj ntfn of Structures_H.ntfn.IdleNtfn \<Rightarrow> notification_CL.state_CL (notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>) = SCAST(32 signed \<rightarrow> 32) NtfnState_Idle \<and> ep_queue_relation' (cslift x) [] (tcb_Ptr (ntfnQueue_head_CL (notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>))) | Structures_H.ntfn.ActiveNtfn msgid \<Rightarrow> notification_CL.state_CL (notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>) = SCAST(32 signed \<rightarrow> 32) NtfnState_Active \<and> msgid = ntfnMsgIdentifier_CL (notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>) \<and> ep_queue_relation' (cslift x) [] (tcb_Ptr (ntfnQueue_head_CL (notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>))) | Structures_H.ntfn.WaitingNtfn q \<Rightarrow> notification_CL.state_CL (notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>) = SCAST(32 signed \<rightarrow> 32) NtfnState_Waiting \<and> ep_queue_relation' (cslift x) q (tcb_Ptr (ntfnQueue_head_CL (notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>)))) \<and> option_to_ctcb_ptr None = NULL
 2. \<And>ntfn \<sigma> x ko' t notification. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x)); cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr; cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); carch_state_relation (ksArchState \<sigma>) (globals x); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> cslift x|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` (if isWaitingNtfn (ntfnObj ntfn) then set (ntfnQueue (ntfnObj ntfn)) else {}))\<^esub> = cslift x|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` (if isWaitingNtfn (ntfnObj ntfn) then set (ntfnQueue (ntfnObj ntfn)) else {}))\<^esub>
 3. \<And>ntfn \<sigma> x ko' t notification. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x)); cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr; cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); carch_state_relation (ksArchState \<sigma>) (globals x); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> carch_state_relation (ksArchState \<sigma>) (globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rparr>)
 4. \<And>ntfn \<sigma> x ko' t notification. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x)); cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr; cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); carch_state_relation (ksArchState \<sigma>) (globals x); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> cmachine_state_relation (ksMachineState \<sigma>) (globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rparr>)
 5. \<And>ntfn \<sigma> x ko' t notification val old ptr ptr' next. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> updateObject val old ptr ptr' next = updateObject_default val old ptr ptr' next
 6. \<And>ntfn \<sigma> x ko' t notification v. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> 1 < 2 ^ objBits v
 7. \<And>ntfn \<sigma> x ko' t notification v v'. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> objBits v = objBits v'
 8. \<And>ntfn \<sigma> x ko' t notification. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> obj_at' (?P173 ntfn \<sigma> x ko' t notification) ntfnptr \<sigma>
 9. \<And>tcbptr ntfnPtr ntfn rv' t t'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcbptr} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcbptr\<rightarrow>[''tcbBoundNotification_C''])) NULL)))) (?d'117 tcbptr ntfnPtr ntfn rv')
 10. \<And>tcbptr ntfnPtr ntfn rv rv'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q117 tcbptr ntfnPtr ntfn rv) (?Q'117 tcbptr ntfnPtr ntfn rv rv') [SKIP] (setBoundNotification None tcb) (?d'117 tcbptr ntfnPtr ntfn rv')
A total of 14 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>ntfn \<sigma> x ko' t notification. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x)); cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr; cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); carch_state_relation (ksArchState \<sigma>) (globals x); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> carch_state_relation (ksArchState \<sigma>) (globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rparr>)
 2. \<And>ntfn \<sigma> x ko' t notification. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x)); cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr; cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); carch_state_relation (ksArchState \<sigma>) (globals x); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> cmachine_state_relation (ksMachineState \<sigma>) (globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rparr>)
 3. \<And>ntfn \<sigma> x ko' t notification val old ptr ptr' next. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> updateObject val old ptr ptr' next = updateObject_default val old ptr ptr' next
 4. \<And>ntfn \<sigma> x ko' t notification v. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> 1 < 2 ^ objBits v
 5. \<And>ntfn \<sigma> x ko' t notification v v'. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> objBits v = objBits v'
 6. \<And>ntfn \<sigma> x ko' t notification. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> obj_at' (?P173 ntfn \<sigma> x ko' t notification) ntfnptr \<sigma>
 7. \<And>tcbptr ntfnPtr ntfn rv' t t'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcbptr} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcbptr\<rightarrow>[''tcbBoundNotification_C''])) NULL)))) (?d'117 tcbptr ntfnPtr ntfn rv')
 8. \<And>tcbptr ntfnPtr ntfn rv rv'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q117 tcbptr ntfnPtr ntfn rv) (?Q'117 tcbptr ntfnPtr ntfn rv rv') [SKIP] (setBoundNotification None tcb) (?d'117 tcbptr ntfnPtr ntfn rv')
 9. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?R117 tcbptr ntfnPtr ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn) \<lbrace>?Q117 tcbptr ntfnPtr ntfn\<rbrace>
 10. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'117 tcbptr ntfnPtr ntfn)
A total of 12 subgoals... proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs' \<sigma>_; ko_at' ntfn_ ntfnptr \<sigma>_; cslift x_ (ntfn_Ptr ntfnptr) = Some ko'_; cnotification_relation (cslift x_) ntfn_ ko'_; notification_lift notification_ = notification_lift ko'_\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t_) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification_) (t_hrs_' (globals x_)); cmap_relation (ctes_of \<sigma>_) (cslift x_) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>_)) (cslift x_) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>_)) (cslift x_) ep_Ptr (cendpoint_relation (cslift x_)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>_)) (cslift x_) ntfn_Ptr (cnotification_relation (cslift x_)); cmap_relation (map_to_pdes (ksPSpace \<sigma>_)) (cslift x_) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>_)) (cslift x_) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>_)) (cslift x_) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>_) (underlying_memory (ksMachineState \<sigma>_))) (cslift x_) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>_) (underlying_memory (ksMachineState \<sigma>_))) (cslift x_) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>_)) (c_h_t_valid x_) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>_)) (c_h_t_valid x_) pt_Ptr; cready_queues_relation (cslift x_) (ksReadyQueues_' (globals x_)) (ksReadyQueues \<sigma>_); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>_) (t_hrs_' (globals x_)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x_)) (ksReadyQueuesL1Bitmap \<sigma>_); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x_)) (ksReadyQueuesL2Bitmap \<sigma>_); ksCurThread_' (globals x_) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>_); ksIdleThread_' (globals x_) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>_); cinterrupt_relation (ksInterruptState \<sigma>_) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x_)); cscheduler_action_relation (ksSchedulerAction \<sigma>_) (ksSchedulerAction_' (globals x_)); carch_state_relation (ksArchState \<sigma>_) (globals x_); cmachine_state_relation (ksMachineState \<sigma>_) (globals x_); cte_array_relation \<sigma>_ (globals x_); tcb_cte_array_relation \<sigma>_ (globals x_); apsnd fst (ghost'state_' (globals x_)) = (gsUserPages \<sigma>_, gsCNodes \<sigma>_); ghost_size_rel (ghost'state_' (globals x_)) (gsMaxObjectSize \<sigma>_); ksWorkUnitsCompleted_' (globals x_) = ksWorkUnitsCompleted \<sigma>_; x_ \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; x_ \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x_))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>_) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x_) = word_of_nat (ksDomScheduleIdx \<sigma>_); ksCurDomain_' (globals x_) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>_); ksDomainTime_' (globals x_) = ksDomainTime \<sigma>_\<rbrakk> \<Longrightarrow> carch_state_relation (ksArchState \<sigma>_) (globals x_\<lparr>t_hrs_' := hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification_) (t_hrs_' (globals x_))\<rparr>) proof (prove)
goal (11 subgoals):
 1. \<And>ntfn \<sigma> x ko' t notification. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x)); cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr; cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); carch_state_relation (ksArchState \<sigma>) (globals x); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> cmachine_state_relation (ksMachineState \<sigma>) (globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rparr>)
 2. \<And>ntfn \<sigma> x ko' t notification val old ptr ptr' next. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> updateObject val old ptr ptr' next = updateObject_default val old ptr ptr' next
 3. \<And>ntfn \<sigma> x ko' t notification v. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> 1 < 2 ^ objBits v
 4. \<And>ntfn \<sigma> x ko' t notification v v'. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> objBits v = objBits v'
 5. \<And>ntfn \<sigma> x ko' t notification. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> obj_at' (?P173 ntfn \<sigma> x ko' t notification) ntfnptr \<sigma>
 6. \<And>tcbptr ntfnPtr ntfn rv' t t'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcbptr} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcbptr\<rightarrow>[''tcbBoundNotification_C''])) NULL)))) (?d'117 tcbptr ntfnPtr ntfn rv')
 7. \<And>tcbptr ntfnPtr ntfn rv rv'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q117 tcbptr ntfnPtr ntfn rv) (?Q'117 tcbptr ntfnPtr ntfn rv rv') [SKIP] (setBoundNotification None tcb) (?d'117 tcbptr ntfnPtr ntfn rv')
 8. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?R117 tcbptr ntfnPtr ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn) \<lbrace>?Q117 tcbptr ntfnPtr ntfn\<rbrace>
 9. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'117 tcbptr ntfnPtr ntfn)
 10. \<And>tcbptr ntfnPtr. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q104 tcbptr ntfnPtr\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and ?R117 tcbptr ntfnPtr ntfn\<rbrace>
A total of 11 subgoals... proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs' \<sigma>_; ko_at' ntfn_ ntfnptr \<sigma>_; cslift x_ (ntfn_Ptr ntfnptr) = Some ko'_; cnotification_relation (cslift x_) ntfn_ ko'_; notification_lift notification_ = notification_lift ko'_\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t_) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification_) (t_hrs_' (globals x_)); cmap_relation (ctes_of \<sigma>_) (cslift x_) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>_)) (cslift x_) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>_)) (cslift x_) ep_Ptr (cendpoint_relation (cslift x_)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>_)) (cslift x_) ntfn_Ptr (cnotification_relation (cslift x_)); cmap_relation (map_to_pdes (ksPSpace \<sigma>_)) (cslift x_) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>_)) (cslift x_) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>_)) (cslift x_) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>_) (underlying_memory (ksMachineState \<sigma>_))) (cslift x_) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>_) (underlying_memory (ksMachineState \<sigma>_))) (cslift x_) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>_)) (c_h_t_valid x_) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>_)) (c_h_t_valid x_) pt_Ptr; cready_queues_relation (cslift x_) (ksReadyQueues_' (globals x_)) (ksReadyQueues \<sigma>_); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>_) (t_hrs_' (globals x_)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x_)) (ksReadyQueuesL1Bitmap \<sigma>_); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x_)) (ksReadyQueuesL2Bitmap \<sigma>_); ksCurThread_' (globals x_) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>_); ksIdleThread_' (globals x_) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>_); cinterrupt_relation (ksInterruptState \<sigma>_) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x_)); cscheduler_action_relation (ksSchedulerAction \<sigma>_) (ksSchedulerAction_' (globals x_)); carch_state_relation (ksArchState \<sigma>_) (globals x_); cmachine_state_relation (ksMachineState \<sigma>_) (globals x_); cte_array_relation \<sigma>_ (globals x_); tcb_cte_array_relation \<sigma>_ (globals x_); apsnd fst (ghost'state_' (globals x_)) = (gsUserPages \<sigma>_, gsCNodes \<sigma>_); ghost_size_rel (ghost'state_' (globals x_)) (gsMaxObjectSize \<sigma>_); ksWorkUnitsCompleted_' (globals x_) = ksWorkUnitsCompleted \<sigma>_; x_ \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; x_ \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x_))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>_) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x_) = word_of_nat (ksDomScheduleIdx \<sigma>_); ksCurDomain_' (globals x_) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>_); ksDomainTime_' (globals x_) = ksDomainTime \<sigma>_\<rbrakk> \<Longrightarrow> cmachine_state_relation (ksMachineState \<sigma>_) (globals x_\<lparr>t_hrs_' := hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification_) (t_hrs_' (globals x_))\<rparr>) proof (prove)
goal (10 subgoals):
 1. \<And>ntfn \<sigma> x ko' t notification val old ptr ptr' next. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> updateObject val old ptr ptr' next = updateObject_default val old ptr ptr' next
 2. \<And>ntfn \<sigma> x ko' t notification v. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> 1 < 2 ^ objBits v
 3. \<And>ntfn \<sigma> x ko' t notification v v'. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> objBits v = objBits v'
 4. \<And>ntfn \<sigma> x ko' t notification. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> obj_at' (?P173 ntfn \<sigma> x ko' t notification) ntfnptr \<sigma>
 5. \<And>tcbptr ntfnPtr ntfn rv' t t'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcbptr} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcbptr\<rightarrow>[''tcbBoundNotification_C''])) NULL)))) (?d'117 tcbptr ntfnPtr ntfn rv')
 6. \<And>tcbptr ntfnPtr ntfn rv rv'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q117 tcbptr ntfnPtr ntfn rv) (?Q'117 tcbptr ntfnPtr ntfn rv rv') [SKIP] (setBoundNotification None tcb) (?d'117 tcbptr ntfnPtr ntfn rv')
 7. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?R117 tcbptr ntfnPtr ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn) \<lbrace>?Q117 tcbptr ntfnPtr ntfn\<rbrace>
 8. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'117 tcbptr ntfnPtr ntfn)
 9. \<And>tcbptr ntfnPtr. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q104 tcbptr ntfnPtr\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and ?R117 tcbptr ntfnPtr ntfn\<rbrace>
 10. \<And>tcbptr ntfnPtr s s'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; (invs' and tcb_at' tcb) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q104 tcbptr ntfnPtr s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (invs' and ko_at' rv ntfnptr and ?R117 tcbptr ntfnPtr rv) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs' \<sigma>_; ko_at' ntfn_ ntfnptr \<sigma>_; (\<sigma>_, x_) \<in> rf_sr; cslift x_ (ntfn_Ptr ntfnptr) = Some ko'_; cnotification_relation (cslift x_) ntfn_ ko'_; notification_lift notification_ = notification_lift ko'_\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t_) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification_) (t_hrs_' (globals x_))\<rbrakk> \<Longrightarrow> updateObject val_ old_ ptr_ ptr'_ next_ = updateObject_default val_ old_ ptr_ ptr'_ next_ proof (prove)
goal (9 subgoals):
 1. \<And>ntfn \<sigma> x ko' t notification v. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> 1 < 2 ^ objBits v
 2. \<And>ntfn \<sigma> x ko' t notification v v'. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> objBits v = objBits v'
 3. \<And>ntfn \<sigma> x ko' t notification. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> obj_at' (?P173 ntfn \<sigma> x ko' t notification) ntfnptr \<sigma>
 4. \<And>tcbptr ntfnPtr ntfn rv' t t'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcbptr} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcbptr\<rightarrow>[''tcbBoundNotification_C''])) NULL)))) (?d'117 tcbptr ntfnPtr ntfn rv')
 5. \<And>tcbptr ntfnPtr ntfn rv rv'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q117 tcbptr ntfnPtr ntfn rv) (?Q'117 tcbptr ntfnPtr ntfn rv rv') [SKIP] (setBoundNotification None tcb) (?d'117 tcbptr ntfnPtr ntfn rv')
 6. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?R117 tcbptr ntfnPtr ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn) \<lbrace>?Q117 tcbptr ntfnPtr ntfn\<rbrace>
 7. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'117 tcbptr ntfnPtr ntfn)
 8. \<And>tcbptr ntfnPtr. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q104 tcbptr ntfnPtr\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and ?R117 tcbptr ntfnPtr ntfn\<rbrace>
 9. \<And>tcbptr ntfnPtr s s'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; (invs' and tcb_at' tcb) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q104 tcbptr ntfnPtr s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (invs' and ko_at' rv ntfnptr and ?R117 tcbptr ntfnPtr rv) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs' \<sigma>_; ko_at' ntfn_ ntfnptr \<sigma>_; (\<sigma>_, x_) \<in> rf_sr; cslift x_ (ntfn_Ptr ntfnptr) = Some ko'_; cnotification_relation (cslift x_) ntfn_ ko'_; notification_lift notification_ = notification_lift ko'_\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t_) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification_) (t_hrs_' (globals x_))\<rbrakk> \<Longrightarrow> 1 < 2 ^ objBits v_ proof (prove)
goal (8 subgoals):
 1. \<And>ntfn \<sigma> x ko' t notification v v'. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> objBits v = objBits v'
 2. \<And>ntfn \<sigma> x ko' t notification. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> obj_at' (?P173 ntfn \<sigma> x ko' t notification) ntfnptr \<sigma>
 3. \<And>tcbptr ntfnPtr ntfn rv' t t'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcbptr} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcbptr\<rightarrow>[''tcbBoundNotification_C''])) NULL)))) (?d'117 tcbptr ntfnPtr ntfn rv')
 4. \<And>tcbptr ntfnPtr ntfn rv rv'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q117 tcbptr ntfnPtr ntfn rv) (?Q'117 tcbptr ntfnPtr ntfn rv rv') [SKIP] (setBoundNotification None tcb) (?d'117 tcbptr ntfnPtr ntfn rv')
 5. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?R117 tcbptr ntfnPtr ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn) \<lbrace>?Q117 tcbptr ntfnPtr ntfn\<rbrace>
 6. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'117 tcbptr ntfnPtr ntfn)
 7. \<And>tcbptr ntfnPtr. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q104 tcbptr ntfnPtr\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and ?R117 tcbptr ntfnPtr ntfn\<rbrace>
 8. \<And>tcbptr ntfnPtr s s'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; (invs' and tcb_at' tcb) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q104 tcbptr ntfnPtr s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (invs' and ko_at' rv ntfnptr and ?R117 tcbptr ntfnPtr rv) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs' \<sigma>_; ko_at' ntfn_ ntfnptr \<sigma>_; (\<sigma>_, x_) \<in> rf_sr; cslift x_ (ntfn_Ptr ntfnptr) = Some ko'_; cnotification_relation (cslift x_) ntfn_ ko'_; notification_lift notification_ = notification_lift ko'_\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t_) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification_) (t_hrs_' (globals x_))\<rbrakk> \<Longrightarrow> objBits v_ = objBits v'_ proof (prove)
goal (7 subgoals):
 1. \<And>ntfn \<sigma> x ko' t notification. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := 0\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> obj_at' (?P173 ntfn \<sigma> x ko' t notification) ntfnptr \<sigma>
 2. \<And>tcbptr ntfnPtr ntfn rv' t t'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcbptr} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcbptr\<rightarrow>[''tcbBoundNotification_C''])) NULL)))) (?d'117 tcbptr ntfnPtr ntfn rv')
 3. \<And>tcbptr ntfnPtr ntfn rv rv'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q117 tcbptr ntfnPtr ntfn rv) (?Q'117 tcbptr ntfnPtr ntfn rv rv') [SKIP] (setBoundNotification None tcb) (?d'117 tcbptr ntfnPtr ntfn rv')
 4. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?R117 tcbptr ntfnPtr ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn) \<lbrace>?Q117 tcbptr ntfnPtr ntfn\<rbrace>
 5. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'117 tcbptr ntfnPtr ntfn)
 6. \<And>tcbptr ntfnPtr. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q104 tcbptr ntfnPtr\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and ?R117 tcbptr ntfnPtr ntfn\<rbrace>
 7. \<And>tcbptr ntfnPtr s s'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; (invs' and tcb_at' tcb) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q104 tcbptr ntfnPtr s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (invs' and ko_at' rv ntfnptr and ?R117 tcbptr ntfnPtr rv) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (6 subgoals):
 1. \<And>tcbptr ntfnPtr ntfn rv' t t'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcbptr} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcbptr\<rightarrow>[''tcbBoundNotification_C''])) NULL)))) (?d'117 tcbptr ntfnPtr ntfn rv')
 2. \<And>tcbptr ntfnPtr ntfn rv rv'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q117 tcbptr ntfnPtr ntfn rv) (?Q'117 tcbptr ntfnPtr ntfn rv rv') [SKIP] (setBoundNotification None tcb) (?d'117 tcbptr ntfnPtr ntfn rv')
 3. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?R117 tcbptr ntfnPtr ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn) \<lbrace>?Q117 tcbptr ntfnPtr ntfn\<rbrace>
 4. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'117 tcbptr ntfnPtr ntfn)
 5. \<And>tcbptr ntfnPtr. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q104 tcbptr ntfnPtr\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and ?R117 tcbptr ntfnPtr ntfn\<rbrace>
 6. \<And>tcbptr ntfnPtr s s'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; (invs' and tcb_at' tcb) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q104 tcbptr ntfnPtr s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (invs' and ko_at' rv ntfnptr and ?R117 tcbptr ntfnPtr rv) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (5 subgoals):
 1. \<And>tcbptr ntfnPtr ntfn rv rv'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q117 tcbptr ntfnPtr ntfn rv) (?Q'117 tcbptr ntfnPtr ntfn rv rv') [SKIP] (setBoundNotification None tcb) (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcbptr} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcbptr\<rightarrow>[''tcbBoundNotification_C''])) NULL))))
 2. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?R117 tcbptr ntfnPtr ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn) \<lbrace>?Q117 tcbptr ntfnPtr ntfn\<rbrace>
 3. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'117 tcbptr ntfnPtr ntfn)
 4. \<And>tcbptr ntfnPtr. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q104 tcbptr ntfnPtr\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and ?R117 tcbptr ntfnPtr ntfn\<rbrace>
 5. \<And>tcbptr ntfnPtr s s'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; (invs' and tcb_at' tcb) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q104 tcbptr ntfnPtr s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (invs' and ko_at' rv ntfnptr and ?R117 tcbptr ntfnPtr rv) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (5 subgoals):
 1. \<And>tcbptr ntfnPtr ntfn rv rv'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?A237 tcbptr ntfnPtr ntfn rv) (?C'236 tcbptr ntfnPtr ntfn rv rv') [SKIP] (setBoundNotification None tcb) (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcbptr\<rightarrow>[''tcbBoundNotification_C''])) NULL)))
 2. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?R117 tcbptr ntfnPtr ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn) \<lbrace>\<lambda>rv. ?A237 tcbptr ntfnPtr ntfn rv and tcb_at' (ctcb_ptr_to_tcb_ptr tcbptr)\<rbrace>
 3. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>rv rv'. ?C'236 tcbptr ntfnPtr ntfn rv rv' \<inter> \<lbrace>True\<rbrace>)
 4. \<And>tcbptr ntfnPtr. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q104 tcbptr ntfnPtr\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and ?R117 tcbptr ntfnPtr ntfn\<rbrace>
 5. \<And>tcbptr ntfnPtr s s'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; (invs' and tcb_at' tcb) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q104 tcbptr ntfnPtr s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (invs' and ko_at' rv ntfnptr and ?R117 tcbptr ntfnPtr rv) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (5 subgoals):
 1. \<And>tcbptr ntfnPtr ntfn rv'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?A237 (tcb_ptr_to_ctcb_ptr tcb) (ntfn_Ptr ntfnptr) ntfn ()) (?C'236 (tcb_ptr_to_ctcb_ptr tcb) (ntfn_Ptr ntfnptr) ntfn () rv') [SKIP] (threadSet (tcbBoundNotification_update (\<lambda>_. None)) tcb) (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcb_ptr_to_ctcb_ptr tcb\<rightarrow>[''tcbBoundNotification_C''])) NULL)))
 2. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?R117 tcbptr ntfnPtr ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn) \<lbrace>\<lambda>rv. ?A237 tcbptr ntfnPtr ntfn rv and tcb_at' (ctcb_ptr_to_tcb_ptr tcbptr)\<rbrace>
 3. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>rv rv'. ?C'236 tcbptr ntfnPtr ntfn rv rv' \<inter> \<lbrace>True\<rbrace>)
 4. \<And>tcbptr ntfnPtr. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q104 tcbptr ntfnPtr\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and ?R117 tcbptr ntfnPtr ntfn\<rbrace>
 5. \<And>tcbptr ntfnPtr s s'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; (invs' and tcb_at' tcb) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q104 tcbptr ntfnPtr s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (invs' and ko_at' rv ntfnptr and ?R117 tcbptr ntfnPtr rv) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (6 subgoals):
 1. \<And>tcbptr ntfnPtr ntfn rv' s tcba. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q249 tcbptr ntfnPtr ntfn rv' s tcba) \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcb_ptr_to_ctcb_ptr tcb\<rightarrow>[''tcbBoundNotification_C''])) NULL)) {s'. (s\<lparr>ksPSpace := (ksPSpace s)(tcb \<mapsto> injectKOS (tcbBoundNotification_update (\<lambda>_. None) tcba))\<rparr>, s') \<in> rf_sr}
 2. \<And>tcbptr ntfnPtr ntfn rv' s s' tcba tcb'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; True; ko_at' tcba tcb s; cslift s' (tcb_ptr_to_ctcb_ptr tcb) = Some tcb'; ctcb_relation tcba tcb'; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> s' \<in> ?Q249 tcbptr ntfnPtr ntfn rv' s tcba
 3. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?R117 tcbptr ntfnPtr ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn) \<lbrace>\<lambda>rv. tcb_at' tcb and (\<lambda>_. True) and tcb_at' (ctcb_ptr_to_tcb_ptr tcbptr)\<rbrace>
 4. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>rv rv'. UNIV \<inter> \<lbrace>True\<rbrace>)
 5. \<And>tcbptr ntfnPtr. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q104 tcbptr ntfnPtr\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and ?R117 tcbptr ntfnPtr ntfn\<rbrace>
 6. \<And>tcbptr ntfnPtr s s'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; (invs' and tcb_at' tcb) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q104 tcbptr ntfnPtr s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (invs' and ko_at' rv ntfnptr and ?R117 tcbptr ntfnPtr rv) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (5 subgoals):
 1. \<And>tcbptr ntfnPtr ntfn rv' s s' tcba tcb'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; True; ko_at' tcba tcb s; cslift s' (tcb_ptr_to_ctcb_ptr tcb) = Some tcb'; ctcb_relation tcba tcb'; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> s' \<in> {sa. (s\<lparr>ksPSpace := (ksPSpace s)(tcb \<mapsto> injectKOS (tcbBoundNotification_update (\<lambda>_. None) tcba))\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcb_ptr_to_ctcb_ptr tcb\<rightarrow>[''tcbBoundNotification_C''])) NULL))) sa) \<in> rf_sr}
 2. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?R117 tcbptr ntfnPtr ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn) \<lbrace>\<lambda>rv. tcb_at' tcb and (\<lambda>_. True) and tcb_at' (ctcb_ptr_to_tcb_ptr tcbptr)\<rbrace>
 3. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>rv rv'. UNIV \<inter> \<lbrace>True\<rbrace>)
 4. \<And>tcbptr ntfnPtr. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q104 tcbptr ntfnPtr\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and ?R117 tcbptr ntfnPtr ntfn\<rbrace>
 5. \<And>tcbptr ntfnPtr s s'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; (invs' and tcb_at' tcb) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q104 tcbptr ntfnPtr s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (invs' and ko_at' rv ntfnptr and ?R117 tcbptr ntfnPtr rv) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (5 subgoals):
 1. \<And>tcbptr ntfnPtr s s' tcba tcb'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; ko_at' tcba tcb s; cslift s' (tcb_ptr_to_ctcb_ptr tcb) = Some tcb'; ctcb_relation tcba tcb'\<rbrakk> \<Longrightarrow> (s\<lparr>ksPSpace := (ksPSpace s)(tcb \<mapsto> KOTCB (tcbBoundNotification_update (\<lambda>_. None) tcba))\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcb_ptr_to_ctcb_ptr tcb\<rightarrow>[''tcbBoundNotification_C''])) NULL))) s') \<in> rf_sr
 2. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?R117 tcbptr ntfnPtr ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn) \<lbrace>\<lambda>rv. tcb_at' tcb and (\<lambda>_. True) and tcb_at' (ctcb_ptr_to_tcb_ptr tcbptr)\<rbrace>
 3. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>rv rv'. UNIV \<inter> \<lbrace>True\<rbrace>)
 4. \<And>tcbptr ntfnPtr. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q104 tcbptr ntfnPtr\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and ?R117 tcbptr ntfnPtr ntfn\<rbrace>
 5. \<And>tcbptr ntfnPtr s s'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; (invs' and tcb_at' tcb) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q104 tcbptr ntfnPtr s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (invs' and ko_at' rv ntfnptr and ?R117 tcbptr ntfnPtr rv) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (11 subgoals):
 1. \<And>tcbptr ntfnPtr s s' tcba tcb'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; ko_at' tcba tcb s; cslift s' (tcb_ptr_to_ctcb_ptr tcb) = Some tcb'; ctcb_relation tcba tcb'\<rbrakk> \<Longrightarrow> hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcb_ptr_to_ctcb_ptr tcb\<rightarrow>[''tcbBoundNotification_C''])) NULL) (t_hrs_' (globals s')) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr tcb) (?ctcb254 tcbptr ntfnPtr s s' tcba tcb')) (t_hrs_' (globals s'))
 2. \<And>tcbptr ntfnPtr s s' tcba tcb'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; ko_at' tcba tcb s; cslift s' (tcb_ptr_to_ctcb_ptr tcb) = Some tcb'; ctcb_relation tcba tcb'\<rbrakk> \<Longrightarrow> tcbEPNext_C (?ctcb254 tcbptr ntfnPtr s s' tcba tcb') = tcbEPNext_C (the (cslift s' (tcb_ptr_to_ctcb_ptr tcb)))
 3. \<And>tcbptr ntfnPtr s s' tcba tcb'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; ko_at' tcba tcb s; cslift s' (tcb_ptr_to_ctcb_ptr tcb) = Some tcb'; ctcb_relation tcba tcb'\<rbrakk> \<Longrightarrow> tcbEPPrev_C (?ctcb254 tcbptr ntfnPtr s s' tcba tcb') = tcbEPPrev_C (the (cslift s' (tcb_ptr_to_ctcb_ptr tcb)))
 4. \<And>tcbptr ntfnPtr s s' tcba tcb'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; ko_at' tcba tcb s; cslift s' (tcb_ptr_to_ctcb_ptr tcb) = Some tcb'; ctcb_relation tcba tcb'\<rbrakk> \<Longrightarrow> tcbSchedNext_C (?ctcb254 tcbptr ntfnPtr s s' tcba tcb') = tcbSchedNext_C (the (cslift s' (tcb_ptr_to_ctcb_ptr tcb)))
 5. \<And>tcbptr ntfnPtr s s' tcba tcb'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; ko_at' tcba tcb s; cslift s' (tcb_ptr_to_ctcb_ptr tcb) = Some tcb'; ctcb_relation tcba tcb'\<rbrakk> \<Longrightarrow> tcbSchedPrev_C (?ctcb254 tcbptr ntfnPtr s s' tcba tcb') = tcbSchedPrev_C (the (cslift s' (tcb_ptr_to_ctcb_ptr tcb)))
 6. \<And>tcbptr ntfnPtr s s' tcba tcb'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; ko_at' tcba tcb s; cslift s' (tcb_ptr_to_ctcb_ptr tcb) = Some tcb'; ctcb_relation tcba tcb'\<rbrakk> \<Longrightarrow> \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> getF (tcbBoundNotification_update (\<lambda>_. None) tcba) = getF tcba
 7. \<And>tcbptr ntfnPtr s s' tcba tcb'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; ko_at' tcba tcb s; cslift s' (tcb_ptr_to_ctcb_ptr tcb) = Some tcb'; ctcb_relation tcba tcb'\<rbrakk> \<Longrightarrow> ctcb_relation (tcbBoundNotification_update (\<lambda>_. None) tcba) (?ctcb254 tcbptr ntfnPtr s s' tcba tcb')
 8. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?R117 tcbptr ntfnPtr ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn) \<lbrace>\<lambda>rv. tcb_at' tcb and (\<lambda>_. True) and tcb_at' (ctcb_ptr_to_tcb_ptr tcbptr)\<rbrace>
 9. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>rv rv'. UNIV \<inter> \<lbrace>True\<rbrace>)
 10. \<And>tcbptr ntfnPtr. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q104 tcbptr ntfnPtr\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and ?R117 tcbptr ntfnPtr ntfn\<rbrace>
A total of 11 subgoals... proof (prove)
goal (6 subgoals):
 1. \<And>tcbptr ntfnPtr s s' tcba tcb'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; ko_at' tcba tcb s; cslift s' (tcb_ptr_to_ctcb_ptr tcb) = Some tcb'; ctcb_relation tcba tcb'\<rbrakk> \<Longrightarrow> \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> getF (tcbBoundNotification_update (\<lambda>_. None) tcba) = getF tcba
 2. \<And>tcbptr ntfnPtr s s' tcba tcb'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; ko_at' tcba tcb s; cslift s' (tcb_ptr_to_ctcb_ptr tcb) = Some tcb'; ctcb_relation tcba tcb'\<rbrakk> \<Longrightarrow> ctcb_relation (tcbBoundNotification_update (\<lambda>_. None) tcba) (tcbBoundNotification_C_update (\<lambda>_. NULL) tcb')
 3. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?R117 tcbptr ntfnPtr ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn) \<lbrace>\<lambda>rv. tcb_at' tcb and (\<lambda>_. True) and tcb_at' (ctcb_ptr_to_tcb_ptr tcbptr)\<rbrace>
 4. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>rv rv'. UNIV \<inter> \<lbrace>True\<rbrace>)
 5. \<And>tcbptr ntfnPtr. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q104 tcbptr ntfnPtr\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and ?R117 tcbptr ntfnPtr ntfn\<rbrace>
 6. \<And>tcbptr ntfnPtr s s'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; (invs' and tcb_at' tcb) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q104 tcbptr ntfnPtr s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (invs' and ko_at' rv ntfnptr and ?R117 tcbptr ntfnPtr rv) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (5 subgoals):
 1. \<And>tcbptr ntfnPtr s s' tcba tcb'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; ko_at' tcba tcb s; cslift s' (tcb_ptr_to_ctcb_ptr tcb) = Some tcb'; ctcb_relation tcba tcb'\<rbrakk> \<Longrightarrow> ctcb_relation (tcbBoundNotification_update (\<lambda>_. None) tcba) (tcbBoundNotification_C_update (\<lambda>_. NULL) tcb')
 2. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?R117 tcbptr ntfnPtr ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn) \<lbrace>\<lambda>rv. tcb_at' tcb and (\<lambda>_. True) and tcb_at' (ctcb_ptr_to_tcb_ptr tcbptr)\<rbrace>
 3. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>rv rv'. UNIV \<inter> \<lbrace>True\<rbrace>)
 4. \<And>tcbptr ntfnPtr. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q104 tcbptr ntfnPtr\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and ?R117 tcbptr ntfnPtr ntfn\<rbrace>
 5. \<And>tcbptr ntfnPtr s s'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; (invs' and tcb_at' tcb) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q104 tcbptr ntfnPtr s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (invs' and ko_at' rv ntfnptr and ?R117 tcbptr ntfnPtr rv) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (4 subgoals):
 1. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?R117 tcbptr ntfnPtr ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn) \<lbrace>\<lambda>rv. tcb_at' tcb and (\<lambda>_. True) and tcb_at' (ctcb_ptr_to_tcb_ptr tcbptr)\<rbrace>
 2. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>rv rv'. UNIV \<inter> \<lbrace>True\<rbrace>)
 3. \<And>tcbptr ntfnPtr. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q104 tcbptr ntfnPtr\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and ?R117 tcbptr ntfnPtr ntfn\<rbrace>
 4. \<And>tcbptr ntfnPtr s s'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; (invs' and tcb_at' tcb) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q104 tcbptr ntfnPtr s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (invs' and ko_at' rv ntfnptr and ?R117 tcbptr ntfnPtr rv) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (4 subgoals):
 1. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?R117 (tcb_ptr_to_ctcb_ptr tcb) (ntfn_Ptr ntfnptr) ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn) \<lbrace>\<lambda>rv. tcb_at' tcb\<rbrace>
 2. \<And>tcbptr ntfnPtr ntfn. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>rv rv'. UNIV \<inter> \<lbrace>True\<rbrace>)
 3. \<And>tcbptr ntfnPtr. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<lbrace>?Q104 tcbptr ntfnPtr\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and ?R117 tcbptr ntfnPtr ntfn\<rbrace>
 4. \<And>tcbptr ntfnPtr s s'. \<lbrakk>tcbptr = tcb_ptr_to_ctcb_ptr tcb; ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; (invs' and tcb_at' tcb) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q104 tcbptr ntfnPtr s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (invs' and ko_at' rv ntfnptr and ?R117 tcbptr ntfnPtr rv) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal:
No subgoals!