theory Ipc_R

lemma possibleSwitchTo_iflive[wp]:
  "\<lbrace>if_live_then_nonz_cap' and ex_nonz_cap_to' t
           and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s)\<rbrace>
     possibleSwitchTo t
   \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace>" apply (simp add: possibleSwitchTo_def curDomain_def) apply (wp | wpc | simp)+ apply (simp only: imp_conv_disj, wp hoare_vcg_all_lift hoare_vcg_disj_lift) apply (wp threadGet_wp)+ apply (auto simp: obj_at'_def projectKOs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_live_then_nonz_cap' and ex_nonz_cap_to' t and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s)\<rbrace> possibleSwitchTo t \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_live_then_nonz_cap' and ex_nonz_cap_to' t and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s)\<rbrace> do curDom <- gets ksCurDomain;
targetDom <- threadGet tcbDomain t;
action <- getSchedulerAction;
if targetDom \<noteq> curDom then tcbSchedEnqueue t else if action \<noteq> ResumeCurrentThread then do y <- rescheduleRequired;
tcbSchedEnqueue t
od else setSchedulerAction (SwitchToThread t)
od \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>curDom. \<lbrace>?B7 curDom\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>targetDom s. (targetDom \<noteq> curDom \<longrightarrow> if_live_then_nonz_cap' s \<and> ex_nonz_cap_to' t s) \<and> (targetDom = curDom \<longrightarrow> (ksSchedulerAction s \<noteq> ResumeCurrentThread \<longrightarrow> if_live_then_nonz_cap' s \<and> (\<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> st_tcb_at' runnable' t s) \<and> ex_nonz_cap_to' t s) \<and> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> if_live_then_nonz_cap' s))\<rbrace>
 2. \<lbrace>?Q6\<rbrace> gets ksCurDomain \<lbrace>?B7\<rbrace>
 3. \<And>s. (if_live_then_nonz_cap' and ex_nonz_cap_to' t and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s)) s \<Longrightarrow> ?Q6 s proof (prove)
goal (5 subgoals):
 1. \<And>curDom. \<lbrace>?P22 curDom\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>rv s. \<not> rv \<noteq> curDom\<rbrace>
 2. \<And>curDom. \<lbrace>?P'22 curDom\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>rv s. if_live_then_nonz_cap' s \<and> ex_nonz_cap_to' t s\<rbrace>
 3. \<And>curDom. \<lbrace>?P'21 curDom\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>rv s. rv \<noteq> curDom \<or> (\<not> ksSchedulerAction s \<noteq> ResumeCurrentThread \<or> if_live_then_nonz_cap' s \<and> (\<forall>t. sch_act_not t s \<or> st_tcb_at' runnable' t s) \<and> ex_nonz_cap_to' t s) \<and> (ksSchedulerAction s \<noteq> ResumeCurrentThread \<or> if_live_then_nonz_cap' s)\<rbrace>
 4. \<lbrace>?Q6\<rbrace> gets ksCurDomain \<lbrace>\<lambda>curDom s. (?P22 curDom s \<or> ?P'22 curDom s) \<and> ?P'21 curDom s\<rbrace>
 5. \<And>s. (if_live_then_nonz_cap' and ex_nonz_cap_to' t and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s)) s \<Longrightarrow> ?Q6 s proof (prove)
goal (1 subgoal):
 1. \<And>s. (if_live_then_nonz_cap' and ex_nonz_cap_to' t and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s)) s \<Longrightarrow> ((tcb_at' t s \<longrightarrow> (\<exists>tcb. ko_at' tcb t s \<and> \<not> tcbDomain tcb \<noteq> ksCurDomain s)) \<or> (tcb_at' t s \<longrightarrow> (\<exists>tcb. ko_at' tcb t s \<and> if_live_then_nonz_cap' s \<and> ex_nonz_cap_to' t s))) \<and> (tcb_at' t s \<longrightarrow> (\<exists>tcb. ko_at' tcb t s \<and> (tcbDomain tcb \<noteq> ksCurDomain s \<or> (\<not> ksSchedulerAction s \<noteq> ResumeCurrentThread \<or> if_live_then_nonz_cap' s \<and> (\<forall>t. sch_act_not t s \<or> st_tcb_at' runnable' t s) \<and> ex_nonz_cap_to' t s) \<and> (ksSchedulerAction s \<noteq> ResumeCurrentThread \<or> if_live_then_nonz_cap' s)))) proof (prove)
goal:
No subgoals!