kings-crown/FVELER_Isabelle huggingface dataset:
theory Schedule_R

lemma switchToIdleThread_ct_not_queued_no_cicd':
  "\<lbrace> invs_no_cicd' \<rbrace> switchToIdleThread \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<rbrace>" apply (simp add: Thread_H.switchToIdleThread_def) apply (wp setCurThread_obj_at') apply (rule idle'_not_tcbQueued') apply (simp add: invs_no_cicd'_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> global.switchToIdleThread \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> do thread <- getIdleThread;
y <- Arch.switchToIdleThread;
setCurThread thread
od \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksIdleThread s) s proof (prove)
goal (3 subgoals):
 1. \<And>s. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> Invariants_H.valid_queues s
 2. \<And>s. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> valid_queues' s
 3. \<And>s. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> valid_idle' s proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma switchToIdleThread_activatable_2[wp]:
  "\<lbrace>invs_no_cicd'\<rbrace> switchToIdleThread \<lbrace>\<lambda>rv. ct_in_state' activatable'\<rbrace>" apply (simp add: Thread_H.switchToIdleThread_def
                   ARM_H.switchToIdleThread_def) apply (wp setCurThread_ct_in_state) apply (clarsimp simp: all_invs_but_ct_idle_or_in_cur_domain'_def valid_state'_def valid_idle'_def
                        pred_tcb_at'_def obj_at'_def idle_tcb'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> global.switchToIdleThread \<lbrace>\<lambda>rv. ct_in_state' activatable'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> do thread <- getIdleThread;
y <- getIdleThread >>= setVMRoot;
setCurThread thread
od \<lbrace>\<lambda>rv. ct_in_state' activatable'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> obj_at' (activatable' \<circ> tcbState) (ksIdleThread s) s proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma switchToThread_tcb_in_cur_domain':
  "\<lbrace>tcb_in_cur_domain' thread\<rbrace>
   ThreadDecls_H.switchToThread thread
   \<lbrace>\<lambda>y s. tcb_in_cur_domain' (ksCurThread s) s\<rbrace>" apply (simp add: Thread_H.switchToThread_def setCurThread_def) apply (wpsimp wp: tcbSchedDequeue_not_tcbQueued) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_in_cur_domain' thread\<rbrace> global.switchToThread thread \<lbrace>\<lambda>y s. tcb_in_cur_domain' (ksCurThread s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_in_cur_domain' thread\<rbrace> do y <- Arch.switchToThread thread;
y <- tcbSchedDequeue thread;
modify (ksCurThread_update (\<lambda>_. thread))
od \<lbrace>\<lambda>y s. tcb_in_cur_domain' (ksCurThread s) s\<rbrace> proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma chooseThread_activatable_2:
  "\<lbrace>invs_no_cicd'\<rbrace> chooseThread \<lbrace>\<lambda>rv. ct_in_state' activatable'\<rbrace>" apply (rule hoare_pre, rule hoare_strengthen_post) apply (rule chooseThread_invs_no_cicd'_posts) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> chooseThread \<lbrace>\<lambda>rv. ct_in_state' activatable'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>?Q\<rbrace> chooseThread \<lbrace>?Q3\<rbrace>
 2. \<And>rv s. ?Q3 rv s \<Longrightarrow> ct_in_state' activatable' s
 3. \<And>s. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<and> ct_in_state' activatable' s \<and> (ksCurThread s = ksIdleThread s \<or> tcb_in_cur_domain' (ksCurThread s) s) \<Longrightarrow> ct_in_state' activatable' s
 2. \<And>s. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma chooseThread_ct_not_queued_2:
  "\<lbrace> invs_no_cicd'\<rbrace> chooseThread \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace>"
    (is "\<lbrace>_\<rbrace> _ \<lbrace>\<lambda>_. ?POST\<rbrace>") apply (rule hoare_pre, rule hoare_strengthen_post) apply (rule chooseThread_invs_no_cicd'_posts) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> chooseThread \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>?Q\<rbrace> chooseThread \<lbrace>?Q3\<rbrace>
 2. \<And>rv s. ?Q3 rv s \<Longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s
 3. \<And>s. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<and> ct_in_state' activatable' s \<and> (ksCurThread s = ksIdleThread s \<or> tcb_in_cur_domain' (ksCurThread s) s) \<Longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s
 2. \<And>s. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma chooseThread_in_cur_domain':
  "\<lbrace> invs_no_cicd' \<rbrace> chooseThread \<lbrace>\<lambda>rv s. ksCurThread s = ksIdleThread s \<or> tcb_in_cur_domain' (ksCurThread s) s\<rbrace>" apply (rule hoare_pre, rule hoare_strengthen_post) apply (rule chooseThread_invs_no_cicd'_posts, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> chooseThread \<lbrace>\<lambda>rv s. ksCurThread s = ksIdleThread s \<or> tcb_in_cur_domain' (ksCurThread s) s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>?Q\<rbrace> chooseThread \<lbrace>?Q3\<rbrace>
 2. \<And>rv s. ?Q3 rv s \<Longrightarrow> ksCurThread s = ksIdleThread s \<or> tcb_in_cur_domain' (ksCurThread s) s
 3. \<And>s. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma scheduleChooseNewThread_invs':
  "\<lbrace> invs' and (\<lambda>s. ksSchedulerAction s = ChooseNewThread) \<rbrace>
   scheduleChooseNewThread
   \<lbrace> \<lambda>_ s. invs' s \<rbrace>" unfolding scheduleChooseNewThread_def apply (wpsimp wp: ssa_invs' chooseThread_invs_no_cicd' chooseThread_ct_not_queued_2
                    chooseThread_activatable_2 chooseThread_invs_no_cicd'
                    chooseThread_in_cur_domain' nextDomain_invs_no_cicd' chooseThread_ct_not_queued_2) apply (clarsimp simp: invs'_to_invs_no_cicd'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and (\<lambda>s. ksSchedulerAction s = ChooseNewThread)\<rbrace> scheduleChooseNewThread \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and (\<lambda>s. ksSchedulerAction s = ChooseNewThread)\<rbrace> do domainTime <- getDomainTime;
when (domainTime = 0) $ nextDomain;
chooseThread;
setSchedulerAction ResumeCurrentThread
od \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>invs' s; ksSchedulerAction s = ChooseNewThread; ksDomainTime s \<noteq> 0\<rbrakk> \<Longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma setCurThread_nosch:
  "\<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace>
  setCurThread t
  \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>" apply (simp add: setCurThread_def) apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> setCurThread t \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> modify (ksCurThread_update (\<lambda>_. t)) \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (ksSchedulerAction s) \<Longrightarrow> P (ksSchedulerAction (s\<lparr>ksCurThread := t\<rparr>)) proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma stt_nosch:
  "\<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace>
  switchToThread t
  \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>" apply (simp add: Thread_H.switchToThread_def ARM_H.switchToThread_def storeWordUser_def) apply (wp setCurThread_nosch hoare_drop_imp |simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> global.switchToThread t \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> do y <- do y <- setVMRoot t;
doMachineOp ARM.clearExMonitor
od;
y <- tcbSchedDequeue t;
setCurThread t
od \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace> proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma stit_nosch[wp]:
  "\<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace>
    switchToIdleThread
   \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>" apply (simp add: Thread_H.switchToIdleThread_def
                   ARM_H.switchToIdleThread_def  storeWordUser_def) apply (wp setCurThread_nosch | simp add: getIdleThread_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> global.switchToIdleThread \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> do thread <- getIdleThread;
y <- getIdleThread >>= setVMRoot;
setCurThread thread
od \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace> proof (prove)
goal:
No subgoals!
theory Schedule_R

lemma schedule_sch:
  "\<lbrace>\<top>\<rbrace> schedule \<lbrace>\<lambda>rv s. ksSchedulerAction s = ResumeCurrentThread\<rbrace>" by (wp setSchedulerAction_direct | wpc| simp add: schedule_def scheduleChooseNewThread_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> ThreadDecls_H.schedule \<lbrace>\<lambda>rv s. ksSchedulerAction s = ResumeCurrentThread\<rbrace>
theory Schedule_R

lemma ssa_ct:
  "\<lbrace>ct_in_state' P\<rbrace> setSchedulerAction sa \<lbrace>\<lambda>rv. ct_in_state' P\<rbrace>" proof - show ?thesis apply (unfold setSchedulerAction_def) apply wp apply (clarsimp simp add: ct_in_state'_def pred_tcb_at'_def) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_in_state' P\<rbrace> setSchedulerAction sa \<lbrace>\<lambda>rv. ct_in_state' P\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>ct_in_state' P\<rbrace> setSchedulerAction sa \<lbrace>\<lambda>rv. ct_in_state' P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_in_state' P\<rbrace> setSchedulerAction sa \<lbrace>\<lambda>rv. ct_in_state' P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_in_state' P\<rbrace> modify (ksSchedulerAction_update (\<lambda>_. sa)) \<lbrace>\<lambda>rv. ct_in_state' P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ct_in_state' P s \<Longrightarrow> ct_in_state' P (s\<lparr>ksSchedulerAction := sa\<rparr>) proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>ct_in_state' P\<rbrace> setSchedulerAction sa \<lbrace>\<lambda>rv. ct_in_state' P\<rbrace>

goal:
No subgoals!
theory Schedule_R

lemma scheduleChooseNewThread_ct_activatable'[wp]:
  "\<lbrace> invs' and (\<lambda>s. ksSchedulerAction s = ChooseNewThread) \<rbrace>
   scheduleChooseNewThread
   \<lbrace>\<lambda>_. ct_in_state' activatable'\<rbrace>" unfolding scheduleChooseNewThread_def by (wpsimp simp: ct_in_state'_def
                wp: ssa_invs' nextDomain_invs_no_cicd'
                    chooseThread_activatable_2[simplified ct_in_state'_def]
         | (rule hoare_lift_Pf[where f=ksCurThread], solves wp)
         | strengthen invs'_invs_no_cicd)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and (\<lambda>s. ksSchedulerAction s = ChooseNewThread)\<rbrace> scheduleChooseNewThread \<lbrace>\<lambda>_. ct_in_state' activatable'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and (\<lambda>s. ksSchedulerAction s = ChooseNewThread)\<rbrace> do domainTime <- getDomainTime;
when (domainTime = 0) $ nextDomain;
chooseThread;
setSchedulerAction ResumeCurrentThread
od \<lbrace>\<lambda>_. ct_in_state' activatable'\<rbrace>
theory Schedule_R

lemma threadSet_sch_act_sane:
  "\<lbrace>sch_act_sane\<rbrace> threadSet f t \<lbrace>\<lambda>_. sch_act_sane\<rbrace>" by (wp sch_act_sane_lift)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>sch_act_sane\<rbrace> threadSet f t \<lbrace>\<lambda>_. sch_act_sane\<rbrace>
theory Schedule_R

lemma rescheduleRequired_sch_act_sane[wp]:
  "\<lbrace>\<top>\<rbrace> rescheduleRequired \<lbrace>\<lambda>rv. sch_act_sane\<rbrace>" apply (simp add: rescheduleRequired_def sch_act_sane_def
                   setSchedulerAction_def) by (wp | wpc | clarsimp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> rescheduleRequired \<lbrace>\<lambda>rv. sch_act_sane\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do action <- getSchedulerAction;
y <- case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return ();
modify (ksSchedulerAction_update (\<lambda>_. ChooseNewThread))
od \<lbrace>\<lambda>rv s. \<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> t \<noteq> ksCurThread s\<rbrace>
theory SimpStrategy

lemma simp_strategy_cong[cong]:
  "simp_strategy name x = simp_strategy name x" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. simp_strategy name x = simp_strategy name x
theory SimpStrategy

lemma Eq_TrueI_ByAssum:
  "P \<Longrightarrow> simp_strategy ByAssum P \<equiv> True" by (simp add: simp_strategy_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P \<Longrightarrow> simp_strategy ByAssum P \<equiv> True
theory SimpStrategy

lemma simp_ByAssum_test:
  "P \<Longrightarrow> simp_strategy ByAssum P" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P \<Longrightarrow> simp_strategy ByAssum P
theory SimpStrategy

lemma simp_strategy_Eq_True:
  "simp_strategy name True \<equiv> True" by (simp add: simp_strategy_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. simp_strategy name True \<equiv> True
theory IpcCancel_R

lemma cancelSignal_simple[wp]:
  "\<lbrace>\<top>\<rbrace> cancelSignal t ntfn \<lbrace>\<lambda>rv. st_tcb_at' simple' t\<rbrace>" apply (simp add: cancelSignal_def Let_def) apply (wp setThreadState_st_tcb | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> cancelSignal t ntfn \<lbrace>\<lambda>rv. st_tcb_at' simple' t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do ntfna <- getNotification ntfn;
y <- assert (case ntfnObj ntfna of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False);
ntfn' <- case delete t (ntfnQueue (ntfnObj ntfna)) of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. delete t (ntfnQueue (ntfnObj ntfna))) (ntfnObj ntfna);
y <- setNotification ntfn (ntfnObj_update (\<lambda>_. ntfn') ntfna);
setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>rv. st_tcb_at' simple' t\<rbrace> proof (prove)
goal:
No subgoals!
theory IpcCancel_R

lemma cancelSignal_pred_tcb_at':
  "\<lbrace>pred_tcb_at' proj P t' and K (t \<noteq> t')\<rbrace>
     cancelSignal t ntfnptr
   \<lbrace>\<lambda>rv. pred_tcb_at' proj P t'\<rbrace>" apply (simp add: cancelSignal_def) apply (wp sts_pred_tcb_neq' getNotification_wp | wpc | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pred_tcb_at' proj P t' and K (t \<noteq> t')\<rbrace> cancelSignal t ntfnptr \<lbrace>\<lambda>rv. pred_tcb_at' proj P t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pred_tcb_at' proj P t' and (\<lambda>y. t \<noteq> t')\<rbrace> do ntfn <- getNotification ntfnptr;
y <- assert (case ntfnObj ntfn of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False);
ntfn' <- case delete t (ntfnQueue (ntfnObj ntfn)) of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. delete t (ntfnQueue (ntfnObj ntfn))) (ntfnObj ntfn);
y <- setNotification ntfnptr (ntfnObj_update (\<lambda>_. ntfn') ntfn);
setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>rv. pred_tcb_at' proj P t'\<rbrace> proof (prove)
goal:
No subgoals!
theory IpcCancel_R

lemma set_ep_pred_tcb_at' [wp]:
  "\<lbrace> pred_tcb_at' proj P t \<rbrace>
   setEndpoint ep v
   \<lbrace> \<lambda>rv. pred_tcb_at' proj P t \<rbrace>" apply (simp add: setEndpoint_def pred_tcb_at'_def) apply (rule obj_at_setObject2) apply simp apply (simp add: updateObject_default_def in_monad projectKOs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pred_tcb_at' proj P t\<rbrace> setEndpoint ep v \<lbrace>\<lambda>rv. pred_tcb_at' proj P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>ko. P (proj (tcb_to_itcb' ko))) t\<rbrace> setObject ep v \<lbrace>\<lambda>rv. obj_at' (\<lambda>ko. P (proj (tcb_to_itcb' ko))) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ko s' v oko x y n s. (ko, s') \<in> fst (updateObject v oko x y n s) \<Longrightarrow> koTypeOf ko \<noteq> koType TYPE(Structures_H.tcb) proof (prove)
goal (1 subgoal):
 1. \<And>ko s' v oko x y n s. (ko, s') \<in> fst (updateObject_default v oko x y n s) \<Longrightarrow> koTypeOf ko \<noteq> TCBT proof (prove)
goal:
No subgoals!
theory IpcCancel_R

lemma valid_inQ_queues_ksSchedulerAction_update[simp]:
  "valid_inQ_queues (ksSchedulerAction_update f s) = valid_inQ_queues s" by (simp add: valid_inQ_queues_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_inQ_queues (ksSchedulerAction_update f s) = valid_inQ_queues s
theory IpcCancel_R

lemma valid_inQ_queues_ksReadyQueuesL1Bitmap_upd[simp]:
  "valid_inQ_queues (ksReadyQueuesL1Bitmap_update f s) = valid_inQ_queues s" unfolding valid_inQ_queues_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_inQ_queues (ksReadyQueuesL1Bitmap_update f s) = valid_inQ_queues s proof (prove)
goal (1 subgoal):
 1. (\<forall>d p. (\<forall>t\<in>set (ksReadyQueues (ksReadyQueuesL1Bitmap_update f s) (d, p)). obj_at' (inQ d p) t (ksReadyQueuesL1Bitmap_update f s)) \<and> distinct (ksReadyQueues (ksReadyQueuesL1Bitmap_update f s) (d, p))) = (\<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). obj_at' (inQ d p) t s) \<and> distinct (ksReadyQueues s (d, p)))
theory IpcCancel_R

lemma valid_inQ_queues_ksReadyQueuesL2Bitmap_upd[simp]:
  "valid_inQ_queues (ksReadyQueuesL2Bitmap_update f s) = valid_inQ_queues s" unfolding valid_inQ_queues_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_inQ_queues (ksReadyQueuesL2Bitmap_update f s) = valid_inQ_queues s proof (prove)
goal (1 subgoal):
 1. (\<forall>d p. (\<forall>t\<in>set (ksReadyQueues (ksReadyQueuesL2Bitmap_update f s) (d, p)). obj_at' (inQ d p) t (ksReadyQueuesL2Bitmap_update f s)) \<and> distinct (ksReadyQueues (ksReadyQueuesL2Bitmap_update f s) (d, p))) = (\<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). obj_at' (inQ d p) t s) \<and> distinct (ksReadyQueues s (d, p)))
theory IpcCancel_R

lemma cancelIPC_tcb_at'[wp]:
  "\<lbrace>tcb_at' t\<rbrace> cancelIPC t' \<lbrace>\<lambda>_. tcb_at' t\<rbrace>" apply (simp add: cancelIPC_def Let_def getThreadReplySlot_def) apply (wp delete_one_typ_ats hoare_drop_imps
       | simp add: o_def if_apply_def2 | wpc | assumption)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at' t\<rbrace> cancelIPC t' \<lbrace>\<lambda>_. tcb_at' t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at' t\<rbrace> do state <- getThreadState t';
case state of Structures_H.thread_state.BlockedOnReceive x xa \<Rightarrow> do ep <- getEndpoint (blockingObject state);
y <- assert (\<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False));
ep' <- case delete t' (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return $ epQueue_update (\<lambda>_. delete t' (epQueue ep)) ep;
y <- setEndpoint (blockingObject state) ep';
setThreadState Structures_H.thread_state.Inactive t'
od | Structures_H.thread_state.BlockedOnReply \<Rightarrow> do y <- threadSet (tcbFault_update (\<lambda>_. None)) t';
slot <- locateSlotTCB t' tcbReplySlot;
callerCap <- liftM (mdbNext \<circ> cteMDBNode) (getCTE slot);
when (callerCap \<noteq> nullPointer) (do y <- stateAssert (capHasProperty callerCap (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne callerCap
od)
od | Structures_H.thread_state.BlockedOnNotification x \<Rightarrow> cancelSignal t' (waitingOnNotification state) | Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<Rightarrow> do ep <- getEndpoint (blockingObject state);
y <- assert (\<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False));
ep' <- case delete t' (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return $ epQueue_update (\<lambda>_. delete t' (epQueue ep)) ep;
y <- setEndpoint (blockingObject state) ep';
setThreadState Structures_H.thread_state.Inactive t'
od | _ \<Rightarrow> return ()
od \<lbrace>\<lambda>_. tcb_at' t\<rbrace> proof (prove)
goal:
No subgoals!
theory IpcCancel_R

lemma invs_weak_sch_act_wf[elim!]:
  "invs' s \<Longrightarrow> weak_sch_act_wf (ksSchedulerAction s) s" apply (drule invs_sch_act_wf') apply (clarsimp simp: weak_sch_act_wf_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs' s \<Longrightarrow> weak_sch_act_wf (ksSchedulerAction s) s proof (prove)
goal (1 subgoal):
 1. sch_act_wf (ksSchedulerAction s) s \<Longrightarrow> weak_sch_act_wf (ksSchedulerAction s) s proof (prove)
goal:
No subgoals!
theory IpcCancel_R

lemma cte_map_tcb_2:
  "cte_map (t, tcb_cnode_index 2) = t + 2*2^cte_level_bits" by (simp add: cte_map_def tcb_cnode_index_def to_bl_1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_map (t, tcb_cnode_index 2) = t + 2 * 2 ^ cte_level_bits
theory IpcCancel_R

lemma cte_wp_at_reply_cap_to_ex_rights:
  "cte_wp_at (is_reply_cap_to t) ptr
   = (\<lambda>s. \<exists>rights. cte_wp_at ((=) (cap.ReplyCap t False rights)) ptr s)" by (rule ext, rule iffI; clarsimp simp: cte_wp_at_def is_reply_cap_to_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at (is_reply_cap_to t) ptr = (\<lambda>s. \<exists>rights. cte_wp_at ((=) (cap.ReplyCap t False rights)) ptr s)