theory Tcb_C

lemma bindNotification_ccorres:
  "ccorres dc xfdc (invs' and tcb_at' tcb)
    (UNIV \<inter> {s. tcb_' s = tcb_ptr_to_ctcb_ptr tcb}
          \<inter> {s. ntfnPtr_' s = ntfn_Ptr ntfnptr}) []
   (bindNotification tcb ntfnptr)
   (Call bindNotification_'proc)" apply (cinit lift: tcb_' ntfnPtr_' simp: bindNotification_def) apply (rule ccorres_symb_exec_l [OF _ get_ntfn_inv' _ empty_fail_getNotification]) apply (rule_tac P="invs' and ko_at' ntfn ntfnptr and tcb_at' tcb" 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) 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
                                    cpspace_relation_def update_ntfn_map_tos
                                    typ_heap_simps') 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") apply (auto simp: option_to_ctcb_ptr_def obj_at'_def objBits_simps projectKOs
                                   bindNTFN_alignment_junk)[4] apply (simp add: carch_state_relation_def typ_heap_simps') apply (simp add: cmachine_state_relation_def) apply (simp add: h_t_valid_clift_Some_iff) apply (simp add: objBits_simps') apply (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,
        (simp add: typ_heap_simps')+, simp_all?)[1] apply (simp add: ctcb_relation_def option_to_ptr_def option_to_0_def) apply simp 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>tcb = tcb_ptr_to_ctcb_ptr tcb\<rbrace> \<inter> \<lbrace>\<acute>ntfnPtr = ntfn_Ptr ntfnptr\<rbrace>) [] (bindNotification tcb ntfnptr) (Call bindNotification_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>ntfnPtr tcba. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q106 ntfnPtr tcba) (?Q'106 ntfnPtr tcba) [SKIP] (do ntfn <- getNotification ntfnptr;
y <- setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. Some tcb) ntfn);
setBoundNotification (Some ntfnptr) tcb
od) (CALL notification_ptr_set_ntfnBoundTCB_'proc(ntfnPtr,UCAST(32 \<rightarrow> 32) (ptr_val tcba));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcba} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcba\<rightarrow>[''tcbBoundNotification_C''])) ntfnPtr))))
 2. \<And>ntfnPtr tcba s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; (invs' and tcb_at' tcb) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q106 ntfnPtr tcba s \<and> s' \<in> ?Q'106 ntfnPtr tcba proof (prove)
goal (3 subgoals):
 1. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q112 ntfnPtr tcba ntfn) (?Q'112 ntfnPtr tcba ntfn) [SKIP] (do y <- setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. Some tcb) ntfn);
setBoundNotification (Some ntfnptr) tcb
od) (CALL notification_ptr_set_ntfnBoundTCB_'proc(ntfnPtr,UCAST(32 \<rightarrow> 32) (ptr_val tcba));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcba} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcba\<rightarrow>[''tcbBoundNotification_C''])) ntfnPtr))))
 2. \<And>ntfnPtr tcba. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q106 ntfnPtr tcba\<rbrace> getNotification ntfnptr \<lbrace>?Q112 ntfnPtr tcba\<rbrace>
 3. \<And>ntfnPtr tcba s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; (invs' and tcb_at' tcb) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q106 ntfnPtr tcba s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ?Q112 ntfnPtr tcba rv s \<longrightarrow> s' \<in> ?Q'112 ntfnPtr tcba rv} proof (prove)
goal (7 subgoals):
 1. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> ccorres (?r'119 ntfnPtr tcba ntfn) (?xf'119 ntfnPtr tcba ntfn) (invs' and ko_at' ntfn ntfnptr and tcb_at' tcb) UNIV [] (setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. Some tcb) ntfn)) (CALL notification_ptr_set_ntfnBoundTCB_'proc(ntfnPtr,UCAST(32 \<rightarrow> 32) (ptr_val tcba)))
 2. \<And>ntfnPtr tcba ntfn rv' t t'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> ceqv \<Gamma> (?xf'119 ntfnPtr tcba ntfn) rv' t t' (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcba} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcba\<rightarrow>[''tcbBoundNotification_C''])) ntfnPtr)))) (?d'119 ntfnPtr tcba ntfn rv')
 3. \<And>ntfnPtr tcba ntfn rv rv'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb; ?r'119 ntfnPtr tcba ntfn rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q119 ntfnPtr tcba ntfn rv) (?Q'119 ntfnPtr tcba ntfn rv rv') [SKIP] (setBoundNotification (Some ntfnptr) tcb) (?d'119 ntfnPtr tcba ntfn rv')
 4. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?R119 ntfnPtr tcba ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. Some tcb) ntfn) \<lbrace>?Q119 ntfnPtr tcba ntfn\<rbrace>
 5. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> guard_is_UNIV (?r'119 ntfnPtr tcba ntfn) (?xf'119 ntfnPtr tcba ntfn) (?Q'119 ntfnPtr tcba ntfn)
 6. \<And>ntfnPtr tcba. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q106 ntfnPtr tcba\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and tcb_at' tcb and ?R119 ntfnPtr tcba ntfn\<rbrace>
 7. \<And>ntfnPtr tcba s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; (invs' and tcb_at' tcb) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q106 ntfnPtr tcba s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (invs' and ko_at' rv ntfnptr and tcb_at' tcb and ?R119 ntfnPtr tcba rv) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (7 subgoals):
 1. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. (invs' and ko_at' ntfn ntfnptr and tcb_at' tcb) \<sigma> \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} CALL notification_ptr_set_ntfnBoundTCB_'proc(ntfnPtr,UCAST(32 \<rightarrow> 32) (ptr_val tcba)) {s. \<exists>(rv, \<sigma>')\<in>fst (setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. Some tcb) ntfn) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)}
 2. \<And>ntfnPtr tcba ntfn rv' t t'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcba} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcba\<rightarrow>[''tcbBoundNotification_C''])) ntfnPtr)))) (?d'119 ntfnPtr tcba ntfn rv')
 3. \<And>ntfnPtr tcba ntfn rv rv'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q119 ntfnPtr tcba ntfn rv) (?Q'119 ntfnPtr tcba ntfn rv rv') [SKIP] (setBoundNotification (Some ntfnptr) tcb) (?d'119 ntfnPtr tcba ntfn rv')
 4. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?R119 ntfnPtr tcba ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. Some tcb) ntfn) \<lbrace>?Q119 ntfnPtr tcba ntfn\<rbrace>
 5. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'119 ntfnPtr tcba ntfn)
 6. \<And>ntfnPtr tcba. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q106 ntfnPtr tcba\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and tcb_at' tcb and ?R119 ntfnPtr tcba ntfn\<rbrace>
 7. \<And>ntfnPtr tcba s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; (invs' and tcb_at' tcb) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q106 ntfnPtr tcba s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (invs' and ko_at' rv ntfnptr and tcb_at' tcb and ?R119 ntfnPtr tcba rv) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (7 subgoals):
 1. \<And>ntfnPtr tcba ntfn \<sigma>. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> {s. (invs' and ko_at' ntfn ntfnptr and tcb_at' tcb) \<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) (ptr_val tcba) && ~~ 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>_. Some tcb) 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>ntfnPtr tcba ntfn rv' t t'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcba} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcba\<rightarrow>[''tcbBoundNotification_C''])) ntfnPtr)))) (?d'119 ntfnPtr tcba ntfn rv')
 3. \<And>ntfnPtr tcba ntfn rv rv'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q119 ntfnPtr tcba ntfn rv) (?Q'119 ntfnPtr tcba ntfn rv rv') [SKIP] (setBoundNotification (Some ntfnptr) tcb) (?d'119 ntfnPtr tcba ntfn rv')
 4. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?R119 ntfnPtr tcba ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. Some tcb) ntfn) \<lbrace>?Q119 ntfnPtr tcba ntfn\<rbrace>
 5. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'119 ntfnPtr tcba ntfn)
 6. \<And>ntfnPtr tcba. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q106 ntfnPtr tcba\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and tcb_at' tcb and ?R119 ntfnPtr tcba ntfn\<rbrace>
 7. \<And>ntfnPtr tcba s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; (invs' and tcb_at' tcb) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q106 ntfnPtr tcba s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (invs' and ko_at' rv ntfnptr and tcb_at' tcb and ?R119 ntfnPtr tcba rv) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (7 subgoals):
 1. \<And>ntfn \<sigma> x. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; tcb_at' tcb \<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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>_. Some tcb) 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>ntfnPtr tcba ntfn rv' t t'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcba} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcba\<rightarrow>[''tcbBoundNotification_C''])) ntfnPtr)))) (?d'119 ntfnPtr tcba ntfn rv')
 3. \<And>ntfnPtr tcba ntfn rv rv'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q119 ntfnPtr tcba ntfn rv) (?Q'119 ntfnPtr tcba ntfn rv rv') [SKIP] (setBoundNotification (Some ntfnptr) tcb) (?d'119 ntfnPtr tcba ntfn rv')
 4. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?R119 ntfnPtr tcba ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. Some tcb) ntfn) \<lbrace>?Q119 ntfnPtr tcba ntfn\<rbrace>
 5. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'119 ntfnPtr tcba ntfn)
 6. \<And>ntfnPtr tcba. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q106 ntfnPtr tcba\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and tcb_at' tcb and ?R119 ntfnPtr tcba ntfn\<rbrace>
 7. \<And>ntfnPtr tcba s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; (invs' and tcb_at' tcb) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q106 ntfnPtr tcba s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (invs' and ko_at' rv ntfnptr and tcb_at' tcb and ?R119 ntfnPtr tcba rv) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (7 subgoals):
 1. \<And>ntfn \<sigma> x. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; tcb_at' tcb \<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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>_. Some tcb) 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>ntfnPtr tcba ntfn rv' t t'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcba} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcba\<rightarrow>[''tcbBoundNotification_C''])) ntfnPtr)))) (?d'119 ntfnPtr tcba ntfn rv')
 3. \<And>ntfnPtr tcba ntfn rv rv'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q119 ntfnPtr tcba ntfn rv) (?Q'119 ntfnPtr tcba ntfn rv rv') [SKIP] (setBoundNotification (Some ntfnptr) tcb) (?d'119 ntfnPtr tcba ntfn rv')
 4. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?R119 ntfnPtr tcba ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. Some tcb) ntfn) \<lbrace>?Q119 ntfnPtr tcba ntfn\<rbrace>
 5. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'119 ntfnPtr tcba ntfn)
 6. \<And>ntfnPtr tcba. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q106 ntfnPtr tcba\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and tcb_at' tcb and ?R119 ntfnPtr tcba ntfn\<rbrace>
 7. \<And>ntfnPtr tcba s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; (invs' and tcb_at' tcb) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q106 ntfnPtr tcba s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (invs' and ko_at' rv ntfnptr and tcb_at' tcb and ?R119 ntfnPtr tcba 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>; tcb_at' tcb \<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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>_. Some tcb) 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>ntfnPtr tcba ntfn rv' t t'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcba} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcba\<rightarrow>[''tcbBoundNotification_C''])) ntfnPtr)))) (?d'119 ntfnPtr tcba ntfn rv')
 3. \<And>ntfnPtr tcba ntfn rv rv'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q119 ntfnPtr tcba ntfn rv) (?Q'119 ntfnPtr tcba ntfn rv rv') [SKIP] (setBoundNotification (Some ntfnptr) tcb) (?d'119 ntfnPtr tcba ntfn rv')
 4. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?R119 ntfnPtr tcba ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. Some tcb) ntfn) \<lbrace>?Q119 ntfnPtr tcba ntfn\<rbrace>
 5. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'119 ntfnPtr tcba ntfn)
 6. \<And>ntfnPtr tcba. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q106 ntfnPtr tcba\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and tcb_at' tcb and ?R119 ntfnPtr tcba ntfn\<rbrace>
 7. \<And>ntfnPtr tcba s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; (invs' and tcb_at' tcb) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q106 ntfnPtr tcba s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (invs' and ko_at' rv ntfnptr and tcb_at' tcb and ?R119 ntfnPtr tcba 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>; tcb_at' tcb \<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>; tcb_at' tcb \<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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>_. Some tcb) 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>ntfnPtr tcba ntfn rv' t t'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcba} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcba\<rightarrow>[''tcbBoundNotification_C''])) ntfnPtr)))) (?d'119 ntfnPtr tcba ntfn rv')
 4. \<And>ntfnPtr tcba ntfn rv rv'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q119 ntfnPtr tcba ntfn rv) (?Q'119 ntfnPtr tcba ntfn rv rv') [SKIP] (setBoundNotification (Some ntfnptr) tcb) (?d'119 ntfnPtr tcba ntfn rv')
 5. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?R119 ntfnPtr tcba ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. Some tcb) ntfn) \<lbrace>?Q119 ntfnPtr tcba ntfn\<rbrace>
 6. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'119 ntfnPtr tcba ntfn)
 7. \<And>ntfnPtr tcba. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q106 ntfnPtr tcba\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and tcb_at' tcb and ?R119 ntfnPtr tcba ntfn\<rbrace>
 8. \<And>ntfnPtr tcba s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; (invs' and tcb_at' tcb) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q106 ntfnPtr tcba s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (invs' and ko_at' rv ntfnptr and tcb_at' tcb and ?R119 ntfnPtr tcba 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>; tcb_at' tcb \<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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>_. Some tcb) 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>ntfnPtr tcba ntfn rv' t t'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcba} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcba\<rightarrow>[''tcbBoundNotification_C''])) ntfnPtr)))) (?d'119 ntfnPtr tcba ntfn rv')
 3. \<And>ntfnPtr tcba ntfn rv rv'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q119 ntfnPtr tcba ntfn rv) (?Q'119 ntfnPtr tcba ntfn rv rv') [SKIP] (setBoundNotification (Some ntfnptr) tcb) (?d'119 ntfnPtr tcba ntfn rv')
 4. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?R119 ntfnPtr tcba ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. Some tcb) ntfn) \<lbrace>?Q119 ntfnPtr tcba ntfn\<rbrace>
 5. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'119 ntfnPtr tcba ntfn)
 6. \<And>ntfnPtr tcba. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q106 ntfnPtr tcba\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and tcb_at' tcb and ?R119 ntfnPtr tcba ntfn\<rbrace>
 7. \<And>ntfnPtr tcba s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; (invs' and tcb_at' tcb) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q106 ntfnPtr tcba s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (invs' and ko_at' rv ntfnptr and tcb_at' tcb and ?R119 ntfnPtr tcba 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>; tcb_at' tcb \<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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>_. Some tcb) 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>ntfnPtr tcba ntfn rv' t t'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcba} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcba\<rightarrow>[''tcbBoundNotification_C''])) ntfnPtr)))) (?d'119 ntfnPtr tcba ntfn rv')
 3. \<And>ntfnPtr tcba ntfn rv rv'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q119 ntfnPtr tcba ntfn rv) (?Q'119 ntfnPtr tcba ntfn rv rv') [SKIP] (setBoundNotification (Some ntfnptr) tcb) (?d'119 ntfnPtr tcba ntfn rv')
 4. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?R119 ntfnPtr tcba ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. Some tcb) ntfn) \<lbrace>?Q119 ntfnPtr tcba ntfn\<rbrace>
 5. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'119 ntfnPtr tcba ntfn)
 6. \<And>ntfnPtr tcba. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q106 ntfnPtr tcba\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and tcb_at' tcb and ?R119 ntfnPtr tcba ntfn\<rbrace>
 7. \<And>ntfnPtr tcba s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; (invs' and tcb_at' tcb) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q106 ntfnPtr tcba s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (invs' and ko_at' rv ntfnptr and tcb_at' tcb and ?R119 ntfnPtr tcba 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>; tcb_at' tcb \<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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>_. Some tcb) 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>; tcb_at' tcb \<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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>; tcb_at' tcb \<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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>; tcb_at' tcb \<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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>; tcb_at' tcb \<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> obj_at' (?P176 ntfn \<sigma> x ko' t notification) ntfnptr \<sigma>
 6. \<And>ntfnPtr tcba ntfn rv' t t'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcba} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcba\<rightarrow>[''tcbBoundNotification_C''])) ntfnPtr)))) (?d'119 ntfnPtr tcba ntfn rv')
 7. \<And>ntfnPtr tcba ntfn rv rv'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q119 ntfnPtr tcba ntfn rv) (?Q'119 ntfnPtr tcba ntfn rv rv') [SKIP] (setBoundNotification (Some ntfnptr) tcb) (?d'119 ntfnPtr tcba ntfn rv')
 8. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?R119 ntfnPtr tcba ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. Some tcb) ntfn) \<lbrace>?Q119 ntfnPtr tcba ntfn\<rbrace>
 9. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'119 ntfnPtr tcba ntfn)
 10. \<And>ntfnPtr tcba. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q106 ntfnPtr tcba\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and tcb_at' tcb and ?R119 ntfnPtr tcba 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>; tcb_at' tcb \<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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>_. Some tcb) 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>; tcb_at' tcb \<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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>; tcb_at' tcb \<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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>; tcb_at' tcb \<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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>; tcb_at' tcb \<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> obj_at' (?P176 ntfn \<sigma> x ko' t notification) ntfnptr \<sigma>
 6. \<And>ntfnPtr tcba ntfn rv' t t'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcba} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcba\<rightarrow>[''tcbBoundNotification_C''])) ntfnPtr)))) (?d'119 ntfnPtr tcba ntfn rv')
 7. \<And>ntfnPtr tcba ntfn rv rv'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q119 ntfnPtr tcba ntfn rv) (?Q'119 ntfnPtr tcba ntfn rv rv') [SKIP] (setBoundNotification (Some ntfnptr) tcb) (?d'119 ntfnPtr tcba ntfn rv')
 8. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?R119 ntfnPtr tcba ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. Some tcb) ntfn) \<lbrace>?Q119 ntfnPtr tcba ntfn\<rbrace>
 9. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'119 ntfnPtr tcba ntfn)
 10. \<And>ntfnPtr tcba. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q106 ntfnPtr tcba\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and tcb_at' tcb and ?R119 ntfnPtr tcba 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>; tcb_at' tcb \<sigma>; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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>_. Some tcb) 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>; tcb_at' tcb \<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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>; tcb_at' tcb \<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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>; tcb_at' tcb \<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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>; tcb_at' tcb \<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> obj_at' (?P176 ntfn \<sigma> x ko' t notification) ntfnptr \<sigma>
 6. \<And>ntfnPtr tcba ntfn rv' t t'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcba} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcba\<rightarrow>[''tcbBoundNotification_C''])) ntfnPtr)))) (?d'119 ntfnPtr tcba ntfn rv')
 7. \<And>ntfnPtr tcba ntfn rv rv'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q119 ntfnPtr tcba ntfn rv) (?Q'119 ntfnPtr tcba ntfn rv rv') [SKIP] (setBoundNotification (Some ntfnptr) tcb) (?d'119 ntfnPtr tcba ntfn rv')
 8. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?R119 ntfnPtr tcba ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. Some tcb) ntfn) \<lbrace>?Q119 ntfnPtr tcba ntfn\<rbrace>
 9. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'119 ntfnPtr tcba ntfn)
 10. \<And>ntfnPtr tcba. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q106 ntfnPtr tcba\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and tcb_at' tcb and ?R119 ntfnPtr tcba 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>; tcb_at' tcb \<sigma>; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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>_. Some tcb) 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>; tcb_at' tcb \<sigma>; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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>; tcb_at' tcb \<sigma>; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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>; tcb_at' tcb \<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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>; tcb_at' tcb \<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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>; tcb_at' tcb \<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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>; tcb_at' tcb \<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> obj_at' (?P176 ntfn \<sigma> x ko' t notification) ntfnptr \<sigma>
 8. \<And>ntfnPtr tcba ntfn rv' t t'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcba} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcba\<rightarrow>[''tcbBoundNotification_C''])) ntfnPtr)))) (?d'119 ntfnPtr tcba ntfn rv')
 9. \<And>ntfnPtr tcba ntfn rv rv'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q119 ntfnPtr tcba ntfn rv) (?Q'119 ntfnPtr tcba ntfn rv rv') [SKIP] (setBoundNotification (Some ntfnptr) tcb) (?d'119 ntfnPtr tcba ntfn rv')
 10. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?R119 ntfnPtr tcba ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. Some tcb) ntfn) \<lbrace>?Q119 ntfnPtr tcba 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>; tcb_at' tcb \<sigma>; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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>_. Some tcb) ntfn) notification
 2. \<And>ntfn \<sigma> x ko' t notification. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; tcb_at' tcb \<sigma>; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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>; tcb_at' tcb \<sigma>; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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>; tcb_at' tcb \<sigma>; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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>; tcb_at' tcb \<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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>; tcb_at' tcb \<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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>; tcb_at' tcb \<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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>; tcb_at' tcb \<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> obj_at' (?P176 ntfn \<sigma> x ko' t notification) ntfnptr \<sigma>
 9. \<And>ntfnPtr tcba ntfn rv' t t'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcba} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcba\<rightarrow>[''tcbBoundNotification_C''])) ntfnPtr)))) (?d'119 ntfnPtr tcba ntfn rv')
 10. \<And>ntfnPtr tcba ntfn rv rv'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q119 ntfnPtr tcba ntfn rv) (?Q'119 ntfnPtr tcba ntfn rv rv') [SKIP] (setBoundNotification (Some ntfnptr) tcb) (?d'119 ntfnPtr tcba 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>; tcb_at' tcb \<sigma>; cslift x (ntfn_Ptr ntfnptr) = Some ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<rparr>))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift ko'\<lparr>ntfnBoundTCB_CL := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<rparr>))) | Structures_H.ntfn.ActiveNtfn msgid \<Rightarrow> notification_CL.state_CL (notification_lift ko'\<lparr>ntfnBoundTCB_CL := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<rparr>) = SCAST(32 signed \<rightarrow> 32) NtfnState_Active \<and> msgid = ntfnMsgIdentifier_CL (notification_lift ko'\<lparr>ntfnBoundTCB_CL := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<rparr>) \<and> ep_queue_relation' (cslift x) [] (tcb_Ptr (ntfnQueue_head_CL (notification_lift ko'\<lparr>ntfnBoundTCB_CL := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<rparr>))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift ko'\<lparr>ntfnBoundTCB_CL := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<rparr>))) | Structures_H.ntfn.WaitingNtfn q \<Rightarrow> notification_CL.state_CL (notification_lift ko'\<lparr>ntfnBoundTCB_CL := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<rparr>))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift ko'\<lparr>ntfnBoundTCB_CL := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<rparr>)))) \<and> option_to_ctcb_ptr (Some tcb) = tcb_Ptr (ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4)
 2. \<And>ntfn \<sigma> x ko' t notification. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; tcb_at' tcb \<sigma>; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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>; tcb_at' tcb \<sigma>; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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>; tcb_at' tcb \<sigma>; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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>; tcb_at' tcb \<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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>; tcb_at' tcb \<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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>; tcb_at' tcb \<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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>; tcb_at' tcb \<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> obj_at' (?P176 ntfn \<sigma> x ko' t notification) ntfnptr \<sigma>
 9. \<And>ntfnPtr tcba ntfn rv' t t'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcba} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcba\<rightarrow>[''tcbBoundNotification_C''])) ntfnPtr)))) (?d'119 ntfnPtr tcba ntfn rv')
 10. \<And>ntfnPtr tcba ntfn rv rv'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q119 ntfnPtr tcba ntfn rv) (?Q'119 ntfnPtr tcba ntfn rv rv') [SKIP] (setBoundNotification (Some ntfnptr) tcb) (?d'119 ntfnPtr tcba ntfn rv')
A total of 14 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>ntfn \<sigma> x ko' t notification. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; tcb_at' tcb \<sigma>; cslift x (ntfn_Ptr ntfnptr) = Some ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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')); ntfnObj ntfn = Structures_H.ntfn.IdleNtfn\<rbrakk> \<Longrightarrow> (case ntfnObj ntfn of Structures_H.ntfn.IdleNtfn \<Rightarrow> notification_CL.state_CL (notification_lift ko'\<lparr>ntfnBoundTCB_CL := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<rparr>))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift ko'\<lparr>ntfnBoundTCB_CL := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<rparr>))) | Structures_H.ntfn.ActiveNtfn msgid \<Rightarrow> notification_CL.state_CL (notification_lift ko'\<lparr>ntfnBoundTCB_CL := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<rparr>) = SCAST(32 signed \<rightarrow> 32) NtfnState_Active \<and> msgid = ntfnMsgIdentifier_CL (notification_lift ko'\<lparr>ntfnBoundTCB_CL := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<rparr>) \<and> ep_queue_relation' (cslift x) [] (tcb_Ptr (ntfnQueue_head_CL (notification_lift ko'\<lparr>ntfnBoundTCB_CL := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<rparr>))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift ko'\<lparr>ntfnBoundTCB_CL := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<rparr>))) | Structures_H.ntfn.WaitingNtfn q \<Rightarrow> notification_CL.state_CL (notification_lift ko'\<lparr>ntfnBoundTCB_CL := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<rparr>))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift ko'\<lparr>ntfnBoundTCB_CL := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<rparr>)))) \<and> option_to_ctcb_ptr (Some tcb) = tcb_Ptr (ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4)
 2. \<And>ntfn \<sigma> x ko' t notification x2. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; tcb_at' tcb \<sigma>; cslift x (ntfn_Ptr ntfnptr) = Some ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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')); ntfnObj ntfn = Structures_H.ntfn.ActiveNtfn x2\<rbrakk> \<Longrightarrow> (case ntfnObj ntfn of Structures_H.ntfn.IdleNtfn \<Rightarrow> notification_CL.state_CL (notification_lift ko'\<lparr>ntfnBoundTCB_CL := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<rparr>))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift ko'\<lparr>ntfnBoundTCB_CL := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<rparr>))) | Structures_H.ntfn.ActiveNtfn msgid \<Rightarrow> notification_CL.state_CL (notification_lift ko'\<lparr>ntfnBoundTCB_CL := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<rparr>) = SCAST(32 signed \<rightarrow> 32) NtfnState_Active \<and> msgid = ntfnMsgIdentifier_CL (notification_lift ko'\<lparr>ntfnBoundTCB_CL := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<rparr>) \<and> ep_queue_relation' (cslift x) [] (tcb_Ptr (ntfnQueue_head_CL (notification_lift ko'\<lparr>ntfnBoundTCB_CL := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<rparr>))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift ko'\<lparr>ntfnBoundTCB_CL := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<rparr>))) | Structures_H.ntfn.WaitingNtfn q \<Rightarrow> notification_CL.state_CL (notification_lift ko'\<lparr>ntfnBoundTCB_CL := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<rparr>))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift ko'\<lparr>ntfnBoundTCB_CL := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<rparr>)))) \<and> option_to_ctcb_ptr (Some tcb) = tcb_Ptr (ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4)
 3. \<And>ntfn \<sigma> x ko' t notification x3. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; tcb_at' tcb \<sigma>; cslift x (ntfn_Ptr ntfnptr) = Some ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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')); ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3\<rbrakk> \<Longrightarrow> (case ntfnObj ntfn of Structures_H.ntfn.IdleNtfn \<Rightarrow> notification_CL.state_CL (notification_lift ko'\<lparr>ntfnBoundTCB_CL := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<rparr>))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift ko'\<lparr>ntfnBoundTCB_CL := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<rparr>))) | Structures_H.ntfn.ActiveNtfn msgid \<Rightarrow> notification_CL.state_CL (notification_lift ko'\<lparr>ntfnBoundTCB_CL := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<rparr>) = SCAST(32 signed \<rightarrow> 32) NtfnState_Active \<and> msgid = ntfnMsgIdentifier_CL (notification_lift ko'\<lparr>ntfnBoundTCB_CL := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<rparr>) \<and> ep_queue_relation' (cslift x) [] (tcb_Ptr (ntfnQueue_head_CL (notification_lift ko'\<lparr>ntfnBoundTCB_CL := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<rparr>))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift ko'\<lparr>ntfnBoundTCB_CL := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<rparr>))) | Structures_H.ntfn.WaitingNtfn q \<Rightarrow> notification_CL.state_CL (notification_lift ko'\<lparr>ntfnBoundTCB_CL := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<rparr>))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift ko'\<lparr>ntfnBoundTCB_CL := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<rparr>)))) \<and> option_to_ctcb_ptr (Some tcb) = tcb_Ptr (ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4)
 4. \<And>ntfn \<sigma> x ko' t notification. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; tcb_at' tcb \<sigma>; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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>
 5. \<And>ntfn \<sigma> x ko' t notification. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; tcb_at' tcb \<sigma>; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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>)
 6. \<And>ntfn \<sigma> x ko' t notification. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; tcb_at' tcb \<sigma>; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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>)
 7. \<And>ntfn \<sigma> x ko' t notification val old ptr ptr' next. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; tcb_at' tcb \<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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
 8. \<And>ntfn \<sigma> x ko' t notification v. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; tcb_at' tcb \<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> 1 < 2 ^ objBits v
 9. \<And>ntfn \<sigma> x ko' t notification v v'. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; tcb_at' tcb \<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> objBits v = objBits v'
 10. \<And>ntfn \<sigma> x ko' t notification. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; tcb_at' tcb \<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> obj_at' (?P176 ntfn \<sigma> x ko' t notification) ntfnptr \<sigma>
A total of 16 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>ntfn \<sigma> x ko' t notification. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; tcb_at' tcb \<sigma>; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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>; tcb_at' tcb \<sigma>; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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>; tcb_at' tcb \<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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>; tcb_at' tcb \<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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>; tcb_at' tcb \<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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>; tcb_at' tcb \<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> obj_at' (?P176 ntfn \<sigma> x ko' t notification) ntfnptr \<sigma>
 7. \<And>ntfnPtr tcba ntfn rv' t t'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcba} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcba\<rightarrow>[''tcbBoundNotification_C''])) ntfnPtr)))) (?d'119 ntfnPtr tcba ntfn rv')
 8. \<And>ntfnPtr tcba ntfn rv rv'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q119 ntfnPtr tcba ntfn rv) (?Q'119 ntfnPtr tcba ntfn rv rv') [SKIP] (setBoundNotification (Some ntfnptr) tcb) (?d'119 ntfnPtr tcba ntfn rv')
 9. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?R119 ntfnPtr tcba ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. Some tcb) ntfn) \<lbrace>?Q119 ntfnPtr tcba ntfn\<rbrace>
 10. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'119 ntfnPtr tcba ntfn)
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>ntfn \<sigma> x ko' t notification. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; tcb_at' tcb \<sigma>; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>ntfnBoundTCB_CL := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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>; tcb_at' tcb \<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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>; tcb_at' tcb \<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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>; tcb_at' tcb \<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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>; tcb_at' tcb \<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> obj_at' (?P176 ntfn \<sigma> x ko' t notification) ntfnptr \<sigma>
 6. \<And>ntfnPtr tcba ntfn rv' t t'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcba} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcba\<rightarrow>[''tcbBoundNotification_C''])) ntfnPtr)))) (?d'119 ntfnPtr tcba ntfn rv')
 7. \<And>ntfnPtr tcba ntfn rv rv'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q119 ntfnPtr tcba ntfn rv) (?Q'119 ntfnPtr tcba ntfn rv rv') [SKIP] (setBoundNotification (Some ntfnptr) tcb) (?d'119 ntfnPtr tcba ntfn rv')
 8. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?R119 ntfnPtr tcba ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. Some tcb) ntfn) \<lbrace>?Q119 ntfnPtr tcba ntfn\<rbrace>
 9. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'119 ntfnPtr tcba ntfn)
 10. \<And>ntfnPtr tcba. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q106 ntfnPtr tcba\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and tcb_at' tcb and ?R119 ntfnPtr tcba ntfn\<rbrace>
A total of 11 subgoals... 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>; tcb_at' tcb \<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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>; tcb_at' tcb \<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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>; tcb_at' tcb \<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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>; tcb_at' tcb \<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> obj_at' (?P176 ntfn \<sigma> x ko' t notification) ntfnptr \<sigma>
 5. \<And>ntfnPtr tcba ntfn rv' t t'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcba} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcba\<rightarrow>[''tcbBoundNotification_C''])) ntfnPtr)))) (?d'119 ntfnPtr tcba ntfn rv')
 6. \<And>ntfnPtr tcba ntfn rv rv'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q119 ntfnPtr tcba ntfn rv) (?Q'119 ntfnPtr tcba ntfn rv rv') [SKIP] (setBoundNotification (Some ntfnptr) tcb) (?d'119 ntfnPtr tcba ntfn rv')
 7. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?R119 ntfnPtr tcba ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. Some tcb) ntfn) \<lbrace>?Q119 ntfnPtr tcba ntfn\<rbrace>
 8. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'119 ntfnPtr tcba ntfn)
 9. \<And>ntfnPtr tcba. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q106 ntfnPtr tcba\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and tcb_at' tcb and ?R119 ntfnPtr tcba ntfn\<rbrace>
 10. \<And>ntfnPtr tcba s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; (invs' and tcb_at' tcb) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q106 ntfnPtr tcba s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (invs' and ko_at' rv ntfnptr and tcb_at' tcb and ?R119 ntfnPtr tcba rv) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (9 subgoals):
 1. \<And>ntfn \<sigma> x ko' t notification v. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; tcb_at' tcb \<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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>; tcb_at' tcb \<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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>; tcb_at' tcb \<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> obj_at' (?P176 ntfn \<sigma> x ko' t notification) ntfnptr \<sigma>
 4. \<And>ntfnPtr tcba ntfn rv' t t'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcba} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcba\<rightarrow>[''tcbBoundNotification_C''])) ntfnPtr)))) (?d'119 ntfnPtr tcba ntfn rv')
 5. \<And>ntfnPtr tcba ntfn rv rv'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q119 ntfnPtr tcba ntfn rv) (?Q'119 ntfnPtr tcba ntfn rv rv') [SKIP] (setBoundNotification (Some ntfnptr) tcb) (?d'119 ntfnPtr tcba ntfn rv')
 6. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?R119 ntfnPtr tcba ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. Some tcb) ntfn) \<lbrace>?Q119 ntfnPtr tcba ntfn\<rbrace>
 7. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'119 ntfnPtr tcba ntfn)
 8. \<And>ntfnPtr tcba. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q106 ntfnPtr tcba\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and tcb_at' tcb and ?R119 ntfnPtr tcba ntfn\<rbrace>
 9. \<And>ntfnPtr tcba s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; (invs' and tcb_at' tcb) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q106 ntfnPtr tcba s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (invs' and ko_at' rv ntfnptr and tcb_at' tcb and ?R119 ntfnPtr tcba rv) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (8 subgoals):
 1. \<And>ntfn \<sigma> x ko' t notification v v'. \<lbrakk>invs' \<sigma>; ko_at' ntfn ntfnptr \<sigma>; tcb_at' tcb \<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<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>; tcb_at' tcb \<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> obj_at' (?P176 ntfn \<sigma> x ko' t notification) ntfnptr \<sigma>
 3. \<And>ntfnPtr tcba ntfn rv' t t'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcba} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcba\<rightarrow>[''tcbBoundNotification_C''])) ntfnPtr)))) (?d'119 ntfnPtr tcba ntfn rv')
 4. \<And>ntfnPtr tcba ntfn rv rv'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q119 ntfnPtr tcba ntfn rv) (?Q'119 ntfnPtr tcba ntfn rv rv') [SKIP] (setBoundNotification (Some ntfnptr) tcb) (?d'119 ntfnPtr tcba ntfn rv')
 5. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?R119 ntfnPtr tcba ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. Some tcb) ntfn) \<lbrace>?Q119 ntfnPtr tcba ntfn\<rbrace>
 6. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'119 ntfnPtr tcba ntfn)
 7. \<And>ntfnPtr tcba. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q106 ntfnPtr tcba\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and tcb_at' tcb and ?R119 ntfnPtr tcba ntfn\<rbrace>
 8. \<And>ntfnPtr tcba s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; (invs' and tcb_at' tcb) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q106 ntfnPtr tcba s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (invs' and ko_at' rv ntfnptr and tcb_at' tcb and ?R119 ntfnPtr tcba 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>; tcb_at' tcb \<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 := ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask 4\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> obj_at' (?P176 ntfn \<sigma> x ko' t notification) ntfnptr \<sigma>
 2. \<And>ntfnPtr tcba ntfn rv' t t'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcba} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcba\<rightarrow>[''tcbBoundNotification_C''])) ntfnPtr)))) (?d'119 ntfnPtr tcba ntfn rv')
 3. \<And>ntfnPtr tcba ntfn rv rv'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q119 ntfnPtr tcba ntfn rv) (?Q'119 ntfnPtr tcba ntfn rv rv') [SKIP] (setBoundNotification (Some ntfnptr) tcb) (?d'119 ntfnPtr tcba ntfn rv')
 4. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?R119 ntfnPtr tcba ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. Some tcb) ntfn) \<lbrace>?Q119 ntfnPtr tcba ntfn\<rbrace>
 5. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'119 ntfnPtr tcba ntfn)
 6. \<And>ntfnPtr tcba. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q106 ntfnPtr tcba\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and tcb_at' tcb and ?R119 ntfnPtr tcba ntfn\<rbrace>
 7. \<And>ntfnPtr tcba s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; (invs' and tcb_at' tcb) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q106 ntfnPtr tcba s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (invs' and ko_at' rv ntfnptr and tcb_at' tcb and ?R119 ntfnPtr tcba rv) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (6 subgoals):
 1. \<And>ntfnPtr tcba ntfn rv' t t'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcba} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcba\<rightarrow>[''tcbBoundNotification_C''])) ntfnPtr)))) (?d'119 ntfnPtr tcba ntfn rv')
 2. \<And>ntfnPtr tcba ntfn rv rv'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q119 ntfnPtr tcba ntfn rv) (?Q'119 ntfnPtr tcba ntfn rv rv') [SKIP] (setBoundNotification (Some ntfnptr) tcb) (?d'119 ntfnPtr tcba ntfn rv')
 3. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?R119 ntfnPtr tcba ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. Some tcb) ntfn) \<lbrace>?Q119 ntfnPtr tcba ntfn\<rbrace>
 4. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'119 ntfnPtr tcba ntfn)
 5. \<And>ntfnPtr tcba. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q106 ntfnPtr tcba\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and tcb_at' tcb and ?R119 ntfnPtr tcba ntfn\<rbrace>
 6. \<And>ntfnPtr tcba s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; (invs' and tcb_at' tcb) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q106 ntfnPtr tcba s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (invs' and ko_at' rv ntfnptr and tcb_at' tcb and ?R119 ntfnPtr tcba rv) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (5 subgoals):
 1. \<And>ntfnPtr tcba ntfn rv rv'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q119 ntfnPtr tcba ntfn rv) (?Q'119 ntfnPtr tcba ntfn rv rv') [SKIP] (setBoundNotification (Some ntfnptr) tcb) (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcba} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcba\<rightarrow>[''tcbBoundNotification_C''])) ntfnPtr))))
 2. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?R119 ntfnPtr tcba ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. Some tcb) ntfn) \<lbrace>?Q119 ntfnPtr tcba ntfn\<rbrace>
 3. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'119 ntfnPtr tcba ntfn)
 4. \<And>ntfnPtr tcba. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q106 ntfnPtr tcba\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and tcb_at' tcb and ?R119 ntfnPtr tcba ntfn\<rbrace>
 5. \<And>ntfnPtr tcba s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; (invs' and tcb_at' tcb) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q106 ntfnPtr tcba s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (invs' and ko_at' rv ntfnptr and tcb_at' tcb and ?R119 ntfnPtr tcba rv) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (5 subgoals):
 1. \<And>ntfnPtr tcba ntfn rv rv'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?A273 ntfnPtr tcba ntfn rv) (?C'272 ntfnPtr tcba ntfn rv rv') [SKIP] (setBoundNotification (Some ntfnptr) tcb) (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcba\<rightarrow>[''tcbBoundNotification_C''])) ntfnPtr)))
 2. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?R119 ntfnPtr tcba ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. Some tcb) ntfn) \<lbrace>\<lambda>rv. ?A273 ntfnPtr tcba ntfn rv and tcb_at' (ctcb_ptr_to_tcb_ptr tcba)\<rbrace>
 3. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>rv rv'. ?C'272 ntfnPtr tcba ntfn rv rv' \<inter> \<lbrace>True\<rbrace>)
 4. \<And>ntfnPtr tcba. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q106 ntfnPtr tcba\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and tcb_at' tcb and ?R119 ntfnPtr tcba ntfn\<rbrace>
 5. \<And>ntfnPtr tcba s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; (invs' and tcb_at' tcb) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q106 ntfnPtr tcba s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (invs' and ko_at' rv ntfnptr and tcb_at' tcb and ?R119 ntfnPtr tcba rv) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (5 subgoals):
 1. \<And>ntfnPtr tcba ntfn rv'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?A273 (ntfn_Ptr ntfnptr) (tcb_ptr_to_ctcb_ptr tcb) ntfn ()) (?C'272 (ntfn_Ptr ntfnptr) (tcb_ptr_to_ctcb_ptr tcb) ntfn () rv') [SKIP] (threadSet (tcbBoundNotification_update (\<lambda>_. Some ntfnptr)) tcb) (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcb_ptr_to_ctcb_ptr tcb\<rightarrow>[''tcbBoundNotification_C''])) (ntfn_Ptr ntfnptr))))
 2. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?R119 ntfnPtr tcba ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. Some tcb) ntfn) \<lbrace>\<lambda>rv. ?A273 ntfnPtr tcba ntfn rv and tcb_at' (ctcb_ptr_to_tcb_ptr tcba)\<rbrace>
 3. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>rv rv'. ?C'272 ntfnPtr tcba ntfn rv rv' \<inter> \<lbrace>True\<rbrace>)
 4. \<And>ntfnPtr tcba. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q106 ntfnPtr tcba\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and tcb_at' tcb and ?R119 ntfnPtr tcba ntfn\<rbrace>
 5. \<And>ntfnPtr tcba s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; (invs' and tcb_at' tcb) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q106 ntfnPtr tcba s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (invs' and ko_at' rv ntfnptr and tcb_at' tcb and ?R119 ntfnPtr tcba rv) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (6 subgoals):
 1. \<And>ntfnPtr tcba ntfn rv' s tcbb. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q285 ntfnPtr tcba ntfn rv' s tcbb) \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcb_ptr_to_ctcb_ptr tcb\<rightarrow>[''tcbBoundNotification_C''])) (ntfn_Ptr ntfnptr))) {s'. (s\<lparr>ksPSpace := (ksPSpace s)(tcb \<mapsto> injectKOS (tcbBoundNotification_update (\<lambda>_. Some ntfnptr) tcbb))\<rparr>, s') \<in> rf_sr}
 2. \<And>ntfnPtr tcba ntfn rv' s s' tcbb tcb'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; True; ko_at' tcbb tcb s; cslift s' (tcb_ptr_to_ctcb_ptr tcb) = Some tcb'; ctcb_relation tcbb tcb'; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> s' \<in> ?Q285 ntfnPtr tcba ntfn rv' s tcbb
 3. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?R119 ntfnPtr tcba ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. Some tcb) ntfn) \<lbrace>\<lambda>rv. tcb_at' tcb and (\<lambda>_. True) and tcb_at' (ctcb_ptr_to_tcb_ptr tcba)\<rbrace>
 4. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>rv rv'. UNIV \<inter> \<lbrace>True\<rbrace>)
 5. \<And>ntfnPtr tcba. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q106 ntfnPtr tcba\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and tcb_at' tcb and ?R119 ntfnPtr tcba ntfn\<rbrace>
 6. \<And>ntfnPtr tcba s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; (invs' and tcb_at' tcb) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q106 ntfnPtr tcba s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (invs' and ko_at' rv ntfnptr and tcb_at' tcb and ?R119 ntfnPtr tcba rv) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (5 subgoals):
 1. \<And>ntfnPtr tcba ntfn rv' s s' tcbb tcb'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; True; ko_at' tcbb tcb s; cslift s' (tcb_ptr_to_ctcb_ptr tcb) = Some tcb'; ctcb_relation tcbb tcb'; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> s' \<in> {sa. (s\<lparr>ksPSpace := (ksPSpace s)(tcb \<mapsto> injectKOS (tcbBoundNotification_update (\<lambda>_. Some ntfnptr) tcbb))\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcb_ptr_to_ctcb_ptr tcb\<rightarrow>[''tcbBoundNotification_C''])) (ntfn_Ptr ntfnptr)))) sa) \<in> rf_sr}
 2. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?R119 ntfnPtr tcba ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. Some tcb) ntfn) \<lbrace>\<lambda>rv. tcb_at' tcb and (\<lambda>_. True) and tcb_at' (ctcb_ptr_to_tcb_ptr tcba)\<rbrace>
 3. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>rv rv'. UNIV \<inter> \<lbrace>True\<rbrace>)
 4. \<And>ntfnPtr tcba. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q106 ntfnPtr tcba\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and tcb_at' tcb and ?R119 ntfnPtr tcba ntfn\<rbrace>
 5. \<And>ntfnPtr tcba s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; (invs' and tcb_at' tcb) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q106 ntfnPtr tcba s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (invs' and ko_at' rv ntfnptr and tcb_at' tcb and ?R119 ntfnPtr tcba rv) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (5 subgoals):
 1. \<And>ntfnPtr tcba s s' tcbb tcb'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; ko_at' tcbb tcb s; cslift s' (tcb_ptr_to_ctcb_ptr tcb) = Some tcb'; ctcb_relation tcbb tcb'\<rbrakk> \<Longrightarrow> (s\<lparr>ksPSpace := (ksPSpace s)(tcb \<mapsto> KOTCB (tcbBoundNotification_update (\<lambda>_. Some ntfnptr) tcbb))\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(notification_C ptr) &(tcb_ptr_to_ctcb_ptr tcb\<rightarrow>[''tcbBoundNotification_C''])) (ntfn_Ptr ntfnptr)))) s') \<in> rf_sr
 2. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?R119 ntfnPtr tcba ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. Some tcb) ntfn) \<lbrace>\<lambda>rv. tcb_at' tcb and (\<lambda>_. True) and tcb_at' (ctcb_ptr_to_tcb_ptr tcba)\<rbrace>
 3. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>rv rv'. UNIV \<inter> \<lbrace>True\<rbrace>)
 4. \<And>ntfnPtr tcba. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q106 ntfnPtr tcba\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and tcb_at' tcb and ?R119 ntfnPtr tcba ntfn\<rbrace>
 5. \<And>ntfnPtr tcba s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; (invs' and tcb_at' tcb) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q106 ntfnPtr tcba s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (invs' and ko_at' rv ntfnptr and tcb_at' tcb and ?R119 ntfnPtr tcba rv) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (5 subgoals):
 1. \<And>ntfnPtr tcba s s' tcbb tcb'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb; ko_at' tcbb tcb s; cslift s' (tcb_ptr_to_ctcb_ptr tcb) = Some tcb'; ctcb_relation tcbb tcb'\<rbrakk> \<Longrightarrow> ctcb_relation (tcbBoundNotification_update (\<lambda>_. Some ntfnptr) tcbb) (tcbBoundNotification_C_update (\<lambda>_. ntfn_Ptr ntfnptr) tcb')
 2. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?R119 ntfnPtr tcba ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. Some tcb) ntfn) \<lbrace>\<lambda>rv. tcb_at' tcb and (\<lambda>_. True) and tcb_at' (ctcb_ptr_to_tcb_ptr tcba)\<rbrace>
 3. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>rv rv'. UNIV \<inter> \<lbrace>True\<rbrace>)
 4. \<And>ntfnPtr tcba. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q106 ntfnPtr tcba\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and tcb_at' tcb and ?R119 ntfnPtr tcba ntfn\<rbrace>
 5. \<And>ntfnPtr tcba s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; (invs' and tcb_at' tcb) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q106 ntfnPtr tcba s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (invs' and ko_at' rv ntfnptr and tcb_at' tcb and ?R119 ntfnPtr tcba rv) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (4 subgoals):
 1. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?R119 ntfnPtr tcba ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. Some tcb) ntfn) \<lbrace>\<lambda>rv. tcb_at' tcb and (\<lambda>_. True) and tcb_at' (ctcb_ptr_to_tcb_ptr tcba)\<rbrace>
 2. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>rv rv'. UNIV \<inter> \<lbrace>True\<rbrace>)
 3. \<And>ntfnPtr tcba. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q106 ntfnPtr tcba\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and tcb_at' tcb and ?R119 ntfnPtr tcba ntfn\<rbrace>
 4. \<And>ntfnPtr tcba s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; (invs' and tcb_at' tcb) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q106 ntfnPtr tcba s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (invs' and ko_at' rv ntfnptr and tcb_at' tcb and ?R119 ntfnPtr tcba rv) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (4 subgoals):
 1. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?R119 (ntfn_Ptr ntfnptr) (tcb_ptr_to_ctcb_ptr tcb) ntfn\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. Some tcb) ntfn) \<lbrace>\<lambda>rv. tcb_at' tcb\<rbrace>
 2. \<And>ntfnPtr tcba ntfn. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>rv rv'. UNIV \<inter> \<lbrace>True\<rbrace>)
 3. \<And>ntfnPtr tcba. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q106 ntfnPtr tcba\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfn. invs' and ko_at' ntfn ntfnptr and tcb_at' tcb and ?R119 ntfnPtr tcba ntfn\<rbrace>
 4. \<And>ntfnPtr tcba s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfnptr; tcba = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; (invs' and tcb_at' tcb) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q106 ntfnPtr tcba s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (invs' and ko_at' rv ntfnptr and tcb_at' tcb and ?R119 ntfnPtr tcba rv) s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal:
No subgoals!