theory IpcCancel_C

lemma cancelSignal_ccorres [corres]:
     "ccorres dc xfdc
      (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) thread)
      (UNIV \<inter> {s. threadPtr_' s = tcb_ptr_to_ctcb_ptr thread} \<inter> {s. ntfnPtr_' s = Ptr ntfn})
      [] (cancelSignal thread ntfn) (Call cancelSignal_'proc)" apply (cinit lift: threadPtr_' ntfnPtr_' simp add: Let_def list_case_return cong add: call_ignore_cong) apply (unfold fun_app_def) apply (simp only: simp_list_case_return return_bind ccorres_seq_skip) apply (rule ccorres_pre_getNotification) apply (rule ccorres_assert) apply (rule ccorres_rhs_assoc2) apply (rule ccorres_rhs_assoc2) apply (rule ccorres_rhs_assoc2) apply (ctac (no_vcg) add: cancelSignal_ccorres_helper) apply (ctac add: setThreadState_ccorres_valid_queues') apply ((wp setNotification_ksQ hoare_vcg_all_lift set_ntfn_valid_objs' | simp add: valid_tcb_state'_def split del: if_split)+)[1] apply (simp add: "StrictC'_thread_state_defs") apply (rule conjI, clarsimp, rule conjI, clarsimp) apply (frule (1) ko_at_valid_ntfn'[OF _ invs_valid_objs']) subgoal by ((auto simp: obj_at'_def projectKOs st_tcb_at'_def invs'_def valid_state'_def
                     isTS_defs cte_wp_at_ctes_of "StrictC'_thread_state_defs"
                     cthread_state_relation_def sch_act_wf_weak valid_ntfn'_def
             dest!: valid_queues_not_runnable'_not_ksQ[where t=thread] |
           clarsimp simp: eq_commute)+) apply (clarsimp) apply (frule (1) ko_at_valid_ntfn'[OF _ invs_valid_objs']) apply (frule (2) ntfn_blocked_in_queueD) by (auto simp: obj_at'_def projectKOs st_tcb_at'_def invs'_def valid_state'_def
                     isTS_defs cte_wp_at_ctes_of "StrictC'_thread_state_defs" valid_ntfn'_def
                     cthread_state_relation_def sch_act_wf_weak isWaitingNtfn_def
             dest!: valid_queues_not_runnable'_not_ksQ[where t=thread]
             split: ntfn.splits option.splits
         |  clarsimp simp: eq_commute
         | drule_tac x=thread in bspec)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) thread) (UNIV \<inter> \<lbrace>\<acute>threadPtr = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>ntfnPtr = ntfn_Ptr ntfn\<rbrace>) [] (cancelSignal thread ntfn) (Call cancelSignal_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>ntfnPtr threadPtr. \<lbrakk>ntfnPtr = ntfn_Ptr ntfn; threadPtr = tcb_ptr_to_ctcb_ptr thread\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q490 ntfnPtr threadPtr) (?Q'490 ntfnPtr threadPtr) [SKIP] (do ntfna <- getNotification ntfn;
y <- assert (case ntfnObj ntfna of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False);
ntfn' <- case remove1 thread (ntfnQueue (ntfnObj ntfna)) of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. remove1 thread (ntfnQueue (ntfnObj ntfna))) (ntfnObj ntfna);
y <- setNotification ntfn (ntfnObj_update (\<lambda>_. ntfn') ntfna);
setThreadState Structures_H.thread_state.Inactive thread
od) (\<acute>ntfn_queue :== CALL ntfn_ptr_get_queue_'proc(ntfnPtr);;
(\<acute>ntfn_queue :== CALL tcbEPDequeue_'proc(threadPtr,\<acute>ntfn_queue);;
(CALL ntfn_ptr_set_queue_'proc(ntfnPtr,\<acute>ntfn_queue);;
(IF head_C \<acute>ntfn_queue = NULL THEN
  CALL notification_ptr_set_state_'proc(ntfnPtr,SCAST(32 signed \<rightarrow> 32) NtfnState_Idle)
FI;;
CALL setThreadState_'proc(threadPtr,SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive)))))
 2. \<And>ntfnPtr threadPtr s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfn; threadPtr = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) thread) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q490 ntfnPtr threadPtr s \<and> s' \<in> ?Q'490 ntfnPtr threadPtr proof (prove)
goal (2 subgoals):
 1. \<And>ntfnPtr threadPtr. \<lbrakk>ntfnPtr = ntfn_Ptr ntfn; threadPtr = tcb_ptr_to_ctcb_ptr thread\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q490 ntfnPtr threadPtr) (?Q'490 ntfnPtr threadPtr) [SKIP] (do ntfna <- getNotification ntfn;
y <- assert (case ntfnObj ntfna of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False);
ntfn' <- case remove1 thread (ntfnQueue (ntfnObj ntfna)) of [] \<Rightarrow> return Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return (ntfnQueue_update (\<lambda>_. remove1 thread (ntfnQueue (ntfnObj ntfna))) (ntfnObj ntfna));
y <- setNotification ntfn (ntfnObj_update (\<lambda>_. ntfn') ntfna);
setThreadState Structures_H.thread_state.Inactive thread
od) (\<acute>ntfn_queue :== CALL ntfn_ptr_get_queue_'proc(ntfnPtr);;
(\<acute>ntfn_queue :== CALL tcbEPDequeue_'proc(threadPtr,\<acute>ntfn_queue);;
(CALL ntfn_ptr_set_queue_'proc(ntfnPtr,\<acute>ntfn_queue);;
(IF head_C \<acute>ntfn_queue = NULL THEN
  CALL notification_ptr_set_state_'proc(ntfnPtr,SCAST(32 signed \<rightarrow> 32) NtfnState_Idle)
FI;;
CALL setThreadState_'proc(threadPtr,SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive)))))
 2. \<And>ntfnPtr threadPtr s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfn; threadPtr = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) thread) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q490 ntfnPtr threadPtr s \<and> s' \<in> ?Q'490 ntfnPtr threadPtr proof (prove)
goal (2 subgoals):
 1. \<And>ntfnPtr threadPtr. \<lbrakk>ntfnPtr = ntfn_Ptr ntfn; threadPtr = tcb_ptr_to_ctcb_ptr thread\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q490 (ntfn_Ptr ntfn) (tcb_ptr_to_ctcb_ptr thread)) (?Q'490 (ntfn_Ptr ntfn) (tcb_ptr_to_ctcb_ptr thread)) [SKIP] (do ntfna <- getNotification ntfn;
y <- assert (case ntfnObj ntfna of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False);
y <- setNotification ntfn (ntfnObj_update (\<lambda>_. if remove1 thread (ntfnQueue (ntfnObj ntfna)) = [] then Structures_H.ntfn.IdleNtfn else ntfnQueue_update (\<lambda>_. remove1 thread (ntfnQueue (ntfnObj ntfna))) (ntfnObj ntfna)) ntfna);
setThreadState Structures_H.thread_state.Inactive thread
od) (\<acute>ntfn_queue :== CALL ntfn_ptr_get_queue_'proc(ntfn_Ptr ntfn);;
(\<acute>ntfn_queue :== CALL tcbEPDequeue_'proc(tcb_ptr_to_ctcb_ptr thread,\<acute>ntfn_queue);;
(CALL ntfn_ptr_set_queue_'proc(ntfn_Ptr ntfn,\<acute>ntfn_queue);;
(IF head_C \<acute>ntfn_queue = NULL THEN
  CALL notification_ptr_set_state_'proc(ntfn_Ptr ntfn,SCAST(32 signed \<rightarrow> 32) NtfnState_Idle)
FI;;
CALL setThreadState_'proc(tcb_ptr_to_ctcb_ptr thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive)))))
 2. \<And>ntfnPtr threadPtr s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfn; threadPtr = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) thread) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q490 ntfnPtr threadPtr s \<and> s' \<in> ?Q'490 ntfnPtr threadPtr proof (prove)
goal (2 subgoals):
 1. \<And>ntfnPtr threadPtr ntfna. \<lbrakk>ntfnPtr = ntfn_Ptr ntfn; threadPtr = tcb_ptr_to_ctcb_ptr thread\<rbrakk> \<Longrightarrow> ccorres dc xfdc (\<lambda>a. ?P498 (ntfn_Ptr ntfn) (tcb_ptr_to_ctcb_ptr thread) a ntfna) (?P'499 (ntfn_Ptr ntfn) (tcb_ptr_to_ctcb_ptr thread) ntfna) [SKIP] (do y <- assert (case ntfnObj ntfna of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False);
y <- setNotification ntfn (ntfnObj_update (\<lambda>_. if remove1 thread (ntfnQueue (ntfnObj ntfna)) = [] then Structures_H.ntfn.IdleNtfn else ntfnQueue_update (\<lambda>_. remove1 thread (ntfnQueue (ntfnObj ntfna))) (ntfnObj ntfna)) ntfna);
setThreadState Structures_H.thread_state.Inactive thread
od) (\<acute>ntfn_queue :== CALL ntfn_ptr_get_queue_'proc(ntfn_Ptr ntfn);;
(\<acute>ntfn_queue :== CALL tcbEPDequeue_'proc(tcb_ptr_to_ctcb_ptr thread,\<acute>ntfn_queue);;
(CALL ntfn_ptr_set_queue_'proc(ntfn_Ptr ntfn,\<acute>ntfn_queue);;
(IF head_C \<acute>ntfn_queue = NULL THEN
  CALL notification_ptr_set_state_'proc(ntfn_Ptr ntfn,SCAST(32 signed \<rightarrow> 32) NtfnState_Idle)
FI;;
CALL setThreadState_'proc(tcb_ptr_to_ctcb_ptr thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive)))))
 2. \<And>ntfnPtr threadPtr s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfn; threadPtr = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) thread) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>ntfna. ko_at' ntfna ntfn s \<longrightarrow> ?P498 ntfnPtr threadPtr s ntfna) \<and> s' \<in> {s'. \<forall>ntfna s. (s, s') \<in> rf_sr \<and> ko_at' ntfna ntfn s \<longrightarrow> s' \<in> ?P'499 ntfnPtr threadPtr ntfna} proof (prove)
goal (2 subgoals):
 1. \<And>ntfnPtr threadPtr ntfna. \<lbrakk>ntfnPtr = ntfn_Ptr ntfn; threadPtr = tcb_ptr_to_ctcb_ptr thread; case ntfnObj ntfna of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?P505 (ntfn_Ptr ntfn) (tcb_ptr_to_ctcb_ptr thread) ntfna) (?P'499 (ntfn_Ptr ntfn) (tcb_ptr_to_ctcb_ptr thread) ntfna) [SKIP] (do y <- setNotification ntfn (ntfnObj_update (\<lambda>_. if remove1 thread (ntfnQueue (ntfnObj ntfna)) = [] then Structures_H.ntfn.IdleNtfn else ntfnQueue_update (\<lambda>_. remove1 thread (ntfnQueue (ntfnObj ntfna))) (ntfnObj ntfna)) ntfna);
setThreadState Structures_H.thread_state.Inactive thread
od) (\<acute>ntfn_queue :== CALL ntfn_ptr_get_queue_'proc(ntfn_Ptr ntfn);;
(\<acute>ntfn_queue :== CALL tcbEPDequeue_'proc(tcb_ptr_to_ctcb_ptr thread,\<acute>ntfn_queue);;
(CALL ntfn_ptr_set_queue_'proc(ntfn_Ptr ntfn,\<acute>ntfn_queue);;
(IF head_C \<acute>ntfn_queue = NULL THEN
  CALL notification_ptr_set_state_'proc(ntfn_Ptr ntfn,SCAST(32 signed \<rightarrow> 32) NtfnState_Idle)
FI;;
CALL setThreadState_'proc(tcb_ptr_to_ctcb_ptr thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive)))))
 2. \<And>ntfnPtr threadPtr s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfn; threadPtr = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) thread) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>ntfna. ko_at' ntfna ntfn s \<longrightarrow> ?P505 ntfnPtr threadPtr ntfna s) \<and> s' \<in> {s'. \<forall>ntfna s. (s, s') \<in> rf_sr \<and> ko_at' ntfna ntfn s \<longrightarrow> s' \<in> ?P'499 ntfnPtr threadPtr ntfna} proof (prove)
goal (2 subgoals):
 1. \<And>ntfnPtr threadPtr ntfna. \<lbrakk>ntfnPtr = ntfn_Ptr ntfn; threadPtr = tcb_ptr_to_ctcb_ptr thread; case ntfnObj ntfna of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?P505 (ntfn_Ptr ntfn) (tcb_ptr_to_ctcb_ptr thread) ntfna) (?P'499 (ntfn_Ptr ntfn) (tcb_ptr_to_ctcb_ptr thread) ntfna) [SKIP] (do y <- setNotification ntfn (ntfnObj_update (\<lambda>_. if remove1 thread (ntfnQueue (ntfnObj ntfna)) = [] then Structures_H.ntfn.IdleNtfn else ntfnQueue_update (\<lambda>_. remove1 thread (ntfnQueue (ntfnObj ntfna))) (ntfnObj ntfna)) ntfna);
setThreadState Structures_H.thread_state.Inactive thread
od) (\<acute>ntfn_queue :== CALL ntfn_ptr_get_queue_'proc(ntfn_Ptr ntfn);;
\<acute>ntfn_queue :== CALL tcbEPDequeue_'proc(tcb_ptr_to_ctcb_ptr thread,\<acute>ntfn_queue);;
(CALL ntfn_ptr_set_queue_'proc(ntfn_Ptr ntfn,\<acute>ntfn_queue);;
(IF head_C \<acute>ntfn_queue = NULL THEN
  CALL notification_ptr_set_state_'proc(ntfn_Ptr ntfn,SCAST(32 signed \<rightarrow> 32) NtfnState_Idle)
FI;;
CALL setThreadState_'proc(tcb_ptr_to_ctcb_ptr thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive))))
 2. \<And>ntfnPtr threadPtr s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfn; threadPtr = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) thread) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>ntfna. ko_at' ntfna ntfn s \<longrightarrow> ?P505 ntfnPtr threadPtr ntfna s) \<and> s' \<in> {s'. \<forall>ntfna s. (s, s') \<in> rf_sr \<and> ko_at' ntfna ntfn s \<longrightarrow> s' \<in> ?P'499 ntfnPtr threadPtr ntfna} proof (prove)
goal (2 subgoals):
 1. \<And>ntfnPtr threadPtr ntfna. \<lbrakk>ntfnPtr = ntfn_Ptr ntfn; threadPtr = tcb_ptr_to_ctcb_ptr thread; case ntfnObj ntfna of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?P505 (ntfn_Ptr ntfn) (tcb_ptr_to_ctcb_ptr thread) ntfna) (?P'499 (ntfn_Ptr ntfn) (tcb_ptr_to_ctcb_ptr thread) ntfna) [SKIP] (do y <- setNotification ntfn (ntfnObj_update (\<lambda>_. if remove1 thread (ntfnQueue (ntfnObj ntfna)) = [] then Structures_H.ntfn.IdleNtfn else ntfnQueue_update (\<lambda>_. remove1 thread (ntfnQueue (ntfnObj ntfna))) (ntfnObj ntfna)) ntfna);
setThreadState Structures_H.thread_state.Inactive thread
od) (\<acute>ntfn_queue :== CALL ntfn_ptr_get_queue_'proc(ntfn_Ptr ntfn);;
\<acute>ntfn_queue :== CALL tcbEPDequeue_'proc(tcb_ptr_to_ctcb_ptr thread,\<acute>ntfn_queue);;
CALL ntfn_ptr_set_queue_'proc(ntfn_Ptr ntfn,\<acute>ntfn_queue);;
(IF head_C \<acute>ntfn_queue = NULL THEN
  CALL notification_ptr_set_state_'proc(ntfn_Ptr ntfn,SCAST(32 signed \<rightarrow> 32) NtfnState_Idle)
FI;;
CALL setThreadState_'proc(tcb_ptr_to_ctcb_ptr thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive)))
 2. \<And>ntfnPtr threadPtr s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfn; threadPtr = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) thread) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>ntfna. ko_at' ntfna ntfn s \<longrightarrow> ?P505 ntfnPtr threadPtr ntfna s) \<and> s' \<in> {s'. \<forall>ntfna s. (s, s') \<in> rf_sr \<and> ko_at' ntfna ntfn s \<longrightarrow> s' \<in> ?P'499 ntfnPtr threadPtr ntfna} proof (prove)
goal (2 subgoals):
 1. \<And>ntfnPtr threadPtr ntfna. \<lbrakk>ntfnPtr = ntfn_Ptr ntfn; threadPtr = tcb_ptr_to_ctcb_ptr thread; case ntfnObj ntfna of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?P505 (ntfn_Ptr ntfn) (tcb_ptr_to_ctcb_ptr thread) ntfna) (?P'499 (ntfn_Ptr ntfn) (tcb_ptr_to_ctcb_ptr thread) ntfna) [SKIP] (do y <- setNotification ntfn (ntfnObj_update (\<lambda>_. if remove1 thread (ntfnQueue (ntfnObj ntfna)) = [] then Structures_H.ntfn.IdleNtfn else ntfnQueue_update (\<lambda>_. remove1 thread (ntfnQueue (ntfnObj ntfna))) (ntfnObj ntfna)) ntfna);
setThreadState Structures_H.thread_state.Inactive thread
od) (\<acute>ntfn_queue :== CALL ntfn_ptr_get_queue_'proc(ntfn_Ptr ntfn);;
\<acute>ntfn_queue :== CALL tcbEPDequeue_'proc(tcb_ptr_to_ctcb_ptr thread,\<acute>ntfn_queue);;
CALL ntfn_ptr_set_queue_'proc(ntfn_Ptr ntfn,\<acute>ntfn_queue);;
IF head_C \<acute>ntfn_queue = NULL THEN
  CALL notification_ptr_set_state_'proc(ntfn_Ptr ntfn,SCAST(32 signed \<rightarrow> 32) NtfnState_Idle)
FI;;
CALL setThreadState_'proc(tcb_ptr_to_ctcb_ptr thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive))
 2. \<And>ntfnPtr threadPtr s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfn; threadPtr = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) thread) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>ntfna. ko_at' ntfna ntfn s \<longrightarrow> ?P505 ntfnPtr threadPtr ntfna s) \<and> s' \<in> {s'. \<forall>ntfna s. (s, s') \<in> rf_sr \<and> ko_at' ntfna ntfn s \<longrightarrow> s' \<in> ?P'499 ntfnPtr threadPtr ntfna} proof (prove)
goal (4 subgoals):
 1. \<And>ntfnPtr threadPtr ntfna rv xfdca. \<lbrakk>ntfnPtr = ntfn_Ptr ntfn; threadPtr = tcb_ptr_to_ctcb_ptr thread; case ntfnObj ntfna of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False; dc rv xfdca\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q524 ntfnPtr threadPtr ntfna rv) (?Q'524 ntfnPtr threadPtr ntfna rv xfdca) [SKIP] (setThreadState Structures_H.thread_state.Inactive thread) (CALL setThreadState_'proc(tcb_ptr_to_ctcb_ptr thread,SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive))
 2. \<And>ntfnPtr threadPtr ntfna. \<lbrakk>ntfnPtr = ntfn_Ptr ntfn; threadPtr = tcb_ptr_to_ctcb_ptr thread; case ntfnObj ntfna of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False\<rbrakk> \<Longrightarrow> \<lbrace>?R528 (ntfn_Ptr ntfn) (tcb_ptr_to_ctcb_ptr thread) ntfna\<rbrace> setNotification ntfn (ntfnObj_update (\<lambda>_. if remove1 thread (ntfnQueue (ntfnObj ntfna)) = [] then Structures_H.ntfn.IdleNtfn else ntfnQueue_update (\<lambda>_. remove1 thread (ntfnQueue (ntfnObj ntfna))) (ntfnObj ntfna)) ntfna) \<lbrace>?Q524 ntfnPtr threadPtr ntfna\<rbrace>
 3. \<And>ntfnPtr threadPtr ntfna s rv. \<lbrakk>ntfnPtr = ntfn_Ptr ntfn; threadPtr = tcb_ptr_to_ctcb_ptr thread; case ntfnObj ntfna of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False; dc rv (xfdc s)\<rbrakk> \<Longrightarrow> s \<in> ?Q'524 ntfnPtr threadPtr ntfna rv (xfdc s)
 4. \<And>ntfnPtr threadPtr s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfn; threadPtr = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) thread) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>ntfna. ko_at' ntfna ntfn s \<longrightarrow> (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) thread and ko_at' ntfna ntfn and ?R528 ntfnPtr threadPtr ntfna) s) \<and> s' \<in> {s'. \<forall>ntfna s. (s, s') \<in> rf_sr \<and> ko_at' ntfna ntfn s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (3 subgoals):
 1. \<And>ntfnPtr threadPtr ntfna. \<lbrakk>ntfnPtr = ntfn_Ptr ntfn; threadPtr = tcb_ptr_to_ctcb_ptr thread; case ntfnObj ntfna of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False\<rbrakk> \<Longrightarrow> \<lbrace>?R528 (ntfn_Ptr ntfn) (tcb_ptr_to_ctcb_ptr thread) ntfna\<rbrace> setNotification ntfn (ntfnObj_update (\<lambda>_. if remove1 thread (ntfnQueue (ntfnObj ntfna)) = [] then Structures_H.ntfn.IdleNtfn else ntfnQueue_update (\<lambda>_. remove1 thread (ntfnQueue (ntfnObj ntfna))) (ntfnObj ntfna)) ntfna) \<lbrace>\<lambda>a b. tcb_at' thread b \<and> valid_queues' b \<and> \<not> runnable' Structures_H.thread_state.Inactive \<and> weak_sch_act_wf (ksSchedulerAction b) b \<and> Invariants_H.valid_queues b \<and> (\<forall>p. thread \<notin> set (ksReadyQueues b p)) \<and> sch_act_not thread b \<and> valid_objs' b \<and> valid_tcb_state' Structures_H.thread_state.Inactive b\<rbrace>
 2. \<And>ntfnPtr threadPtr ntfna s rv. \<lbrakk>ntfnPtr = ntfn_Ptr ntfn; threadPtr = tcb_ptr_to_ctcb_ptr thread; case ntfnObj ntfna of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False; dc rv (xfdc s)\<rbrakk> \<Longrightarrow> s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive) (tptr_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr thread) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.Inactive (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr thread\<rbrace>}
 3. \<And>ntfnPtr threadPtr s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfn; threadPtr = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) thread) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>ntfna. ko_at' ntfna ntfn s \<longrightarrow> (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) thread and ko_at' ntfna ntfn and ?R528 ntfnPtr threadPtr ntfna) s) \<and> s' \<in> {s'. \<forall>ntfna s. (s, s') \<in> rf_sr \<and> ko_at' ntfna ntfn s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (2 subgoals):
 1. \<And>ntfnPtr threadPtr ntfna s rv. \<lbrakk>ntfnPtr = ntfn_Ptr ntfn; threadPtr = tcb_ptr_to_ctcb_ptr thread; case ntfnObj ntfna of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False; dc rv (xfdc s)\<rbrakk> \<Longrightarrow> s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_Inactive) (tptr_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr thread) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.Inactive (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr thread\<rbrace>}
 2. \<And>ntfnPtr threadPtr s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfn; threadPtr = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) thread) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>ntfna. ko_at' ntfna ntfn s \<longrightarrow> (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) thread and ko_at' ntfna ntfn and (\<lambda>a. tcb_at' thread a \<and> valid_queues' a \<and> \<not> runnable' Structures_H.thread_state.Inactive \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> Invariants_H.valid_queues a \<and> (\<forall>x. thread \<notin> set (ksReadyQueues a x)) \<and> sch_act_not thread a \<and> (valid_objs' and valid_ntfn' (ntfnObj_update (\<lambda>_. if remove1 thread (ntfnQueue (ntfnObj ntfna)) = [] then Structures_H.ntfn.IdleNtfn else ntfnQueue_update (\<lambda>_. remove1 thread (ntfnQueue (ntfnObj ntfna))) (ntfnObj ntfna)) ntfna)) a \<and> True)) s) \<and> s' \<in> {s'. \<forall>ntfna s. (s, s') \<in> rf_sr \<and> ko_at' ntfna ntfn s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (1 subgoal):
 1. \<And>ntfnPtr threadPtr s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfn; threadPtr = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) thread) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>ntfna. ko_at' ntfna ntfn s \<longrightarrow> (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) thread and ko_at' ntfna ntfn and (\<lambda>a. tcb_at' thread a \<and> valid_queues' a \<and> \<not> runnable' Structures_H.thread_state.Inactive \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> Invariants_H.valid_queues a \<and> (\<forall>x. thread \<notin> set (ksReadyQueues a x)) \<and> sch_act_not thread a \<and> (valid_objs' and valid_ntfn' (ntfnObj_update (\<lambda>_. if remove1 thread (ntfnQueue (ntfnObj ntfna)) = [] then Structures_H.ntfn.IdleNtfn else ntfnQueue_update (\<lambda>_. remove1 thread (ntfnQueue (ntfnObj ntfna))) (ntfnObj ntfna)) ntfna)) a \<and> True)) s) \<and> s' \<in> {s'. \<forall>ntfna s. (s, s') \<in> rf_sr \<and> ko_at' ntfna ntfn s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (3 subgoals):
 1. \<And>s s' ntfna. \<lbrakk>(s, s') \<in> rf_sr; invs' s; st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) thread s; remove1 thread (ntfnQueue (ntfnObj ntfna)) = []; ko_at' ntfna ntfn s\<rbrakk> \<Longrightarrow> tcb_at' thread s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> sch_act_not thread s \<and> valid_objs' s \<and> valid_ntfn' (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfna) s
 2. \<And>s s' ntfna. \<lbrakk>(s, s') \<in> rf_sr; invs' s; st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) thread s\<rbrakk> \<Longrightarrow> remove1 thread (ntfnQueue (ntfnObj ntfna)) \<noteq> [] \<longrightarrow> ko_at' ntfna ntfn s \<longrightarrow> tcb_at' thread s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> sch_act_not thread s \<and> valid_objs' s \<and> valid_ntfn' (ntfnObj_update (\<lambda>_. ntfnQueue_update (\<lambda>_. remove1 thread (ntfnQueue (ntfnObj ntfna))) (ntfnObj ntfna)) ntfna) s
 3. \<And>ntfnPtr threadPtr s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfn; threadPtr = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) thread) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> s' \<in> {s'. \<forall>ntfna s. (s, s') \<in> rf_sr \<and> ko_at' ntfna ntfn s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (3 subgoals):
 1. \<And>s s' ntfna. \<lbrakk>(s, s') \<in> rf_sr; invs' s; st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) thread s; remove1 thread (ntfnQueue (ntfnObj ntfna)) = []; ko_at' ntfna ntfn s; valid_ntfn' ntfna s\<rbrakk> \<Longrightarrow> tcb_at' thread s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> sch_act_not thread s \<and> valid_objs' s \<and> valid_ntfn' (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfna) s
 2. \<And>s s' ntfna. \<lbrakk>(s, s') \<in> rf_sr; invs' s; st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) thread s\<rbrakk> \<Longrightarrow> remove1 thread (ntfnQueue (ntfnObj ntfna)) \<noteq> [] \<longrightarrow> ko_at' ntfna ntfn s \<longrightarrow> tcb_at' thread s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> sch_act_not thread s \<and> valid_objs' s \<and> valid_ntfn' (ntfnObj_update (\<lambda>_. ntfnQueue_update (\<lambda>_. remove1 thread (ntfnQueue (ntfnObj ntfna))) (ntfnObj ntfna)) ntfna) s
 3. \<And>ntfnPtr threadPtr s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfn; threadPtr = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) thread) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> s' \<in> {s'. \<forall>ntfna s. (s, s') \<in> rf_sr \<and> ko_at' ntfna ntfn s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s_, s'_) \<in> rf_sr; invs' s_; st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) thread s_; remove1 thread (ntfnQueue (ntfnObj ntfna_)) = []; ko_at' ntfna_ ntfn s_; valid_ntfn' ntfna_ s_\<rbrakk> \<Longrightarrow> tcb_at' thread s_ \<and> valid_queues' s_ \<and> weak_sch_act_wf (ksSchedulerAction s_) s_ \<and> Invariants_H.valid_queues s_ \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s_ (a, b))) \<and> sch_act_not thread s_ \<and> valid_objs' s_ \<and> valid_ntfn' (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfna_) s_ proof (prove)
goal (2 subgoals):
 1. \<And>s s' ntfna. \<lbrakk>(s, s') \<in> rf_sr; invs' s; st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) thread s\<rbrakk> \<Longrightarrow> remove1 thread (ntfnQueue (ntfnObj ntfna)) \<noteq> [] \<longrightarrow> ko_at' ntfna ntfn s \<longrightarrow> tcb_at' thread s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> sch_act_not thread s \<and> valid_objs' s \<and> valid_ntfn' (ntfnObj_update (\<lambda>_. ntfnQueue_update (\<lambda>_. remove1 thread (ntfnQueue (ntfnObj ntfna))) (ntfnObj ntfna)) ntfna) s
 2. \<And>ntfnPtr threadPtr s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfn; threadPtr = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) thread) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> s' \<in> {s'. \<forall>ntfna s. (s, s') \<in> rf_sr \<and> ko_at' ntfna ntfn s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (2 subgoals):
 1. \<And>s s' ntfna. \<lbrakk>(s, s') \<in> rf_sr; invs' s; st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) thread s; remove1 thread (ntfnQueue (ntfnObj ntfna)) \<noteq> []; ko_at' ntfna ntfn s\<rbrakk> \<Longrightarrow> tcb_at' thread s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> sch_act_not thread s \<and> valid_objs' s \<and> valid_ntfn' (ntfnObj_update (\<lambda>_. ntfnQueue_update (\<lambda>_. remove1 thread (ntfnQueue (ntfnObj ntfna))) (ntfnObj ntfna)) ntfna) s
 2. \<And>ntfnPtr threadPtr s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfn; threadPtr = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) thread) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> s' \<in> {s'. \<forall>ntfna s. (s, s') \<in> rf_sr \<and> ko_at' ntfna ntfn s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (2 subgoals):
 1. \<And>s s' ntfna. \<lbrakk>(s, s') \<in> rf_sr; invs' s; st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) thread s; remove1 thread (ntfnQueue (ntfnObj ntfna)) \<noteq> []; ko_at' ntfna ntfn s; valid_ntfn' ntfna s\<rbrakk> \<Longrightarrow> tcb_at' thread s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> sch_act_not thread s \<and> valid_objs' s \<and> valid_ntfn' (ntfnObj_update (\<lambda>_. ntfnQueue_update (\<lambda>_. remove1 thread (ntfnQueue (ntfnObj ntfna))) (ntfnObj ntfna)) ntfna) s
 2. \<And>ntfnPtr threadPtr s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfn; threadPtr = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) thread) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> s' \<in> {s'. \<forall>ntfna s. (s, s') \<in> rf_sr \<and> ko_at' ntfna ntfn s \<longrightarrow> s' \<in> UNIV} proof (prove)
goal (2 subgoals):
 1. \<And>s s' ntfna. \<lbrakk>(s, s') \<in> rf_sr; invs' s; st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) thread s; remove1 thread (ntfnQueue (ntfnObj ntfna)) \<noteq> []; ko_at' ntfna ntfn s; valid_ntfn' ntfna s; thread \<in> set (ntfnQueue (ntfnObj ntfna)) \<and> isWaitingNtfn (ntfnObj ntfna)\<rbrakk> \<Longrightarrow> tcb_at' thread s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> sch_act_not thread s \<and> valid_objs' s \<and> valid_ntfn' (ntfnObj_update (\<lambda>_. ntfnQueue_update (\<lambda>_. remove1 thread (ntfnQueue (ntfnObj ntfna))) (ntfnObj ntfna)) ntfna) s
 2. \<And>ntfnPtr threadPtr s s'. \<lbrakk>ntfnPtr = ntfn_Ptr ntfn; threadPtr = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (invs' and st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) thread) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> s' \<in> {s'. \<forall>ntfna s. (s, s') \<in> rf_sr \<and> ko_at' ntfna ntfn s \<longrightarrow> s' \<in> UNIV}