theory Finalise_C

lemma unbindNotification_ccorres:
  "ccorres dc xfdc
    (invs') (UNIV \<inter> {s. tcb_' s = tcb_ptr_to_ctcb_ptr tcb}) []
    (unbindNotification tcb) (Call unbindNotification_'proc)" supply option.case_cong[cong] apply (cinit lift: tcb_') apply (rule_tac xf'=ntfnPtr_'
                    and r'="\<lambda>rv rv'. rv' = option_to_ptr rv \<and> rv \<noteq> Some 0"
                    in ccorres_split_nothrow) apply (simp add: getBoundNotification_def) apply (rule_tac P="no_0_obj' and valid_objs'" in threadGet_vcg_corres_P) apply (rule allI, rule conseqPre, vcg) apply clarsimp apply (drule obj_at_ko_at', clarsimp) apply (drule spec, drule(1) mp, clarsimp) apply (clarsimp simp: typ_heap_simps ctcb_relation_def) apply (drule(1) ko_at_valid_objs', simp add: projectKOs) apply (clarsimp simp: option_to_ptr_def option_to_0_def projectKOs
                             valid_obj'_def valid_tcb'_def) apply ceqv apply simp apply wpc apply (rule ccorres_cond_false) apply (rule ccorres_return_Skip) apply (rule ccorres_cond_true) apply (ctac (no_vcg) add: doUnbindNotification_ccorres[simplified]) apply (wp gbn_wp') apply vcg apply (clarsimp simp: option_to_ptr_def option_to_0_def pred_tcb_at'_def
                        obj_at'_weakenE[OF _ TrueI]
                 split: option.splits) apply (clarsimp simp: invs'_def valid_pspace'_def valid_state'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc invs' (UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr tcb\<rbrace>) [] (unbindNotification tcb) (Call unbindNotification_'proc) proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc invs' (UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr tcb\<rbrace>) [] (unbindNotification tcb) (Call unbindNotification_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>tcba. tcba = tcb_ptr_to_ctcb_ptr tcb \<Longrightarrow> ccorres dc xfdc (?Q98 tcba) (?Q'98 tcba) [SKIP] (do ntfnPtr <- getBoundNotification tcb;
case ntfnPtr of None \<Rightarrow> return () | Some ntfnPtr' \<Rightarrow> do ntfn <- getNotification ntfnPtr';
y <- setNotification ntfnPtr' (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None tcb
od
od) (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcba} (\<acute>ntfnPtr :== h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcba\<rightarrow>[''tcbBoundNotification_C''])));;
IF \<acute>ntfnPtr \<noteq> NULL THEN
  CALL doUnbindNotification_'proc(\<acute>ntfnPtr,tcba)
FI)
 2. \<And>tcba s s'. \<lbrakk>tcba = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q98 tcba s \<and> s' \<in> ?Q'98 tcba proof (prove)
goal (6 subgoals):
 1. \<And>tcba. tcba = tcb_ptr_to_ctcb_ptr tcb \<Longrightarrow> ccorres (\<lambda>rv rv'. rv' = option_to_ptr rv \<and> rv \<noteq> Some 0) ntfnPtr_' (?P104 tcba) (?P'104 tcba) [SKIP] (getBoundNotification tcb) (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcba} (\<acute>ntfnPtr :== h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcba\<rightarrow>[''tcbBoundNotification_C'']))))
 2. \<And>tcba rv' t t'. tcba = tcb_ptr_to_ctcb_ptr tcb \<Longrightarrow> ceqv \<Gamma> ntfnPtr_' rv' t t' (IF \<acute>ntfnPtr \<noteq> NULL THEN
  CALL doUnbindNotification_'proc(\<acute>ntfnPtr,tcba)
FI) (?d'104 tcba rv')
 3. \<And>tcba rv rv'. \<lbrakk>tcba = tcb_ptr_to_ctcb_ptr tcb; rv' = option_to_ptr rv \<and> rv \<noteq> Some 0\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q104 tcba rv) (?Q'104 tcba rv rv') [SKIP] (case rv of None \<Rightarrow> return () | Some ntfnPtr' \<Rightarrow> do ntfn <- getNotification ntfnPtr';
y <- setNotification ntfnPtr' (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None tcb
od) (?d'104 tcba rv')
 4. \<And>tcba. tcba = tcb_ptr_to_ctcb_ptr tcb \<Longrightarrow> \<lbrace>?R104 tcba\<rbrace> getBoundNotification tcb \<lbrace>?Q104 tcba\<rbrace>
 5. \<And>tcba. tcba = tcb_ptr_to_ctcb_ptr tcb \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F104 tcba\<^esub> (?R'104 tcba) Guard C_Guard {s. s \<Turnstile>\<^sub>c tcba} (\<acute>ntfnPtr :== h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcba\<rightarrow>[''tcbBoundNotification_C'']))) {s. \<forall>rv. ntfnPtr_' s = option_to_ptr rv \<and> rv \<noteq> Some 0 \<longrightarrow> s \<in> ?Q'104 tcba rv (ntfnPtr_' s)}
 6. \<And>tcba s s'. \<lbrakk>tcba = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (?P104 tcba and ?R104 tcba) s \<and> s' \<in> ?P'104 tcba \<inter> ?R'104 tcba proof (prove)
goal (6 subgoals):
 1. ccorres (\<lambda>rv rv'. rv' = option_to_ptr rv \<and> rv \<noteq> Some 0) ntfnPtr_' (?P104 (tcb_ptr_to_ctcb_ptr tcb)) (?P'104 (tcb_ptr_to_ctcb_ptr tcb)) [SKIP] (threadGet tcbBoundNotification tcb) (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr tcb} (\<acute>ntfnPtr :== h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcb_ptr_to_ctcb_ptr tcb\<rightarrow>[''tcbBoundNotification_C'']))))
 2. \<And>tcba rv' t t'. tcba = tcb_ptr_to_ctcb_ptr tcb \<Longrightarrow> ceqv \<Gamma> ntfnPtr_' rv' t t' (IF \<acute>ntfnPtr \<noteq> NULL THEN
  CALL doUnbindNotification_'proc(\<acute>ntfnPtr,tcba)
FI) (?d'104 tcba rv')
 3. \<And>tcba rv rv'. \<lbrakk>tcba = tcb_ptr_to_ctcb_ptr tcb; rv' = option_to_ptr rv \<and> rv \<noteq> Some 0\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q104 tcba rv) (?Q'104 tcba rv rv') [SKIP] (case rv of None \<Rightarrow> return () | Some ntfnPtr' \<Rightarrow> do ntfn <- getNotification ntfnPtr';
y <- setNotification ntfnPtr' (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None tcb
od) (?d'104 tcba rv')
 4. \<And>tcba. tcba = tcb_ptr_to_ctcb_ptr tcb \<Longrightarrow> \<lbrace>?R104 tcba\<rbrace> getBoundNotification tcb \<lbrace>?Q104 tcba\<rbrace>
 5. \<And>tcba. tcba = tcb_ptr_to_ctcb_ptr tcb \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F104 tcba\<^esub> (?R'104 tcba) Guard C_Guard {s. s \<Turnstile>\<^sub>c tcba} (\<acute>ntfnPtr :== h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcba\<rightarrow>[''tcbBoundNotification_C'']))) {s. \<forall>rv. ntfnPtr_' s = option_to_ptr rv \<and> rv \<noteq> Some 0 \<longrightarrow> s \<in> ?Q'104 tcba rv (ntfnPtr_' s)}
 6. \<And>tcba s s'. \<lbrakk>tcba = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (?P104 tcba and ?R104 tcba) s \<and> s' \<in> ?P'104 tcba \<inter> ?R'104 tcba proof (prove)
goal (6 subgoals):
 1. \<And>x. \<forall>\<sigma>. \<Gamma>\<turnstile> {s. (\<sigma>, s) \<in> rf_sr \<and> tcb_at' tcb \<sigma> \<and> (no_0_obj' and valid_objs') \<sigma> \<and> (\<forall>tcba. ko_at' tcba tcb \<sigma> \<longrightarrow> (\<exists>tcb'. x = tcbBoundNotification tcba \<and> cslift s (tcb_ptr_to_ctcb_ptr tcb) = Some tcb' \<and> ctcb_relation tcba tcb'))} Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr tcb} (\<acute>ntfnPtr :== h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcb_ptr_to_ctcb_ptr tcb\<rightarrow>[''tcbBoundNotification_C'']))) {s. (\<sigma>, s) \<in> rf_sr \<and> ntfnPtr_' s = option_to_ptr x \<and> x \<noteq> Some 0}
 2. \<And>tcba rv' t t'. tcba = tcb_ptr_to_ctcb_ptr tcb \<Longrightarrow> ceqv \<Gamma> ntfnPtr_' rv' t t' (IF \<acute>ntfnPtr \<noteq> NULL THEN
  CALL doUnbindNotification_'proc(\<acute>ntfnPtr,tcba)
FI) (?d'104 tcba rv')
 3. \<And>tcba rv rv'. \<lbrakk>tcba = tcb_ptr_to_ctcb_ptr tcb; rv' = option_to_ptr rv \<and> rv \<noteq> Some 0\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q104 tcba rv) (?Q'104 tcba rv rv') [SKIP] (case rv of None \<Rightarrow> return () | Some ntfnPtr' \<Rightarrow> do ntfn <- getNotification ntfnPtr';
y <- setNotification ntfnPtr' (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None tcb
od) (?d'104 tcba rv')
 4. \<And>tcba. tcba = tcb_ptr_to_ctcb_ptr tcb \<Longrightarrow> \<lbrace>?R104 tcba\<rbrace> getBoundNotification tcb \<lbrace>?Q104 tcba\<rbrace>
 5. \<And>tcba. tcba = tcb_ptr_to_ctcb_ptr tcb \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F104 tcba\<^esub> (?R'104 tcba) Guard C_Guard {s. s \<Turnstile>\<^sub>c tcba} (\<acute>ntfnPtr :== h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcba\<rightarrow>[''tcbBoundNotification_C'']))) {s. \<forall>rv. ntfnPtr_' s = option_to_ptr rv \<and> rv \<noteq> Some 0 \<longrightarrow> s \<in> ?Q'104 tcba rv (ntfnPtr_' s)}
 6. \<And>tcba s s'. \<lbrakk>tcba = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (no_0_obj' and valid_objs' and ?R104 tcba) s \<and> s' \<in> UNIV \<inter> ?R'104 tcba proof (prove)
goal (6 subgoals):
 1. \<And>x \<sigma>. {s. (\<sigma>, s) \<in> rf_sr \<and> tcb_at' tcb \<sigma> \<and> (no_0_obj' and valid_objs') \<sigma> \<and> (\<forall>tcba. ko_at' tcba tcb \<sigma> \<longrightarrow> (\<exists>tcb'. x = tcbBoundNotification tcba \<and> cslift s (tcb_ptr_to_ctcb_ptr tcb) = Some tcb' \<and> ctcb_relation tcba tcb'))} \<subseteq> {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr tcb \<and> (\<sigma>, ntfnPtr_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (PTR(notification_C ptr) &(tcb_ptr_to_ctcb_ptr tcb\<rightarrow>[''tcbBoundNotification_C'']))) s) \<in> rf_sr \<and> h_val (hrs_mem (t_hrs_' (globals s))) (PTR(notification_C ptr) &(tcb_ptr_to_ctcb_ptr tcb\<rightarrow>[''tcbBoundNotification_C''])) = option_to_ptr x \<and> x \<noteq> Some 0}
 2. \<And>tcba rv' t t'. tcba = tcb_ptr_to_ctcb_ptr tcb \<Longrightarrow> ceqv \<Gamma> ntfnPtr_' rv' t t' (IF \<acute>ntfnPtr \<noteq> NULL THEN
  CALL doUnbindNotification_'proc(\<acute>ntfnPtr,tcba)
FI) (?d'104 tcba rv')
 3. \<And>tcba rv rv'. \<lbrakk>tcba = tcb_ptr_to_ctcb_ptr tcb; rv' = option_to_ptr rv \<and> rv \<noteq> Some 0\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q104 tcba rv) (?Q'104 tcba rv rv') [SKIP] (case rv of None \<Rightarrow> return () | Some ntfnPtr' \<Rightarrow> do ntfn <- getNotification ntfnPtr';
y <- setNotification ntfnPtr' (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None tcb
od) (?d'104 tcba rv')
 4. \<And>tcba. tcba = tcb_ptr_to_ctcb_ptr tcb \<Longrightarrow> \<lbrace>?R104 tcba\<rbrace> getBoundNotification tcb \<lbrace>?Q104 tcba\<rbrace>
 5. \<And>tcba. tcba = tcb_ptr_to_ctcb_ptr tcb \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F104 tcba\<^esub> (?R'104 tcba) Guard C_Guard {s. s \<Turnstile>\<^sub>c tcba} (\<acute>ntfnPtr :== h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcba\<rightarrow>[''tcbBoundNotification_C'']))) {s. \<forall>rv. ntfnPtr_' s = option_to_ptr rv \<and> rv \<noteq> Some 0 \<longrightarrow> s \<in> ?Q'104 tcba rv (ntfnPtr_' s)}
 6. \<And>tcba s s'. \<lbrakk>tcba = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (no_0_obj' and valid_objs' and ?R104 tcba) s \<and> s' \<in> UNIV \<inter> ?R'104 tcba proof (prove)
goal (6 subgoals):
 1. \<And>x \<sigma> xa. \<lbrakk>(\<sigma>, xa) \<in> rf_sr; tcb_at' tcb \<sigma>; no_0_obj' \<sigma>; valid_objs' \<sigma>; \<forall>tcba. ko_at' tcba tcb \<sigma> \<longrightarrow> x = tcbBoundNotification tcba \<and> (\<exists>tcb'. cslift xa (tcb_ptr_to_ctcb_ptr tcb) = Some tcb' \<and> ctcb_relation tcba tcb')\<rbrakk> \<Longrightarrow> xa \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr tcb \<and> h_val (hrs_mem (t_hrs_' (globals xa))) (PTR(notification_C ptr) &(tcb_ptr_to_ctcb_ptr tcb\<rightarrow>[''tcbBoundNotification_C''])) = option_to_ptr x \<and> x \<noteq> Some 0
 2. \<And>tcba rv' t t'. tcba = tcb_ptr_to_ctcb_ptr tcb \<Longrightarrow> ceqv \<Gamma> ntfnPtr_' rv' t t' (IF \<acute>ntfnPtr \<noteq> NULL THEN
  CALL doUnbindNotification_'proc(\<acute>ntfnPtr,tcba)
FI) (?d'104 tcba rv')
 3. \<And>tcba rv rv'. \<lbrakk>tcba = tcb_ptr_to_ctcb_ptr tcb; rv' = option_to_ptr rv \<and> rv \<noteq> Some 0\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q104 tcba rv) (?Q'104 tcba rv rv') [SKIP] (case rv of None \<Rightarrow> return () | Some ntfnPtr' \<Rightarrow> do ntfn <- getNotification ntfnPtr';
y <- setNotification ntfnPtr' (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None tcb
od) (?d'104 tcba rv')
 4. \<And>tcba. tcba = tcb_ptr_to_ctcb_ptr tcb \<Longrightarrow> \<lbrace>?R104 tcba\<rbrace> getBoundNotification tcb \<lbrace>?Q104 tcba\<rbrace>
 5. \<And>tcba. tcba = tcb_ptr_to_ctcb_ptr tcb \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F104 tcba\<^esub> (?R'104 tcba) Guard C_Guard {s. s \<Turnstile>\<^sub>c tcba} (\<acute>ntfnPtr :== h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcba\<rightarrow>[''tcbBoundNotification_C'']))) {s. \<forall>rv. ntfnPtr_' s = option_to_ptr rv \<and> rv \<noteq> Some 0 \<longrightarrow> s \<in> ?Q'104 tcba rv (ntfnPtr_' s)}
 6. \<And>tcba s s'. \<lbrakk>tcba = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (no_0_obj' and valid_objs' and ?R104 tcba) s \<and> s' \<in> UNIV \<inter> ?R'104 tcba proof (prove)
goal (6 subgoals):
 1. \<And>x \<sigma> xa ko. \<lbrakk>(\<sigma>, xa) \<in> rf_sr; no_0_obj' \<sigma>; valid_objs' \<sigma>; \<forall>tcba. ko_at' tcba tcb \<sigma> \<longrightarrow> x = tcbBoundNotification tcba \<and> (\<exists>tcb'. cslift xa (tcb_ptr_to_ctcb_ptr tcb) = Some tcb' \<and> ctcb_relation tcba tcb'); ko_at' ko tcb \<sigma>\<rbrakk> \<Longrightarrow> xa \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr tcb \<and> h_val (hrs_mem (t_hrs_' (globals xa))) (PTR(notification_C ptr) &(tcb_ptr_to_ctcb_ptr tcb\<rightarrow>[''tcbBoundNotification_C''])) = option_to_ptr (tcbBoundNotification ko) \<and> tcbBoundNotification ko \<noteq> Some 0
 2. \<And>tcba rv' t t'. tcba = tcb_ptr_to_ctcb_ptr tcb \<Longrightarrow> ceqv \<Gamma> ntfnPtr_' rv' t t' (IF \<acute>ntfnPtr \<noteq> NULL THEN
  CALL doUnbindNotification_'proc(\<acute>ntfnPtr,tcba)
FI) (?d'104 tcba rv')
 3. \<And>tcba rv rv'. \<lbrakk>tcba = tcb_ptr_to_ctcb_ptr tcb; rv' = option_to_ptr rv \<and> rv \<noteq> Some 0\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q104 tcba rv) (?Q'104 tcba rv rv') [SKIP] (case rv of None \<Rightarrow> return () | Some ntfnPtr' \<Rightarrow> do ntfn <- getNotification ntfnPtr';
y <- setNotification ntfnPtr' (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None tcb
od) (?d'104 tcba rv')
 4. \<And>tcba. tcba = tcb_ptr_to_ctcb_ptr tcb \<Longrightarrow> \<lbrace>?R104 tcba\<rbrace> getBoundNotification tcb \<lbrace>?Q104 tcba\<rbrace>
 5. \<And>tcba. tcba = tcb_ptr_to_ctcb_ptr tcb \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F104 tcba\<^esub> (?R'104 tcba) Guard C_Guard {s. s \<Turnstile>\<^sub>c tcba} (\<acute>ntfnPtr :== h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcba\<rightarrow>[''tcbBoundNotification_C'']))) {s. \<forall>rv. ntfnPtr_' s = option_to_ptr rv \<and> rv \<noteq> Some 0 \<longrightarrow> s \<in> ?Q'104 tcba rv (ntfnPtr_' s)}
 6. \<And>tcba s s'. \<lbrakk>tcba = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (no_0_obj' and valid_objs' and ?R104 tcba) s \<and> s' \<in> UNIV \<inter> ?R'104 tcba proof (prove)
goal (6 subgoals):
 1. \<And>\<sigma> xa ko tcb'. \<lbrakk>(\<sigma>, xa) \<in> rf_sr; no_0_obj' \<sigma>; valid_objs' \<sigma>; ko_at' ko tcb \<sigma>; cslift xa (tcb_ptr_to_ctcb_ptr tcb) = Some tcb'; ctcb_relation ko tcb'\<rbrakk> \<Longrightarrow> xa \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr tcb \<and> h_val (hrs_mem (t_hrs_' (globals xa))) (PTR(notification_C ptr) &(tcb_ptr_to_ctcb_ptr tcb\<rightarrow>[''tcbBoundNotification_C''])) = option_to_ptr (tcbBoundNotification ko) \<and> tcbBoundNotification ko \<noteq> Some 0
 2. \<And>tcba rv' t t'. tcba = tcb_ptr_to_ctcb_ptr tcb \<Longrightarrow> ceqv \<Gamma> ntfnPtr_' rv' t t' (IF \<acute>ntfnPtr \<noteq> NULL THEN
  CALL doUnbindNotification_'proc(\<acute>ntfnPtr,tcba)
FI) (?d'104 tcba rv')
 3. \<And>tcba rv rv'. \<lbrakk>tcba = tcb_ptr_to_ctcb_ptr tcb; rv' = option_to_ptr rv \<and> rv \<noteq> Some 0\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q104 tcba rv) (?Q'104 tcba rv rv') [SKIP] (case rv of None \<Rightarrow> return () | Some ntfnPtr' \<Rightarrow> do ntfn <- getNotification ntfnPtr';
y <- setNotification ntfnPtr' (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None tcb
od) (?d'104 tcba rv')
 4. \<And>tcba. tcba = tcb_ptr_to_ctcb_ptr tcb \<Longrightarrow> \<lbrace>?R104 tcba\<rbrace> getBoundNotification tcb \<lbrace>?Q104 tcba\<rbrace>
 5. \<And>tcba. tcba = tcb_ptr_to_ctcb_ptr tcb \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F104 tcba\<^esub> (?R'104 tcba) Guard C_Guard {s. s \<Turnstile>\<^sub>c tcba} (\<acute>ntfnPtr :== h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcba\<rightarrow>[''tcbBoundNotification_C'']))) {s. \<forall>rv. ntfnPtr_' s = option_to_ptr rv \<and> rv \<noteq> Some 0 \<longrightarrow> s \<in> ?Q'104 tcba rv (ntfnPtr_' s)}
 6. \<And>tcba s s'. \<lbrakk>tcba = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (no_0_obj' and valid_objs' and ?R104 tcba) s \<and> s' \<in> UNIV \<inter> ?R'104 tcba proof (prove)
goal (6 subgoals):
 1. \<And>\<sigma> xa ko tcb'. \<lbrakk>(\<sigma>, xa) \<in> rf_sr; no_0_obj' \<sigma>; valid_objs' \<sigma>; ko_at' ko tcb \<sigma>; cslift xa (tcb_ptr_to_ctcb_ptr tcb) = Some tcb'; tcbFaultHandler ko = tcbFaultHandler_C tcb'; cthread_state_relation (tcbState ko) (tcbState_C tcb', tcbFault_C tcb'); tcbIPCBuffer ko = tcbIPCBuffer_C tcb'; carch_tcb_relation (tcbArch ko) (tcbArch_C tcb'); tcbQueued ko = to_bool (tcbQueued_CL (thread_state_lift (tcbState_C tcb'))); UCAST(8 \<rightarrow> 32) (tcbDomain ko) = tcbDomain_C tcb'; UCAST(8 \<rightarrow> 32) (tcbPriority ko) = tcbPriority_C tcb'; UCAST(8 \<rightarrow> 32) (tcbMCP ko) = tcbMCP_C tcb'; tcbTimeSlice ko = unat (tcbTimeSlice_C tcb'); cfault_rel (tcbFault ko) (seL4_Fault_lift (tcbFault_C tcb')) (lookup_fault_lift (tcbLookupFailure_C tcb')); option_to_ptr (Some 0) = tcbBoundNotification_C tcb'; tcbBoundNotification ko = Some 0\<rbrakk> \<Longrightarrow> False
 2. \<And>tcba rv' t t'. tcba = tcb_ptr_to_ctcb_ptr tcb \<Longrightarrow> ceqv \<Gamma> ntfnPtr_' rv' t t' (IF \<acute>ntfnPtr \<noteq> NULL THEN
  CALL doUnbindNotification_'proc(\<acute>ntfnPtr,tcba)
FI) (?d'104 tcba rv')
 3. \<And>tcba rv rv'. \<lbrakk>tcba = tcb_ptr_to_ctcb_ptr tcb; rv' = option_to_ptr rv \<and> rv \<noteq> Some 0\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q104 tcba rv) (?Q'104 tcba rv rv') [SKIP] (case rv of None \<Rightarrow> return () | Some ntfnPtr' \<Rightarrow> do ntfn <- getNotification ntfnPtr';
y <- setNotification ntfnPtr' (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None tcb
od) (?d'104 tcba rv')
 4. \<And>tcba. tcba = tcb_ptr_to_ctcb_ptr tcb \<Longrightarrow> \<lbrace>?R104 tcba\<rbrace> getBoundNotification tcb \<lbrace>?Q104 tcba\<rbrace>
 5. \<And>tcba. tcba = tcb_ptr_to_ctcb_ptr tcb \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F104 tcba\<^esub> (?R'104 tcba) Guard C_Guard {s. s \<Turnstile>\<^sub>c tcba} (\<acute>ntfnPtr :== h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcba\<rightarrow>[''tcbBoundNotification_C'']))) {s. \<forall>rv. ntfnPtr_' s = option_to_ptr rv \<and> rv \<noteq> Some 0 \<longrightarrow> s \<in> ?Q'104 tcba rv (ntfnPtr_' s)}
 6. \<And>tcba s s'. \<lbrakk>tcba = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (no_0_obj' and valid_objs' and ?R104 tcba) s \<and> s' \<in> UNIV \<inter> ?R'104 tcba proof (prove)
goal (6 subgoals):
 1. \<And>\<sigma> xa ko tcb'. \<lbrakk>(\<sigma>, xa) \<in> rf_sr; no_0_obj' \<sigma>; valid_objs' \<sigma>; cslift xa (tcb_ptr_to_ctcb_ptr tcb) = Some tcb'; tcbFaultHandler ko = tcbFaultHandler_C tcb'; cthread_state_relation (tcbState ko) (tcbState_C tcb', tcbFault_C tcb'); tcbIPCBuffer ko = tcbIPCBuffer_C tcb'; carch_tcb_relation (tcbArch ko) (tcbArch_C tcb'); tcbQueued ko = to_bool (tcbQueued_CL (thread_state_lift (tcbState_C tcb'))); UCAST(8 \<rightarrow> 32) (tcbDomain ko) = tcbDomain_C tcb'; UCAST(8 \<rightarrow> 32) (tcbPriority ko) = tcbPriority_C tcb'; UCAST(8 \<rightarrow> 32) (tcbMCP ko) = tcbMCP_C tcb'; tcbTimeSlice ko = unat (tcbTimeSlice_C tcb'); cfault_rel (tcbFault ko) (seL4_Fault_lift (tcbFault_C tcb')) (lookup_fault_lift (tcbLookupFailure_C tcb')); option_to_ptr (Some 0) = tcbBoundNotification_C tcb'; tcbBoundNotification ko = Some 0; valid_obj' (injectKOS ko) \<sigma>\<rbrakk> \<Longrightarrow> False
 2. \<And>tcba rv' t t'. tcba = tcb_ptr_to_ctcb_ptr tcb \<Longrightarrow> ceqv \<Gamma> ntfnPtr_' rv' t t' (IF \<acute>ntfnPtr \<noteq> NULL THEN
  CALL doUnbindNotification_'proc(\<acute>ntfnPtr,tcba)
FI) (?d'104 tcba rv')
 3. \<And>tcba rv rv'. \<lbrakk>tcba = tcb_ptr_to_ctcb_ptr tcb; rv' = option_to_ptr rv \<and> rv \<noteq> Some 0\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q104 tcba rv) (?Q'104 tcba rv rv') [SKIP] (case rv of None \<Rightarrow> return () | Some ntfnPtr' \<Rightarrow> do ntfn <- getNotification ntfnPtr';
y <- setNotification ntfnPtr' (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None tcb
od) (?d'104 tcba rv')
 4. \<And>tcba. tcba = tcb_ptr_to_ctcb_ptr tcb \<Longrightarrow> \<lbrace>?R104 tcba\<rbrace> getBoundNotification tcb \<lbrace>?Q104 tcba\<rbrace>
 5. \<And>tcba. tcba = tcb_ptr_to_ctcb_ptr tcb \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F104 tcba\<^esub> (?R'104 tcba) Guard C_Guard {s. s \<Turnstile>\<^sub>c tcba} (\<acute>ntfnPtr :== h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcba\<rightarrow>[''tcbBoundNotification_C'']))) {s. \<forall>rv. ntfnPtr_' s = option_to_ptr rv \<and> rv \<noteq> Some 0 \<longrightarrow> s \<in> ?Q'104 tcba rv (ntfnPtr_' s)}
 6. \<And>tcba s s'. \<lbrakk>tcba = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (no_0_obj' and valid_objs' and ?R104 tcba) s \<and> s' \<in> UNIV \<inter> ?R'104 tcba proof (prove)
goal (5 subgoals):
 1. \<And>tcba rv' t t'. tcba = tcb_ptr_to_ctcb_ptr tcb \<Longrightarrow> ceqv \<Gamma> ntfnPtr_' rv' t t' (IF \<acute>ntfnPtr \<noteq> NULL THEN
  CALL doUnbindNotification_'proc(\<acute>ntfnPtr,tcba)
FI) (?d'104 tcba rv')
 2. \<And>tcba rv rv'. \<lbrakk>tcba = tcb_ptr_to_ctcb_ptr tcb; rv' = option_to_ptr rv \<and> rv \<noteq> Some 0\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q104 tcba rv) (?Q'104 tcba rv rv') [SKIP] (case rv of None \<Rightarrow> return () | Some ntfnPtr' \<Rightarrow> do ntfn <- getNotification ntfnPtr';
y <- setNotification ntfnPtr' (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None tcb
od) (?d'104 tcba rv')
 3. \<And>tcba. tcba = tcb_ptr_to_ctcb_ptr tcb \<Longrightarrow> \<lbrace>?R104 tcba\<rbrace> getBoundNotification tcb \<lbrace>?Q104 tcba\<rbrace>
 4. \<And>tcba. tcba = tcb_ptr_to_ctcb_ptr tcb \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F104 tcba\<^esub> (?R'104 tcba) Guard C_Guard {s. s \<Turnstile>\<^sub>c tcba} (\<acute>ntfnPtr :== h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcba\<rightarrow>[''tcbBoundNotification_C'']))) {s. \<forall>rv. ntfnPtr_' s = option_to_ptr rv \<and> rv \<noteq> Some 0 \<longrightarrow> s \<in> ?Q'104 tcba rv (ntfnPtr_' s)}
 5. \<And>tcba s s'. \<lbrakk>tcba = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (no_0_obj' and valid_objs' and ?R104 tcba) s \<and> s' \<in> UNIV \<inter> ?R'104 tcba proof (prove)
goal (4 subgoals):
 1. \<And>tcba rv rv'. \<lbrakk>tcba = tcb_ptr_to_ctcb_ptr tcb; rv' = option_to_ptr rv \<and> rv \<noteq> Some 0\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q104 tcba rv) (?Q'104 tcba rv rv') [SKIP] (case rv of None \<Rightarrow> return () | Some ntfnPtr' \<Rightarrow> do ntfn <- getNotification ntfnPtr';
y <- setNotification ntfnPtr' (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None tcb
od) (IF rv' \<noteq> NULL THEN
  CALL doUnbindNotification_'proc(rv',tcba)
FI)
 2. \<And>tcba. tcba = tcb_ptr_to_ctcb_ptr tcb \<Longrightarrow> \<lbrace>?R104 tcba\<rbrace> getBoundNotification tcb \<lbrace>?Q104 tcba\<rbrace>
 3. \<And>tcba. tcba = tcb_ptr_to_ctcb_ptr tcb \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F104 tcba\<^esub> (?R'104 tcba) Guard C_Guard {s. s \<Turnstile>\<^sub>c tcba} (\<acute>ntfnPtr :== h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcba\<rightarrow>[''tcbBoundNotification_C'']))) {s. \<forall>rv. ntfnPtr_' s = option_to_ptr rv \<and> rv \<noteq> Some 0 \<longrightarrow> s \<in> ?Q'104 tcba rv (ntfnPtr_' s)}
 4. \<And>tcba s s'. \<lbrakk>tcba = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (no_0_obj' and valid_objs' and ?R104 tcba) s \<and> s' \<in> UNIV \<inter> ?R'104 tcba proof (prove)
goal (4 subgoals):
 1. \<And>tcba rv. \<lbrakk>tcba = tcb_ptr_to_ctcb_ptr tcb; rv \<noteq> Some 0\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q104 (tcb_ptr_to_ctcb_ptr tcb) rv) (?Q'104 (tcb_ptr_to_ctcb_ptr tcb) rv (option_to_ptr rv)) [SKIP] (case rv of None \<Rightarrow> return () | Some ntfnPtr' \<Rightarrow> do ntfn <- getNotification ntfnPtr';
y <- setNotification ntfnPtr' (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None tcb
od) (Cond (if option_to_ptr rv \<noteq> NULL then UNIV else {}) (CALL doUnbindNotification_'proc(option_to_ptr rv,tcb_ptr_to_ctcb_ptr tcb)) SKIP)
 2. \<And>tcba. tcba = tcb_ptr_to_ctcb_ptr tcb \<Longrightarrow> \<lbrace>?R104 tcba\<rbrace> getBoundNotification tcb \<lbrace>?Q104 tcba\<rbrace>
 3. \<And>tcba. tcba = tcb_ptr_to_ctcb_ptr tcb \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F104 tcba\<^esub> (?R'104 tcba) Guard C_Guard {s. s \<Turnstile>\<^sub>c tcba} (\<acute>ntfnPtr :== h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcba\<rightarrow>[''tcbBoundNotification_C'']))) {s. \<forall>rv. ntfnPtr_' s = option_to_ptr rv \<and> rv \<noteq> Some 0 \<longrightarrow> s \<in> ?Q'104 tcba rv (ntfnPtr_' s)}
 4. \<And>tcba s s'. \<lbrakk>tcba = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (no_0_obj' and valid_objs' and ?R104 tcba) s \<and> s' \<in> UNIV \<inter> ?R'104 tcba proof (prove)
goal (5 subgoals):
 1. \<And>tcba rv. \<lbrakk>tcba = tcb_ptr_to_ctcb_ptr tcb; rv \<noteq> Some 0; rv = None\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R219 (tcb_ptr_to_ctcb_ptr tcb) rv) (?R''222 (tcb_ptr_to_ctcb_ptr tcb) rv (option_to_ptr rv)) [SKIP] (return ()) (Cond (if option_to_ptr rv \<noteq> NULL then UNIV else {}) (CALL doUnbindNotification_'proc(option_to_ptr rv,tcb_ptr_to_ctcb_ptr tcb)) SKIP)
 2. \<And>tcba rv x2. \<lbrakk>tcba = tcb_ptr_to_ctcb_ptr tcb; rv \<noteq> Some 0; rv = Some x2\<rbrakk> \<Longrightarrow> ccorres dc xfdc (\<lambda>a. ?R218 (tcb_ptr_to_ctcb_ptr tcb) rv a x2) (?R''220 (tcb_ptr_to_ctcb_ptr tcb) rv (option_to_ptr rv) x2) [SKIP] (do ntfn <- getNotification x2;
y <- setNotification x2 (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None tcb
od) (Cond (if option_to_ptr rv \<noteq> NULL then UNIV else {}) (CALL doUnbindNotification_'proc(option_to_ptr rv,tcb_ptr_to_ctcb_ptr tcb)) SKIP)
 3. \<And>tcba. tcba = tcb_ptr_to_ctcb_ptr tcb \<Longrightarrow> \<lbrace>?R104 tcba\<rbrace> getBoundNotification tcb \<lbrace>\<lambda>a b. (a = None \<longrightarrow> ?R219 tcba a b) \<and> (\<forall>x. a = Some x \<longrightarrow> ?R218 tcba a b x)\<rbrace>
 4. \<And>tcba. tcba = tcb_ptr_to_ctcb_ptr tcb \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F104 tcba\<^esub> (?R'104 tcba) Guard C_Guard {s. s \<Turnstile>\<^sub>c tcba} (\<acute>ntfnPtr :== h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcba\<rightarrow>[''tcbBoundNotification_C'']))) {s. \<forall>rv. ntfnPtr_' s = option_to_ptr rv \<and> rv \<noteq> Some 0 \<longrightarrow> s \<in> {sa. rv = None \<longrightarrow> sa \<in> ?R''222 tcba rv (ntfnPtr_' s)} \<inter> {sa. \<forall>x. sa \<in> {sa. rv = Some x \<longrightarrow> sa \<in> ?R''220 tcba rv (ntfnPtr_' s) x}}}
 5. \<And>tcba s s'. \<lbrakk>tcba = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (no_0_obj' and valid_objs' and ?R104 tcba) s \<and> s' \<in> UNIV \<inter> ?R'104 tcba proof (prove)
goal (5 subgoals):
 1. \<And>tcba rv. \<lbrakk>tcba = tcb_ptr_to_ctcb_ptr tcb; rv \<noteq> Some 0; rv = None\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R219 (tcb_ptr_to_ctcb_ptr tcb) rv) (?R'230 (tcb_ptr_to_ctcb_ptr tcb) rv (option_to_ptr rv)) [SKIP] (return ()) SKIP
 2. \<And>tcba rv x2. \<lbrakk>tcba = tcb_ptr_to_ctcb_ptr tcb; rv \<noteq> Some 0; rv = Some x2\<rbrakk> \<Longrightarrow> ccorres dc xfdc (\<lambda>a. ?R218 (tcb_ptr_to_ctcb_ptr tcb) rv a x2) (?R''220 (tcb_ptr_to_ctcb_ptr tcb) rv (option_to_ptr rv) x2) [SKIP] (do ntfn <- getNotification x2;
y <- setNotification x2 (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None tcb
od) (Cond (if option_to_ptr rv \<noteq> NULL then UNIV else {}) (CALL doUnbindNotification_'proc(option_to_ptr rv,tcb_ptr_to_ctcb_ptr tcb)) SKIP)
 3. \<And>tcba. tcba = tcb_ptr_to_ctcb_ptr tcb \<Longrightarrow> \<lbrace>?R104 tcba\<rbrace> getBoundNotification tcb \<lbrace>\<lambda>a b. (a = None \<longrightarrow> ?R219 tcba a b) \<and> (\<forall>x. a = Some x \<longrightarrow> ?R218 tcba a b x)\<rbrace>
 4. \<And>tcba. tcba = tcb_ptr_to_ctcb_ptr tcb \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F104 tcba\<^esub> (?R'104 tcba) Guard C_Guard {s. s \<Turnstile>\<^sub>c tcba} (\<acute>ntfnPtr :== h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcba\<rightarrow>[''tcbBoundNotification_C'']))) {s. \<forall>rv. ntfnPtr_' s = option_to_ptr rv \<and> rv \<noteq> Some 0 \<longrightarrow> s \<in> {sa. rv = None \<longrightarrow> sa \<in> ?R'230 tcba rv (ntfnPtr_' s) \<inter> - (if ntfnPtr_' s \<noteq> NULL then UNIV else {})} \<inter> {sa. \<forall>x. sa \<in> {sa. rv = Some x \<longrightarrow> sa \<in> ?R''220 tcba rv (ntfnPtr_' s) x}}}
 5. \<And>tcba s s'. \<lbrakk>tcba = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (no_0_obj' and valid_objs' and ?R104 tcba) s \<and> s' \<in> UNIV \<inter> ?R'104 tcba proof (prove)
goal (4 subgoals):
 1. \<And>tcba rv x2. \<lbrakk>tcba = tcb_ptr_to_ctcb_ptr tcb; rv \<noteq> Some 0; rv = Some x2\<rbrakk> \<Longrightarrow> ccorres dc xfdc (\<lambda>a. ?R218 (tcb_ptr_to_ctcb_ptr tcb) rv a x2) (?R''220 (tcb_ptr_to_ctcb_ptr tcb) rv (option_to_ptr rv) x2) [SKIP] (do ntfn <- getNotification x2;
y <- setNotification x2 (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None tcb
od) (Cond (if option_to_ptr rv \<noteq> NULL then UNIV else {}) (CALL doUnbindNotification_'proc(option_to_ptr rv,tcb_ptr_to_ctcb_ptr tcb)) SKIP)
 2. \<And>tcba. tcba = tcb_ptr_to_ctcb_ptr tcb \<Longrightarrow> \<lbrace>?R104 tcba\<rbrace> getBoundNotification tcb \<lbrace>\<lambda>a b. (a = None \<longrightarrow> True) \<and> (\<forall>x. a = Some x \<longrightarrow> ?R218 tcba a b x)\<rbrace>
 3. \<And>tcba. tcba = tcb_ptr_to_ctcb_ptr tcb \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F104 tcba\<^esub> (?R'104 tcba) Guard C_Guard {s. s \<Turnstile>\<^sub>c tcba} (\<acute>ntfnPtr :== h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcba\<rightarrow>[''tcbBoundNotification_C'']))) {s. \<forall>rv. ntfnPtr_' s = option_to_ptr rv \<and> rv \<noteq> Some 0 \<longrightarrow> s \<in> {sa. rv = None \<longrightarrow> sa \<in> UNIV \<inter> - (if ntfnPtr_' s \<noteq> NULL then UNIV else {})} \<inter> {sa. \<forall>x. sa \<in> {sa. rv = Some x \<longrightarrow> sa \<in> ?R''220 tcba rv (ntfnPtr_' s) x}}}
 4. \<And>tcba s s'. \<lbrakk>tcba = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (no_0_obj' and valid_objs' and ?R104 tcba) s \<and> s' \<in> UNIV \<inter> ?R'104 tcba proof (prove)
goal (4 subgoals):
 1. \<And>tcba rv x2. \<lbrakk>tcba = tcb_ptr_to_ctcb_ptr tcb; rv \<noteq> Some 0; rv = Some x2\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R238 (tcb_ptr_to_ctcb_ptr tcb) rv x2) (?R'236 (tcb_ptr_to_ctcb_ptr tcb) rv (option_to_ptr rv) x2) [SKIP] (do ntfn <- getNotification x2;
y <- setNotification x2 (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None tcb
od) (CALL doUnbindNotification_'proc(option_to_ptr rv,tcb_ptr_to_ctcb_ptr tcb))
 2. \<And>tcba. tcba = tcb_ptr_to_ctcb_ptr tcb \<Longrightarrow> \<lbrace>?R104 tcba\<rbrace> getBoundNotification tcb \<lbrace>\<lambda>a b. (a = None \<longrightarrow> True) \<and> (\<forall>x. a = Some x \<longrightarrow> ?R238 tcba a x b)\<rbrace>
 3. \<And>tcba. tcba = tcb_ptr_to_ctcb_ptr tcb \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F104 tcba\<^esub> (?R'104 tcba) Guard C_Guard {s. s \<Turnstile>\<^sub>c tcba} (\<acute>ntfnPtr :== h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcba\<rightarrow>[''tcbBoundNotification_C'']))) {s. \<forall>rv. ntfnPtr_' s = option_to_ptr rv \<and> rv \<noteq> Some 0 \<longrightarrow> s \<in> {sa. rv = None \<longrightarrow> sa \<in> UNIV \<inter> - (if ntfnPtr_' s \<noteq> NULL then UNIV else {})} \<inter> {sa. \<forall>x. sa \<in> {sa. rv = Some x \<longrightarrow> sa \<in> ?R'236 tcba rv (ntfnPtr_' s) x \<inter> (if ntfnPtr_' s \<noteq> NULL then UNIV else {})}}}
 4. \<And>tcba s s'. \<lbrakk>tcba = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (no_0_obj' and valid_objs' and ?R104 tcba) s \<and> s' \<in> UNIV \<inter> ?R'104 tcba proof (prove)
goal (3 subgoals):
 1. \<And>tcba. tcba = tcb_ptr_to_ctcb_ptr tcb \<Longrightarrow> \<lbrace>?R104 tcba\<rbrace> getBoundNotification tcb \<lbrace>\<lambda>a b. (a = None \<longrightarrow> True) \<and> (\<forall>x. a = Some x \<longrightarrow> (invs' and tcb_at' tcb) b)\<rbrace>
 2. \<And>tcba. tcba = tcb_ptr_to_ctcb_ptr tcb \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F104 tcba\<^esub> (?R'104 tcba) Guard C_Guard {s. s \<Turnstile>\<^sub>c tcba} (\<acute>ntfnPtr :== h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcba\<rightarrow>[''tcbBoundNotification_C'']))) {s. \<forall>rv. ntfnPtr_' s = option_to_ptr rv \<and> rv \<noteq> Some 0 \<longrightarrow> s \<in> {sa. rv = None \<longrightarrow> sa \<in> UNIV \<inter> - (if ntfnPtr_' s \<noteq> NULL then UNIV else {})} \<inter> {sa. \<forall>x. sa \<in> {sa. rv = Some x \<longrightarrow> sa \<in> {sa. tcbptr_'_update (\<lambda>_. tcba) (ntfnPtr_'_update (\<lambda>_. ntfnPtr_' s) sa) \<in> \<lbrace>\<acute>ntfnPtr = ntfn_Ptr x\<rbrace> \<inter> \<lbrace>\<acute>tcbptr = tcba\<rbrace>} \<inter> (if ntfnPtr_' s \<noteq> NULL then UNIV else {})}}}
 3. \<And>tcba s s'. \<lbrakk>tcba = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (no_0_obj' and valid_objs' and ?R104 tcba) s \<and> s' \<in> UNIV \<inter> ?R'104 tcba proof (prove)
goal (2 subgoals):
 1. \<And>tcba. tcba = tcb_ptr_to_ctcb_ptr tcb \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F104 tcba\<^esub> (?R'104 tcba) Guard C_Guard {s. s \<Turnstile>\<^sub>c tcba} (\<acute>ntfnPtr :== h_val (hrs_mem \<acute>t_hrs) (PTR(notification_C ptr) &(tcba\<rightarrow>[''tcbBoundNotification_C'']))) {s. \<forall>rv. ntfnPtr_' s = option_to_ptr rv \<and> rv \<noteq> Some 0 \<longrightarrow> s \<in> {sa. rv = None \<longrightarrow> sa \<in> UNIV \<inter> - (if ntfnPtr_' s \<noteq> NULL then UNIV else {})} \<inter> {sa. \<forall>x. sa \<in> {sa. rv = Some x \<longrightarrow> sa \<in> {sa. tcbptr_'_update (\<lambda>_. tcba) (ntfnPtr_'_update (\<lambda>_. ntfnPtr_' s) sa) \<in> \<lbrace>\<acute>ntfnPtr = ntfn_Ptr x\<rbrace> \<inter> \<lbrace>\<acute>tcbptr = tcba\<rbrace>} \<inter> (if ntfnPtr_' s \<noteq> NULL then UNIV else {})}}}
 2. \<And>tcba s s'. \<lbrakk>tcba = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (no_0_obj' and valid_objs' and (\<lambda>s. \<forall>ntfn. bound_tcb_at' ((=) ntfn) tcb s \<longrightarrow> (ntfn = None \<longrightarrow> True) \<and> (\<forall>x. ntfn = Some x \<longrightarrow> (invs' and tcb_at' tcb) s))) s \<and> s' \<in> UNIV \<inter> ?R'104 tcba proof (prove)
goal (1 subgoal):
 1. \<And>tcba s s'. \<lbrakk>tcba = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (no_0_obj' and valid_objs' and (\<lambda>s. \<forall>ntfn. bound_tcb_at' ((=) ntfn) tcb s \<longrightarrow> (ntfn = None \<longrightarrow> True) \<and> (\<forall>x. ntfn = Some x \<longrightarrow> (invs' and tcb_at' tcb) s))) s \<and> s' \<in> UNIV \<inter> {s. s \<Turnstile>\<^sub>c tcba \<longrightarrow> (\<forall>rv. h_val (hrs_mem (t_hrs_' (globals s))) (PTR(notification_C ptr) &(tcba\<rightarrow>[''tcbBoundNotification_C''])) = option_to_ptr rv \<and> rv \<noteq> Some 0 \<longrightarrow> (rv = None \<longrightarrow> ntfnPtr_'_update (\<lambda>_. option_to_ptr None) s \<in> - (if option_to_ptr None \<noteq> NULL then UNIV else {})) \<and> (\<forall>x. rv = Some x \<longrightarrow> option_to_ptr (Some x) = ntfn_Ptr x \<and> ntfnPtr_'_update (\<lambda>_. option_to_ptr (Some x)) s \<in> (if option_to_ptr (Some x) \<noteq> NULL then UNIV else {})))} proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s\<rbrakk> \<Longrightarrow> no_0_obj' s \<and> valid_objs' s proof (prove)
goal:
No subgoals!