theory IpcCancel_C

lemma setThreadState_ccorres[corres]:
   "ccorres dc xfdc
   (\<lambda>s. tcb_at' thread s \<and> valid_queues s \<and> valid_objs' s \<and> valid_tcb_state' st s \<and>
                 (ksSchedulerAction s = SwitchToThread thread \<longrightarrow> runnable' st) \<and>
                 (\<forall>p. thread \<in> set (ksReadyQueues s p) \<longrightarrow> runnable' st) \<and>
                 sch_act_wf (ksSchedulerAction s) s)
     ({s'. (\<forall>cl fl. cthread_state_relation_lifted st (cl\<lparr>tsType_CL := ts_' s' && mask 4\<rparr>, fl))}
    \<inter> {s. tptr_' s = tcb_ptr_to_ctcb_ptr thread}) []
         (setThreadState st thread) (Call setThreadState_'proc)" apply (cinit lift: tptr_' cong add: call_ignore_cong) apply (ctac (no_vcg) add: threadSet_tcbState_simple_corres) apply (ctac add: scheduleTCB_ccorres) apply (wp threadSet_weak_sch_act_wf_runnable' threadSet_valid_queues_and_runnable'
            threadSet_valid_objs') by (clarsimp simp: weak_sch_act_wf_def valid_queues_def valid_tcb'_tcbState_update)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (\<lambda>s. tcb_at' thread s \<and> Invariants_H.valid_queues s \<and> valid_objs' s \<and> valid_tcb_state' st s \<and> (ksSchedulerAction s = SwitchToThread thread \<longrightarrow> runnable' st) \<and> (\<forall>p. thread \<in> set (ksReadyQueues s p) \<longrightarrow> runnable' st) \<and> sch_act_wf (ksSchedulerAction s) s) (\<lbrace>\<forall>cl fl. cthread_state_relation_lifted st (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr thread\<rbrace>) [] (setThreadState st thread) (Call setThreadState_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> ccorres dc xfdc (?Q68 tptr) (?Q'68 tptr) [SKIP] (do y <- threadSet (tcbState_update (\<lambda>_. st)) thread;
runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = thread \<and> action = ResumeCurrentThread) rescheduleRequired
od) (Guard C_Guard {s. s \<Turnstile>\<^sub>c tptr} (CALL thread_state_ptr_set_tsType_'proc(PTR(thread_state_C) &(tptr\<rightarrow>[''tcbState_C'']),UCAST(32 \<rightarrow> 32) \<acute>ts));;
CALL scheduleTCB_'proc(tptr))
 2. \<And>tptr s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; tcb_at' thread s \<and> Invariants_H.valid_queues s \<and> valid_objs' s \<and> valid_tcb_state' st s \<and> (ksSchedulerAction s = SwitchToThread thread \<longrightarrow> runnable' st) \<and> ((\<exists>a b. thread \<in> set (ksReadyQueues s (a, b))) \<longrightarrow> runnable' st) \<and> sch_act_wf (ksSchedulerAction s) s; s' \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted st (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace>\<rbrakk> \<Longrightarrow> ?Q68 tptr s \<and> s' \<in> ?Q'68 tptr proof (prove)
goal (3 subgoals):
 1. \<And>tptr rv xfdca. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr thread; dc rv xfdca\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q77 tptr rv) (?Q'77 tptr rv xfdca) [SKIP] (do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = thread \<and> action = ResumeCurrentThread) rescheduleRequired
od) (CALL scheduleTCB_'proc(tptr))
 2. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?R77 tptr\<rbrace> threadSet (tcbState_update (\<lambda>_. st)) thread \<lbrace>?Q77 tptr\<rbrace>
 3. \<And>tptr s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; tcb_at' thread s \<and> Invariants_H.valid_queues s \<and> valid_objs' s \<and> valid_tcb_state' st s \<and> (ksSchedulerAction s = SwitchToThread thread \<longrightarrow> runnable' st) \<and> ((\<exists>a b. thread \<in> set (ksReadyQueues s (a, b))) \<longrightarrow> runnable' st) \<and> sch_act_wf (ksSchedulerAction s) s; s' \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted st (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace>\<rbrakk> \<Longrightarrow> (tcb_at' thread and ?R77 tptr and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)) s \<and> s' \<in> {s. v32_'_update (\<lambda>_. UCAST(32 \<rightarrow> 32) (ts_' s)) (thread_state_ptr_'_update (\<lambda>_. PTR(thread_state_C) &(tptr\<rightarrow>[''tcbState_C''])) s) \<in> \<lbrace>(\<forall>cl fl. cthread_state_relation_lifted st (cl\<lparr>tsType_CL := \<acute>v32 && mask 4\<rparr>, fl)) \<and> \<acute>thread_state_ptr = PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> ?Q'77 tptr rv (xfdc t)} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?R77 tptr\<rbrace> threadSet (tcbState_update (\<lambda>_. st)) thread \<lbrace>\<lambda>rv. tcb_at' thread and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs'\<rbrace>
 2. \<And>tptr s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; tcb_at' thread s \<and> Invariants_H.valid_queues s \<and> valid_objs' s \<and> valid_tcb_state' st s \<and> (ksSchedulerAction s = SwitchToThread thread \<longrightarrow> runnable' st) \<and> ((\<exists>a b. thread \<in> set (ksReadyQueues s (a, b))) \<longrightarrow> runnable' st) \<and> sch_act_wf (ksSchedulerAction s) s; s' \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted st (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace>\<rbrakk> \<Longrightarrow> (tcb_at' thread and ?R77 tptr and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)) s \<and> s' \<in> {s. v32_'_update (\<lambda>_. UCAST(32 \<rightarrow> 32) (ts_' s)) (thread_state_ptr_'_update (\<lambda>_. PTR(thread_state_C) &(tptr\<rightarrow>[''tcbState_C''])) s) \<in> \<lbrace>(\<forall>cl fl. cthread_state_relation_lifted st (cl\<lparr>tsType_CL := \<acute>v32 && mask 4\<rparr>, fl)) \<and> \<acute>thread_state_ptr = PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. tptr_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr thread\<rbrace>}} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>tptr s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; tcb_at' thread s \<and> Invariants_H.valid_queues s \<and> valid_objs' s \<and> valid_tcb_state' st s \<and> (ksSchedulerAction s = SwitchToThread thread \<longrightarrow> runnable' st) \<and> ((\<exists>a b. thread \<in> set (ksReadyQueues s (a, b))) \<longrightarrow> runnable' st) \<and> sch_act_wf (ksSchedulerAction s) s; s' \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted st (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace>\<rbrakk> \<Longrightarrow> (tcb_at' thread and (\<lambda>s. obj_at' (\<lambda>obj. if thread = thread then True else True) thread s \<and> ((ksSchedulerAction s = SwitchToThread thread \<longrightarrow> runnable' st) \<and> weak_sch_act_wf (ksSchedulerAction s) s) \<and> (Invariants_H.valid_queues s \<and> (\<forall>p. thread \<in> set (ksReadyQueues s p) \<longrightarrow> runnable' st)) \<and> (valid_objs' and (\<lambda>s. \<forall>tcb. valid_tcb' tcb s \<longrightarrow> valid_tcb' (tcbState_update (\<lambda>_. st) tcb) s)) s) and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)) s \<and> s' \<in> {s. v32_'_update (\<lambda>_. UCAST(32 \<rightarrow> 32) (ts_' s)) (thread_state_ptr_'_update (\<lambda>_. PTR(thread_state_C) &(tptr\<rightarrow>[''tcbState_C''])) s) \<in> \<lbrace>(\<forall>cl fl. cthread_state_relation_lifted st (cl\<lparr>tsType_CL := \<acute>v32 && mask 4\<rparr>, fl)) \<and> \<acute>thread_state_ptr = PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. tptr_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr thread\<rbrace>}} \<inter> \<lbrace>True\<rbrace>