theory Syscall_R

lemma threadSet_tcbDomain_update_sch_act_wf[wp]:
  "\<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> sch_act_not t s\<rbrace>
    threadSet (tcbDomain_update (\<lambda>_. domain)) t
   \<lbrace>\<lambda>_ s. sch_act_wf (ksSchedulerAction s) s\<rbrace>" apply (simp add: sch_act_wf_cases split: scheduler_action.split) apply (wp hoare_vcg_conj_lift) apply (simp add: threadSet_def) apply wp apply (wps setObject_sa_unchanged) apply (wp hoare_weak_lift_imp getObject_tcb_wp hoare_vcg_all_lift)+ apply (rename_tac word) apply (rule_tac Q="\<lambda>_ s. ksSchedulerAction s = SwitchToThread word \<longrightarrow>
                            st_tcb_at' runnable' word s \<and> tcb_in_cur_domain' word s \<and> word \<noteq> t"
                   in hoare_strengthen_post) apply (wp hoare_vcg_all_lift hoare_vcg_conj_lift hoare_vcg_imp_lift)+ apply (simp add: threadSet_def) apply (wp getObject_tcb_wp threadSet_tcbDomain_triv')+ apply (auto simp: obj_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> sch_act_not t s\<rbrace> threadSet (tcbDomain_update (\<lambda>_. domain)) t \<lbrace>\<lambda>_ s. sch_act_wf (ksSchedulerAction s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ct_in_state' activatable' s) \<and> (\<forall>x3. ksSchedulerAction s = SwitchToThread x3 \<longrightarrow> st_tcb_at' runnable' x3 s \<and> tcb_in_cur_domain' x3 s \<and> x3 \<noteq> t)\<rbrace> threadSet (tcbDomain_update (\<lambda>_. domain)) t \<lbrace>\<lambda>_ s. (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ct_in_state' activatable' s) \<and> (\<forall>x3. ksSchedulerAction s = SwitchToThread x3 \<longrightarrow> st_tcb_at' runnable' x3 s \<and> tcb_in_cur_domain' x3 s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P18\<rbrace> threadSet (tcbDomain_update (\<lambda>_. domain)) t \<lbrace>\<lambda>rv s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ct_in_state' activatable' s\<rbrace>
 2. \<lbrace>?P'18\<rbrace> threadSet (tcbDomain_update (\<lambda>_. domain)) t \<lbrace>\<lambda>rv s. \<forall>x3. ksSchedulerAction s = SwitchToThread x3 \<longrightarrow> st_tcb_at' runnable' x3 s \<and> tcb_in_cur_domain' x3 s\<rbrace>
 3. \<And>s. (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ct_in_state' activatable' s) \<and> (\<forall>x3. ksSchedulerAction s = SwitchToThread x3 \<longrightarrow> st_tcb_at' runnable' x3 s \<and> tcb_in_cur_domain' x3 s \<and> x3 \<noteq> t) \<Longrightarrow> ?P18 s \<and> ?P'18 s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P18\<rbrace> do tcb <- getObject t;
setObject t (tcbDomain_update (\<lambda>_. domain) tcb)
od \<lbrace>\<lambda>rv s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ct_in_state' activatable' s\<rbrace>
 2. \<lbrace>?P'18\<rbrace> threadSet (tcbDomain_update (\<lambda>_. domain)) t \<lbrace>\<lambda>rv s. \<forall>x3. ksSchedulerAction s = SwitchToThread x3 \<longrightarrow> st_tcb_at' runnable' x3 s \<and> tcb_in_cur_domain' x3 s\<rbrace>
 3. \<And>s. (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ct_in_state' activatable' s) \<and> (\<forall>x3. ksSchedulerAction s = SwitchToThread x3 \<longrightarrow> st_tcb_at' runnable' x3 s \<and> tcb_in_cur_domain' x3 s \<and> x3 \<noteq> t) \<Longrightarrow> ?P18 s \<and> ?P'18 s proof (prove)
goal (4 subgoals):
 1. \<And>tcb. \<lbrace>?B20 tcb\<rbrace> setObject t (tcbDomain_update (\<lambda>_. domain) tcb) \<lbrace>\<lambda>rv s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ct_in_state' activatable' s\<rbrace>
 2. \<lbrace>?P18\<rbrace> getObject t \<lbrace>?B20\<rbrace>
 3. \<lbrace>?P'18\<rbrace> threadSet (tcbDomain_update (\<lambda>_. domain)) t \<lbrace>\<lambda>rv s. \<forall>x3. ksSchedulerAction s = SwitchToThread x3 \<longrightarrow> st_tcb_at' runnable' x3 s \<and> tcb_in_cur_domain' x3 s\<rbrace>
 4. \<And>s. (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ct_in_state' activatable' s) \<and> (\<forall>x3. ksSchedulerAction s = SwitchToThread x3 \<longrightarrow> st_tcb_at' runnable' x3 s \<and> tcb_in_cur_domain' x3 s \<and> x3 \<noteq> t) \<Longrightarrow> ?P18 s \<and> ?P'18 s proof (prove)
goal (4 subgoals):
 1. \<And>tcb prev_s. \<lbrace>?P22 tcb prev_s\<rbrace> setObject t (tcbDomain_update (\<lambda>_. domain) tcb) \<lbrace>\<lambda>rv s'. ksSchedulerAction prev_s = ResumeCurrentThread \<longrightarrow> ct_in_state' activatable' s'\<rbrace>
 2. \<lbrace>?P18\<rbrace> getObject t \<lbrace>\<lambda>tcb s. ?P22 tcb s s\<rbrace>
 3. \<lbrace>?P'18\<rbrace> threadSet (tcbDomain_update (\<lambda>_. domain)) t \<lbrace>\<lambda>rv s. \<forall>x3. ksSchedulerAction s = SwitchToThread x3 \<longrightarrow> st_tcb_at' runnable' x3 s \<and> tcb_in_cur_domain' x3 s\<rbrace>
 4. \<And>s. (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ct_in_state' activatable' s) \<and> (\<forall>x3. ksSchedulerAction s = SwitchToThread x3 \<longrightarrow> st_tcb_at' runnable' x3 s \<and> tcb_in_cur_domain' x3 s \<and> x3 \<noteq> t) \<Longrightarrow> ?P18 s \<and> ?P'18 s proof (prove)
goal (2 subgoals):
 1. \<And>x3. \<lbrace>?P36 x3\<rbrace> threadSet (tcbDomain_update (\<lambda>_. domain)) t \<lbrace>\<lambda>rv s. ksSchedulerAction s = SwitchToThread x3 \<longrightarrow> st_tcb_at' runnable' x3 s \<and> tcb_in_cur_domain' x3 s\<rbrace>
 2. \<And>s. (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ct_in_state' activatable' s) \<and> (\<forall>x3. ksSchedulerAction s = SwitchToThread x3 \<longrightarrow> st_tcb_at' runnable' x3 s \<and> tcb_in_cur_domain' x3 s \<and> x3 \<noteq> t) \<Longrightarrow> (tcb_at' t s \<longrightarrow> (\<exists>ta. ko_at' ta t s \<and> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> (ct_in_state' activatable' and obj_at' ((=) ta) t) s))) \<and> (\<forall>x. ?P36 x s) proof (prove)
goal (2 subgoals):
 1. \<And>word. \<lbrace>?P36 word\<rbrace> threadSet (tcbDomain_update (\<lambda>_. domain)) t \<lbrace>\<lambda>rv s. ksSchedulerAction s = SwitchToThread word \<longrightarrow> st_tcb_at' runnable' word s \<and> tcb_in_cur_domain' word s\<rbrace>
 2. \<And>s. (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ct_in_state' activatable' s) \<and> (\<forall>x3. ksSchedulerAction s = SwitchToThread x3 \<longrightarrow> st_tcb_at' runnable' x3 s \<and> tcb_in_cur_domain' x3 s \<and> x3 \<noteq> t) \<Longrightarrow> (tcb_at' t s \<longrightarrow> (\<exists>ta. ko_at' ta t s \<and> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> (ct_in_state' activatable' and obj_at' ((=) ta) t) s))) \<and> (\<forall>x. ?P36 x s) proof (prove)
goal (3 subgoals):
 1. \<And>word. \<lbrace>?P36 word\<rbrace> threadSet (tcbDomain_update (\<lambda>_. domain)) t \<lbrace>\<lambda>_ s. ksSchedulerAction s = SwitchToThread word \<longrightarrow> st_tcb_at' runnable' word s \<and> tcb_in_cur_domain' word s \<and> word \<noteq> t\<rbrace>
 2. \<And>word rv s. ksSchedulerAction s = SwitchToThread word \<longrightarrow> st_tcb_at' runnable' word s \<and> tcb_in_cur_domain' word s \<and> word \<noteq> t \<Longrightarrow> ksSchedulerAction s = SwitchToThread word \<longrightarrow> st_tcb_at' runnable' word s \<and> tcb_in_cur_domain' word s
 3. \<And>s. (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ct_in_state' activatable' s) \<and> (\<forall>x3. ksSchedulerAction s = SwitchToThread x3 \<longrightarrow> st_tcb_at' runnable' x3 s \<and> tcb_in_cur_domain' x3 s \<and> x3 \<noteq> t) \<Longrightarrow> (tcb_at' t s \<longrightarrow> (\<exists>ta. ko_at' ta t s \<and> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> (ct_in_state' activatable' and obj_at' ((=) ta) t) s))) \<and> (\<forall>x. ?P36 x s) proof (prove)
goal (4 subgoals):
 1. \<And>word. \<lbrace>?P43 word\<rbrace> threadSet (tcbDomain_update (\<lambda>_. domain)) t \<lbrace>\<lambda>rv. st_tcb_at' runnable' word\<rbrace>
 2. \<And>word. \<lbrace>?P'43 word\<rbrace> threadSet (tcbDomain_update (\<lambda>_. domain)) t \<lbrace>\<lambda>rv s. tcb_in_cur_domain' word s \<and> word \<noteq> t\<rbrace>
 3. \<And>word rv s. ksSchedulerAction s = SwitchToThread word \<longrightarrow> st_tcb_at' runnable' word s \<and> tcb_in_cur_domain' word s \<and> word \<noteq> t \<Longrightarrow> ksSchedulerAction s = SwitchToThread word \<longrightarrow> st_tcb_at' runnable' word s \<and> tcb_in_cur_domain' word s
 4. \<And>s. (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ct_in_state' activatable' s) \<and> (\<forall>x3. ksSchedulerAction s = SwitchToThread x3 \<longrightarrow> st_tcb_at' runnable' x3 s \<and> tcb_in_cur_domain' x3 s \<and> x3 \<noteq> t) \<Longrightarrow> (tcb_at' t s \<longrightarrow> (\<exists>ta. ko_at' ta t s \<and> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> (ct_in_state' activatable' and obj_at' ((=) ta) t) s))) \<and> (\<forall>x. sch_act_not x s \<or> ?P43 x s \<and> ?P'43 x s) proof (prove)
goal (4 subgoals):
 1. \<And>word. \<lbrace>?P43 word\<rbrace> do tcb <- getObject t;
setObject t (tcbDomain_update (\<lambda>_. domain) tcb)
od \<lbrace>\<lambda>rv. st_tcb_at' runnable' word\<rbrace>
 2. \<And>word. \<lbrace>?P'43 word\<rbrace> threadSet (tcbDomain_update (\<lambda>_. domain)) t \<lbrace>\<lambda>rv s. tcb_in_cur_domain' word s \<and> word \<noteq> t\<rbrace>
 3. \<And>word rv s. ksSchedulerAction s = SwitchToThread word \<longrightarrow> st_tcb_at' runnable' word s \<and> tcb_in_cur_domain' word s \<and> word \<noteq> t \<Longrightarrow> ksSchedulerAction s = SwitchToThread word \<longrightarrow> st_tcb_at' runnable' word s \<and> tcb_in_cur_domain' word s
 4. \<And>s. (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ct_in_state' activatable' s) \<and> (\<forall>x3. ksSchedulerAction s = SwitchToThread x3 \<longrightarrow> st_tcb_at' runnable' x3 s \<and> tcb_in_cur_domain' x3 s \<and> x3 \<noteq> t) \<Longrightarrow> (tcb_at' t s \<longrightarrow> (\<exists>ta. ko_at' ta t s \<and> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> (ct_in_state' activatable' and obj_at' ((=) ta) t) s))) \<and> (\<forall>x. sch_act_not x s \<or> ?P43 x s \<and> ?P'43 x s) proof (prove)
goal (2 subgoals):
 1. \<And>word rv s. ksSchedulerAction s = SwitchToThread word \<longrightarrow> st_tcb_at' runnable' word s \<and> tcb_in_cur_domain' word s \<and> word \<noteq> t \<Longrightarrow> ksSchedulerAction s = SwitchToThread word \<longrightarrow> st_tcb_at' runnable' word s \<and> tcb_in_cur_domain' word s
 2. \<And>s. (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ct_in_state' activatable' s) \<and> (\<forall>x3. ksSchedulerAction s = SwitchToThread x3 \<longrightarrow> st_tcb_at' runnable' x3 s \<and> tcb_in_cur_domain' x3 s \<and> x3 \<noteq> t) \<Longrightarrow> (tcb_at' t s \<longrightarrow> (\<exists>ta. ko_at' ta t s \<and> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> (ct_in_state' activatable' and obj_at' ((=) ta) t) s))) \<and> (\<forall>x. sch_act_not x s \<or> (tcb_at' t s \<longrightarrow> (\<exists>ta. ko_at' ta t s \<and> (st_tcb_at' runnable' x and obj_at' ((=) ta) t) s)) \<and> (tcb_in_cur_domain' x and K (t \<noteq> x)) s \<and> x \<noteq> t) proof (prove)
goal:
No subgoals!