theory IpcCancel_C

lemma threadSet_queued_ccorres [corres]:
  shows "ccorres dc xfdc (tcb_at' thread)
        {s. v32_' s = from_bool v \<and> thread_state_ptr_' s = Ptr &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])} []
        (threadSet (tcbQueued_update (\<lambda>_. v)) thread)
        (Call thread_state_ptr_set_tcbQueued_'proc)" apply (rule threadSet_corres_lemma) apply (rule thread_state_ptr_set_tcbQueued_spec) apply (rule thread_state_ptr_set_tcbQueued_modifies) apply clarsimp apply (frule (1) obj_at_cslift_tcb) apply clarsimp apply (rule rf_sr_tcb_update_no_queue_gen, assumption+, simp, simp_all) apply (rule ball_tcb_cte_casesI, simp_all) apply (simp add: ctcb_relation_def cthread_state_relation_def) apply (case_tac "tcbState ko"; simp) apply (frule (1) obj_at_cslift_tcb) apply (clarsimp simp: typ_heap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (tcb_at' thread) \<lbrace>\<acute>v32 = from_bool v \<and> \<acute>thread_state_ptr = PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])\<rbrace> [] (threadSet (tcbQueued_update (\<lambda>_. v)) thread) (Call thread_state_ptr_set_tcbQueued_'proc) proof (prove)
goal (4 subgoals):
 1. \<forall>s. \<Gamma>\<turnstile> \<lbrace>s. ?P s\<rbrace> Call thread_state_ptr_set_tcbQueued_'proc {t. ?Q s t}
 2. \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Call thread_state_ptr_set_tcbQueued_'proc {t. t may_only_modify_globals s in [t_hrs]}
 3. \<And>\<sigma> x t ko. \<lbrakk>(\<sigma>, x) \<in> rf_sr; ?Q x t; x \<in> \<lbrace>\<acute>v32 = from_bool v \<and> \<acute>thread_state_ptr = PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])\<rbrace>; ko_at' ko thread \<sigma>\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(thread \<mapsto> KOTCB (tcbQueued_update (\<lambda>_. v) ko))\<rparr>, t\<lparr>globals := globals x\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>) \<in> rf_sr
 4. \<And>s x. \<lbrakk>tcb_at' thread s; x \<in> \<lbrace>\<acute>v32 = from_bool v \<and> \<acute>thread_state_ptr = PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])\<rbrace>; (s, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> ?P x proof (prove)
goal (3 subgoals):
 1. \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Call thread_state_ptr_set_tcbQueued_'proc {t. t may_only_modify_globals s in [t_hrs]}
 2. \<And>\<sigma> x t ko. \<lbrakk>(\<sigma>, x) \<in> rf_sr; \<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (cslift x (cparent (thread_state_ptr_' x) [''tcbState_C'']))))\<lparr>tcbQueued_CL := v32_' x && mask 1\<rparr> \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cparent (thread_state_ptr_' x) [''tcbState_C'']) (tcbState_C_update (\<lambda>_. thread_state) (the (cslift x (cparent (thread_state_ptr_' x) [''tcbState_C'']))))) (t_hrs_' (globals x)); x \<in> \<lbrace>\<acute>v32 = from_bool v \<and> \<acute>thread_state_ptr = PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])\<rbrace>; ko_at' ko thread \<sigma>\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(thread \<mapsto> KOTCB (tcbQueued_update (\<lambda>_. v) ko))\<rparr>, t\<lparr>globals := globals x\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>) \<in> rf_sr
 3. \<And>s x. \<lbrakk>tcb_at' thread s; x \<in> \<lbrace>\<acute>v32 = from_bool v \<and> \<acute>thread_state_ptr = PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])\<rbrace>; (s, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> x \<Turnstile>\<^sub>c cparent (thread_state_ptr_' x) [''tcbState_C''] proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x t ko. \<lbrakk>(\<sigma>, x) \<in> rf_sr; \<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (cslift x (cparent (thread_state_ptr_' x) [''tcbState_C'']))))\<lparr>tcbQueued_CL := v32_' x && mask 1\<rparr> \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cparent (thread_state_ptr_' x) [''tcbState_C'']) (tcbState_C_update (\<lambda>_. thread_state) (the (cslift x (cparent (thread_state_ptr_' x) [''tcbState_C'']))))) (t_hrs_' (globals x)); x \<in> \<lbrace>\<acute>v32 = from_bool v \<and> \<acute>thread_state_ptr = PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])\<rbrace>; ko_at' ko thread \<sigma>\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(thread \<mapsto> KOTCB (tcbQueued_update (\<lambda>_. v) ko))\<rparr>, t\<lparr>globals := globals x\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>) \<in> rf_sr
 2. \<And>s x. \<lbrakk>tcb_at' thread s; x \<in> \<lbrace>\<acute>v32 = from_bool v \<and> \<acute>thread_state_ptr = PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])\<rbrace>; (s, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> x \<Turnstile>\<^sub>c cparent (thread_state_ptr_' x) [''tcbState_C''] proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x t ko thread_state. \<lbrakk>(\<sigma>, x) \<in> rf_sr; ko_at' ko thread \<sigma>; v32_' x = from_bool v; thread_state_ptr_' x = PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']); thread_state_lift thread_state = thread_state_lift (tcbState_C (the (cslift x (tcb_ptr_to_ctcb_ptr thread))))\<lparr>tcbQueued_CL := from_bool v\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) (the (cslift x (tcb_ptr_to_ctcb_ptr thread))))) (t_hrs_' (globals x))\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(thread \<mapsto> KOTCB (tcbQueued_update (\<lambda>_. v) ko))\<rparr>, t\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) (the (cslift x (tcb_ptr_to_ctcb_ptr thread))))) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr
 2. \<And>s x. \<lbrakk>tcb_at' thread s; x \<in> \<lbrace>\<acute>v32 = from_bool v \<and> \<acute>thread_state_ptr = PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])\<rbrace>; (s, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> x \<Turnstile>\<^sub>c cparent (thread_state_ptr_' x) [''tcbState_C''] proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x t ko thread_state. \<lbrakk>(\<sigma>, x) \<in> rf_sr; ko_at' ko thread \<sigma>; v32_' x = from_bool v; thread_state_ptr_' x = PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']); thread_state_lift thread_state = thread_state_lift (tcbState_C (the (cslift x (tcb_ptr_to_ctcb_ptr thread))))\<lparr>tcbQueued_CL := from_bool v\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) (the (cslift x (tcb_ptr_to_ctcb_ptr thread))))) (t_hrs_' (globals x)); \<exists>koa ko'. ko_at' koa thread \<sigma> \<and> koa = ko \<and> cslift x (tcb_ptr_to_ctcb_ptr thread) = Some ko' \<and> ctcb_relation koa ko'\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(thread \<mapsto> KOTCB (tcbQueued_update (\<lambda>_. v) ko))\<rparr>, t\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) (the (cslift x (tcb_ptr_to_ctcb_ptr thread))))) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr
 2. \<And>s x. \<lbrakk>tcb_at' thread s; x \<in> \<lbrace>\<acute>v32 = from_bool v \<and> \<acute>thread_state_ptr = PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])\<rbrace>; (s, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> x \<Turnstile>\<^sub>c cparent (thread_state_ptr_' x) [''tcbState_C''] proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x t ko thread_state ko'. \<lbrakk>(\<sigma>, x) \<in> rf_sr; ko_at' ko thread \<sigma>; v32_' x = from_bool v; thread_state_ptr_' x = PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']); thread_state_lift thread_state = thread_state_lift (tcbState_C ko')\<lparr>tcbQueued_CL := from_bool v\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) ko')) (t_hrs_' (globals x)); cslift x (tcb_ptr_to_ctcb_ptr thread) = Some ko'; ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(thread \<mapsto> KOTCB (tcbQueued_update (\<lambda>_. v) ko))\<rparr>, t\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) ko')) (t_hrs_' (globals x))\<rparr>\<rparr>) \<in> rf_sr
 2. \<And>s x. \<lbrakk>tcb_at' thread s; x \<in> \<lbrace>\<acute>v32 = from_bool v \<and> \<acute>thread_state_ptr = PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])\<rbrace>; (s, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> x \<Turnstile>\<^sub>c cparent (thread_state_ptr_' x) [''tcbState_C''] proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma> x t ko thread_state ko'. \<lbrakk>(\<sigma>, x) \<in> rf_sr; ko_at' ko thread \<sigma>; v32_' x = from_bool v; thread_state_ptr_' x = PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']); thread_state_lift thread_state = thread_state_lift (tcbState_C ko')\<lparr>tcbQueued_CL := from_bool v\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) ko')) (t_hrs_' (globals x)); cslift x (tcb_ptr_to_ctcb_ptr thread) = Some ko'; ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> getF (tcbQueued_update (\<lambda>_. v) ko) = getF ko
 2. \<And>\<sigma> x t ko thread_state ko'. \<lbrakk>(\<sigma>, x) \<in> rf_sr; ko_at' ko thread \<sigma>; v32_' x = from_bool v; thread_state_ptr_' x = PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']); thread_state_lift thread_state = thread_state_lift (tcbState_C ko')\<lparr>tcbQueued_CL := from_bool v\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) ko')) (t_hrs_' (globals x)); cslift x (tcb_ptr_to_ctcb_ptr thread) = Some ko'; ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> ctcb_relation (tcbQueued_update (\<lambda>_. v) ko) (tcbState_C_update (\<lambda>_. thread_state) ko')
 3. \<And>s x. \<lbrakk>tcb_at' thread s; v32_' x = from_bool v \<and> thread_state_ptr_' x = PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']); (s, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> x \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x t ko thread_state ko'. \<lbrakk>(\<sigma>, x) \<in> rf_sr; ko_at' ko thread \<sigma>; v32_' x = from_bool v; thread_state_ptr_' x = PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']); thread_state_lift thread_state = thread_state_lift (tcbState_C ko')\<lparr>tcbQueued_CL := from_bool v\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) ko')) (t_hrs_' (globals x)); cslift x (tcb_ptr_to_ctcb_ptr thread) = Some ko'; ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> ctcb_relation (tcbQueued_update (\<lambda>_. v) ko) (tcbState_C_update (\<lambda>_. thread_state) ko')
 2. \<And>s x. \<lbrakk>tcb_at' thread s; v32_' x = from_bool v \<and> thread_state_ptr_' x = PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']); (s, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> x \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x t ko thread_state ko'. \<lbrakk>(\<sigma>, x) \<in> rf_sr; ko_at' ko thread \<sigma>; v32_' x = from_bool v; thread_state_ptr_' x = PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']); thread_state_lift thread_state = thread_state_lift (tcbState_C ko')\<lparr>tcbQueued_CL := from_bool v\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) ko')) (t_hrs_' (globals x)); cslift x (tcb_ptr_to_ctcb_ptr thread) = Some ko'; tcbFaultHandler ko = tcbFaultHandler_C ko' \<and> cthread_state_relation_lifted (tcbState ko) (thread_state_lift (tcbState_C ko'), seL4_Fault_lift (tcbFault_C ko')) \<and> tcbIPCBuffer ko = tcbIPCBuffer_C ko' \<and> carch_tcb_relation (tcbArch ko) (tcbArch_C ko') \<and> tcbQueued ko = to_bool (tcbQueued_CL (thread_state_lift (tcbState_C ko'))) \<and> UCAST(8 \<rightarrow> 32) (tcbDomain ko) = tcbDomain_C ko' \<and> UCAST(8 \<rightarrow> 32) (tcbPriority ko) = tcbPriority_C ko' \<and> UCAST(8 \<rightarrow> 32) (tcbMCP ko) = tcbMCP_C ko' \<and> tcbTimeSlice ko = unat (tcbTimeSlice_C ko') \<and> cfault_rel (tcbFault ko) (seL4_Fault_lift (tcbFault_C ko')) (lookup_fault_lift (tcbLookupFailure_C ko')) \<and> option_to_ptr (tcbBoundNotification ko) = tcbBoundNotification_C ko'\<rbrakk> \<Longrightarrow> cthread_state_relation_lifted (tcbState ko) (thread_state_lift (tcbState_C ko')\<lparr>tcbQueued_CL := from_bool v\<rparr>, seL4_Fault_lift (tcbFault_C ko'))
 2. \<And>s x. \<lbrakk>tcb_at' thread s; v32_' x = from_bool v \<and> thread_state_ptr_' x = PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']); (s, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> x \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>tcb_at' thread s; v32_' x = from_bool v \<and> thread_state_ptr_' x = PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']); (s, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> x \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>tcb_at' thread s; v32_' x = from_bool v \<and> thread_state_ptr_' x = PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']); (s, x) \<in> rf_sr; \<exists>ko ko'. ko_at' ko thread s \<and> True \<and> cslift x (tcb_ptr_to_ctcb_ptr thread) = Some ko' \<and> ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> x \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread proof (prove)
goal:
No subgoals!