theory IpcCancel_C

lemma setThreadState_ccorres_valid_queues':
   "ccorres dc xfdc
   (\<lambda>s. tcb_at' thread s \<and> valid_queues' s \<and> \<not> runnable' st \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> (\<forall>p. thread \<notin> set (ksReadyQueues s p)) \<and> sch_act_not thread s \<and> valid_objs' s \<and> valid_tcb_state' st 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_valid_queues') apply (wp threadSet_valid_queues'_and_not_runnable' threadSet_weak_sch_act_wf_runnable' threadSet_valid_queues_and_runnable' threadSet_valid_objs') by (clarsimp simp: valid_tcb'_def tcb_cte_cases_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (\<lambda>s. tcb_at' thread s \<and> valid_queues' s \<and> \<not> runnable' st \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> (\<forall>p. thread \<notin> set (ksReadyQueues s p)) \<and> sch_act_not thread s \<and> valid_objs' s \<and> valid_tcb_state' st 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 (?Q65 tptr) (?Q'65 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> valid_queues' s \<and> \<not> runnable' st \<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_tcb_state' st 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> ?Q65 tptr s \<and> s' \<in> ?Q'65 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 (?Q74 tptr rv) (?Q'74 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>?R74 tptr\<rbrace> threadSet (tcbState_update (\<lambda>_. st)) thread \<lbrace>?Q74 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> valid_queues' s \<and> \<not> runnable' st \<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_tcb_state' st 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 ?R74 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'74 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>?R74 tptr\<rbrace> threadSet (tcbState_update (\<lambda>_. st)) thread \<lbrace>\<lambda>rv. tcb_at' thread and st_tcb_at' (not runnable') thread and valid_queues' and Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) 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> valid_queues' s \<and> \<not> runnable' st \<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_tcb_state' st 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 ?R74 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> valid_queues' s \<and> \<not> runnable' st \<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_tcb_state' st 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. (tcb_at' thread and valid_queues' and (\<lambda>s. \<not> runnable' st)) s \<and> (Invariants_H.valid_queues s \<and> (\<forall>p. thread \<in> set (ksReadyQueues s p) \<longrightarrow> runnable' st)) \<and> ((ksSchedulerAction s = SwitchToThread thread \<longrightarrow> runnable' st) \<and> weak_sch_act_wf (ksSchedulerAction s) s) \<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>