theory Tcb_C

lemma decodeUnbindNotification_ccorres:
  "ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
       (invs' and (\<lambda>s. ksCurThread s = thread) and ct_active' and sch_act_simple
              and valid_cap' cp and K (isThreadCap cp)
              and tcb_at' (capTCBPtr cp)
              and (\<lambda>s. \<forall>rf \<in> zobj_refs' cp. ex_nonz_cap_to' rf s))
       (UNIV \<inter> {s. ccap_relation cp (cap_' s)}) []
     (decodeUnbindNotification cp >>= invocationCatch thread isBlocking isCall InvokeTCB)
     (Call decodeUnbindNotification_'proc)" apply (cinit' lift: cap_' simp: decodeUnbindNotification_def) apply csymbr apply csymbr apply (rule ccorres_Guard_Seq) apply (simp add: liftE_bindE bind_assoc) apply (rule ccorres_pre_getBoundNotification) apply (rule_tac P="\<lambda>s. ntfn \<noteq> Some 0" in ccorres_cross_over_guard) apply (simp add: bindE_bind_linearise) apply wpc apply (simp add: bindE_bind_linearise[symmetric]
                     injection_handler_throwError
                     invocationCatch_use_injection_handler) apply (rule ccorres_cond_true_seq) apply (rule ccorres_from_vcg_split_throws[where P=\<top> and P'=UNIV]) apply vcg apply (rule conseqPre, vcg) apply (clarsimp simp: throwError_def return_def syscall_error_rel_def
                         syscall_error_to_H_cases exception_defs) apply (simp add: returnOk_bind ccorres_invocationCatch_Inr
                     performInvocation_def) apply (rule ccorres_cond_false_seq) apply simp apply (ctac add: setThreadState_ccorres) apply (ctac add: invokeTCB_NotificationControl_unbind_ccorres) apply simp apply (rule ccorres_alternative2) apply (rule ccorres_return_CE, simp+)[1] apply (rule ccorres_return_C_errorE, simp+)[1] apply wp apply (vcg exspec=invokeTCB_NotificationControl_modifies) apply simp apply (wp sts_invs_minor' hoare_case_option_wp sts_bound_tcb_at' | wpc | simp)+ apply (vcg exspec=setThreadState_modifies) apply (clarsimp, frule obj_at_ko_at', clarsimp) apply (rule cmap_relationE1[OF cmap_relation_tcb], assumption) apply (erule ko_at_projectKO_opt) apply (clarsimp simp: isCap_simps) apply (frule cap_get_tag_isCap_unfolded_H_cap) apply (auto simp: ctcb_relation_def typ_heap_simps cap_get_tag_ThreadCap ct_in_state'_def
                         option_to_ptr_def option_to_0_def ThreadState_Restart_def
                         mask_def rf_sr_ksCurThread valid_tcb_state'_def
                  elim!: pred_tcb'_weakenE
                  dest!: valid_objs_boundNTFN_NULL) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (invs' and (\<lambda>s. ksCurThread s = thread) and ct_active' and sch_act_simple and valid_cap' cp and K (isThreadCap cp) and tcb_at' (capTCBPtr cp) and (\<lambda>s. \<forall>rf\<in>zobj_refs' cp. ex_nonz_cap_to' rf s)) (UNIV \<inter> \<lbrace>ccap_relation cp \<acute>cap\<rbrace>) [] (decodeUnbindNotification cp >>= invocationCatch thread isBlocking isCall Invocations_H.invocation.InvokeTCB) (Call decodeUnbindNotification_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>cap. ccap_relation cp cap \<Longrightarrow> ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q414 cap) (?Q'414 cap) [SKIP] (doE ntfn <- liftE (getBoundNotification (capTCBPtr cp));
y <- case ntfn of None \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation | Some v15 \<Rightarrow> returnOk ();
returnOk (tcbinvocation.NotificationControl (capTCBPtr cp) None)
odE >>= invocationCatch thread isBlocking isCall Invocations_H.invocation.InvokeTCB) (\<acute>ret__unsigned :== CALL cap_thread_cap_get_capTCBPtr_'proc(cap);;
(\<acute>tcb :== tcb_Ptr \<acute>ret__unsigned;;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_' s} (IF h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(\<acute>tcb\<rightarrow>[''tcbBoundNotification_C''])) = NULL THEN
  \<acute>current_syscall_error :== type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_IllegalOperation) \<acute>current_syscall_error;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR)
FI);;
(CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
(\<acute>ret__unsigned_long :== CALL invokeTCB_NotificationControl_'proc(\<acute>tcb,PTR_COERCE(unit \<rightarrow> notification_C) (PTR(unit) (SCAST(32 signed \<rightarrow> 32) 0)));;
return_C ret__unsigned_long_'_update ret__unsigned_long_')))))
 2. \<And>cap s s'. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. ksCurThread s = thread) and ct_active' and sch_act_simple and valid_cap' cp and (\<lambda>y. isThreadCap cp) and tcb_at' (capTCBPtr cp) and (\<lambda>s. \<forall>rf\<in>zobj_refs' cp. ex_nonz_cap_to' rf s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q414 cap s \<and> s' \<in> ?Q'414 cap proof (prove)
goal (2 subgoals):
 1. \<And>cap ret__unsigned. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)\<rbrakk> \<Longrightarrow> ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q414 cap) (?G'423 cap ret__unsigned) [SKIP] (doE ntfn <- liftE (getBoundNotification (capTCBPtr cp));
y <- case ntfn of None \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation | Some v15 \<Rightarrow> returnOk ();
returnOk (tcbinvocation.NotificationControl (capTCBPtr cp) None)
odE >>= invocationCatch thread isBlocking isCall Invocations_H.invocation.InvokeTCB) (\<acute>tcb :== tcb_Ptr ret__unsigned;;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_' s} (IF h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(\<acute>tcb\<rightarrow>[''tcbBoundNotification_C''])) = NULL THEN
  \<acute>current_syscall_error :== type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_IllegalOperation) \<acute>current_syscall_error;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR)
FI);;
(CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
(\<acute>ret__unsigned_long :== CALL invokeTCB_NotificationControl_'proc(\<acute>tcb,PTR_COERCE(unit \<rightarrow> notification_C) (PTR(unit) (SCAST(32 signed \<rightarrow> 32) 0)));;
return_C ret__unsigned_long_'_update ret__unsigned_long_'))))
 2. \<And>cap s s'. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. ksCurThread s = thread) and ct_active' and sch_act_simple and valid_cap' cp and (\<lambda>y. isThreadCap cp) and tcb_at' (capTCBPtr cp) and (\<lambda>s. \<forall>rf\<in>zobj_refs' cp. ex_nonz_cap_to' rf s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q414 cap s \<and> s' \<in> {s. \<forall>v v'. v = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift (cap_' (cap_'_update (\<lambda>_. cap) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> ?G'423 cap v}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap) s)) = SCAST(32 signed \<rightarrow> 32) cap_thread_cap} proof (prove)
goal (2 subgoals):
 1. \<And>cap ret__unsigned. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)\<rbrakk> \<Longrightarrow> ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q414 cap) (?G'583 cap ret__unsigned) [SKIP] (doE ntfn <- liftE (getBoundNotification (capTCBPtr cp));
y <- case ntfn of None \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation | Some v15 \<Rightarrow> returnOk ();
returnOk (tcbinvocation.NotificationControl (capTCBPtr cp) None)
odE >>= invocationCatch thread isBlocking isCall Invocations_H.invocation.InvokeTCB) (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_Ptr ret__unsigned} (IF h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcb_Ptr ret__unsigned\<rightarrow>[''tcbBoundNotification_C''])) = NULL THEN
  \<acute>current_syscall_error :== type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_IllegalOperation) \<acute>current_syscall_error;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR)
FI);;
(CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
(\<acute>ret__unsigned_long :== CALL invokeTCB_NotificationControl_'proc(tcb_Ptr ret__unsigned,PTR_COERCE(unit \<rightarrow> notification_C) (PTR(unit) (SCAST(32 signed \<rightarrow> 32) 0)));;
return_C ret__unsigned_long_'_update ret__unsigned_long_')))
 2. \<And>cap s s'. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. ksCurThread s = thread) and ct_active' and sch_act_simple and valid_cap' cp and (\<lambda>y. isThreadCap cp) and tcb_at' (capTCBPtr cp) and (\<lambda>s. \<forall>rf\<in>zobj_refs' cp. ex_nonz_cap_to' rf s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q414 cap s \<and> s' \<in> {s. \<forall>v v'. v = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift (cap_' (cap_'_update (\<lambda>_. cap) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. tcb_'_update (\<lambda>_. tcb_Ptr v) s \<in> ?G'583 cap v}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap) s)) = SCAST(32 signed \<rightarrow> 32) cap_thread_cap} proof (prove)
goal (2 subgoals):
 1. \<And>cap ret__unsigned. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)\<rbrakk> \<Longrightarrow> ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q414 cap) (?C'724 cap ret__unsigned) [SKIP] (doE ntfn <- liftE (getBoundNotification (capTCBPtr cp));
y <- case ntfn of None \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation | Some v15 \<Rightarrow> returnOk ();
returnOk (tcbinvocation.NotificationControl (capTCBPtr cp) None)
odE >>= invocationCatch thread isBlocking isCall Invocations_H.invocation.InvokeTCB) (IF h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcb_Ptr ret__unsigned\<rightarrow>[''tcbBoundNotification_C''])) = NULL THEN
  \<acute>current_syscall_error :== type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_IllegalOperation) \<acute>current_syscall_error;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR)
FI;;
(CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
(\<acute>ret__unsigned_long :== CALL invokeTCB_NotificationControl_'proc(tcb_Ptr ret__unsigned,PTR_COERCE(unit \<rightarrow> notification_C) (PTR(unit) (SCAST(32 signed \<rightarrow> 32) 0)));;
return_C ret__unsigned_long_'_update ret__unsigned_long_')))
 2. \<And>cap s s'. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. ksCurThread s = thread) and ct_active' and sch_act_simple and valid_cap' cp and (\<lambda>y. isThreadCap cp) and tcb_at' (capTCBPtr cp) and (\<lambda>s. \<forall>rf\<in>zobj_refs' cp. ex_nonz_cap_to' rf s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q414 cap s \<and> s' \<in> {s. \<forall>v v'. v = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift (cap_' (cap_'_update (\<lambda>_. cap) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. tcb_'_update (\<lambda>_. tcb_Ptr v) s \<in> ?C'724 cap v \<inter> {s. s \<Turnstile>\<^sub>c tcb_Ptr v}}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap) s)) = SCAST(32 signed \<rightarrow> 32) cap_thread_cap} proof (prove)
goal (2 subgoals):
 1. \<And>cap ret__unsigned. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)\<rbrakk> \<Longrightarrow> ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q414 cap) (?C'724 cap (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap))) [SKIP] (do ntfn <- getBoundNotification (capTCBPtr cp);
doE y <- case ntfn of None \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation | Some v15 \<Rightarrow> returnOk ();
returnOk (tcbinvocation.NotificationControl (capTCBPtr cp) None)
odE >>= invocationCatch thread isBlocking isCall Invocations_H.invocation.InvokeTCB
od) (IF h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap))\<rightarrow>[''tcbBoundNotification_C''])) = NULL THEN
  \<acute>current_syscall_error :== type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_IllegalOperation) \<acute>current_syscall_error;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR)
FI;;
(CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
(\<acute>ret__unsigned_long :== CALL invokeTCB_NotificationControl_'proc(tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)),NULL);;
return_C ret__unsigned_long_'_update ret__unsigned_long_')))
 2. \<And>cap s s'. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. ksCurThread s = thread) and ct_active' and sch_act_simple and valid_cap' cp and (\<lambda>y. isThreadCap cp) and tcb_at' (capTCBPtr cp) and (\<lambda>s. \<forall>rf\<in>zobj_refs' cp. ex_nonz_cap_to' rf s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q414 cap s \<and> s' \<in> {s. \<forall>v v'. v = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift (cap_' (cap_'_update (\<lambda>_. cap) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. tcb_'_update (\<lambda>_. tcb_Ptr v) s \<in> ?C'724 cap v \<inter> {s. s \<Turnstile>\<^sub>c tcb_Ptr v}}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap) s)) = SCAST(32 signed \<rightarrow> 32) cap_thread_cap} proof (prove)
goal (2 subgoals):
 1. \<And>cap ret__unsigned ntfn. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)\<rbrakk> \<Longrightarrow> ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?P736 cap ntfn) (?P'735 cap ntfn) [SKIP] (doE y <- case ntfn of None \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation | Some v15 \<Rightarrow> returnOk ();
returnOk (tcbinvocation.NotificationControl (capTCBPtr cp) None)
odE >>= invocationCatch thread isBlocking isCall Invocations_H.invocation.InvokeTCB) (IF h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap))\<rightarrow>[''tcbBoundNotification_C''])) = NULL THEN
  \<acute>current_syscall_error :== type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_IllegalOperation) \<acute>current_syscall_error;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR)
FI;;
(CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
(\<acute>ret__unsigned_long :== CALL invokeTCB_NotificationControl_'proc(tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)),NULL);;
return_C ret__unsigned_long_'_update ret__unsigned_long_')))
 2. \<And>cap s s'. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. ksCurThread s = thread) and ct_active' and sch_act_simple and valid_cap' cp and (\<lambda>y. isThreadCap cp) and tcb_at' (capTCBPtr cp) and (\<lambda>s. \<forall>rf\<in>zobj_refs' cp. ex_nonz_cap_to' rf s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb (capTCBPtr cp) s \<longrightarrow> ?P736 cap (tcbBoundNotification tcb) s) \<and> s' \<in> {s. \<forall>v v'. v = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift (cap_' (cap_'_update (\<lambda>_. cap) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. tcb_'_update (\<lambda>_. tcb_Ptr v) s \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr (capTCBPtr cp)) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> ?P'734 cap v tcb} \<inter> {s. s \<Turnstile>\<^sub>c tcb_Ptr v}}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap) s)) = SCAST(32 signed \<rightarrow> 32) cap_thread_cap}
flex-flex pairs:
\<lambda>cap tcb. ?P'735 cap (tcbBoundNotification tcb) \<equiv>\<^sup>? \<lambda>cap. ?P'734 cap (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) proof (prove)
goal (2 subgoals):
 1. \<And>cap ret__unsigned ntfn. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)\<rbrakk> \<Longrightarrow> ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?P'747 cap ntfn) (?Q744 cap ntfn) [SKIP] (doE y <- case ntfn of None \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation | Some v15 \<Rightarrow> returnOk ();
returnOk (tcbinvocation.NotificationControl (capTCBPtr cp) None)
odE >>= invocationCatch thread isBlocking isCall Invocations_H.invocation.InvokeTCB) (IF h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap))\<rightarrow>[''tcbBoundNotification_C''])) = NULL THEN
  \<acute>current_syscall_error :== type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_IllegalOperation) \<acute>current_syscall_error;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR)
FI;;
(CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
(\<acute>ret__unsigned_long :== CALL invokeTCB_NotificationControl_'proc(tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)),NULL);;
return_C ret__unsigned_long_'_update ret__unsigned_long_')))
 2. \<And>cap s s'. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. ksCurThread s = thread) and ct_active' and sch_act_simple and valid_cap' cp and (\<lambda>y. isThreadCap cp) and tcb_at' (capTCBPtr cp) and (\<lambda>s. \<forall>rf\<in>zobj_refs' cp. ex_nonz_cap_to' rf s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb (capTCBPtr cp) s \<longrightarrow> ((\<lambda>s. tcbBoundNotification tcb \<noteq> Some 0) and ?P'747 cap (tcbBoundNotification tcb)) s) \<and> s' \<in> {s. \<forall>v v'. v = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift (cap_' (cap_'_update (\<lambda>_. cap) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. tcb_'_update (\<lambda>_. tcb_Ptr v) s \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr (capTCBPtr cp)) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s'. \<forall>s. (s, s') \<in> rf_sr \<and> tcbBoundNotification tcb \<noteq> Some 0 \<longrightarrow> s' \<in> ?Q745 cap v tcb}} \<inter> {s. s \<Turnstile>\<^sub>c tcb_Ptr v}}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap) s)) = SCAST(32 signed \<rightarrow> 32) cap_thread_cap}
flex-flex pairs:
\<lambda>cap tcb. ?Q744 cap (tcbBoundNotification tcb) \<equiv>\<^sup>? \<lambda>cap. ?Q745 cap (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) proof (prove)
goal (2 subgoals):
 1. \<And>cap ret__unsigned ntfn. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)\<rbrakk> \<Longrightarrow> ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?P'747 cap ntfn) (?Q744 cap ntfn) [SKIP] ((case ntfn of None \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation | Some v15 \<Rightarrow> returnOk ()) >>= case_sum (invocationCatch thread isBlocking isCall Invocations_H.invocation.InvokeTCB \<circ> Inl) (\<lambda>rv. returnOk (tcbinvocation.NotificationControl (capTCBPtr cp) None) >>= invocationCatch thread isBlocking isCall Invocations_H.invocation.InvokeTCB)) (IF h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap))\<rightarrow>[''tcbBoundNotification_C''])) = NULL THEN
  \<acute>current_syscall_error :== type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_IllegalOperation) \<acute>current_syscall_error;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR)
FI;;
(CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
(\<acute>ret__unsigned_long :== CALL invokeTCB_NotificationControl_'proc(tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)),NULL);;
return_C ret__unsigned_long_'_update ret__unsigned_long_')))
 2. \<And>cap s s'. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. ksCurThread s = thread) and ct_active' and sch_act_simple and valid_cap' cp and (\<lambda>y. isThreadCap cp) and tcb_at' (capTCBPtr cp) and (\<lambda>s. \<forall>rf\<in>zobj_refs' cp. ex_nonz_cap_to' rf s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb (capTCBPtr cp) s \<longrightarrow> ((\<lambda>s. tcbBoundNotification tcb \<noteq> Some 0) and ?P'747 cap (tcbBoundNotification tcb)) s) \<and> s' \<in> {s. \<forall>v v'. v = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift (cap_' (cap_'_update (\<lambda>_. cap) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. tcb_'_update (\<lambda>_. tcb_Ptr v) s \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr (capTCBPtr cp)) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s'. \<forall>s. (s, s') \<in> rf_sr \<and> tcbBoundNotification tcb \<noteq> Some 0 \<longrightarrow> s' \<in> ?Q745 cap v tcb}} \<inter> {s. s \<Turnstile>\<^sub>c tcb_Ptr v}}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap) s)) = SCAST(32 signed \<rightarrow> 32) cap_thread_cap}
flex-flex pairs:
\<lambda>cap tcb. ?Q744 cap (tcbBoundNotification tcb) \<equiv>\<^sup>? \<lambda>cap. ?Q745 cap (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) proof (prove)
goal (3 subgoals):
 1. \<And>cap ret__unsigned ntfn. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); ntfn = None\<rbrakk> \<Longrightarrow> ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R777 cap ntfn) (?R''773 cap ntfn) [SKIP] (do a <- throw Fault_H.syscall_error.IllegalOperation;
case a of Inl a \<Rightarrow> (invocationCatch thread isBlocking isCall Invocations_H.invocation.InvokeTCB \<circ> Inl) a | Inr rv \<Rightarrow> returnOk (tcbinvocation.NotificationControl (capTCBPtr cp) None) >>= invocationCatch thread isBlocking isCall Invocations_H.invocation.InvokeTCB
od) (IF h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap))\<rightarrow>[''tcbBoundNotification_C''])) = NULL THEN
  \<acute>current_syscall_error :== type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_IllegalOperation) \<acute>current_syscall_error;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR)
FI;;
(CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
(\<acute>ret__unsigned_long :== CALL invokeTCB_NotificationControl_'proc(tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)),NULL);;
return_C ret__unsigned_long_'_update ret__unsigned_long_')))
 2. \<And>cap ret__unsigned ntfn x2. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); ntfn = Some x2\<rbrakk> \<Longrightarrow> ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (\<lambda>a. ?R776 cap ntfn a x2) (?R''771 cap ntfn x2) [SKIP] (do a <- returnOk ();
case a of Inl a \<Rightarrow> (invocationCatch thread isBlocking isCall Invocations_H.invocation.InvokeTCB \<circ> Inl) a | Inr rv \<Rightarrow> returnOk (tcbinvocation.NotificationControl (capTCBPtr cp) None) >>= invocationCatch thread isBlocking isCall Invocations_H.invocation.InvokeTCB
od) (IF h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap))\<rightarrow>[''tcbBoundNotification_C''])) = NULL THEN
  \<acute>current_syscall_error :== type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_IllegalOperation) \<acute>current_syscall_error;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR)
FI;;
(CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
(\<acute>ret__unsigned_long :== CALL invokeTCB_NotificationControl_'proc(tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)),NULL);;
return_C ret__unsigned_long_'_update ret__unsigned_long_')))
 3. \<And>cap s s'. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. ksCurThread s = thread) and ct_active' and sch_act_simple and valid_cap' cp and (\<lambda>y. isThreadCap cp) and tcb_at' (capTCBPtr cp) and (\<lambda>s. \<forall>rf\<in>zobj_refs' cp. ex_nonz_cap_to' rf s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb (capTCBPtr cp) s \<longrightarrow> ((\<lambda>s. tcbBoundNotification tcb \<noteq> Some 0) and (\<lambda>a. (tcbBoundNotification tcb = None \<longrightarrow> ?R777 cap (tcbBoundNotification tcb) a) \<and> (\<forall>x. tcbBoundNotification tcb = Some x \<longrightarrow> ?R776 cap (tcbBoundNotification tcb) a x))) s) \<and> s' \<in> {s. \<forall>v v'. v = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift (cap_' (cap_'_update (\<lambda>_. cap) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. tcb_'_update (\<lambda>_. tcb_Ptr v) s \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr (capTCBPtr cp)) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s'. \<forall>s. (s, s') \<in> rf_sr \<and> tcbBoundNotification tcb \<noteq> Some 0 \<longrightarrow> s' \<in> {s. tcbBoundNotification tcb = None \<longrightarrow> s \<in> ?R''775 cap v tcb} \<inter> {s. \<forall>x. s \<in> {s. tcbBoundNotification tcb = Some x \<longrightarrow> s \<in> ?R''774 cap v tcb x}}}} \<inter> {s. s \<Turnstile>\<^sub>c tcb_Ptr v}}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap) s)) = SCAST(32 signed \<rightarrow> 32) cap_thread_cap}
flex-flex pairs:
\<lambda>cap. ?R''775 cap (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) \<equiv>\<^sup>? \<lambda>cap tcb. ?R''773 cap (tcbBoundNotification tcb)
\<lambda>cap. ?R''774 cap (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) \<equiv>\<^sup>? \<lambda>cap tcb. ?R''771 cap (tcbBoundNotification tcb) proof (prove)
goal (3 subgoals):
 1. \<And>cap ret__unsigned ntfn. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); ntfn = None\<rbrakk> \<Longrightarrow> ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R777 cap None) (?R''773 cap None) [SKIP] (throwError (Inl Fault_H.syscall_error.IllegalOperation)) (IF h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap))\<rightarrow>[''tcbBoundNotification_C''])) = NULL THEN
  \<acute>current_syscall_error :== type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_IllegalOperation) \<acute>current_syscall_error;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR)
FI;;
(CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
(\<acute>ret__unsigned_long :== CALL invokeTCB_NotificationControl_'proc(tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)),NULL);;
return_C ret__unsigned_long_'_update ret__unsigned_long_')))
 2. \<And>cap ret__unsigned ntfn x2. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); ntfn = Some x2\<rbrakk> \<Longrightarrow> ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (\<lambda>a. ?R776 cap ntfn a x2) (?R''771 cap ntfn x2) [SKIP] (do a <- returnOk ();
case a of Inl a \<Rightarrow> (invocationCatch thread isBlocking isCall Invocations_H.invocation.InvokeTCB \<circ> Inl) a | Inr rv \<Rightarrow> returnOk (tcbinvocation.NotificationControl (capTCBPtr cp) None) >>= invocationCatch thread isBlocking isCall Invocations_H.invocation.InvokeTCB
od) (IF h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap))\<rightarrow>[''tcbBoundNotification_C''])) = NULL THEN
  \<acute>current_syscall_error :== type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_IllegalOperation) \<acute>current_syscall_error;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR)
FI;;
(CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
(\<acute>ret__unsigned_long :== CALL invokeTCB_NotificationControl_'proc(tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)),NULL);;
return_C ret__unsigned_long_'_update ret__unsigned_long_')))
 3. \<And>cap s s'. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. ksCurThread s = thread) and ct_active' and sch_act_simple and valid_cap' cp and (\<lambda>y. isThreadCap cp) and tcb_at' (capTCBPtr cp) and (\<lambda>s. \<forall>rf\<in>zobj_refs' cp. ex_nonz_cap_to' rf s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb (capTCBPtr cp) s \<longrightarrow> ((\<lambda>s. tcbBoundNotification tcb \<noteq> Some 0) and (\<lambda>a. (tcbBoundNotification tcb = None \<longrightarrow> ?R777 cap (tcbBoundNotification tcb) a) \<and> (\<forall>x. tcbBoundNotification tcb = Some x \<longrightarrow> ?R776 cap (tcbBoundNotification tcb) a x))) s) \<and> s' \<in> {s. \<forall>v v'. v = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift (cap_' (cap_'_update (\<lambda>_. cap) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. tcb_'_update (\<lambda>_. tcb_Ptr v) s \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr (capTCBPtr cp)) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s'. \<forall>s. (s, s') \<in> rf_sr \<and> tcbBoundNotification tcb \<noteq> Some 0 \<longrightarrow> s' \<in> {s. tcbBoundNotification tcb = None \<longrightarrow> s \<in> ?R''775 cap v tcb} \<inter> {s. \<forall>x. s \<in> {s. tcbBoundNotification tcb = Some x \<longrightarrow> s \<in> ?R''774 cap v tcb x}}}} \<inter> {s. s \<Turnstile>\<^sub>c tcb_Ptr v}}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap) s)) = SCAST(32 signed \<rightarrow> 32) cap_thread_cap}
flex-flex pairs:
\<lambda>cap. ?R''775 cap (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) \<equiv>\<^sup>? \<lambda>cap tcb. ?R''773 cap (tcbBoundNotification tcb)
\<lambda>cap. ?R''774 cap (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) \<equiv>\<^sup>? \<lambda>cap tcb. ?R''771 cap (tcbBoundNotification tcb) proof (prove)
goal (3 subgoals):
 1. \<And>cap ret__unsigned ntfn. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); ntfn = None\<rbrakk> \<Longrightarrow> ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R777 cap None) (?R'785 cap None) [SKIP] (throwError (Inl Fault_H.syscall_error.IllegalOperation)) (\<acute>current_syscall_error :== type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_IllegalOperation) \<acute>current_syscall_error;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR);;
(CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
(\<acute>ret__unsigned_long :== CALL invokeTCB_NotificationControl_'proc(tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)),NULL);;
return_C ret__unsigned_long_'_update ret__unsigned_long_')))
 2. \<And>cap ret__unsigned ntfn x2. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); ntfn = Some x2\<rbrakk> \<Longrightarrow> ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (\<lambda>a. ?R776 cap ntfn a x2) (?R''771 cap ntfn x2) [SKIP] (do a <- returnOk ();
case a of Inl a \<Rightarrow> (invocationCatch thread isBlocking isCall Invocations_H.invocation.InvokeTCB \<circ> Inl) a | Inr rv \<Rightarrow> returnOk (tcbinvocation.NotificationControl (capTCBPtr cp) None) >>= invocationCatch thread isBlocking isCall Invocations_H.invocation.InvokeTCB
od) (IF h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap))\<rightarrow>[''tcbBoundNotification_C''])) = NULL THEN
  \<acute>current_syscall_error :== type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_IllegalOperation) \<acute>current_syscall_error;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR)
FI;;
(CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
(\<acute>ret__unsigned_long :== CALL invokeTCB_NotificationControl_'proc(tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)),NULL);;
return_C ret__unsigned_long_'_update ret__unsigned_long_')))
 3. \<And>cap s s'. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. ksCurThread s = thread) and ct_active' and sch_act_simple and valid_cap' cp and (\<lambda>y. isThreadCap cp) and tcb_at' (capTCBPtr cp) and (\<lambda>s. \<forall>rf\<in>zobj_refs' cp. ex_nonz_cap_to' rf s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb (capTCBPtr cp) s \<longrightarrow> ((\<lambda>s. tcbBoundNotification tcb \<noteq> Some 0) and (\<lambda>a. (tcbBoundNotification tcb = None \<longrightarrow> ?R777 cap (tcbBoundNotification tcb) a) \<and> (\<forall>x. tcbBoundNotification tcb = Some x \<longrightarrow> ?R776 cap (tcbBoundNotification tcb) a x))) s) \<and> s' \<in> {s. \<forall>v v'. v = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift (cap_' (cap_'_update (\<lambda>_. cap) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. tcb_'_update (\<lambda>_. tcb_Ptr v) s \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr (capTCBPtr cp)) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s'. \<forall>s. (s, s') \<in> rf_sr \<and> tcbBoundNotification tcb \<noteq> Some 0 \<longrightarrow> s' \<in> {s. tcbBoundNotification tcb = None \<longrightarrow> s \<in> ?R'786 cap v tcb \<inter> \<lbrace>h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcb_Ptr v\<rightarrow>[''tcbBoundNotification_C''])) = NULL\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. tcbBoundNotification tcb = Some x \<longrightarrow> s \<in> ?R''774 cap v tcb x}}}} \<inter> {s. s \<Turnstile>\<^sub>c tcb_Ptr v}}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap) s)) = SCAST(32 signed \<rightarrow> 32) cap_thread_cap}
flex-flex pairs:
\<lambda>cap. ?R'786 cap (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) \<equiv>\<^sup>? \<lambda>cap tcb. ?R'785 cap (tcbBoundNotification tcb)
\<lambda>cap. ?R''774 cap (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) \<equiv>\<^sup>? \<lambda>cap tcb. ?R''771 cap (tcbBoundNotification tcb) proof (prove)
goal (4 subgoals):
 1. \<And>cap ret__unsigned ntfn. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); ntfn = None\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'791 cap None) \<acute>current_syscall_error :== type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_IllegalOperation) \<acute>current_syscall_error;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR) {},UNIV
 2. \<And>cap ret__unsigned ntfn \<sigma>. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); ntfn = None\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<acute>current_syscall_error :== type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_IllegalOperation) \<acute>current_syscall_error;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR) UNIV,{s. \<exists>(rv, \<sigma>')\<in>fst (throwError (Inl Fault_H.syscall_error.IllegalOperation) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> (intr_and_se_rel \<currency> dc) rv (liftxf errstate id (K ()) ret__unsigned_long_' s)}
 3. \<And>cap ret__unsigned ntfn x2. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); ntfn = Some x2\<rbrakk> \<Longrightarrow> ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (\<lambda>a. ?R776 cap ntfn a x2) (?R''771 cap ntfn x2) [SKIP] (do a <- returnOk ();
case a of Inl a \<Rightarrow> (invocationCatch thread isBlocking isCall Invocations_H.invocation.InvokeTCB \<circ> Inl) a | Inr rv \<Rightarrow> returnOk (tcbinvocation.NotificationControl (capTCBPtr cp) None) >>= invocationCatch thread isBlocking isCall Invocations_H.invocation.InvokeTCB
od) (IF h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap))\<rightarrow>[''tcbBoundNotification_C''])) = NULL THEN
  \<acute>current_syscall_error :== type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_IllegalOperation) \<acute>current_syscall_error;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR)
FI;;
(CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
(\<acute>ret__unsigned_long :== CALL invokeTCB_NotificationControl_'proc(tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)),NULL);;
return_C ret__unsigned_long_'_update ret__unsigned_long_')))
 4. \<And>cap s s'. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. ksCurThread s = thread) and ct_active' and sch_act_simple and valid_cap' cp and (\<lambda>y. isThreadCap cp) and tcb_at' (capTCBPtr cp) and (\<lambda>s. \<forall>rf\<in>zobj_refs' cp. ex_nonz_cap_to' rf s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb (capTCBPtr cp) s \<longrightarrow> ((\<lambda>s. tcbBoundNotification tcb \<noteq> Some 0) and (\<lambda>a. (tcbBoundNotification tcb = None \<longrightarrow> True) \<and> (\<forall>x. tcbBoundNotification tcb = Some x \<longrightarrow> ?R776 cap (tcbBoundNotification tcb) a x))) s) \<and> s' \<in> {s. \<forall>v v'. v = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift (cap_' (cap_'_update (\<lambda>_. cap) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. tcb_'_update (\<lambda>_. tcb_Ptr v) s \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr (capTCBPtr cp)) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s'. \<forall>s. (s, s') \<in> rf_sr \<and> tcbBoundNotification tcb \<noteq> Some 0 \<longrightarrow> s' \<in> {s. tcbBoundNotification tcb = None \<longrightarrow> s \<in> UNIV \<inter> ?R'792 cap v tcb \<inter> \<lbrace>h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcb_Ptr v\<rightarrow>[''tcbBoundNotification_C''])) = NULL\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. tcbBoundNotification tcb = Some x \<longrightarrow> s \<in> ?R''774 cap v tcb x}}}} \<inter> {s. s \<Turnstile>\<^sub>c tcb_Ptr v}}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap) s)) = SCAST(32 signed \<rightarrow> 32) cap_thread_cap}
flex-flex pairs:
\<lambda>cap. ?R'792 cap (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) \<equiv>\<^sup>? \<lambda>cap tcb. ?R'791 cap (tcbBoundNotification tcb)
\<lambda>cap. ?R''774 cap (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) \<equiv>\<^sup>? \<lambda>cap tcb. ?R''771 cap (tcbBoundNotification tcb) proof (prove)
goal (3 subgoals):
 1. \<And>cap ret__unsigned ntfn \<sigma>. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); ntfn = None\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<acute>current_syscall_error :== type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_IllegalOperation) \<acute>current_syscall_error;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR) UNIV,{s. \<exists>(rv, \<sigma>')\<in>fst (throwError (Inl Fault_H.syscall_error.IllegalOperation) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> (intr_and_se_rel \<currency> dc) rv (liftxf errstate id (K ()) ret__unsigned_long_' s)}
 2. \<And>cap ret__unsigned ntfn x2. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); ntfn = Some x2\<rbrakk> \<Longrightarrow> ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (\<lambda>a. ?R776 cap ntfn a x2) (?R''771 cap ntfn x2) [SKIP] (do a <- returnOk ();
case a of Inl a \<Rightarrow> (invocationCatch thread isBlocking isCall Invocations_H.invocation.InvokeTCB \<circ> Inl) a | Inr rv \<Rightarrow> returnOk (tcbinvocation.NotificationControl (capTCBPtr cp) None) >>= invocationCatch thread isBlocking isCall Invocations_H.invocation.InvokeTCB
od) (IF h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap))\<rightarrow>[''tcbBoundNotification_C''])) = NULL THEN
  \<acute>current_syscall_error :== type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_IllegalOperation) \<acute>current_syscall_error;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR)
FI;;
(CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
(\<acute>ret__unsigned_long :== CALL invokeTCB_NotificationControl_'proc(tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)),NULL);;
return_C ret__unsigned_long_'_update ret__unsigned_long_')))
 3. \<And>cap s s'. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. ksCurThread s = thread) and ct_active' and sch_act_simple and valid_cap' cp and (\<lambda>y. isThreadCap cp) and tcb_at' (capTCBPtr cp) and (\<lambda>s. \<forall>rf\<in>zobj_refs' cp. ex_nonz_cap_to' rf s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb (capTCBPtr cp) s \<longrightarrow> ((\<lambda>s. tcbBoundNotification tcb \<noteq> Some 0) and (\<lambda>a. (tcbBoundNotification tcb = None \<longrightarrow> True) \<and> (\<forall>x. tcbBoundNotification tcb = Some x \<longrightarrow> ?R776 cap (tcbBoundNotification tcb) a x))) s) \<and> s' \<in> {s. \<forall>v v'. v = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift (cap_' (cap_'_update (\<lambda>_. cap) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. tcb_'_update (\<lambda>_. tcb_Ptr v) s \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr (capTCBPtr cp)) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s'. \<forall>s. (s, s') \<in> rf_sr \<and> tcbBoundNotification tcb \<noteq> Some 0 \<longrightarrow> s' \<in> {s. tcbBoundNotification tcb = None \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace> \<inter> \<lbrace>h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcb_Ptr v\<rightarrow>[''tcbBoundNotification_C''])) = NULL\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. tcbBoundNotification tcb = Some x \<longrightarrow> s \<in> ?R''774 cap v tcb x}}}} \<inter> {s. s \<Turnstile>\<^sub>c tcb_Ptr v}}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap) s)) = SCAST(32 signed \<rightarrow> 32) cap_thread_cap}
flex-flex pairs:
\<lambda>cap. ?R''774 cap (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) \<equiv>\<^sup>? \<lambda>cap tcb. ?R''771 cap (tcbBoundNotification tcb) proof (prove)
goal (3 subgoals):
 1. \<And>cap ret__unsigned ntfn \<sigma>. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); ntfn = None\<rbrakk> \<Longrightarrow> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (throwError (Inl Fault_H.syscall_error.IllegalOperation) \<sigma>). (\<sigma>', globals_update (current_syscall_error_'_update (\<lambda>_. type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_IllegalOperation) (current_syscall_error_' (globals s)))) s\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR, global_exn_var_' := Return\<rparr>) \<in> rf_sr \<and> (intr_and_se_rel \<currency> dc) rv (liftxf errstate id (K ()) ret__unsigned_long_' (globals_update (current_syscall_error_'_update (\<lambda>_. type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_IllegalOperation) (current_syscall_error_' (globals s)))) s\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR, global_exn_var_' := Return\<rparr>))}
 2. \<And>cap ret__unsigned ntfn x2. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); ntfn = Some x2\<rbrakk> \<Longrightarrow> ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (\<lambda>a. ?R776 cap ntfn a x2) (?R''771 cap ntfn x2) [SKIP] (do a <- returnOk ();
case a of Inl a \<Rightarrow> (invocationCatch thread isBlocking isCall Invocations_H.invocation.InvokeTCB \<circ> Inl) a | Inr rv \<Rightarrow> returnOk (tcbinvocation.NotificationControl (capTCBPtr cp) None) >>= invocationCatch thread isBlocking isCall Invocations_H.invocation.InvokeTCB
od) (IF h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap))\<rightarrow>[''tcbBoundNotification_C''])) = NULL THEN
  \<acute>current_syscall_error :== type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_IllegalOperation) \<acute>current_syscall_error;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR)
FI;;
(CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
(\<acute>ret__unsigned_long :== CALL invokeTCB_NotificationControl_'proc(tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)),NULL);;
return_C ret__unsigned_long_'_update ret__unsigned_long_')))
 3. \<And>cap s s'. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. ksCurThread s = thread) and ct_active' and sch_act_simple and valid_cap' cp and (\<lambda>y. isThreadCap cp) and tcb_at' (capTCBPtr cp) and (\<lambda>s. \<forall>rf\<in>zobj_refs' cp. ex_nonz_cap_to' rf s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb (capTCBPtr cp) s \<longrightarrow> ((\<lambda>s. tcbBoundNotification tcb \<noteq> Some 0) and (\<lambda>a. (tcbBoundNotification tcb = None \<longrightarrow> True) \<and> (\<forall>x. tcbBoundNotification tcb = Some x \<longrightarrow> ?R776 cap (tcbBoundNotification tcb) a x))) s) \<and> s' \<in> {s. \<forall>v v'. v = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift (cap_' (cap_'_update (\<lambda>_. cap) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. tcb_'_update (\<lambda>_. tcb_Ptr v) s \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr (capTCBPtr cp)) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s'. \<forall>s. (s, s') \<in> rf_sr \<and> tcbBoundNotification tcb \<noteq> Some 0 \<longrightarrow> s' \<in> {s. tcbBoundNotification tcb = None \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace> \<inter> \<lbrace>h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcb_Ptr v\<rightarrow>[''tcbBoundNotification_C''])) = NULL\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. tcbBoundNotification tcb = Some x \<longrightarrow> s \<in> ?R''774 cap v tcb x}}}} \<inter> {s. s \<Turnstile>\<^sub>c tcb_Ptr v}}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap) s)) = SCAST(32 signed \<rightarrow> 32) cap_thread_cap}
flex-flex pairs:
\<lambda>cap. ?R''774 cap (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) \<equiv>\<^sup>? \<lambda>cap tcb. ?R''771 cap (tcbBoundNotification tcb) proof (prove)
goal (2 subgoals):
 1. \<And>cap ret__unsigned ntfn x2. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); ntfn = Some x2\<rbrakk> \<Longrightarrow> ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (\<lambda>a. ?R776 cap ntfn a x2) (?R''771 cap ntfn x2) [SKIP] (do a <- returnOk ();
case a of Inl a \<Rightarrow> (invocationCatch thread isBlocking isCall Invocations_H.invocation.InvokeTCB \<circ> Inl) a | Inr rv \<Rightarrow> returnOk (tcbinvocation.NotificationControl (capTCBPtr cp) None) >>= invocationCatch thread isBlocking isCall Invocations_H.invocation.InvokeTCB
od) (IF h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap))\<rightarrow>[''tcbBoundNotification_C''])) = NULL THEN
  \<acute>current_syscall_error :== type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_IllegalOperation) \<acute>current_syscall_error;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR)
FI;;
(CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
(\<acute>ret__unsigned_long :== CALL invokeTCB_NotificationControl_'proc(tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)),NULL);;
return_C ret__unsigned_long_'_update ret__unsigned_long_')))
 2. \<And>cap s s'. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. ksCurThread s = thread) and ct_active' and sch_act_simple and valid_cap' cp and (\<lambda>y. isThreadCap cp) and tcb_at' (capTCBPtr cp) and (\<lambda>s. \<forall>rf\<in>zobj_refs' cp. ex_nonz_cap_to' rf s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb (capTCBPtr cp) s \<longrightarrow> ((\<lambda>s. tcbBoundNotification tcb \<noteq> Some 0) and (\<lambda>a. (tcbBoundNotification tcb = None \<longrightarrow> True) \<and> (\<forall>x. tcbBoundNotification tcb = Some x \<longrightarrow> ?R776 cap (tcbBoundNotification tcb) a x))) s) \<and> s' \<in> {s. \<forall>v v'. v = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift (cap_' (cap_'_update (\<lambda>_. cap) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. tcb_'_update (\<lambda>_. tcb_Ptr v) s \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr (capTCBPtr cp)) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s'. \<forall>s. (s, s') \<in> rf_sr \<and> tcbBoundNotification tcb \<noteq> Some 0 \<longrightarrow> s' \<in> {s. tcbBoundNotification tcb = None \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace> \<inter> \<lbrace>h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcb_Ptr v\<rightarrow>[''tcbBoundNotification_C''])) = NULL\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. tcbBoundNotification tcb = Some x \<longrightarrow> s \<in> ?R''774 cap v tcb x}}}} \<inter> {s. s \<Turnstile>\<^sub>c tcb_Ptr v}}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap) s)) = SCAST(32 signed \<rightarrow> 32) cap_thread_cap}
flex-flex pairs:
\<lambda>cap. ?R''774 cap (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) \<equiv>\<^sup>? \<lambda>cap tcb. ?R''771 cap (tcbBoundNotification tcb) proof (prove)
goal (2 subgoals):
 1. \<And>cap ret__unsigned ntfn x2. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); ntfn = Some x2\<rbrakk> \<Longrightarrow> ccorres ((intr_and_se_rel \<circ> Inr) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (\<lambda>a. ?R776 cap (Some x2) a x2) (?R''771 cap (Some x2) x2) [SKIP] (do _ <- setThreadState Structures_H.thread_state.Restart thread;
doE reply <- invokeTCB (tcbinvocation.NotificationControl (capTCBPtr cp) None);
if reply = [] then liftE (replyOnRestart thread [] isCall) \<sqinter> returnOk () else liftE (replyOnRestart thread reply isCall)
odE
od) (IF h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap))\<rightarrow>[''tcbBoundNotification_C''])) = NULL THEN
  \<acute>current_syscall_error :== type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_IllegalOperation) \<acute>current_syscall_error;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR)
FI;;
(CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
(\<acute>ret__unsigned_long :== CALL invokeTCB_NotificationControl_'proc(tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)),NULL);;
return_C ret__unsigned_long_'_update ret__unsigned_long_')))
 2. \<And>cap s s'. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. ksCurThread s = thread) and ct_active' and sch_act_simple and valid_cap' cp and (\<lambda>y. isThreadCap cp) and tcb_at' (capTCBPtr cp) and (\<lambda>s. \<forall>rf\<in>zobj_refs' cp. ex_nonz_cap_to' rf s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb (capTCBPtr cp) s \<longrightarrow> ((\<lambda>s. tcbBoundNotification tcb \<noteq> Some 0) and (\<lambda>a. (tcbBoundNotification tcb = None \<longrightarrow> True) \<and> (\<forall>x. tcbBoundNotification tcb = Some x \<longrightarrow> ?R776 cap (tcbBoundNotification tcb) a x))) s) \<and> s' \<in> {s. \<forall>v v'. v = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift (cap_' (cap_'_update (\<lambda>_. cap) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. tcb_'_update (\<lambda>_. tcb_Ptr v) s \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr (capTCBPtr cp)) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s'. \<forall>s. (s, s') \<in> rf_sr \<and> tcbBoundNotification tcb \<noteq> Some 0 \<longrightarrow> s' \<in> {s. tcbBoundNotification tcb = None \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace> \<inter> \<lbrace>h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcb_Ptr v\<rightarrow>[''tcbBoundNotification_C''])) = NULL\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. tcbBoundNotification tcb = Some x \<longrightarrow> s \<in> ?R''774 cap v tcb x}}}} \<inter> {s. s \<Turnstile>\<^sub>c tcb_Ptr v}}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap) s)) = SCAST(32 signed \<rightarrow> 32) cap_thread_cap}
flex-flex pairs:
\<lambda>cap. ?R''774 cap (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) \<equiv>\<^sup>? \<lambda>cap tcb. ?R''771 cap (tcbBoundNotification tcb) proof (prove)
goal (2 subgoals):
 1. \<And>cap ret__unsigned ntfn x2. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); ntfn = Some x2\<rbrakk> \<Longrightarrow> ccorres ((intr_and_se_rel \<circ> Inr) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R819 cap (Some x2) x2) (?R'816 cap (Some x2) x2) [SKIP] (do _ <- setThreadState Structures_H.thread_state.Restart thread;
doE reply <- invokeTCB (tcbinvocation.NotificationControl (capTCBPtr cp) None);
if reply = [] then liftE (replyOnRestart thread [] isCall) \<sqinter> returnOk () else liftE (replyOnRestart thread reply isCall)
odE
od) (SKIP;;
(CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
(\<acute>ret__unsigned_long :== CALL invokeTCB_NotificationControl_'proc(tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)),NULL);;
return_C ret__unsigned_long_'_update ret__unsigned_long_')))
 2. \<And>cap s s'. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. ksCurThread s = thread) and ct_active' and sch_act_simple and valid_cap' cp and (\<lambda>y. isThreadCap cp) and tcb_at' (capTCBPtr cp) and (\<lambda>s. \<forall>rf\<in>zobj_refs' cp. ex_nonz_cap_to' rf s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb (capTCBPtr cp) s \<longrightarrow> ((\<lambda>s. tcbBoundNotification tcb \<noteq> Some 0) and (\<lambda>a. (tcbBoundNotification tcb = None \<longrightarrow> True) \<and> (\<forall>x. tcbBoundNotification tcb = Some x \<longrightarrow> ?R819 cap (tcbBoundNotification tcb) x a))) s) \<and> s' \<in> {s. \<forall>v v'. v = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift (cap_' (cap_'_update (\<lambda>_. cap) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. tcb_'_update (\<lambda>_. tcb_Ptr v) s \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr (capTCBPtr cp)) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s'. \<forall>s. (s, s') \<in> rf_sr \<and> tcbBoundNotification tcb \<noteq> Some 0 \<longrightarrow> s' \<in> {s. tcbBoundNotification tcb = None \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace> \<inter> \<lbrace>h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcb_Ptr v\<rightarrow>[''tcbBoundNotification_C''])) = NULL\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. tcbBoundNotification tcb = Some x \<longrightarrow> s \<in> ?R'817 cap v tcb x \<inter> - \<lbrace>h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcb_Ptr v\<rightarrow>[''tcbBoundNotification_C''])) = NULL\<rbrace>}}}} \<inter> {s. s \<Turnstile>\<^sub>c tcb_Ptr v}}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap) s)) = SCAST(32 signed \<rightarrow> 32) cap_thread_cap}
flex-flex pairs:
\<lambda>cap. ?R'817 cap (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) \<equiv>\<^sup>? \<lambda>cap tcb. ?R'816 cap (tcbBoundNotification tcb) proof (prove)
goal (2 subgoals):
 1. \<And>cap ret__unsigned ntfn x2. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); ntfn = Some x2\<rbrakk> \<Longrightarrow> ccorres ((intr_and_se_rel \<circ> Inr) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R819 cap (Some x2) x2) (?R'816 cap (Some x2) x2) [SKIP] (do _ <- setThreadState Structures_H.thread_state.Restart thread;
doE reply <- invokeTCB (tcbinvocation.NotificationControl (capTCBPtr cp) None);
if reply = [] then liftE (replyOnRestart thread [] isCall) \<sqinter> returnOk () else liftE (replyOnRestart thread reply isCall)
odE
od) (CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
(\<acute>ret__unsigned_long :== CALL invokeTCB_NotificationControl_'proc(tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)),NULL);;
return_C ret__unsigned_long_'_update ret__unsigned_long_'))
 2. \<And>cap s s'. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. ksCurThread s = thread) and ct_active' and sch_act_simple and valid_cap' cp and (\<lambda>y. isThreadCap cp) and tcb_at' (capTCBPtr cp) and (\<lambda>s. \<forall>rf\<in>zobj_refs' cp. ex_nonz_cap_to' rf s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb (capTCBPtr cp) s \<longrightarrow> ((\<lambda>s. tcbBoundNotification tcb \<noteq> Some 0) and (\<lambda>a. (tcbBoundNotification tcb = None \<longrightarrow> True) \<and> (\<forall>x. tcbBoundNotification tcb = Some x \<longrightarrow> ?R819 cap (tcbBoundNotification tcb) x a))) s) \<and> s' \<in> {s. \<forall>v v'. v = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift (cap_' (cap_'_update (\<lambda>_. cap) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. tcb_'_update (\<lambda>_. tcb_Ptr v) s \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr (capTCBPtr cp)) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s'. \<forall>s. (s, s') \<in> rf_sr \<and> tcbBoundNotification tcb \<noteq> Some 0 \<longrightarrow> s' \<in> {s. tcbBoundNotification tcb = None \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace> \<inter> \<lbrace>h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcb_Ptr v\<rightarrow>[''tcbBoundNotification_C''])) = NULL\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. tcbBoundNotification tcb = Some x \<longrightarrow> s \<in> ?R'817 cap v tcb x \<inter> - \<lbrace>h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcb_Ptr v\<rightarrow>[''tcbBoundNotification_C''])) = NULL\<rbrace>}}}} \<inter> {s. s \<Turnstile>\<^sub>c tcb_Ptr v}}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap) s)) = SCAST(32 signed \<rightarrow> 32) cap_thread_cap}
flex-flex pairs:
\<lambda>cap. ?R'817 cap (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) \<equiv>\<^sup>? \<lambda>cap tcb. ?R'816 cap (tcbBoundNotification tcb) proof (prove)
goal (4 subgoals):
 1. \<And>cap ret__unsigned ntfn x2 rv xfdc. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); ntfn = Some x2; dc rv xfdc\<rbrakk> \<Longrightarrow> ccorres ((intr_and_se_rel \<circ> Inr) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q830 cap ret__unsigned ntfn x2 rv) (?Q'830 cap ret__unsigned ntfn x2 rv xfdc) [SKIP] (doE reply <- invokeTCB (tcbinvocation.NotificationControl (capTCBPtr cp) None);
if reply = [] then liftE (replyOnRestart thread [] isCall) \<sqinter> returnOk () else liftE (replyOnRestart thread reply isCall)
odE) (\<acute>ret__unsigned_long :== CALL invokeTCB_NotificationControl_'proc(tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)),NULL);;
return_C ret__unsigned_long_'_update ret__unsigned_long_')
 2. \<And>cap ret__unsigned ntfn x2. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); ntfn = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R841 cap (Some x2) x2\<rbrace> setThreadState Structures_H.thread_state.Restart thread \<lbrace>?Q830 cap ret__unsigned ntfn x2\<rbrace>
 3. \<And>cap ret__unsigned ntfn x2. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); ntfn = Some x2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'831 cap (Some x2) x2) CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> ?Q'830 cap ret__unsigned ntfn x2 rv (xfdc s)}
 4. \<And>cap s s'. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. ksCurThread s = thread) and ct_active' and sch_act_simple and valid_cap' cp and (\<lambda>y. isThreadCap cp) and tcb_at' (capTCBPtr cp) and (\<lambda>s. \<forall>rf\<in>zobj_refs' cp. ex_nonz_cap_to' rf s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb (capTCBPtr cp) s \<longrightarrow> ((\<lambda>s. tcbBoundNotification tcb \<noteq> Some 0) and (\<lambda>a. (tcbBoundNotification tcb = None \<longrightarrow> True) \<and> (\<forall>x. tcbBoundNotification tcb = Some x \<longrightarrow> ((\<lambda>a. tcb_at' thread a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.Restart a \<and> (ksSchedulerAction a = SwitchToThread thread \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> (\<forall>p. thread \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R841 cap (tcbBoundNotification tcb) x) a))) s) \<and> s' \<in> {s. \<forall>v v'. v = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift (cap_' (cap_'_update (\<lambda>_. cap) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. tcb_'_update (\<lambda>_. tcb_Ptr v) s \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr (capTCBPtr cp)) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s'. \<forall>s. (s, s') \<in> rf_sr \<and> tcbBoundNotification tcb \<noteq> Some 0 \<longrightarrow> s' \<in> {s. tcbBoundNotification tcb = None \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace> \<inter> \<lbrace>h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcb_Ptr v\<rightarrow>[''tcbBoundNotification_C''])) = NULL\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. tcbBoundNotification tcb = Some x \<longrightarrow> s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) (tptr_'_update (\<lambda>_. ksCurThread_' (globals s)) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.Restart (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr thread\<rbrace>} \<inter> ?R'833 cap v tcb x \<inter> - \<lbrace>h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcb_Ptr v\<rightarrow>[''tcbBoundNotification_C''])) = NULL\<rbrace>}}}} \<inter> {s. s \<Turnstile>\<^sub>c tcb_Ptr v}}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap) s)) = SCAST(32 signed \<rightarrow> 32) cap_thread_cap}
flex-flex pairs:
\<lambda>cap. ?R'833 cap (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) \<equiv>\<^sup>? \<lambda>cap tcb. ?R'831 cap (tcbBoundNotification tcb) proof (prove)
goal (7 subgoals):
 1. \<And>cap ret__unsigned ntfn x2 rv xfdc rva ret__unsigned_long. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); ntfn = Some x2; dc rv xfdc; rva = []; id ret__unsigned_long = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres ((intr_and_se_rel \<circ> Inr) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q881 cap ret__unsigned ntfn x2 rv xfdc rva) (?Q'881 cap ret__unsigned ntfn x2 rv xfdc rva ret__unsigned_long) [SKIP] (if rva = [] then liftE (replyOnRestart thread [] isCall) \<sqinter> returnOk () else liftE (replyOnRestart thread rva isCall)) (return_C ret__unsigned_long_'_update (\<lambda>a. ret__unsigned_long))
 2. \<And>cap ret__unsigned ntfn x2 rv xfdc err rv' ret__unsigned_long. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); ntfn = Some x2; dc rv xfdc; id rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; cintr err (id rv') ret__unsigned_long\<rbrakk> \<Longrightarrow> ccorres ((intr_and_se_rel \<circ> Inr) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?QE881 cap ret__unsigned ntfn x2 rv xfdc err) (?Q''881 cap ret__unsigned ntfn x2 rv xfdc err rv' ret__unsigned_long) [SKIP] (throwError err) (return_C ret__unsigned_long_'_update (\<lambda>a. rv'))
 3. \<And>cap ret__unsigned ntfn x2 rv xfdc. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); ntfn = Some x2; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R885 cap ret__unsigned ntfn x2 rv\<rbrace> invokeTCB (tcbinvocation.NotificationControl (capTCBPtr cp) None) \<lbrace>?Q881 cap ret__unsigned ntfn x2 rv xfdc\<rbrace>, \<lbrace>?QE881 cap ret__unsigned ntfn x2 rv xfdc\<rbrace>
 4. \<And>cap ret__unsigned ntfn x2 rv xfdc. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); ntfn = Some x2; dc rv xfdc\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'881 cap ret__unsigned ntfn x2 rv xfdc) \<acute>ret__unsigned_long :== CALL invokeTCB_NotificationControl_'proc(tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)),NULL) {s. (id (ret__unsigned_long_' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rva. rva = [] \<longrightarrow> s \<in> ?Q'881 cap ret__unsigned ntfn x2 rv xfdc rva (ret__unsigned_long_' s))) \<and> (id (ret__unsigned_long_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. cintr err (id (ret__unsigned_long_' s)) (errstate s) \<longrightarrow> s \<in> ?Q''881 cap ret__unsigned ntfn x2 rv xfdc err (ret__unsigned_long_' s) (errstate s)))}
 5. \<And>cap ret__unsigned ntfn x2. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); ntfn = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R841 cap (Some x2) x2\<rbrace> setThreadState Structures_H.thread_state.Restart thread \<lbrace>\<lambda>a. invs' and tcb_inv_wf' (tcbinvocation.NotificationControl (capTCBPtr cp) None) and ?R885 cap ret__unsigned ntfn x2 a\<rbrace>
 6. \<And>cap ret__unsigned ntfn x2. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); ntfn = Some x2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'831 cap (Some x2) x2) CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {s. ntfnPtr_'_update (\<lambda>_. NULL) (tcb_'_update (\<lambda>_. tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap))) s) \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr (capTCBPtr cp)\<rbrace> \<inter> \<lbrace>\<acute>ntfnPtr = NULL\<rbrace>} \<inter> ?R'881 cap ret__unsigned ntfn x2 rv (xfdc s)}
 7. \<And>cap s s'. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. ksCurThread s = thread) and ct_active' and sch_act_simple and valid_cap' cp and (\<lambda>y. isThreadCap cp) and tcb_at' (capTCBPtr cp) and (\<lambda>s. \<forall>rf\<in>zobj_refs' cp. ex_nonz_cap_to' rf s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb (capTCBPtr cp) s \<longrightarrow> ((\<lambda>s. tcbBoundNotification tcb \<noteq> Some 0) and (\<lambda>a. (tcbBoundNotification tcb = None \<longrightarrow> True) \<and> (\<forall>x. tcbBoundNotification tcb = Some x \<longrightarrow> ((\<lambda>a. tcb_at' thread a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.Restart a \<and> (ksSchedulerAction a = SwitchToThread thread \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> (\<forall>p. thread \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R841 cap (tcbBoundNotification tcb) x) a))) s) \<and> s' \<in> {s. \<forall>v v'. v = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift (cap_' (cap_'_update (\<lambda>_. cap) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. tcb_'_update (\<lambda>_. tcb_Ptr v) s \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr (capTCBPtr cp)) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s'. \<forall>s. (s, s') \<in> rf_sr \<and> tcbBoundNotification tcb \<noteq> Some 0 \<longrightarrow> s' \<in> {s. tcbBoundNotification tcb = None \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace> \<inter> \<lbrace>h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcb_Ptr v\<rightarrow>[''tcbBoundNotification_C''])) = NULL\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. tcbBoundNotification tcb = Some x \<longrightarrow> s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) (tptr_'_update (\<lambda>_. ksCurThread_' (globals s)) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.Restart (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr thread\<rbrace>} \<inter> ?R'833 cap v tcb x \<inter> - \<lbrace>h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcb_Ptr v\<rightarrow>[''tcbBoundNotification_C''])) = NULL\<rbrace>}}}} \<inter> {s. s \<Turnstile>\<^sub>c tcb_Ptr v}}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap) s)) = SCAST(32 signed \<rightarrow> 32) cap_thread_cap}
flex-flex pairs:
\<lambda>cap. ?R'833 cap (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) \<equiv>\<^sup>? \<lambda>cap tcb. ?R'831 cap (tcbBoundNotification tcb) proof (prove)
goal (7 subgoals):
 1. \<And>cap ret__unsigned ntfn x2 xfdc rva ret__unsigned_long. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); ntfn = Some x2; rva = []; ret__unsigned_long = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres ((intr_and_se_rel \<circ> Inr) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q881 cap (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) (Some x2) x2 () xfdc []) (?Q'881 cap (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) (Some x2) x2 () xfdc [] (SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)) [SKIP] (liftE (replyOnRestart thread [] isCall) \<sqinter> returnOk ()) (return_C ret__unsigned_long_'_update (\<lambda>a. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>cap ret__unsigned ntfn x2 rv xfdc err rv' ret__unsigned_long. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); ntfn = Some x2; dc rv xfdc; id rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; cintr err (id rv') ret__unsigned_long\<rbrakk> \<Longrightarrow> ccorres ((intr_and_se_rel \<circ> Inr) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?QE881 cap ret__unsigned ntfn x2 rv xfdc err) (?Q''881 cap ret__unsigned ntfn x2 rv xfdc err rv' ret__unsigned_long) [SKIP] (throwError err) (return_C ret__unsigned_long_'_update (\<lambda>a. rv'))
 3. \<And>cap ret__unsigned ntfn x2 rv xfdc. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); ntfn = Some x2; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R885 cap ret__unsigned ntfn x2 rv\<rbrace> invokeTCB (tcbinvocation.NotificationControl (capTCBPtr cp) None) \<lbrace>?Q881 cap ret__unsigned ntfn x2 rv xfdc\<rbrace>, \<lbrace>?QE881 cap ret__unsigned ntfn x2 rv xfdc\<rbrace>
 4. \<And>cap ret__unsigned ntfn x2 rv xfdc. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); ntfn = Some x2; dc rv xfdc\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'881 cap ret__unsigned ntfn x2 rv xfdc) \<acute>ret__unsigned_long :== CALL invokeTCB_NotificationControl_'proc(tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)),NULL) {s. (id (ret__unsigned_long_' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rva. rva = [] \<longrightarrow> s \<in> ?Q'881 cap ret__unsigned ntfn x2 rv xfdc rva (ret__unsigned_long_' s))) \<and> (id (ret__unsigned_long_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. cintr err (id (ret__unsigned_long_' s)) (errstate s) \<longrightarrow> s \<in> ?Q''881 cap ret__unsigned ntfn x2 rv xfdc err (ret__unsigned_long_' s) (errstate s)))}
 5. \<And>cap ret__unsigned ntfn x2. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); ntfn = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R841 cap (Some x2) x2\<rbrace> setThreadState Structures_H.thread_state.Restart thread \<lbrace>\<lambda>a. invs' and tcb_inv_wf' (tcbinvocation.NotificationControl (capTCBPtr cp) None) and ?R885 cap ret__unsigned ntfn x2 a\<rbrace>
 6. \<And>cap ret__unsigned ntfn x2. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); ntfn = Some x2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'831 cap (Some x2) x2) CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {s. ntfnPtr_'_update (\<lambda>_. NULL) (tcb_'_update (\<lambda>_. tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap))) s) \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr (capTCBPtr cp)\<rbrace> \<inter> \<lbrace>\<acute>ntfnPtr = NULL\<rbrace>} \<inter> ?R'881 cap ret__unsigned ntfn x2 rv (xfdc s)}
 7. \<And>cap s s'. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. ksCurThread s = thread) and ct_active' and sch_act_simple and valid_cap' cp and (\<lambda>y. isThreadCap cp) and tcb_at' (capTCBPtr cp) and (\<lambda>s. \<forall>rf\<in>zobj_refs' cp. ex_nonz_cap_to' rf s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb (capTCBPtr cp) s \<longrightarrow> ((\<lambda>s. tcbBoundNotification tcb \<noteq> Some 0) and (\<lambda>a. (tcbBoundNotification tcb = None \<longrightarrow> True) \<and> (\<forall>x. tcbBoundNotification tcb = Some x \<longrightarrow> ((\<lambda>a. tcb_at' thread a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.Restart a \<and> (ksSchedulerAction a = SwitchToThread thread \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> (\<forall>p. thread \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R841 cap (tcbBoundNotification tcb) x) a))) s) \<and> s' \<in> {s. \<forall>v v'. v = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift (cap_' (cap_'_update (\<lambda>_. cap) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. tcb_'_update (\<lambda>_. tcb_Ptr v) s \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr (capTCBPtr cp)) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s'. \<forall>s. (s, s') \<in> rf_sr \<and> tcbBoundNotification tcb \<noteq> Some 0 \<longrightarrow> s' \<in> {s. tcbBoundNotification tcb = None \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace> \<inter> \<lbrace>h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcb_Ptr v\<rightarrow>[''tcbBoundNotification_C''])) = NULL\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. tcbBoundNotification tcb = Some x \<longrightarrow> s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) (tptr_'_update (\<lambda>_. ksCurThread_' (globals s)) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.Restart (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr thread\<rbrace>} \<inter> ?R'833 cap v tcb x \<inter> - \<lbrace>h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcb_Ptr v\<rightarrow>[''tcbBoundNotification_C''])) = NULL\<rbrace>}}}} \<inter> {s. s \<Turnstile>\<^sub>c tcb_Ptr v}}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap) s)) = SCAST(32 signed \<rightarrow> 32) cap_thread_cap}
flex-flex pairs:
\<lambda>cap. ?R'833 cap (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) \<equiv>\<^sup>? \<lambda>cap tcb. ?R'831 cap (tcbBoundNotification tcb) proof (prove)
goal (7 subgoals):
 1. \<And>cap ret__unsigned ntfn x2 xfdc rva ret__unsigned_long. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); ntfn = Some x2; rva = []; ret__unsigned_long = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres ((intr_and_se_rel \<circ> Inr) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q881 cap (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) (Some x2) x2 () xfdc []) (?Q'881 cap (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) (Some x2) x2 () xfdc [] (SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)) [SKIP] (returnOk ()) (return_C ret__unsigned_long_'_update (\<lambda>a. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>cap ret__unsigned ntfn x2 rv xfdc err rv' ret__unsigned_long. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); ntfn = Some x2; dc rv xfdc; id rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; cintr err (id rv') ret__unsigned_long\<rbrakk> \<Longrightarrow> ccorres ((intr_and_se_rel \<circ> Inr) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?QE881 cap ret__unsigned ntfn x2 rv xfdc err) (?Q''881 cap ret__unsigned ntfn x2 rv xfdc err rv' ret__unsigned_long) [SKIP] (throwError err) (return_C ret__unsigned_long_'_update (\<lambda>a. rv'))
 3. \<And>cap ret__unsigned ntfn x2 rv xfdc. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); ntfn = Some x2; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R885 cap ret__unsigned ntfn x2 rv\<rbrace> invokeTCB (tcbinvocation.NotificationControl (capTCBPtr cp) None) \<lbrace>?Q881 cap ret__unsigned ntfn x2 rv xfdc\<rbrace>, \<lbrace>?QE881 cap ret__unsigned ntfn x2 rv xfdc\<rbrace>
 4. \<And>cap ret__unsigned ntfn x2 rv xfdc. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); ntfn = Some x2; dc rv xfdc\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'881 cap ret__unsigned ntfn x2 rv xfdc) \<acute>ret__unsigned_long :== CALL invokeTCB_NotificationControl_'proc(tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)),NULL) {s. (id (ret__unsigned_long_' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rva. rva = [] \<longrightarrow> s \<in> ?Q'881 cap ret__unsigned ntfn x2 rv xfdc rva (ret__unsigned_long_' s))) \<and> (id (ret__unsigned_long_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. cintr err (id (ret__unsigned_long_' s)) (errstate s) \<longrightarrow> s \<in> ?Q''881 cap ret__unsigned ntfn x2 rv xfdc err (ret__unsigned_long_' s) (errstate s)))}
 5. \<And>cap ret__unsigned ntfn x2. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); ntfn = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R841 cap (Some x2) x2\<rbrace> setThreadState Structures_H.thread_state.Restart thread \<lbrace>\<lambda>a. invs' and tcb_inv_wf' (tcbinvocation.NotificationControl (capTCBPtr cp) None) and ?R885 cap ret__unsigned ntfn x2 a\<rbrace>
 6. \<And>cap ret__unsigned ntfn x2. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); ntfn = Some x2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'831 cap (Some x2) x2) CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {s. ntfnPtr_'_update (\<lambda>_. NULL) (tcb_'_update (\<lambda>_. tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap))) s) \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr (capTCBPtr cp)\<rbrace> \<inter> \<lbrace>\<acute>ntfnPtr = NULL\<rbrace>} \<inter> ?R'881 cap ret__unsigned ntfn x2 rv (xfdc s)}
 7. \<And>cap s s'. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. ksCurThread s = thread) and ct_active' and sch_act_simple and valid_cap' cp and (\<lambda>y. isThreadCap cp) and tcb_at' (capTCBPtr cp) and (\<lambda>s. \<forall>rf\<in>zobj_refs' cp. ex_nonz_cap_to' rf s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb (capTCBPtr cp) s \<longrightarrow> ((\<lambda>s. tcbBoundNotification tcb \<noteq> Some 0) and (\<lambda>a. (tcbBoundNotification tcb = None \<longrightarrow> True) \<and> (\<forall>x. tcbBoundNotification tcb = Some x \<longrightarrow> ((\<lambda>a. tcb_at' thread a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.Restart a \<and> (ksSchedulerAction a = SwitchToThread thread \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> (\<forall>p. thread \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R841 cap (tcbBoundNotification tcb) x) a))) s) \<and> s' \<in> {s. \<forall>v v'. v = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift (cap_' (cap_'_update (\<lambda>_. cap) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. tcb_'_update (\<lambda>_. tcb_Ptr v) s \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr (capTCBPtr cp)) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s'. \<forall>s. (s, s') \<in> rf_sr \<and> tcbBoundNotification tcb \<noteq> Some 0 \<longrightarrow> s' \<in> {s. tcbBoundNotification tcb = None \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace> \<inter> \<lbrace>h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcb_Ptr v\<rightarrow>[''tcbBoundNotification_C''])) = NULL\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. tcbBoundNotification tcb = Some x \<longrightarrow> s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) (tptr_'_update (\<lambda>_. ksCurThread_' (globals s)) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.Restart (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr thread\<rbrace>} \<inter> ?R'833 cap v tcb x \<inter> - \<lbrace>h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcb_Ptr v\<rightarrow>[''tcbBoundNotification_C''])) = NULL\<rbrace>}}}} \<inter> {s. s \<Turnstile>\<^sub>c tcb_Ptr v}}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap) s)) = SCAST(32 signed \<rightarrow> 32) cap_thread_cap}
flex-flex pairs:
\<lambda>cap. ?R'833 cap (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) \<equiv>\<^sup>? \<lambda>cap tcb. ?R'831 cap (tcbBoundNotification tcb) proof (prove)
goal (6 subgoals):
 1. \<And>cap ret__unsigned ntfn x2 rv xfdc err rv' ret__unsigned_long. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); ntfn = Some x2; dc rv xfdc; id rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; cintr err (id rv') ret__unsigned_long\<rbrakk> \<Longrightarrow> ccorres ((intr_and_se_rel \<circ> Inr) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?QE881 cap ret__unsigned ntfn x2 rv xfdc err) (?Q''881 cap ret__unsigned ntfn x2 rv xfdc err rv' ret__unsigned_long) [SKIP] (throwError err) (return_C ret__unsigned_long_'_update (\<lambda>a. rv'))
 2. \<And>cap ret__unsigned ntfn x2 rv xfdc. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); ntfn = Some x2; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R885 cap ret__unsigned ntfn x2 rv\<rbrace> invokeTCB (tcbinvocation.NotificationControl (capTCBPtr cp) None) \<lbrace>\<lambda>a b. True\<rbrace>, \<lbrace>?QE881 cap ret__unsigned ntfn x2 rv xfdc\<rbrace>
 3. \<And>cap ret__unsigned ntfn x2 rv xfdc. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); ntfn = Some x2; dc rv xfdc\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'881 cap ret__unsigned ntfn x2 rv xfdc) \<acute>ret__unsigned_long :== CALL invokeTCB_NotificationControl_'proc(tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)),NULL) {s. (id (ret__unsigned_long_' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rva. rva = [] \<longrightarrow> s \<in> \<lbrace>id \<^bsup>s\<^esup>ret__unsigned_long = \<^bsup>s\<^esup>ret__unsigned_long \<and> dc rv (K rv \<^bsup>s\<^esup>ret__unsigned_long)\<rbrace>)) \<and> (id (ret__unsigned_long_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. cintr err (id (ret__unsigned_long_' s)) (errstate s) \<longrightarrow> s \<in> ?Q''881 cap ret__unsigned ntfn x2 rv xfdc err (ret__unsigned_long_' s) (errstate s)))}
 4. \<And>cap ret__unsigned ntfn x2. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); ntfn = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R841 cap (Some x2) x2\<rbrace> setThreadState Structures_H.thread_state.Restart thread \<lbrace>\<lambda>a. invs' and tcb_inv_wf' (tcbinvocation.NotificationControl (capTCBPtr cp) None) and ?R885 cap ret__unsigned ntfn x2 a\<rbrace>
 5. \<And>cap ret__unsigned ntfn x2. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); ntfn = Some x2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'831 cap (Some x2) x2) CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {s. ntfnPtr_'_update (\<lambda>_. NULL) (tcb_'_update (\<lambda>_. tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap))) s) \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr (capTCBPtr cp)\<rbrace> \<inter> \<lbrace>\<acute>ntfnPtr = NULL\<rbrace>} \<inter> ?R'881 cap ret__unsigned ntfn x2 rv (xfdc s)}
 6. \<And>cap s s'. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. ksCurThread s = thread) and ct_active' and sch_act_simple and valid_cap' cp and (\<lambda>y. isThreadCap cp) and tcb_at' (capTCBPtr cp) and (\<lambda>s. \<forall>rf\<in>zobj_refs' cp. ex_nonz_cap_to' rf s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb (capTCBPtr cp) s \<longrightarrow> ((\<lambda>s. tcbBoundNotification tcb \<noteq> Some 0) and (\<lambda>a. (tcbBoundNotification tcb = None \<longrightarrow> True) \<and> (\<forall>x. tcbBoundNotification tcb = Some x \<longrightarrow> ((\<lambda>a. tcb_at' thread a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.Restart a \<and> (ksSchedulerAction a = SwitchToThread thread \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> (\<forall>p. thread \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R841 cap (tcbBoundNotification tcb) x) a))) s) \<and> s' \<in> {s. \<forall>v v'. v = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift (cap_' (cap_'_update (\<lambda>_. cap) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. tcb_'_update (\<lambda>_. tcb_Ptr v) s \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr (capTCBPtr cp)) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s'. \<forall>s. (s, s') \<in> rf_sr \<and> tcbBoundNotification tcb \<noteq> Some 0 \<longrightarrow> s' \<in> {s. tcbBoundNotification tcb = None \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace> \<inter> \<lbrace>h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcb_Ptr v\<rightarrow>[''tcbBoundNotification_C''])) = NULL\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. tcbBoundNotification tcb = Some x \<longrightarrow> s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) (tptr_'_update (\<lambda>_. ksCurThread_' (globals s)) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.Restart (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr thread\<rbrace>} \<inter> ?R'833 cap v tcb x \<inter> - \<lbrace>h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcb_Ptr v\<rightarrow>[''tcbBoundNotification_C''])) = NULL\<rbrace>}}}} \<inter> {s. s \<Turnstile>\<^sub>c tcb_Ptr v}}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap) s)) = SCAST(32 signed \<rightarrow> 32) cap_thread_cap}
flex-flex pairs:
\<lambda>cap. ?R'833 cap (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) \<equiv>\<^sup>? \<lambda>cap tcb. ?R'831 cap (tcbBoundNotification tcb) proof (prove)
goal (5 subgoals):
 1. \<And>cap ret__unsigned ntfn x2 rv xfdc. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); ntfn = Some x2; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R885 cap ret__unsigned ntfn x2 rv\<rbrace> invokeTCB (tcbinvocation.NotificationControl (capTCBPtr cp) None) \<lbrace>\<lambda>a b. True\<rbrace>, \<lbrace>\<lambda>a b. True\<rbrace>
 2. \<And>cap ret__unsigned ntfn x2 rv xfdc. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); ntfn = Some x2; dc rv xfdc\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'881 cap ret__unsigned ntfn x2 rv xfdc) \<acute>ret__unsigned_long :== CALL invokeTCB_NotificationControl_'proc(tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)),NULL) {s. (id (ret__unsigned_long_' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rva. rva = [] \<longrightarrow> s \<in> \<lbrace>id \<^bsup>s\<^esup>ret__unsigned_long = \<^bsup>s\<^esup>ret__unsigned_long \<and> dc rv (K rv \<^bsup>s\<^esup>ret__unsigned_long)\<rbrace>)) \<and> (id (ret__unsigned_long_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. cintr err (id (ret__unsigned_long_' s)) (errstate s) \<longrightarrow> s \<in> {sa. id (ret__unsigned_long_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> (intr_and_se_rel \<circ> Inr) err (id (ret__unsigned_long_' s)) (errstate sa)}))}
 3. \<And>cap ret__unsigned ntfn x2. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); ntfn = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R841 cap (Some x2) x2\<rbrace> setThreadState Structures_H.thread_state.Restart thread \<lbrace>\<lambda>a. invs' and tcb_inv_wf' (tcbinvocation.NotificationControl (capTCBPtr cp) None) and ?R885 cap ret__unsigned ntfn x2 a\<rbrace>
 4. \<And>cap ret__unsigned ntfn x2. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); ntfn = Some x2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'831 cap (Some x2) x2) CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {s. ntfnPtr_'_update (\<lambda>_. NULL) (tcb_'_update (\<lambda>_. tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap))) s) \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr (capTCBPtr cp)\<rbrace> \<inter> \<lbrace>\<acute>ntfnPtr = NULL\<rbrace>} \<inter> ?R'881 cap ret__unsigned ntfn x2 rv (xfdc s)}
 5. \<And>cap s s'. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. ksCurThread s = thread) and ct_active' and sch_act_simple and valid_cap' cp and (\<lambda>y. isThreadCap cp) and tcb_at' (capTCBPtr cp) and (\<lambda>s. \<forall>rf\<in>zobj_refs' cp. ex_nonz_cap_to' rf s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb (capTCBPtr cp) s \<longrightarrow> ((\<lambda>s. tcbBoundNotification tcb \<noteq> Some 0) and (\<lambda>a. (tcbBoundNotification tcb = None \<longrightarrow> True) \<and> (\<forall>x. tcbBoundNotification tcb = Some x \<longrightarrow> ((\<lambda>a. tcb_at' thread a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.Restart a \<and> (ksSchedulerAction a = SwitchToThread thread \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> (\<forall>p. thread \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R841 cap (tcbBoundNotification tcb) x) a))) s) \<and> s' \<in> {s. \<forall>v v'. v = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift (cap_' (cap_'_update (\<lambda>_. cap) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. tcb_'_update (\<lambda>_. tcb_Ptr v) s \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr (capTCBPtr cp)) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s'. \<forall>s. (s, s') \<in> rf_sr \<and> tcbBoundNotification tcb \<noteq> Some 0 \<longrightarrow> s' \<in> {s. tcbBoundNotification tcb = None \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace> \<inter> \<lbrace>h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcb_Ptr v\<rightarrow>[''tcbBoundNotification_C''])) = NULL\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. tcbBoundNotification tcb = Some x \<longrightarrow> s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) (tptr_'_update (\<lambda>_. ksCurThread_' (globals s)) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.Restart (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr thread\<rbrace>} \<inter> ?R'833 cap v tcb x \<inter> - \<lbrace>h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcb_Ptr v\<rightarrow>[''tcbBoundNotification_C''])) = NULL\<rbrace>}}}} \<inter> {s. s \<Turnstile>\<^sub>c tcb_Ptr v}}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap) s)) = SCAST(32 signed \<rightarrow> 32) cap_thread_cap}
flex-flex pairs:
\<lambda>cap. ?R'833 cap (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) \<equiv>\<^sup>? \<lambda>cap tcb. ?R'831 cap (tcbBoundNotification tcb) proof (prove)
goal (4 subgoals):
 1. \<And>cap ret__unsigned ntfn x2 rv xfdc. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); ntfn = Some x2; dc rv xfdc\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'881 cap ret__unsigned ntfn x2 rv xfdc) \<acute>ret__unsigned_long :== CALL invokeTCB_NotificationControl_'proc(tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)),NULL) {s. (id (ret__unsigned_long_' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rva. rva = [] \<longrightarrow> s \<in> \<lbrace>id \<^bsup>s\<^esup>ret__unsigned_long = \<^bsup>s\<^esup>ret__unsigned_long \<and> dc rv (K rv \<^bsup>s\<^esup>ret__unsigned_long)\<rbrace>)) \<and> (id (ret__unsigned_long_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. cintr err (id (ret__unsigned_long_' s)) (errstate s) \<longrightarrow> s \<in> {sa. id (ret__unsigned_long_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> (intr_and_se_rel \<circ> Inr) err (id (ret__unsigned_long_' s)) (errstate sa)}))}
 2. \<And>cap ret__unsigned ntfn x2. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); ntfn = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R841 cap (Some x2) x2\<rbrace> setThreadState Structures_H.thread_state.Restart thread \<lbrace>\<lambda>a. invs' and tcb_inv_wf' (tcbinvocation.NotificationControl (capTCBPtr cp) None) and (\<lambda>a. True \<and> True)\<rbrace>
 3. \<And>cap ret__unsigned ntfn x2. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); ntfn = Some x2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'831 cap (Some x2) x2) CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {s. ntfnPtr_'_update (\<lambda>_. NULL) (tcb_'_update (\<lambda>_. tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap))) s) \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr (capTCBPtr cp)\<rbrace> \<inter> \<lbrace>\<acute>ntfnPtr = NULL\<rbrace>} \<inter> ?R'881 cap ret__unsigned ntfn x2 rv (xfdc s)}
 4. \<And>cap s s'. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. ksCurThread s = thread) and ct_active' and sch_act_simple and valid_cap' cp and (\<lambda>y. isThreadCap cp) and tcb_at' (capTCBPtr cp) and (\<lambda>s. \<forall>rf\<in>zobj_refs' cp. ex_nonz_cap_to' rf s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb (capTCBPtr cp) s \<longrightarrow> ((\<lambda>s. tcbBoundNotification tcb \<noteq> Some 0) and (\<lambda>a. (tcbBoundNotification tcb = None \<longrightarrow> True) \<and> (\<forall>x. tcbBoundNotification tcb = Some x \<longrightarrow> ((\<lambda>a. tcb_at' thread a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.Restart a \<and> (ksSchedulerAction a = SwitchToThread thread \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> (\<forall>p. thread \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R841 cap (tcbBoundNotification tcb) x) a))) s) \<and> s' \<in> {s. \<forall>v v'. v = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift (cap_' (cap_'_update (\<lambda>_. cap) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. tcb_'_update (\<lambda>_. tcb_Ptr v) s \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr (capTCBPtr cp)) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s'. \<forall>s. (s, s') \<in> rf_sr \<and> tcbBoundNotification tcb \<noteq> Some 0 \<longrightarrow> s' \<in> {s. tcbBoundNotification tcb = None \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace> \<inter> \<lbrace>h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcb_Ptr v\<rightarrow>[''tcbBoundNotification_C''])) = NULL\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. tcbBoundNotification tcb = Some x \<longrightarrow> s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) (tptr_'_update (\<lambda>_. ksCurThread_' (globals s)) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.Restart (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr thread\<rbrace>} \<inter> ?R'833 cap v tcb x \<inter> - \<lbrace>h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcb_Ptr v\<rightarrow>[''tcbBoundNotification_C''])) = NULL\<rbrace>}}}} \<inter> {s. s \<Turnstile>\<^sub>c tcb_Ptr v}}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap) s)) = SCAST(32 signed \<rightarrow> 32) cap_thread_cap}
flex-flex pairs:
\<lambda>cap. ?R'833 cap (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) \<equiv>\<^sup>? \<lambda>cap tcb. ?R'831 cap (tcbBoundNotification tcb) proof (prove)
goal (3 subgoals):
 1. \<And>cap ret__unsigned ntfn x2. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); ntfn = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R841 cap (Some x2) x2\<rbrace> setThreadState Structures_H.thread_state.Restart thread \<lbrace>\<lambda>a. invs' and tcb_inv_wf' (tcbinvocation.NotificationControl (capTCBPtr cp) None) and (\<lambda>a. True \<and> True)\<rbrace>
 2. \<And>cap ret__unsigned ntfn x2. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); ntfn = Some x2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'831 cap (Some x2) x2) CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {s. ntfnPtr_'_update (\<lambda>_. NULL) (tcb_'_update (\<lambda>_. tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap))) s) \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr (capTCBPtr cp)\<rbrace> \<inter> \<lbrace>\<acute>ntfnPtr = NULL\<rbrace>} \<inter> {s. \<forall>t. (id (ret__unsigned_long_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE = ret__unsigned_long_' t \<and> dc rv (K rv (ret__unsigned_long_' t))) \<and> (id (ret__unsigned_long_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. cintr err (id (ret__unsigned_long_' t)) (errstate (s\<lparr>globals := globals s\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr>)) \<longrightarrow> intr_and_se_rel (Inr err) (id (ret__unsigned_long_' t)) (errstate (s\<lparr>globals := globals s\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr>))))}}
 3. \<And>cap s s'. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. ksCurThread s = thread) and ct_active' and sch_act_simple and valid_cap' cp and (\<lambda>y. isThreadCap cp) and tcb_at' (capTCBPtr cp) and (\<lambda>s. \<forall>rf\<in>zobj_refs' cp. ex_nonz_cap_to' rf s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb (capTCBPtr cp) s \<longrightarrow> ((\<lambda>s. tcbBoundNotification tcb \<noteq> Some 0) and (\<lambda>a. (tcbBoundNotification tcb = None \<longrightarrow> True) \<and> (\<forall>x. tcbBoundNotification tcb = Some x \<longrightarrow> ((\<lambda>a. tcb_at' thread a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.Restart a \<and> (ksSchedulerAction a = SwitchToThread thread \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> (\<forall>p. thread \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R841 cap (tcbBoundNotification tcb) x) a))) s) \<and> s' \<in> {s. \<forall>v v'. v = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift (cap_' (cap_'_update (\<lambda>_. cap) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. tcb_'_update (\<lambda>_. tcb_Ptr v) s \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr (capTCBPtr cp)) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s'. \<forall>s. (s, s') \<in> rf_sr \<and> tcbBoundNotification tcb \<noteq> Some 0 \<longrightarrow> s' \<in> {s. tcbBoundNotification tcb = None \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace> \<inter> \<lbrace>h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcb_Ptr v\<rightarrow>[''tcbBoundNotification_C''])) = NULL\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. tcbBoundNotification tcb = Some x \<longrightarrow> s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) (tptr_'_update (\<lambda>_. ksCurThread_' (globals s)) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.Restart (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr thread\<rbrace>} \<inter> ?R'833 cap v tcb x \<inter> - \<lbrace>h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcb_Ptr v\<rightarrow>[''tcbBoundNotification_C''])) = NULL\<rbrace>}}}} \<inter> {s. s \<Turnstile>\<^sub>c tcb_Ptr v}}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap) s)) = SCAST(32 signed \<rightarrow> 32) cap_thread_cap}
flex-flex pairs:
\<lambda>cap. ?R'833 cap (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) \<equiv>\<^sup>? \<lambda>cap tcb. ?R'831 cap (tcbBoundNotification tcb) proof (prove)
goal (3 subgoals):
 1. \<And>cap ret__unsigned ntfn x2. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); ntfn = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R841 cap (Some x2) x2\<rbrace> setThreadState Structures_H.thread_state.Restart thread \<lbrace>\<lambda>a b. invs' b \<and> tcb_at' (capTCBPtr cp) b \<and> ex_nonz_cap_to' (capTCBPtr cp) b\<rbrace>
 2. \<And>cap ret__unsigned ntfn x2. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); ntfn = Some x2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'831 cap (Some x2) x2) CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {s. ntfnPtr_'_update (\<lambda>_. NULL) (tcb_'_update (\<lambda>_. tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap))) s) \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr (capTCBPtr cp)\<rbrace> \<inter> \<lbrace>\<acute>ntfnPtr = NULL\<rbrace>} \<inter> {s. \<forall>t. (id (ret__unsigned_long_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE = ret__unsigned_long_' t \<and> dc rv (K rv (ret__unsigned_long_' t))) \<and> (id (ret__unsigned_long_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. cintr err (id (ret__unsigned_long_' t)) (errstate (s\<lparr>globals := globals s\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr>)) \<longrightarrow> intr_and_se_rel (Inr err) (id (ret__unsigned_long_' t)) (errstate (s\<lparr>globals := globals s\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr>))))}}
 3. \<And>cap s s'. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. ksCurThread s = thread) and ct_active' and sch_act_simple and valid_cap' cp and (\<lambda>y. isThreadCap cp) and tcb_at' (capTCBPtr cp) and (\<lambda>s. \<forall>rf\<in>zobj_refs' cp. ex_nonz_cap_to' rf s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb (capTCBPtr cp) s \<longrightarrow> ((\<lambda>s. tcbBoundNotification tcb \<noteq> Some 0) and (\<lambda>a. (tcbBoundNotification tcb = None \<longrightarrow> True) \<and> (\<forall>x. tcbBoundNotification tcb = Some x \<longrightarrow> ((\<lambda>a. tcb_at' thread a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.Restart a \<and> (ksSchedulerAction a = SwitchToThread thread \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> (\<forall>p. thread \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R841 cap (tcbBoundNotification tcb) x) a))) s) \<and> s' \<in> {s. \<forall>v v'. v = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift (cap_' (cap_'_update (\<lambda>_. cap) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. tcb_'_update (\<lambda>_. tcb_Ptr v) s \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr (capTCBPtr cp)) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s'. \<forall>s. (s, s') \<in> rf_sr \<and> tcbBoundNotification tcb \<noteq> Some 0 \<longrightarrow> s' \<in> {s. tcbBoundNotification tcb = None \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace> \<inter> \<lbrace>h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcb_Ptr v\<rightarrow>[''tcbBoundNotification_C''])) = NULL\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. tcbBoundNotification tcb = Some x \<longrightarrow> s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) (tptr_'_update (\<lambda>_. ksCurThread_' (globals s)) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.Restart (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr thread\<rbrace>} \<inter> ?R'833 cap v tcb x \<inter> - \<lbrace>h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcb_Ptr v\<rightarrow>[''tcbBoundNotification_C''])) = NULL\<rbrace>}}}} \<inter> {s. s \<Turnstile>\<^sub>c tcb_Ptr v}}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap) s)) = SCAST(32 signed \<rightarrow> 32) cap_thread_cap}
flex-flex pairs:
\<lambda>cap. ?R'833 cap (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) \<equiv>\<^sup>? \<lambda>cap tcb. ?R'831 cap (tcbBoundNotification tcb) proof (prove)
goal (2 subgoals):
 1. \<And>cap ret__unsigned ntfn x2. \<lbrakk>ccap_relation cp cap; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); ntfn = Some x2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'831 cap (Some x2) x2) CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) (if tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) = tcb_ptr_to_ctcb_ptr (capTCBPtr cp) then UNIV else {})
 2. \<And>cap s s'. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. ksCurThread s = thread) and ct_active' and sch_act_simple and valid_cap' cp and (\<lambda>y. isThreadCap cp) and tcb_at' (capTCBPtr cp) and (\<lambda>s. \<forall>rf\<in>zobj_refs' cp. ex_nonz_cap_to' rf s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb (capTCBPtr cp) s \<longrightarrow> ((\<lambda>s. tcbBoundNotification tcb \<noteq> Some 0) and (\<lambda>a. (tcbBoundNotification tcb = None \<longrightarrow> True) \<and> (\<forall>x. tcbBoundNotification tcb = Some x \<longrightarrow> ((\<lambda>a. tcb_at' thread a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.Restart a \<and> (ksSchedulerAction a = SwitchToThread thread \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> (\<forall>p. thread \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> sch_act_wf (ksSchedulerAction a) a) and (\<lambda>a. (st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' Structures_H.thread_state.Restart \<and> (Structures_H.thread_state.Restart \<noteq> Structures_H.thread_state.Inactive \<and> Structures_H.thread_state.Restart \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) thread and (\<lambda>s. thread = ksIdleThread s \<longrightarrow> idle' Structures_H.thread_state.Restart) and (\<lambda>s. (\<exists>p. thread \<in> set (ksReadyQueues s p)) \<longrightarrow> runnable' Structures_H.thread_state.Restart) and (\<lambda>s. runnable' Structures_H.thread_state.Restart \<and> obj_at' tcbQueued thread s \<longrightarrow> st_tcb_at' runnable' thread s) and sch_act_simple and invs') a \<and> tcb_at' (capTCBPtr cp) a \<and> ex_nonz_cap_to' (capTCBPtr cp) a)) a))) s) \<and> s' \<in> {s. \<forall>v v'. v = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift (cap_' (cap_'_update (\<lambda>_. cap) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. tcb_'_update (\<lambda>_. tcb_Ptr v) s \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr (capTCBPtr cp)) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s'. \<forall>s. (s, s') \<in> rf_sr \<and> tcbBoundNotification tcb \<noteq> Some 0 \<longrightarrow> s' \<in> {s. tcbBoundNotification tcb = None \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace> \<inter> \<lbrace>h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcb_Ptr v\<rightarrow>[''tcbBoundNotification_C''])) = NULL\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. tcbBoundNotification tcb = Some x \<longrightarrow> s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) (tptr_'_update (\<lambda>_. ksCurThread_' (globals s)) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.Restart (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr thread\<rbrace>} \<inter> ?R'833 cap v tcb x \<inter> - \<lbrace>h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcb_Ptr v\<rightarrow>[''tcbBoundNotification_C''])) = NULL\<rbrace>}}}} \<inter> {s. s \<Turnstile>\<^sub>c tcb_Ptr v}}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap) s)) = SCAST(32 signed \<rightarrow> 32) cap_thread_cap}
flex-flex pairs:
\<lambda>cap. ?R'833 cap (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) \<equiv>\<^sup>? \<lambda>cap tcb. ?R'831 cap (tcbBoundNotification tcb) proof (prove)
goal (1 subgoal):
 1. \<And>cap s s'. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. ksCurThread s = thread) and ct_active' and sch_act_simple and valid_cap' cp and (\<lambda>y. isThreadCap cp) and tcb_at' (capTCBPtr cp) and (\<lambda>s. \<forall>rf\<in>zobj_refs' cp. ex_nonz_cap_to' rf s)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb (capTCBPtr cp) s \<longrightarrow> ((\<lambda>s. tcbBoundNotification tcb \<noteq> Some 0) and (\<lambda>a. (tcbBoundNotification tcb = None \<longrightarrow> True) \<and> (\<forall>x. tcbBoundNotification tcb = Some x \<longrightarrow> ((\<lambda>a. tcb_at' thread a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.Restart a \<and> (ksSchedulerAction a = SwitchToThread thread \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> (\<forall>p. thread \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> sch_act_wf (ksSchedulerAction a) a) and (\<lambda>a. (st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' Structures_H.thread_state.Restart \<and> (Structures_H.thread_state.Restart \<noteq> Structures_H.thread_state.Inactive \<and> Structures_H.thread_state.Restart \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) thread and (\<lambda>s. thread = ksIdleThread s \<longrightarrow> idle' Structures_H.thread_state.Restart) and (\<lambda>s. (\<exists>p. thread \<in> set (ksReadyQueues s p)) \<longrightarrow> runnable' Structures_H.thread_state.Restart) and (\<lambda>s. runnable' Structures_H.thread_state.Restart \<and> obj_at' tcbQueued thread s \<longrightarrow> st_tcb_at' runnable' thread s) and sch_act_simple and invs') a \<and> tcb_at' (capTCBPtr cp) a \<and> ex_nonz_cap_to' (capTCBPtr cp) a)) a))) s) \<and> s' \<in> {s. \<forall>v v'. v = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift (cap_' (cap_'_update (\<lambda>_. cap) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. tcb_'_update (\<lambda>_. tcb_Ptr v) s \<in> {s'. \<forall>tcb ctcb. cslift s' (tcb_ptr_to_ctcb_ptr (capTCBPtr cp)) = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> {s'. \<forall>s. (s, s') \<in> rf_sr \<and> tcbBoundNotification tcb \<noteq> Some 0 \<longrightarrow> s' \<in> {s. tcbBoundNotification tcb = None \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace> \<inter> \<lbrace>h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcb_Ptr v\<rightarrow>[''tcbBoundNotification_C''])) = NULL\<rbrace>} \<inter> {s. \<forall>x. s \<in> {s. tcbBoundNotification tcb = Some x \<longrightarrow> s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) (tptr_'_update (\<lambda>_. ksCurThread_' (globals s)) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.Restart (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr thread\<rbrace>} \<inter> {s. \<forall>t. s\<lparr>globals := globals s\<lparr>ksReadyQueues_' := ksReadyQueues_' (globals t), ksReadyQueuesL1Bitmap_' := ksReadyQueuesL1Bitmap_' (globals t), ksReadyQueuesL2Bitmap_' := ksReadyQueuesL2Bitmap_' (globals t), ksSchedulerAction_' := ksSchedulerAction_' (globals t), t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr> \<in> (if tcb_Ptr v = tcb_ptr_to_ctcb_ptr (capTCBPtr cp) then UNIV else {})} \<inter> - \<lbrace>h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcb_Ptr v\<rightarrow>[''tcbBoundNotification_C''])) = NULL\<rbrace>}}}} \<inter> {s. s \<Turnstile>\<^sub>c tcb_Ptr v}}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap) s)) = SCAST(32 signed \<rightarrow> 32) cap_thread_cap} proof (prove)
goal (1 subgoal):
 1. \<And>cap s s' ko. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; invs' s; thread = ksCurThread s; ct_active' s; sch_act_simple s; valid_cap' cp s; isThreadCap cp; tcb_at' (capTCBPtr cp) s; \<forall>rf\<in>zobj_refs' cp. ex_nonz_cap_to' rf s; ko_at' ko (capTCBPtr cp) s\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb (capTCBPtr cp) s \<longrightarrow> tcbBoundNotification tcb \<noteq> Some 0 \<and> ((\<exists>x. tcbBoundNotification tcb = Some x) \<longrightarrow> tcb_at' (ksCurThread s) s \<and> Invariants_H.valid_queues s \<and> valid_objs' s \<and> valid_tcb_state' Structures_H.thread_state.Restart s \<and> sch_act_wf (ksSchedulerAction s) s \<and> st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = {} \<and> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState) (ksCurThread s) s \<and> (obj_at' tcbQueued (ksCurThread s) s \<longrightarrow> st_tcb_at' runnable' (ksCurThread s) s) \<and> ex_nonz_cap_to' (capTCBPtr cp) s)) \<and> (\<forall>tcb. (\<exists>ctcb. cslift s' (tcb_ptr_to_ctcb_ptr (capTCBPtr cp)) = Some ctcb \<and> ctcb_relation tcb ctcb) \<longrightarrow> (\<exists>s. (s, s') \<in> rf_sr) \<and> tcbBoundNotification tcb \<noteq> Some 0 \<longrightarrow> (tcbBoundNotification tcb = None \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(notification_C ptr) &(tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap))\<rightarrow>[''tcbBoundNotification_C''])) = NULL) \<and> ((\<exists>x. tcbBoundNotification tcb = Some x) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) ThreadState_Restart && mask 4 = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart \<and> ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s) \<and> (\<forall>t. s'\<lparr>ret__unsigned_' := cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap), tcb_' := tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)), globals := globals s'\<lparr>ksReadyQueues_' := ksReadyQueues_' (globals t), ksReadyQueuesL1Bitmap_' := ksReadyQueuesL1Bitmap_' (globals t), ksReadyQueuesL2Bitmap_' := ksReadyQueuesL2Bitmap_' (globals t), ksSchedulerAction_' := ksSchedulerAction_' (globals t), t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr> \<in> (if tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) = tcb_ptr_to_ctcb_ptr (capTCBPtr cp) then UNIV else {})) \<and> h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(notification_C ptr) &(tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap))\<rightarrow>[''tcbBoundNotification_C''])) \<noteq> NULL)) \<and> s' \<Turnstile>\<^sub>c tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) \<and> s' \<in> (if cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_thread_cap then UNIV else {}) proof (prove)
goal (2 subgoals):
 1. \<And>cap s s' ko. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; invs' s; thread = ksCurThread s; ct_active' s; sch_act_simple s; valid_cap' cp s; isThreadCap cp; tcb_at' (capTCBPtr cp) s; \<forall>rf\<in>zobj_refs' cp. ex_nonz_cap_to' rf s; ko_at' ko (capTCBPtr cp) s\<rbrakk> \<Longrightarrow> map_to_tcbs (ksPSpace s) (?x1046 cap s s' ko) = Some (?y1046 cap s s' ko)
 2. \<And>cap s s' ko y'. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; invs' s; thread = ksCurThread s; ct_active' s; sch_act_simple s; valid_cap' cp s; isThreadCap cp; tcb_at' (capTCBPtr cp) s; \<forall>rf\<in>zobj_refs' cp. ex_nonz_cap_to' rf s; ko_at' ko (capTCBPtr cp) s; map_to_tcbs (ksPSpace s) (?x1046 cap s s' ko) = Some (?y1046 cap s s' ko); ctcb_relation (?y1046 cap s s' ko) y'; cslift s' (tcb_ptr_to_ctcb_ptr (?x1046 cap s s' ko)) = Some y'\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb (capTCBPtr cp) s \<longrightarrow> tcbBoundNotification tcb \<noteq> Some 0 \<and> ((\<exists>x. tcbBoundNotification tcb = Some x) \<longrightarrow> tcb_at' (ksCurThread s) s \<and> Invariants_H.valid_queues s \<and> valid_objs' s \<and> valid_tcb_state' Structures_H.thread_state.Restart s \<and> sch_act_wf (ksSchedulerAction s) s \<and> st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = {} \<and> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState) (ksCurThread s) s \<and> (obj_at' tcbQueued (ksCurThread s) s \<longrightarrow> st_tcb_at' runnable' (ksCurThread s) s) \<and> ex_nonz_cap_to' (capTCBPtr cp) s)) \<and> (\<forall>tcb. (\<exists>ctcb. cslift s' (tcb_ptr_to_ctcb_ptr (capTCBPtr cp)) = Some ctcb \<and> ctcb_relation tcb ctcb) \<longrightarrow> (\<exists>s. (s, s') \<in> rf_sr) \<and> tcbBoundNotification tcb \<noteq> Some 0 \<longrightarrow> (tcbBoundNotification tcb = None \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(notification_C ptr) &(tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap))\<rightarrow>[''tcbBoundNotification_C''])) = NULL) \<and> ((\<exists>x. tcbBoundNotification tcb = Some x) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) ThreadState_Restart && mask 4 = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart \<and> ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s) \<and> (\<forall>t. s'\<lparr>ret__unsigned_' := cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap), tcb_' := tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)), globals := globals s'\<lparr>ksReadyQueues_' := ksReadyQueues_' (globals t), ksReadyQueuesL1Bitmap_' := ksReadyQueuesL1Bitmap_' (globals t), ksReadyQueuesL2Bitmap_' := ksReadyQueuesL2Bitmap_' (globals t), ksSchedulerAction_' := ksSchedulerAction_' (globals t), t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr> \<in> (if tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) = tcb_ptr_to_ctcb_ptr (capTCBPtr cp) then UNIV else {})) \<and> h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(notification_C ptr) &(tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap))\<rightarrow>[''tcbBoundNotification_C''])) \<noteq> NULL)) \<and> s' \<Turnstile>\<^sub>c tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) \<and> s' \<in> (if cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_thread_cap then UNIV else {}) proof (prove)
goal (1 subgoal):
 1. \<And>cap s s' ko y'. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; invs' s; thread = ksCurThread s; ct_active' s; sch_act_simple s; valid_cap' cp s; isThreadCap cp; tcb_at' (capTCBPtr cp) s; \<forall>rf\<in>zobj_refs' cp. ex_nonz_cap_to' rf s; ko_at' ko (capTCBPtr cp) s; map_to_tcbs (ksPSpace s) (capTCBPtr cp) = Some ko; ctcb_relation ko y'; cslift s' (tcb_ptr_to_ctcb_ptr (capTCBPtr cp)) = Some y'\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb (capTCBPtr cp) s \<longrightarrow> tcbBoundNotification tcb \<noteq> Some 0 \<and> ((\<exists>x. tcbBoundNotification tcb = Some x) \<longrightarrow> tcb_at' (ksCurThread s) s \<and> Invariants_H.valid_queues s \<and> valid_objs' s \<and> valid_tcb_state' Structures_H.thread_state.Restart s \<and> sch_act_wf (ksSchedulerAction s) s \<and> st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = {} \<and> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState) (ksCurThread s) s \<and> (obj_at' tcbQueued (ksCurThread s) s \<longrightarrow> st_tcb_at' runnable' (ksCurThread s) s) \<and> ex_nonz_cap_to' (capTCBPtr cp) s)) \<and> (\<forall>tcb. (\<exists>ctcb. cslift s' (tcb_ptr_to_ctcb_ptr (capTCBPtr cp)) = Some ctcb \<and> ctcb_relation tcb ctcb) \<longrightarrow> (\<exists>s. (s, s') \<in> rf_sr) \<and> tcbBoundNotification tcb \<noteq> Some 0 \<longrightarrow> (tcbBoundNotification tcb = None \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(notification_C ptr) &(tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap))\<rightarrow>[''tcbBoundNotification_C''])) = NULL) \<and> ((\<exists>x. tcbBoundNotification tcb = Some x) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) ThreadState_Restart && mask 4 = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart \<and> ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s) \<and> (\<forall>t. s'\<lparr>ret__unsigned_' := cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap), tcb_' := tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)), globals := globals s'\<lparr>ksReadyQueues_' := ksReadyQueues_' (globals t), ksReadyQueuesL1Bitmap_' := ksReadyQueuesL1Bitmap_' (globals t), ksReadyQueuesL2Bitmap_' := ksReadyQueuesL2Bitmap_' (globals t), ksSchedulerAction_' := ksSchedulerAction_' (globals t), t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr> \<in> (if tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) = tcb_ptr_to_ctcb_ptr (capTCBPtr cp) then UNIV else {})) \<and> h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(notification_C ptr) &(tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap))\<rightarrow>[''tcbBoundNotification_C''])) \<noteq> NULL)) \<and> s' \<Turnstile>\<^sub>c tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) \<and> s' \<in> (if cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_thread_cap then UNIV else {}) proof (prove)
goal (1 subgoal):
 1. \<And>cap s s' ko y' v0. \<lbrakk>ccap_relation (capability.ThreadCap v0) cap; (s, s') \<in> rf_sr; invs' s; thread = ksCurThread s; ct_active' s; sch_act_simple s; valid_cap' (capability.ThreadCap v0) s; tcb_at' v0 s; ex_nonz_cap_to' v0 s; ko_at' ko v0 s; map_to_tcbs (ksPSpace s) v0 = Some ko; ctcb_relation ko y'; cslift s' (tcb_ptr_to_ctcb_ptr v0) = Some y'; cp = capability.ThreadCap v0\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb v0 s \<longrightarrow> tcbBoundNotification tcb \<noteq> Some 0 \<and> ((\<exists>x. tcbBoundNotification tcb = Some x) \<longrightarrow> tcb_at' (ksCurThread s) s \<and> Invariants_H.valid_queues s \<and> valid_objs' s \<and> valid_tcb_state' Structures_H.thread_state.Restart s \<and> sch_act_wf (ksSchedulerAction s) s \<and> st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = {} \<and> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState) (ksCurThread s) s \<and> (obj_at' tcbQueued (ksCurThread s) s \<longrightarrow> st_tcb_at' runnable' (ksCurThread s) s))) \<and> (\<forall>tcb. ctcb_relation tcb y' \<longrightarrow> (\<exists>s. (s, s') \<in> rf_sr) \<and> tcbBoundNotification tcb \<noteq> Some 0 \<longrightarrow> (tcbBoundNotification tcb = None \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(notification_C ptr) &(tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap))\<rightarrow>[''tcbBoundNotification_C''])) = NULL) \<and> ((\<exists>x. tcbBoundNotification tcb = Some x) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) ThreadState_Restart && mask 4 = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart \<and> ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s) \<and> (\<forall>t. s'\<lparr>ret__unsigned_' := cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap), tcb_' := tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)), globals := globals s'\<lparr>ksReadyQueues_' := ksReadyQueues_' (globals t), ksReadyQueuesL1Bitmap_' := ksReadyQueuesL1Bitmap_' (globals t), ksReadyQueuesL2Bitmap_' := ksReadyQueuesL2Bitmap_' (globals t), ksSchedulerAction_' := ksSchedulerAction_' (globals t), t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr> \<in> (if tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) = tcb_ptr_to_ctcb_ptr v0 then UNIV else {})) \<and> h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(notification_C ptr) &(tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap))\<rightarrow>[''tcbBoundNotification_C''])) \<noteq> NULL)) \<and> s' \<Turnstile>\<^sub>c tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) \<and> s' \<in> (if cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_thread_cap then UNIV else {}) proof (prove)
goal (1 subgoal):
 1. \<And>cap s s' ko y' v0. \<lbrakk>ccap_relation (capability.ThreadCap v0) cap; (s, s') \<in> rf_sr; invs' s; thread = ksCurThread s; ct_active' s; sch_act_simple s; valid_cap' (capability.ThreadCap v0) s; tcb_at' v0 s; ex_nonz_cap_to' v0 s; ko_at' ko v0 s; map_to_tcbs (ksPSpace s) v0 = Some ko; ctcb_relation ko y'; cslift s' (tcb_ptr_to_ctcb_ptr v0) = Some y'; cp = capability.ThreadCap v0; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_thread_cap\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb v0 s \<longrightarrow> tcbBoundNotification tcb \<noteq> Some 0 \<and> ((\<exists>x. tcbBoundNotification tcb = Some x) \<longrightarrow> tcb_at' (ksCurThread s) s \<and> Invariants_H.valid_queues s \<and> valid_objs' s \<and> valid_tcb_state' Structures_H.thread_state.Restart s \<and> sch_act_wf (ksSchedulerAction s) s \<and> st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = {} \<and> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState) (ksCurThread s) s \<and> (obj_at' tcbQueued (ksCurThread s) s \<longrightarrow> st_tcb_at' runnable' (ksCurThread s) s))) \<and> (\<forall>tcb. ctcb_relation tcb y' \<longrightarrow> (\<exists>s. (s, s') \<in> rf_sr) \<and> tcbBoundNotification tcb \<noteq> Some 0 \<longrightarrow> (tcbBoundNotification tcb = None \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(notification_C ptr) &(tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap))\<rightarrow>[''tcbBoundNotification_C''])) = NULL) \<and> ((\<exists>x. tcbBoundNotification tcb = Some x) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) ThreadState_Restart && mask 4 = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart \<and> ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s) \<and> (\<forall>t. s'\<lparr>ret__unsigned_' := cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap), tcb_' := tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)), globals := globals s'\<lparr>ksReadyQueues_' := ksReadyQueues_' (globals t), ksReadyQueuesL1Bitmap_' := ksReadyQueuesL1Bitmap_' (globals t), ksReadyQueuesL2Bitmap_' := ksReadyQueuesL2Bitmap_' (globals t), ksSchedulerAction_' := ksSchedulerAction_' (globals t), t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr> \<in> (if tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) = tcb_ptr_to_ctcb_ptr v0 then UNIV else {})) \<and> h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(notification_C ptr) &(tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap))\<rightarrow>[''tcbBoundNotification_C''])) \<noteq> NULL)) \<and> s' \<Turnstile>\<^sub>c tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) \<and> s' \<in> (if cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_thread_cap then UNIV else {}) proof (prove)
goal:
No subgoals!