kings-crown/FVELER_Isabelle huggingface dataset:
theory IpcCancel_C

lemma getCurDomain_maxDom_ccorres_dom_':
  "ccorres (\<lambda>rv rv'. rv' = ucast rv) dom_'
     (\<lambda>s. ksCurDomain s \<le> maxDomain) UNIV hs
     curDomain (\<acute>dom :== (if maxDom \<noteq> 0 then \<acute>ksCurDomain else 0))" apply (rule ccorres_from_vcg) apply (rule allI, rule conseqPre, vcg) using maxDom_to_H apply (clarsimp simp: curDomain_def simpler_gets_def
                        rf_sr_ksCurDomain) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (\<lambda>rv rv'. rv' = UCAST(8 \<rightarrow> 32) rv) dom_' (\<lambda>s. ksCurDomain s \<le> maxDomain) UNIV hs curDomain (\<acute>dom :== (if maxDom \<noteq> 0 then \<acute>ksCurDomain else 0)) proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma>. \<Gamma>\<turnstile> {s. ksCurDomain \<sigma> \<le> maxDomain \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<acute>dom :== (if maxDom \<noteq> 0 then \<acute>ksCurDomain else 0) {s. \<exists>(rv, \<sigma>')\<in>fst (curDomain \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dom_' s = UCAST(8 \<rightarrow> 32) rv} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma>. {s. ksCurDomain \<sigma> \<le> maxDomain \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (curDomain \<sigma>). (\<sigma>', dom_'_update (\<lambda>_. if maxDom \<noteq> 0 then ksCurDomain_' (globals s) else 0) s) \<in> rf_sr \<and> (if maxDom \<noteq> 0 then ksCurDomain_' (globals s) else 0) = UCAST(8 \<rightarrow> 32) rv} proof (prove)
using this:
UCAST(32 signed \<rightarrow> 8) maxDom = maxDomain

goal (1 subgoal):
 1. \<And>\<sigma>. {s. ksCurDomain \<sigma> \<le> maxDomain \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (curDomain \<sigma>). (\<sigma>', dom_'_update (\<lambda>_. if maxDom \<noteq> 0 then ksCurDomain_' (globals s) else 0) s) \<in> rf_sr \<and> (if maxDom \<noteq> 0 then ksCurDomain_' (globals s) else 0) = UCAST(8 \<rightarrow> 32) rv} proof (prove)
goal:
No subgoals!
theory IpcCancel_C

lemma threadGet_get_obj_at'_has_domain:
  "\<lbrace> tcb_at' t \<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. rv = tcbDomain tcb) t\<rbrace>" by (wp threadGet_obj_at') (simp add: obj_at'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at' t\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. rv = tcbDomain tcb) t\<rbrace>
theory IpcCancel_C

lemma threadSet_weak_sch_act_wf_runnable':
            "\<lbrace> \<lambda>s. (ksSchedulerAction s = SwitchToThread thread \<longrightarrow> runnable' st) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<rbrace>
               threadSet (tcbState_update (\<lambda>_. st)) thread
             \<lbrace> \<lambda>rv s. weak_sch_act_wf (ksSchedulerAction s) s \<rbrace>" apply (simp add: weak_sch_act_wf_def) apply (wp hoare_vcg_all_lift hoare_vcg_imp_lift threadSet_pred_tcb_at_state
            threadSet_tcbDomain_triv) apply simp apply (clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (ksSchedulerAction s = SwitchToThread thread \<longrightarrow> runnable' st) \<and> weak_sch_act_wf (ksSchedulerAction s) s\<rbrace> threadSet (tcbState_update (\<lambda>_. st)) thread \<lbrace>\<lambda>rv s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (ksSchedulerAction s = SwitchToThread thread \<longrightarrow> runnable' st) \<and> (\<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> st_tcb_at' runnable' t s \<and> tcb_in_cur_domain' t s)\<rbrace> threadSet (tcbState_update (\<lambda>_. st)) thread \<lbrace>\<lambda>rv s. \<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> st_tcb_at' runnable' t s \<and> tcb_in_cur_domain' t s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>t tcb. tcbDomain (tcbState_update (\<lambda>_. st) tcb) = tcbDomain tcb
 2. \<And>s. (ksSchedulerAction s = SwitchToThread thread \<longrightarrow> runnable' st) \<and> (\<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> st_tcb_at' runnable' t s \<and> tcb_in_cur_domain' t s) \<Longrightarrow> \<forall>x. sch_act_not x s \<or> (tcb_at' thread s \<longrightarrow> (if x = thread then obj_at' (\<lambda>tcb. runnable' (itcbState (tcb_to_itcb' (tcbState_update (\<lambda>_. st) tcb)))) thread s else st_tcb_at' runnable' x s)) \<and> tcb_in_cur_domain' x s proof (prove)
goal (1 subgoal):
 1. \<And>s. (ksSchedulerAction s = SwitchToThread thread \<longrightarrow> runnable' st) \<and> (\<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> st_tcb_at' runnable' t s \<and> tcb_in_cur_domain' t s) \<Longrightarrow> \<forall>x. sch_act_not x s \<or> (tcb_at' thread s \<longrightarrow> (if x = thread then obj_at' (\<lambda>tcb. runnable' (itcbState (tcb_to_itcb' (tcbState_update (\<lambda>_. st) tcb)))) thread s else st_tcb_at' runnable' x s)) \<and> tcb_in_cur_domain' x s proof (prove)
goal:
No subgoals!
theory IpcCancel_C

lemma threadSet_valid_queues_and_runnable': "\<lbrace>\<lambda>s. valid_queues s \<and> (\<forall>p. thread \<in> set (ksReadyQueues s p) \<longrightarrow> runnable' st)\<rbrace>
                 threadSet (tcbState_update (\<lambda>_. st)) thread
               \<lbrace>\<lambda>rv s. valid_queues s\<rbrace>" apply (wp threadSet_valid_queues) apply (clarsimp simp: inQ_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Invariants_H.valid_queues s \<and> (\<forall>p. thread \<in> set (ksReadyQueues s p) \<longrightarrow> runnable' st)\<rbrace> threadSet (tcbState_update (\<lambda>_. st)) thread \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. Invariants_H.valid_queues s \<and> (\<forall>p. thread \<in> set (ksReadyQueues s p) \<longrightarrow> runnable' st) \<Longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. \<forall>d p. (\<exists>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbState_update (\<lambda>_. st) tcb) \<and> runnable' (tcbState (tcbState_update (\<lambda>_. st) tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbState_update (\<lambda>_. st) tcb) \<and> runnable' (tcbState (tcbState_update (\<lambda>_. st) tcb)))) thread s \<longrightarrow> thread \<notin> set (ksReadyQueues s (d, p)))) s proof (prove)
goal:
No subgoals!
theory IpcCancel_C

lemma threadSet_valid_queues'_and_not_runnable': "\<lbrace>tcb_at' thread and valid_queues' and (\<lambda>s. (\<not> runnable' st))\<rbrace>
                  threadSet (tcbState_update (\<lambda>_. st)) thread
               \<lbrace>\<lambda>rv. tcb_at' thread and st_tcb_at' (not runnable') thread and valid_queues' \<rbrace>" apply (wp threadSet_valid_queues' threadSet_tcbState_st_tcb_at') apply (clarsimp simp: pred_neg_def valid_queues'_def inQ_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at' thread and valid_queues' and (\<lambda>s. \<not> runnable' st)\<rbrace> threadSet (tcbState_update (\<lambda>_. st)) thread \<lbrace>\<lambda>rv. tcb_at' thread and st_tcb_at' (not runnable') thread and valid_queues'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (tcb_at' thread and valid_queues' and (\<lambda>s. \<not> runnable' st)) s \<Longrightarrow> obj_at' (\<lambda>obj. if thread = thread then True else True) thread s \<and> (not runnable') st \<and> (\<forall>ko qdom prio. ko_at' ko thread s \<and> inQ qdom prio (tcbState_update (\<lambda>_. st) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> thread \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s proof (prove)
goal:
No subgoals!
theory IpcCancel_C

lemma simp_list_case_return:
  "(case x of [] \<Rightarrow> return e | y # ys \<Rightarrow> return f) = return (if x = [] then e else f)" by (clarsimp split: list.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (case x of [] \<Rightarrow> return e | y # ys \<Rightarrow> return f) = return (if x = [] then e else f)
theory IpcCancel_C

lemma ep_ptr_get_queue_spec:
  "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. s \<Turnstile>\<^sub>c \<acute>epptr\<rbrace> \<acute>ret__struct_tcb_queue_C :== PROC ep_ptr_get_queue(\<acute>epptr)
       \<lbrace>head_C \<acute>ret__struct_tcb_queue_C = Ptr (epQueue_head_CL (endpoint_lift (the (cslift s \<^bsup>s\<^esup>epptr)))) \<and>
        end_C \<acute>ret__struct_tcb_queue_C = Ptr (epQueue_tail_CL (endpoint_lift (the (cslift s \<^bsup>s\<^esup>epptr))))\<rbrace>" apply vcg apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> \<lbrace>s. s \<Turnstile>\<^sub>c \<acute>epptr\<rbrace> Call ep_ptr_get_queue_'proc \<lbrace>head_C \<acute>ret__struct_tcb_queue_C = tcb_Ptr (epQueue_head_CL (endpoint_lift (the (cslift s \<^bsup>s\<^esup>epptr)))) \<and> StateRelation_C.end_C \<acute>ret__struct_tcb_queue_C = tcb_Ptr (epQueue_tail_CL (endpoint_lift (the (cslift s \<^bsup>s\<^esup>epptr))))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>t_hrs epptr. hrs_htd t_hrs \<Turnstile>\<^sub>t epptr \<Longrightarrow> \<forall>v. hrs_htd t_hrs \<Turnstile>\<^sub>t epptr \<and> (\<forall>ret__unsigned. ret__unsigned = epQueue_head_CL (endpoint_lift (the (clift t_hrs epptr))) \<longrightarrow> hrs_htd t_hrs \<Turnstile>\<^sub>t epptr \<and> (\<forall>ret__unsigned. ret__unsigned = epQueue_tail_CL (endpoint_lift (the (clift t_hrs epptr))) \<longrightarrow> head_C (tcb_queue_C.end_C_update (\<lambda>_. tcb_Ptr (UCAST(32 \<rightarrow> 32) (epQueue_tail_CL (endpoint_lift (the (clift t_hrs epptr)))))) (head_C_update (\<lambda>_. tcb_Ptr (UCAST(32 \<rightarrow> 32) (epQueue_head_CL (endpoint_lift (the (clift t_hrs epptr)))))) v)) = tcb_Ptr (epQueue_head_CL (endpoint_lift (the (clift t_hrs epptr)))) \<and> StateRelation_C.end_C (tcb_queue_C.end_C_update (\<lambda>_. tcb_Ptr (UCAST(32 \<rightarrow> 32) (epQueue_tail_CL (endpoint_lift (the (clift t_hrs epptr)))))) (head_C_update (\<lambda>_. tcb_Ptr (UCAST(32 \<rightarrow> 32) (epQueue_head_CL (endpoint_lift (the (clift t_hrs epptr)))))) v)) = tcb_Ptr (epQueue_tail_CL (endpoint_lift (the (clift t_hrs epptr)))))) proof (prove)
goal:
No subgoals!
theory IpcCancel_C

lemma ep_ptr_set_queue_spec:
  "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. s \<Turnstile>\<^sub>c \<acute>epptr\<rbrace> Call ep_ptr_set_queue_'proc
           {t. (\<exists>ep'. endpoint_lift ep' =
  (endpoint_lift (the (cslift s (\<^bsup>s\<^esup>epptr))))\<lparr> epQueue_head_CL := ptr_val (head_C \<^bsup>s\<^esup>queue) && ~~ mask 4,
                                                      epQueue_tail_CL := ptr_val (end_C \<^bsup>s\<^esup>queue) && ~~ mask 4 \<rparr>
             \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (\<^bsup>s\<^esup>epptr) ep')
                 (t_hrs_' (globals s)))}" apply vcg apply (auto simp: split_def h_t_valid_clift_Some_iff
                    typ_heap_simps packed_heap_update_collapse_hrs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> \<lbrace>s. s \<Turnstile>\<^sub>c \<acute>epptr\<rbrace> Call ep_ptr_set_queue_'proc \<lbrace>\<exists>ep'. endpoint_lift ep' = endpoint_lift (the (cslift s \<^bsup>s\<^esup>epptr))\<lparr>epQueue_head_CL := ptr_val (head_C \<^bsup>s\<^esup>queue) && ~~ mask 4, epQueue_tail_CL := ptr_val (StateRelation_C.end_C \<^bsup>s\<^esup>queue) && ~~ mask 4\<rparr> \<and> \<acute>t_hrs = hrs_mem_update (heap_update \<^bsup>s\<^esup>epptr ep') \<^bsup>s\<^esup>t_hrs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>t_hrs queue epptr. hrs_htd t_hrs \<Turnstile>\<^sub>t epptr \<Longrightarrow> hrs_htd t_hrs \<Turnstile>\<^sub>t epptr \<and> (\<forall>t_hrsa. (\<exists>endpoint. endpoint_lift endpoint = endpoint_lift (the (clift t_hrs epptr))\<lparr>epQueue_head_CL := UCAST(32 \<rightarrow> 32) (ptr_val (head_C queue)) && ~~ mask 4\<rparr> \<and> t_hrsa = hrs_mem_update (heap_update epptr endpoint) t_hrs) \<longrightarrow> hrs_htd t_hrsa \<Turnstile>\<^sub>t epptr \<and> (\<forall>t_hrsb. (\<exists>endpoint. endpoint_lift endpoint = endpoint_lift (the (clift t_hrsa epptr))\<lparr>epQueue_tail_CL := UCAST(32 \<rightarrow> 32) (ptr_val (StateRelation_C.end_C queue)) && ~~ mask 4\<rparr> \<and> t_hrsb = hrs_mem_update (heap_update epptr endpoint) t_hrsa) \<longrightarrow> (\<exists>ep'. endpoint_lift ep' = endpoint_lift (the (clift t_hrs epptr))\<lparr>epQueue_head_CL := ptr_val (head_C queue) && ~~ mask 4, epQueue_tail_CL := ptr_val (StateRelation_C.end_C queue) && ~~ mask 4\<rparr> \<and> t_hrsb = hrs_mem_update (heap_update epptr ep') t_hrs))) proof (prove)
goal:
No subgoals!
theory IpcCancel_C

lemma valid_ep_blockedD:
  "\<lbrakk> valid_ep' ep s; (isSendEP ep \<or> isRecvEP ep) \<rbrakk> \<Longrightarrow> (epQueue ep) \<noteq> [] \<and> (\<forall>t\<in>set (epQueue ep). tcb_at' t s) \<and> distinct (epQueue ep)" unfolding valid_ep'_def isSendEP_def isRecvEP_def by (clarsimp split: endpoint.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_ep' ep s; isSendEP ep \<or> isRecvEP ep\<rbrakk> \<Longrightarrow> epQueue ep \<noteq> [] \<and> (\<forall>t\<in>set (epQueue ep). tcb_at' t s) \<and> distinct (epQueue ep) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>case ep of Structures_H.endpoint.RecvEP ts \<Rightarrow> ts \<noteq> [] \<and> (\<forall>t\<in>set ts. tcb_at' t s) \<and> distinct ts | Structures_H.endpoint.IdleEP \<Rightarrow> True | Structures_H.endpoint.SendEP ts \<Rightarrow> ts \<noteq> [] \<and> (\<forall>t\<in>set ts. tcb_at' t s) \<and> distinct ts; (case ep of Structures_H.endpoint.SendEP v0 \<Rightarrow> True | _ \<Rightarrow> False) \<or> (case ep of Structures_H.endpoint.RecvEP v0 \<Rightarrow> True | _ \<Rightarrow> False)\<rbrakk> \<Longrightarrow> epQueue ep \<noteq> [] \<and> (\<forall>t\<in>set (epQueue ep). tcb_at' t s) \<and> distinct (epQueue ep)
theory IpcCancel_C

lemma endpoint_not_idle_cases:
  "ep \<noteq> IdleEP \<Longrightarrow> isSendEP ep \<or> isRecvEP ep" by (clarsimp simp: isRecvEP_def isSendEP_def split: Structures_H.endpoint.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ep \<noteq> Structures_H.endpoint.IdleEP \<Longrightarrow> isSendEP ep \<or> isRecvEP ep
theory IpcCancel_C

lemma cpspace_relation_ep_update_ep:
  fixes ep :: "endpoint"
  defines "qs \<equiv> if (isSendEP ep \<or> isRecvEP ep) then set (epQueue ep) else {}"
  assumes koat: "ko_at' ep epptr s"
  and     invs: "invs' s"
  and      cp: "cmap_relation (map_to_eps (ksPSpace s)) (cslift t) Ptr (cendpoint_relation mp)"
  and     rel: "cendpoint_relation mp' ep' endpoint"
  and    mpeq: "(mp' |` (- (tcb_ptr_to_ctcb_ptr ` qs))) = (mp |` (- (tcb_ptr_to_ctcb_ptr ` qs)))"
  shows "cmap_relation (map_to_eps ((ksPSpace s)(epptr \<mapsto> KOEndpoint ep')))
           ((cslift t)(Ptr epptr \<mapsto> endpoint)) Ptr (cendpoint_relation mp')" using invs apply (intro cpspace_relation_ep_update_an_ep[OF koat cp rel mpeq]) apply clarsimp+ apply (clarsimp simp add: qs_def image_image simp del: imp_disjL) apply (rule ep_ep_disjoint[OF _ _ koat endpoint_not_idle_cases], auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cmap_relation (map_to_eps ((ksPSpace s)(epptr \<mapsto> KOEndpoint ep'))) ((cslift t)(ep_Ptr epptr \<mapsto> endpoint)) ep_Ptr (cendpoint_relation mp') proof (prove)
using this:
invs' s

goal (1 subgoal):
 1. cmap_relation (map_to_eps ((ksPSpace s)(epptr \<mapsto> KOEndpoint ep'))) ((cslift t)(ep_Ptr epptr \<mapsto> endpoint)) ep_Ptr (cendpoint_relation mp') proof (prove)
goal (3 subgoals):
 1. invs' s \<Longrightarrow> pspace_aligned' s
 2. invs' s \<Longrightarrow> pspace_distinct' s
 3. \<And>epptr' ep'. \<lbrakk>invs' s; ko_at' ep' epptr' s; epptr' \<noteq> epptr; ep' \<noteq> Structures_H.endpoint.IdleEP\<rbrakk> \<Longrightarrow> set (epQueue ep') \<inter> ctcb_ptr_to_tcb_ptr ` tcb_ptr_to_ctcb_ptr ` qs = {} proof (prove)
goal (1 subgoal):
 1. \<And>epptr' ep'. \<lbrakk>invs' s; ko_at' ep' epptr' s; epptr' \<noteq> epptr; ep' \<noteq> Structures_H.endpoint.IdleEP\<rbrakk> \<Longrightarrow> set (epQueue ep') \<inter> ctcb_ptr_to_tcb_ptr ` tcb_ptr_to_ctcb_ptr ` qs = {} proof (prove)
goal (1 subgoal):
 1. \<And>epptr' ep'. \<lbrakk>invs' s; ko_at' ep' epptr' s; epptr' \<noteq> epptr; ep' \<noteq> Structures_H.endpoint.IdleEP; isSendEP ep \<or> isRecvEP ep\<rbrakk> \<Longrightarrow> set (epQueue ep') \<inter> set (epQueue ep) = {} proof (prove)
goal:
No subgoals!
theory IpcCancel_C

lemma epQueue_head_mask_4 [simp]:
  "epQueue_head_CL (endpoint_lift ko') && ~~ mask 4 = epQueue_head_CL (endpoint_lift ko')" unfolding endpoint_lift_def by (clarsimp simp: mask_def word_bw_assocs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. epQueue_head_CL (endpoint_lift ko') && ~~ mask 4 = epQueue_head_CL (endpoint_lift ko') proof (prove)
goal (1 subgoal):
 1. epQueue_head_CL \<lparr>epQueue_head_CL = (endpoint_C.words_C ko'.[1] << 0) && ~~ mask 4, epQueue_tail_CL = (endpoint_C.words_C ko'.[0] << 0) && ~~ mask 4, state_CL = (endpoint_C.words_C ko'.[0] >> 0) && mask 2\<rparr> && ~~ mask 4 = epQueue_head_CL \<lparr>epQueue_head_CL = (endpoint_C.words_C ko'.[1] << 0) && ~~ mask 4, epQueue_tail_CL = (endpoint_C.words_C ko'.[0] << 0) && ~~ mask 4, state_CL = (endpoint_C.words_C ko'.[0] >> 0) && mask 2\<rparr>
theory IpcCancel_C

lemma epQueue_tail_mask_4 [simp]:
  "epQueue_tail_CL (endpoint_lift ko') && ~~ mask 4 = epQueue_tail_CL (endpoint_lift ko')" unfolding endpoint_lift_def by (clarsimp simp: mask_def word_bw_assocs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. epQueue_tail_CL (endpoint_lift ko') && ~~ mask 4 = epQueue_tail_CL (endpoint_lift ko') proof (prove)
goal (1 subgoal):
 1. epQueue_tail_CL \<lparr>epQueue_head_CL = (endpoint_C.words_C ko'.[1] << 0) && ~~ mask 4, epQueue_tail_CL = (endpoint_C.words_C ko'.[0] << 0) && ~~ mask 4, state_CL = (endpoint_C.words_C ko'.[0] >> 0) && mask 2\<rparr> && ~~ mask 4 = epQueue_tail_CL \<lparr>epQueue_head_CL = (endpoint_C.words_C ko'.[1] << 0) && ~~ mask 4, epQueue_tail_CL = (endpoint_C.words_C ko'.[0] << 0) && ~~ mask 4, state_CL = (endpoint_C.words_C ko'.[0] >> 0) && mask 2\<rparr>
theory IpcCancel_C

lemma ep_blocked_in_queueD_recv:
  "\<lbrakk>st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnReceive x gr)) thread \<sigma>; ko_at' ep' x \<sigma>; invs' \<sigma>\<rbrakk> \<Longrightarrow> thread \<in> set (epQueue ep') \<and> isRecvEP ep'" apply (frule sym_refs_st_tcb_atD', clarsimp) apply (clarsimp simp: refs_of_rev' obj_at'_def ko_wp_at'_def projectKOs) apply (cases ep', simp_all add: isSendEP_def isRecvEP_def)[1] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnReceive x gr)) thread \<sigma>; ko_at' ep' x \<sigma>; invs' \<sigma>\<rbrakk> \<Longrightarrow> thread \<in> set (epQueue ep') \<and> isRecvEP ep' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnReceive x gr)) thread \<sigma>; ko_at' ep' x \<sigma>; invs' \<sigma>; \<exists>ts ntfnptr. Structures_H.thread_state.BlockedOnReceive x gr = ts \<and> obj_at' (tcb_ntfn_is_bound' ntfnptr) thread \<sigma> \<and> state_refs_of' \<sigma> thread = tcb_st_refs_of' ts \<union> tcb_bound_refs' ntfnptr \<and> (\<forall>(x, tp)\<in>tcb_st_refs_of' ts \<union> tcb_bound_refs' ntfnptr. ko_wp_at' (\<lambda>ko. (thread, symreftype tp) \<in> refs_of' ko) x \<sigma>)\<rbrakk> \<Longrightarrow> thread \<in> set (epQueue ep') \<and> isRecvEP ep' proof (prove)
goal (1 subgoal):
 1. \<And>ntfnptr obj. \<lbrakk>st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnReceive x gr)) thread \<sigma>; invs' \<sigma>; ksPSpace \<sigma> x = Some (KOEndpoint ep'); is_aligned x (objBitsKO (KOEndpoint ep')); ps_clear x (objBitsKO (KOEndpoint ep')) \<sigma>; state_refs_of' \<sigma> thread = insert (x, TCBBlockedRecv) (tcb_bound_refs' ntfnptr); ksPSpace \<sigma> thread = Some (KOTCB obj); (thread, EPRecv) \<in> ep_q_refs_of' ep'; \<forall>x\<in>tcb_bound_refs' ntfnptr. case x of (x, tp) \<Rightarrow> \<exists>ko. ksPSpace \<sigma> x = Some ko \<and> is_aligned x (objBitsKO ko) \<and> (thread, symreftype tp) \<in> refs_of' ko \<and> ps_clear x (objBitsKO ko) \<sigma>; is_aligned thread (objBitsKO (KOTCB obj)); tcb_ntfn_is_bound' ntfnptr obj; ps_clear thread (objBitsKO (KOTCB obj)) \<sigma>\<rbrakk> \<Longrightarrow> thread \<in> set (epQueue ep') \<and> isRecvEP ep' proof (prove)
goal:
No subgoals!
theory IpcCancel_C

lemma ep_blocked_in_queueD_send:
  "\<lbrakk>st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnSend x xa xb xc xd)) thread \<sigma>; ko_at' ep' x \<sigma>; invs' \<sigma>\<rbrakk> \<Longrightarrow> thread \<in> set (epQueue ep') \<and> isSendEP ep'" apply (frule sym_refs_st_tcb_atD', clarsimp) apply (clarsimp simp: refs_of_rev' obj_at'_def ko_wp_at'_def projectKOs) apply (cases ep', simp_all add: isSendEP_def isRecvEP_def)[1] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnSend x xa xb xc xd)) thread \<sigma>; ko_at' ep' x \<sigma>; invs' \<sigma>\<rbrakk> \<Longrightarrow> thread \<in> set (epQueue ep') \<and> isSendEP ep' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnSend x xa xb xc xd)) thread \<sigma>; ko_at' ep' x \<sigma>; invs' \<sigma>; \<exists>ts ntfnptr. Structures_H.thread_state.BlockedOnSend x xa xb xc xd = ts \<and> obj_at' (tcb_ntfn_is_bound' ntfnptr) thread \<sigma> \<and> state_refs_of' \<sigma> thread = tcb_st_refs_of' ts \<union> tcb_bound_refs' ntfnptr \<and> (\<forall>(x, tp)\<in>tcb_st_refs_of' ts \<union> tcb_bound_refs' ntfnptr. ko_wp_at' (\<lambda>ko. (thread, symreftype tp) \<in> refs_of' ko) x \<sigma>)\<rbrakk> \<Longrightarrow> thread \<in> set (epQueue ep') \<and> isSendEP ep' proof (prove)
goal (1 subgoal):
 1. \<And>ntfnptr obj. \<lbrakk>st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnSend x xa xb xc xd)) thread \<sigma>; invs' \<sigma>; ksPSpace \<sigma> x = Some (KOEndpoint ep'); is_aligned x (objBitsKO (KOEndpoint ep')); ps_clear x (objBitsKO (KOEndpoint ep')) \<sigma>; state_refs_of' \<sigma> thread = insert (x, TCBBlockedSend) (tcb_bound_refs' ntfnptr); ksPSpace \<sigma> thread = Some (KOTCB obj); (thread, EPSend) \<in> ep_q_refs_of' ep'; \<forall>x\<in>tcb_bound_refs' ntfnptr. case x of (x, tp) \<Rightarrow> \<exists>ko. ksPSpace \<sigma> x = Some ko \<and> is_aligned x (objBitsKO ko) \<and> (thread, symreftype tp) \<in> refs_of' ko \<and> ps_clear x (objBitsKO ko) \<sigma>; is_aligned thread (objBitsKO (KOTCB obj)); tcb_ntfn_is_bound' ntfnptr obj; ps_clear thread (objBitsKO (KOTCB obj)) \<sigma>\<rbrakk> \<Longrightarrow> thread \<in> set (epQueue ep') \<and> isSendEP ep' proof (prove)
goal:
No subgoals!
theory Finalise_C

lemma obj_at_ko_at2':
  "\<lbrakk> obj_at' P p s; ko_at' ko p s \<rbrakk> \<Longrightarrow> P ko" apply (drule obj_at_ko_at') apply clarsimp apply (drule ko_at_obj_congD', simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>obj_at' P p s; ko_at' ko p s\<rbrakk> \<Longrightarrow> P ko proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at' ko p s; \<exists>ko. ko_at' ko p s \<and> P ko\<rbrakk> \<Longrightarrow> P ko proof (prove)
goal (1 subgoal):
 1. \<And>koa. \<lbrakk>ko_at' ko p s; ko_at' koa p s; P koa\<rbrakk> \<Longrightarrow> P ko proof (prove)
goal:
No subgoals!
theory Finalise_C

lemma ctcb_relation_tcbDomain:
  "ctcb_relation tcb tcb' \<Longrightarrow> ucast (tcbDomain tcb) = tcbDomain_C tcb'" by (simp add: ctcb_relation_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ctcb_relation tcb tcb' \<Longrightarrow> UCAST(8 \<rightarrow> 32) (tcbDomain tcb) = tcbDomain_C tcb'
theory Finalise_C

lemma ctcb_relation_tcbPriority:
  "ctcb_relation tcb tcb' \<Longrightarrow> ucast (tcbPriority tcb) = tcbPriority_C tcb'" by (simp add: ctcb_relation_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ctcb_relation tcb tcb' \<Longrightarrow> UCAST(8 \<rightarrow> 32) (tcbPriority tcb) = tcbPriority_C tcb'