theory IpcCancel_R

lemma (in delete_one_conc) cancelIPC_invs[wp]:
  shows "\<lbrace>tcb_at' t and invs'\<rbrace> cancelIPC t \<lbrace>\<lambda>rv. invs'\<rbrace>" proof - have P: "\<And>xs v f. (case xs of [] \<Rightarrow> return v | y # ys \<Rightarrow> return (f (y # ys)))
                         = return (case xs of [] \<Rightarrow> v | y # ys \<Rightarrow> f xs)" by (clarsimp split: list.split) have NIQ: "\<And>s. \<lbrakk> Invariants_H.valid_queues s; st_tcb_at' (Not \<circ> runnable') t s \<rbrakk>
                                       \<Longrightarrow> \<forall>x. t \<notin> set (ksReadyQueues s x)" apply (clarsimp simp add: pred_tcb_at'_def Invariants_H.valid_queues_def valid_queues_no_bitmap_def) apply (drule spec | drule(1) bspec | clarsimp simp: obj_at'_def inQ_def)+ done have EPSCHN: "\<And>eeptr ep'. \<lbrace>\<lambda>s. sch_act_not (ksCurThread s) s\<rbrace>
                             setEndpoint eeptr ep'
                             \<lbrace>\<lambda>_ s. sch_act_not (ksCurThread s) s\<rbrace>" apply (rule hoare_weaken_pre) apply (wps setEndpoint_ct') apply (wp, simp) done have Q:
    "\<And>epptr. \<lbrace>st_tcb_at' (\<lambda>st. \<exists>a. (st = BlockedOnReceive epptr a)
                            \<or> (\<exists>a b c d. st = BlockedOnSend epptr a b c d)) t
                  and invs'\<rbrace>
      do ep \<leftarrow> getEndpoint epptr;
         y \<leftarrow> assert (\<not> (case ep of IdleEP \<Rightarrow> True | _ \<Rightarrow> False));
         ep' \<leftarrow> case remove1 t (epQueue ep)
                of [] \<Rightarrow> return Structures_H.endpoint.IdleEP
                | x # xs \<Rightarrow> return (epQueue_update (%_. x # xs) ep);
         y \<leftarrow> setEndpoint epptr ep';
         setThreadState Inactive t
      od \<lbrace>\<lambda>rv. invs'\<rbrace>" apply (simp add: invs'_def valid_state'_def) apply (subst P) apply (wp valid_irq_node_lift valid_global_refs_lift' valid_arch_state_lift'
              irqs_masked_lift sts_sch_act'
              hoare_vcg_all_lift [OF setEndpoint_ksQ]
              sts_valid_queues setThreadState_ct_not_inQ EPSCHN
              hoare_vcg_all_lift setNotification_ksQ
              | simp add: valid_tcb_state'_def split del: if_split
              | wpc)+ prefer 2 apply assumption apply (rule hoare_strengthen_post [OF get_ep_sp']) apply (clarsimp simp: pred_tcb_at' fun_upd_def[symmetric] conj_comms
               split del: if_split cong: if_cong) apply (rule conjI, clarsimp simp: valid_idle'_def pred_tcb_at'_def obj_at'_def idle_tcb'_def) apply (frule obj_at_valid_objs', clarsimp) apply (clarsimp simp: projectKOs valid_obj'_def) apply (rule conjI) apply (clarsimp simp: obj_at'_def valid_ep'_def projectKOs
                    dest!: pred_tcb_at') apply (frule NIQ) apply (erule pred_tcb'_weakenE, fastforce) apply (clarsimp, rule conjI) apply (auto simp: pred_tcb_at'_def obj_at'_def)[1] apply (rule conjI) apply (clarsimp split: Structures_H.endpoint.split_asm list.split
                      simp: valid_ep'_def) apply (rename_tac list x xs) apply (frule distinct_remove1[where x=t]) apply (cut_tac xs=list in set_remove1_subset[where x=t]) apply auto[1] apply (rename_tac list x xs) apply (frule distinct_remove1[where x=t]) apply (cut_tac xs=list in set_remove1_subset[where x=t]) apply auto[1] apply (frule(1) sym_refs_ko_atD') apply (rule conjI) apply (clarsimp elim!: if_live_state_refsE split: Structures_H.endpoint.split_asm) apply (drule st_tcb_at_state_refs_ofD') apply (clarsimp simp: ep_redux_simps3 valid_ep'_def
                   split: Structures_H.endpoint.split_asm
                    cong: list.case_cong) apply (frule_tac x=t in distinct_remove1) apply (frule_tac x=t in set_remove1_eq) by (auto elim!: delta_sym_refs
               simp: symreftype_inverse' tcb_st_refs_of'_def tcb_bound_refs'_def
              split: thread_state.splits if_split_asm) have R:
    "\<lbrace>invs' and tcb_at' t\<rbrace>
     do y \<leftarrow> threadSet (\<lambda>tcb. tcb \<lparr> tcbFault := None \<rparr>) t;
        slot \<leftarrow> getThreadReplySlot t;
        callerCap \<leftarrow> liftM (mdbNext \<circ> cteMDBNode) (getCTE slot);
        when (callerCap \<noteq> nullPointer) (do
            y \<leftarrow> stateAssert (capHasProperty callerCap (\<lambda>cap. isReplyCap cap
                                                           \<and> \<not> capReplyMaster cap))
                [];
            cteDeleteOne callerCap
        od)
     od
     \<lbrace>\<lambda>rv. invs'\<rbrace>" unfolding getThreadReplySlot_def by (wp valid_irq_node_lift delete_one_invs hoare_drop_imps
           threadSet_invs_trivial irqs_masked_lift
      | simp add: o_def if_apply_def2
      | fastforce simp: inQ_def)+ show ?thesis apply (simp add:   cancelIPC_def crunch_simps
               cong:   if_cong list.case_cong) apply (rule hoare_seq_ext [OF _ gts_sp']) apply (case_tac state,
           simp_all add: isTS_defs) apply (safe intro!: hoare_weaken_pre[OF Q]
                               hoare_weaken_pre[OF R]
                               hoare_weaken_pre[OF return_wp]
                               hoare_weaken_pre[OF cancelSignal_invs']
                       elim!: pred_tcb'_weakenE) apply (auto simp: pred_tcb_at'_def obj_at'_def
                      dest: invs_sch_act_wf') done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at' t and invs'\<rbrace> cancelIPC t \<lbrace>\<lambda>rv. invs'\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>tcb_at' t and invs'\<rbrace> cancelIPC t \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>xs v f. (case xs of [] \<Rightarrow> return v | y # ys \<Rightarrow> return (f (y # ys))) = return (case xs of [] \<Rightarrow> v | y # ys \<Rightarrow> f xs) proof (state)
this:
(case ?xs of [] \<Rightarrow> return ?v | y # ys \<Rightarrow> return (?f (y # ys))) = return (case ?xs of [] \<Rightarrow> ?v | y # ys \<Rightarrow> ?f ?xs)

goal (1 subgoal):
 1. \<lbrace>tcb_at' t and invs'\<rbrace> cancelIPC t \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>Invariants_H.valid_queues s; st_tcb_at' (Not \<circ> runnable') t s\<rbrakk> \<Longrightarrow> \<forall>x. t \<notin> set (ksReadyQueues s x) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>obj_at' (\<lambda>ko. \<not> runnable' (tcbState ko)) t s; \<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). obj_at' (inQ d p and runnable' \<circ> tcbState) t s) \<and> distinct (ksReadyQueues s (d, p)) \<and> (maxDomain < d \<longrightarrow> ksReadyQueues s (d, p) = []) \<and> (maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = []); valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; t \<in> set (ksReadyQueues s (a, b))\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>Invariants_H.valid_queues ?s1; st_tcb_at' (Not \<circ> runnable') t ?s1\<rbrakk> \<Longrightarrow> \<forall>x. t \<notin> set (ksReadyQueues ?s1 x)

goal (1 subgoal):
 1. \<lbrace>tcb_at' t and invs'\<rbrace> cancelIPC t \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>eeptr ep'. \<lbrace>\<lambda>s. sch_act_not (ksCurThread s) s\<rbrace> setEndpoint eeptr ep' \<lbrace>\<lambda>_ s. sch_act_not (ksCurThread s) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>eeptr ep'. \<lbrace>?Q eeptr ep'\<rbrace> setEndpoint eeptr ep' \<lbrace>\<lambda>_ s. sch_act_not (ksCurThread s) s\<rbrace>
 2. \<And>eeptr ep' s. sch_act_not (ksCurThread s) s \<Longrightarrow> ?Q eeptr ep' s proof (prove)
goal (2 subgoals):
 1. \<And>eeptr ep' prev_s. \<lbrace>?P3 eeptr ep' prev_s\<rbrace> setEndpoint eeptr ep' \<lbrace>\<lambda>rv s'. sch_act_not (ksCurThread prev_s) prev_s\<rbrace>
 2. \<And>eeptr ep' s. sch_act_not (ksCurThread s) s \<Longrightarrow> ?P3 eeptr ep' s s proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>\<lambda>s. sch_act_not (ksCurThread s) s\<rbrace> setEndpoint ?eeptr1 ?ep'1 \<lbrace>\<lambda>_ s. sch_act_not (ksCurThread s) s\<rbrace>

goal (1 subgoal):
 1. \<lbrace>tcb_at' t and invs'\<rbrace> cancelIPC t \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>epptr. \<lbrace>st_tcb_at' (\<lambda>st. \<exists>a. st = Structures_H.thread_state.BlockedOnReceive epptr a \<or> (\<exists>a b c d. st = Structures_H.thread_state.BlockedOnSend epptr a b c d)) t and invs'\<rbrace> do ep <- getEndpoint epptr;
y <- assert (\<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False));
ep' <- case remove1 t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | x # xs \<Rightarrow> return (epQueue_update (\<lambda>_. x # xs) ep);
y <- setEndpoint epptr ep';
setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>epptr. \<lbrace>st_tcb_at' (\<lambda>st. (\<exists>a. st = Structures_H.thread_state.BlockedOnReceive epptr a) \<or> (\<exists>a b c d. st = Structures_H.thread_state.BlockedOnSend epptr a b c d)) t and ((\<lambda>s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)) \<and> untyped_ranges_zero' s) and cur_tcb')\<rbrace> do ep <- getEndpoint epptr;
y <- assert (\<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False));
ep' <- case remove1 t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | x # xs \<Rightarrow> return (epQueue_update (\<lambda>_. x # xs) ep);
y <- setEndpoint epptr ep';
setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>rv. (\<lambda>s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)) \<and> untyped_ranges_zero' s) and cur_tcb'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>epptr. \<lbrace>st_tcb_at' (\<lambda>st. (\<exists>a. st = Structures_H.thread_state.BlockedOnReceive epptr a) \<or> (\<exists>a b c d. st = Structures_H.thread_state.BlockedOnSend epptr a b c d)) t and ((\<lambda>s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)) \<and> untyped_ranges_zero' s) and cur_tcb')\<rbrace> do ep <- getEndpoint epptr;
y <- assert (\<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False));
ep' <- return (case remove1 t (epQueue ep) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue ep)) ep);
y <- setEndpoint epptr ep';
setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>rv. (\<lambda>s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)) \<and> untyped_ranges_zero' s) and cur_tcb'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>epptr. \<lbrace>?Q1 epptr\<rbrace> getEndpoint epptr \<lbrace>\<lambda>ep s. \<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False) \<longrightarrow> valid_pspace' s \<and> valid_ep' (case remove1 t (epQueue ep) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue ep)) ep) s \<and> tcb_at' t s \<and> sch_act_not t s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues s (x, xa))) \<and> sym_refs (\<lambda>a. if a = t then {r \<in> ((state_refs_of' s)(epptr := ep_q_refs_of' (case remove1 t (epQueue ep) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue ep)) ep))) t. snd r = TCBBound} else ((state_refs_of' s)(epptr := ep_q_refs_of' (case remove1 t (epQueue ep) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue ep)) ep))) a) \<and> if_live_then_nonz_cap' s \<and> ((case remove1 t (epQueue ep) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue ep)) ep) \<noteq> Structures_H.endpoint.IdleEP \<longrightarrow> ex_nonz_cap_to' epptr s) \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_pspace' s \<and> valid_ep' (case remove1 t (epQueue ep) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue ep)) ep) s \<and> t \<noteq> ksIdleThread s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)) \<and> untyped_ranges_zero' s \<and> cur_tcb' s\<rbrace>
 2. \<And>epptr s. (st_tcb_at' (\<lambda>st. (\<exists>a. st = Structures_H.thread_state.BlockedOnReceive epptr a) \<or> (\<exists>a b c d. st = Structures_H.thread_state.BlockedOnSend epptr a b c d)) t and ((\<lambda>s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)) \<and> untyped_ranges_zero' s) and cur_tcb')) s \<Longrightarrow> ?Q1 epptr s proof (prove)
goal (2 subgoals):
 1. \<And>epptr s. (st_tcb_at' (\<lambda>st. (\<exists>a. st = Structures_H.thread_state.BlockedOnReceive epptr a) \<or> (\<exists>a b c d. st = Structures_H.thread_state.BlockedOnSend epptr a b c d)) t and ((\<lambda>s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)) \<and> untyped_ranges_zero' s) and cur_tcb')) s \<Longrightarrow> ?Q1 epptr s
 2. \<And>epptr. \<lbrace>?Q1 epptr\<rbrace> getEndpoint epptr \<lbrace>\<lambda>ep s. \<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False) \<longrightarrow> valid_pspace' s \<and> valid_ep' (case remove1 t (epQueue ep) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue ep)) ep) s \<and> tcb_at' t s \<and> sch_act_not t s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues s (x, xa))) \<and> sym_refs (\<lambda>a. if a = t then {r \<in> ((state_refs_of' s)(epptr := ep_q_refs_of' (case remove1 t (epQueue ep) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue ep)) ep))) t. snd r = TCBBound} else ((state_refs_of' s)(epptr := ep_q_refs_of' (case remove1 t (epQueue ep) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue ep)) ep))) a) \<and> if_live_then_nonz_cap' s \<and> ((case remove1 t (epQueue ep) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue ep)) ep) \<noteq> Structures_H.endpoint.IdleEP \<longrightarrow> ex_nonz_cap_to' epptr s) \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_pspace' s \<and> valid_ep' (case remove1 t (epQueue ep) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue ep)) ep) s \<and> t \<noteq> ksIdleThread s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)) \<and> untyped_ranges_zero' s \<and> cur_tcb' s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>epptr. \<lbrace>st_tcb_at' (\<lambda>st. (\<exists>a. st = Structures_H.thread_state.BlockedOnReceive epptr a) \<or> (\<exists>a b c d. st = Structures_H.thread_state.BlockedOnSend epptr a b c d)) t and ((\<lambda>s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)) \<and> untyped_ranges_zero' s) and cur_tcb')\<rbrace> getEndpoint epptr \<lbrace>\<lambda>ep s. \<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False) \<longrightarrow> valid_pspace' s \<and> valid_ep' (case remove1 t (epQueue ep) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue ep)) ep) s \<and> tcb_at' t s \<and> sch_act_not t s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues s (x, xa))) \<and> sym_refs (\<lambda>a. if a = t then {r \<in> ((state_refs_of' s)(epptr := ep_q_refs_of' (case remove1 t (epQueue ep) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue ep)) ep))) t. snd r = TCBBound} else ((state_refs_of' s)(epptr := ep_q_refs_of' (case remove1 t (epQueue ep) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue ep)) ep))) a) \<and> if_live_then_nonz_cap' s \<and> ((case remove1 t (epQueue ep) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue ep)) ep) \<noteq> Structures_H.endpoint.IdleEP \<longrightarrow> ex_nonz_cap_to' epptr s) \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_pspace' s \<and> valid_ep' (case remove1 t (epQueue ep) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue ep)) ep) s \<and> t \<noteq> ksIdleThread s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)) \<and> untyped_ranges_zero' s \<and> cur_tcb' s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>epptr rv s. (st_tcb_at' (\<lambda>st. (\<exists>a. st = Structures_H.thread_state.BlockedOnReceive epptr a) \<or> (\<exists>a b c d. st = Structures_H.thread_state.BlockedOnSend epptr a b c d)) t and ((\<lambda>s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)) \<and> untyped_ranges_zero' s) and cur_tcb') and ko_at' rv epptr) s \<Longrightarrow> \<not> (case rv of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False) \<longrightarrow> valid_pspace' s \<and> valid_ep' (case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv) s \<and> tcb_at' t s \<and> sch_act_not t s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues s (x, xa))) \<and> sym_refs (\<lambda>a. if a = t then {r \<in> ((state_refs_of' s)(epptr := ep_q_refs_of' (case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv))) t. snd r = TCBBound} else ((state_refs_of' s)(epptr := ep_q_refs_of' (case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv))) a) \<and> if_live_then_nonz_cap' s \<and> ((case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv) \<noteq> Structures_H.endpoint.IdleEP \<longrightarrow> ex_nonz_cap_to' epptr s) \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_pspace' s \<and> valid_ep' (case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv) s \<and> t \<noteq> ksIdleThread s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)) \<and> untyped_ranges_zero' s \<and> cur_tcb' s proof (prove)
goal (1 subgoal):
 1. \<And>epptr rv s. \<lbrakk>ct_idle_or_in_cur_domain' s; ct_not_inQ s; cur_tcb' s; if_live_then_nonz_cap' s; if_unsafe_then_cap' s; irqs_masked' s; pspace_domain_valid s; valid_arch_state' s; valid_global_refs' s; valid_idle' s; valid_irq_handlers' s; valid_machine_state' s; valid_pde_mappings' s; valid_pspace' s; Invariants_H.valid_queues s; valid_queues' s; sym_refs (state_refs_of' s); sch_act_wf (ksSchedulerAction s) s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; untyped_ranges_zero' s; valid_irq_node' (irq_node' s) s; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ko_at' rv epptr s; valid_irq_states' s; ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; st_tcb_at' (\<lambda>st. (\<exists>a. st = Structures_H.thread_state.BlockedOnReceive epptr a) \<or> (\<exists>a b c d. st = Structures_H.thread_state.BlockedOnSend epptr a b c d)) t s; \<not> (case rv of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False)\<rbrakk> \<Longrightarrow> t \<noteq> ksIdleThread s \<and> sch_act_not t s \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues s (x, xa))) \<and> valid_ep' (case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv) s \<and> ((case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv) \<noteq> Structures_H.endpoint.IdleEP \<longrightarrow> ex_nonz_cap_to' epptr s) \<and> sym_refs ((state_refs_of' s)(epptr := ep_q_refs_of' (case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv), t := {r. snd r = TCBBound \<and> r \<in> (if t = epptr then ep_q_refs_of' (case remove1 epptr (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv) else state_refs_of' s t)})) proof (prove)
goal (1 subgoal):
 1. \<And>epptr rv s. \<lbrakk>ct_idle_or_in_cur_domain' s; ct_not_inQ s; cur_tcb' s; if_live_then_nonz_cap' s; if_unsafe_then_cap' s; irqs_masked' s; pspace_domain_valid s; valid_arch_state' s; valid_global_refs' s; valid_idle' s; valid_irq_handlers' s; valid_machine_state' s; valid_pde_mappings' s; valid_pspace' s; Invariants_H.valid_queues s; valid_queues' s; sym_refs (state_refs_of' s); sch_act_wf (ksSchedulerAction s) s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; untyped_ranges_zero' s; valid_irq_node' (irq_node' s) s; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ko_at' rv epptr s; valid_irq_states' s; ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; st_tcb_at' (\<lambda>st. (\<exists>a. st = Structures_H.thread_state.BlockedOnReceive epptr a) \<or> (\<exists>a b c d. st = Structures_H.thread_state.BlockedOnSend epptr a b c d)) t s; \<not> (case rv of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False)\<rbrakk> \<Longrightarrow> sch_act_not t s \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues s (x, xa))) \<and> valid_ep' (case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv) s \<and> ((case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv) \<noteq> Structures_H.endpoint.IdleEP \<longrightarrow> ex_nonz_cap_to' epptr s) \<and> sym_refs ((state_refs_of' s)(epptr := ep_q_refs_of' (case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv), t := {r. snd r = TCBBound \<and> r \<in> (if t = epptr then ep_q_refs_of' (case remove1 epptr (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv) else state_refs_of' s t)})) proof (prove)
goal (1 subgoal):
 1. \<And>epptr rv s. \<lbrakk>ct_idle_or_in_cur_domain' s; ct_not_inQ s; cur_tcb' s; if_live_then_nonz_cap' s; if_unsafe_then_cap' s; irqs_masked' s; pspace_domain_valid s; valid_arch_state' s; valid_global_refs' s; valid_idle' s; valid_irq_handlers' s; valid_machine_state' s; valid_pde_mappings' s; valid_pspace' s; Invariants_H.valid_queues s; valid_queues' s; sym_refs (state_refs_of' s); sch_act_wf (ksSchedulerAction s) s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; untyped_ranges_zero' s; valid_irq_node' (irq_node' s) s; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ko_at' rv epptr s; valid_irq_states' s; ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; st_tcb_at' (\<lambda>st. (\<exists>a. st = Structures_H.thread_state.BlockedOnReceive epptr a) \<or> (\<exists>a b c d. st = Structures_H.thread_state.BlockedOnSend epptr a b c d)) t s; \<not> (case rv of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False); \<exists>k. k = rv \<and> ((\<forall>ko. projectKO_opt ko = Some k \<longrightarrow> injectKO k = ko) \<longrightarrow> valid_obj' (injectKO k) s)\<rbrakk> \<Longrightarrow> sch_act_not t s \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues s (x, xa))) \<and> valid_ep' (case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv) s \<and> ((case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv) \<noteq> Structures_H.endpoint.IdleEP \<longrightarrow> ex_nonz_cap_to' epptr s) \<and> sym_refs ((state_refs_of' s)(epptr := ep_q_refs_of' (case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv), t := {r. snd r = TCBBound \<and> r \<in> (if t = epptr then ep_q_refs_of' (case remove1 epptr (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv) else state_refs_of' s t)})) proof (prove)
goal (1 subgoal):
 1. \<And>epptr rv s. \<lbrakk>ct_idle_or_in_cur_domain' s; ct_not_inQ s; cur_tcb' s; if_live_then_nonz_cap' s; if_unsafe_then_cap' s; irqs_masked' s; pspace_domain_valid s; valid_arch_state' s; valid_global_refs' s; valid_idle' s; valid_irq_handlers' s; valid_machine_state' s; valid_pde_mappings' s; valid_pspace' s; Invariants_H.valid_queues s; valid_queues' s; sym_refs (state_refs_of' s); sch_act_wf (ksSchedulerAction s) s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; untyped_ranges_zero' s; valid_irq_node' (irq_node' s) s; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ko_at' rv epptr s; valid_irq_states' s; ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; st_tcb_at' (\<lambda>st. (\<exists>a. st = Structures_H.thread_state.BlockedOnReceive epptr a) \<or> (\<exists>a b c d. st = Structures_H.thread_state.BlockedOnSend epptr a b c d)) t s; \<not> (case rv of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False); valid_ep' rv s\<rbrakk> \<Longrightarrow> (t = epptr \<longrightarrow> sch_act_not epptr s \<and> (\<forall>x xa. epptr \<notin> set (ksReadyQueues s (x, xa))) \<and> valid_ep' (case remove1 epptr (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv) s \<and> ((case remove1 epptr (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv) \<noteq> Structures_H.endpoint.IdleEP \<longrightarrow> ex_nonz_cap_to' epptr s) \<and> sym_refs ((state_refs_of' s)(epptr := {r. snd r = TCBBound \<and> r \<in> ep_q_refs_of' (case remove1 epptr (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv)}))) \<and> (t \<noteq> epptr \<longrightarrow> sch_act_not t s \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues s (x, xa))) \<and> valid_ep' (case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv) s \<and> ((case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv) \<noteq> Structures_H.endpoint.IdleEP \<longrightarrow> ex_nonz_cap_to' epptr s) \<and> sym_refs ((state_refs_of' s)(epptr := ep_q_refs_of' (case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv), t := {r. snd r = TCBBound \<and> r \<in> state_refs_of' s t}))) proof (prove)
goal (2 subgoals):
 1. \<And>epptr rv s. \<lbrakk>ct_idle_or_in_cur_domain' s; ct_not_inQ s; cur_tcb' s; if_live_then_nonz_cap' s; if_unsafe_then_cap' s; irqs_masked' s; pspace_domain_valid s; valid_arch_state' s; valid_global_refs' s; valid_idle' s; valid_irq_handlers' s; valid_machine_state' s; valid_pde_mappings' s; valid_pspace' s; Invariants_H.valid_queues s; valid_queues' s; sym_refs (state_refs_of' s); sch_act_wf (ksSchedulerAction s) s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; untyped_ranges_zero' s; valid_irq_node' (irq_node' s) s; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ko_at' rv epptr s; valid_irq_states' s; ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; st_tcb_at' (\<lambda>st. (\<exists>a. st = Structures_H.thread_state.BlockedOnReceive epptr a) \<or> (\<exists>a b c d. st = Structures_H.thread_state.BlockedOnSend epptr a b c d)) t s; \<not> (case rv of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False); valid_ep' rv s\<rbrakk> \<Longrightarrow> t = epptr \<longrightarrow> sch_act_not epptr s \<and> (\<forall>x xa. epptr \<notin> set (ksReadyQueues s (x, xa))) \<and> valid_ep' (case remove1 epptr (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv) s \<and> ((case remove1 epptr (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv) \<noteq> Structures_H.endpoint.IdleEP \<longrightarrow> ex_nonz_cap_to' epptr s) \<and> sym_refs ((state_refs_of' s)(epptr := {r. snd r = TCBBound \<and> r \<in> ep_q_refs_of' (case remove1 epptr (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv)}))
 2. \<And>epptr rv s. \<lbrakk>ct_idle_or_in_cur_domain' s; ct_not_inQ s; cur_tcb' s; if_live_then_nonz_cap' s; if_unsafe_then_cap' s; irqs_masked' s; pspace_domain_valid s; valid_arch_state' s; valid_global_refs' s; valid_idle' s; valid_irq_handlers' s; valid_machine_state' s; valid_pde_mappings' s; valid_pspace' s; Invariants_H.valid_queues s; valid_queues' s; sym_refs (state_refs_of' s); sch_act_wf (ksSchedulerAction s) s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; untyped_ranges_zero' s; valid_irq_node' (irq_node' s) s; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ko_at' rv epptr s; valid_irq_states' s; ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; st_tcb_at' (\<lambda>st. (\<exists>a. st = Structures_H.thread_state.BlockedOnReceive epptr a) \<or> (\<exists>a b c d. st = Structures_H.thread_state.BlockedOnSend epptr a b c d)) t s; \<not> (case rv of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False); valid_ep' rv s\<rbrakk> \<Longrightarrow> t \<noteq> epptr \<longrightarrow> sch_act_not t s \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues s (x, xa))) \<and> valid_ep' (case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv) s \<and> ((case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv) \<noteq> Structures_H.endpoint.IdleEP \<longrightarrow> ex_nonz_cap_to' epptr s) \<and> sym_refs ((state_refs_of' s)(epptr := ep_q_refs_of' (case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv), t := {r. snd r = TCBBound \<and> r \<in> state_refs_of' s t})) proof (prove)
goal (1 subgoal):
 1. \<And>epptr rv s. \<lbrakk>ct_idle_or_in_cur_domain' s; ct_not_inQ s; cur_tcb' s; if_live_then_nonz_cap' s; if_unsafe_then_cap' s; irqs_masked' s; pspace_domain_valid s; valid_arch_state' s; valid_global_refs' s; valid_idle' s; valid_irq_handlers' s; valid_machine_state' s; valid_pde_mappings' s; valid_pspace' s; Invariants_H.valid_queues s; valid_queues' s; sym_refs (state_refs_of' s); sch_act_wf (ksSchedulerAction s) s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; untyped_ranges_zero' s; valid_irq_node' (irq_node' s) s; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ko_at' rv epptr s; valid_irq_states' s; ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; st_tcb_at' (\<lambda>st. (\<exists>a. st = Structures_H.thread_state.BlockedOnReceive epptr a) \<or> (\<exists>a b c d. st = Structures_H.thread_state.BlockedOnSend epptr a b c d)) t s; \<not> (case rv of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False); valid_ep' rv s\<rbrakk> \<Longrightarrow> t \<noteq> epptr \<longrightarrow> sch_act_not t s \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues s (x, xa))) \<and> valid_ep' (case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv) s \<and> ((case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv) \<noteq> Structures_H.endpoint.IdleEP \<longrightarrow> ex_nonz_cap_to' epptr s) \<and> sym_refs ((state_refs_of' s)(epptr := ep_q_refs_of' (case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv), t := {r. snd r = TCBBound \<and> r \<in> state_refs_of' s t})) proof (prove)
goal (2 subgoals):
 1. \<And>epptr rv s. \<lbrakk>ct_idle_or_in_cur_domain' s; ct_not_inQ s; cur_tcb' s; if_live_then_nonz_cap' s; if_unsafe_then_cap' s; irqs_masked' s; pspace_domain_valid s; valid_arch_state' s; valid_global_refs' s; valid_idle' s; valid_irq_handlers' s; valid_machine_state' s; valid_pde_mappings' s; valid_pspace' s; Invariants_H.valid_queues s; valid_queues' s; sym_refs (state_refs_of' s); sch_act_wf (ksSchedulerAction s) s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; untyped_ranges_zero' s; valid_irq_node' (irq_node' s) s; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ko_at' rv epptr s; valid_irq_states' s; ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; st_tcb_at' (\<lambda>st. (\<exists>a. st = Structures_H.thread_state.BlockedOnReceive epptr a) \<or> (\<exists>a b c d. st = Structures_H.thread_state.BlockedOnSend epptr a b c d)) t s; \<not> (case rv of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False); valid_ep' rv s\<rbrakk> \<Longrightarrow> st_tcb_at' (Not \<circ> runnable') t s
 2. \<And>epptr rv s. \<lbrakk>ct_idle_or_in_cur_domain' s; ct_not_inQ s; cur_tcb' s; if_live_then_nonz_cap' s; if_unsafe_then_cap' s; irqs_masked' s; pspace_domain_valid s; valid_arch_state' s; valid_global_refs' s; valid_idle' s; valid_irq_handlers' s; valid_machine_state' s; valid_pde_mappings' s; valid_pspace' s; Invariants_H.valid_queues s; valid_queues' s; sym_refs (state_refs_of' s); sch_act_wf (ksSchedulerAction s) s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; untyped_ranges_zero' s; valid_irq_node' (irq_node' s) s; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ko_at' rv epptr s; valid_irq_states' s; ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; st_tcb_at' (\<lambda>st. (\<exists>a. st = Structures_H.thread_state.BlockedOnReceive epptr a) \<or> (\<exists>a b c d. st = Structures_H.thread_state.BlockedOnSend epptr a b c d)) t s; \<not> (case rv of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False); valid_ep' rv s; \<forall>x. t \<notin> set (ksReadyQueues s x)\<rbrakk> \<Longrightarrow> t \<noteq> epptr \<longrightarrow> sch_act_not t s \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues s (x, xa))) \<and> valid_ep' (case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv) s \<and> ((case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv) \<noteq> Structures_H.endpoint.IdleEP \<longrightarrow> ex_nonz_cap_to' epptr s) \<and> sym_refs ((state_refs_of' s)(epptr := ep_q_refs_of' (case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv), t := {r. snd r = TCBBound \<and> r \<in> state_refs_of' s t})) proof (prove)
goal (1 subgoal):
 1. \<And>epptr rv s. \<lbrakk>ct_idle_or_in_cur_domain' s; ct_not_inQ s; cur_tcb' s; if_live_then_nonz_cap' s; if_unsafe_then_cap' s; irqs_masked' s; pspace_domain_valid s; valid_arch_state' s; valid_global_refs' s; valid_idle' s; valid_irq_handlers' s; valid_machine_state' s; valid_pde_mappings' s; valid_pspace' s; Invariants_H.valid_queues s; valid_queues' s; sym_refs (state_refs_of' s); sch_act_wf (ksSchedulerAction s) s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; untyped_ranges_zero' s; valid_irq_node' (irq_node' s) s; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ko_at' rv epptr s; valid_irq_states' s; ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; st_tcb_at' (\<lambda>st. (\<exists>a. st = Structures_H.thread_state.BlockedOnReceive epptr a) \<or> (\<exists>a b c d. st = Structures_H.thread_state.BlockedOnSend epptr a b c d)) t s; \<not> (case rv of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False); valid_ep' rv s; \<forall>x. t \<notin> set (ksReadyQueues s x)\<rbrakk> \<Longrightarrow> t \<noteq> epptr \<longrightarrow> sch_act_not t s \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues s (x, xa))) \<and> valid_ep' (case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv) s \<and> ((case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv) \<noteq> Structures_H.endpoint.IdleEP \<longrightarrow> ex_nonz_cap_to' epptr s) \<and> sym_refs ((state_refs_of' s)(epptr := ep_q_refs_of' (case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv), t := {r. snd r = TCBBound \<and> r \<in> state_refs_of' s t})) proof (prove)
goal (2 subgoals):
 1. \<And>epptr rv s. \<lbrakk>ct_idle_or_in_cur_domain' s; ct_not_inQ s; cur_tcb' s; if_live_then_nonz_cap' s; if_unsafe_then_cap' s; irqs_masked' s; pspace_domain_valid s; valid_arch_state' s; valid_global_refs' s; valid_idle' s; valid_irq_handlers' s; valid_machine_state' s; valid_pde_mappings' s; valid_pspace' s; Invariants_H.valid_queues s; valid_queues' s; sym_refs (state_refs_of' s); sch_act_wf (ksSchedulerAction s) s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; untyped_ranges_zero' s; valid_irq_node' (irq_node' s) s; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ko_at' rv epptr s; valid_irq_states' s; ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; st_tcb_at' (\<lambda>st. (\<exists>a. st = Structures_H.thread_state.BlockedOnReceive epptr a) \<or> (\<exists>a b c d. st = Structures_H.thread_state.BlockedOnSend epptr a b c d)) t s; \<not> (case rv of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False); valid_ep' rv s; \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)); t \<noteq> epptr\<rbrakk> \<Longrightarrow> sch_act_not t s
 2. \<And>epptr rv s. \<lbrakk>ct_idle_or_in_cur_domain' s; ct_not_inQ s; cur_tcb' s; if_live_then_nonz_cap' s; if_unsafe_then_cap' s; irqs_masked' s; pspace_domain_valid s; valid_arch_state' s; valid_global_refs' s; valid_idle' s; valid_irq_handlers' s; valid_machine_state' s; valid_pde_mappings' s; valid_pspace' s; Invariants_H.valid_queues s; valid_queues' s; sym_refs (state_refs_of' s); sch_act_wf (ksSchedulerAction s) s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; untyped_ranges_zero' s; valid_irq_node' (irq_node' s) s; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ko_at' rv epptr s; valid_irq_states' s; ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; st_tcb_at' (\<lambda>st. (\<exists>a. st = Structures_H.thread_state.BlockedOnReceive epptr a) \<or> (\<exists>a b c d. st = Structures_H.thread_state.BlockedOnSend epptr a b c d)) t s; \<not> (case rv of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False); valid_ep' rv s; \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)); t \<noteq> epptr\<rbrakk> \<Longrightarrow> valid_ep' (case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv) s \<and> ((case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv) \<noteq> Structures_H.endpoint.IdleEP \<longrightarrow> ex_nonz_cap_to' epptr s) \<and> sym_refs ((state_refs_of' s)(epptr := ep_q_refs_of' (case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv), t := {r. snd r = TCBBound \<and> r \<in> state_refs_of' s t})) proof (prove)
goal (1 subgoal):
 1. \<And>epptr rv s. \<lbrakk>ct_idle_or_in_cur_domain' s; ct_not_inQ s; cur_tcb' s; if_live_then_nonz_cap' s; if_unsafe_then_cap' s; irqs_masked' s; pspace_domain_valid s; valid_arch_state' s; valid_global_refs' s; valid_idle' s; valid_irq_handlers' s; valid_machine_state' s; valid_pde_mappings' s; valid_pspace' s; Invariants_H.valid_queues s; valid_queues' s; sym_refs (state_refs_of' s); sch_act_wf (ksSchedulerAction s) s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; untyped_ranges_zero' s; valid_irq_node' (irq_node' s) s; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ko_at' rv epptr s; valid_irq_states' s; ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; st_tcb_at' (\<lambda>st. (\<exists>a. st = Structures_H.thread_state.BlockedOnReceive epptr a) \<or> (\<exists>a b c d. st = Structures_H.thread_state.BlockedOnSend epptr a b c d)) t s; \<not> (case rv of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False); valid_ep' rv s; \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)); t \<noteq> epptr\<rbrakk> \<Longrightarrow> valid_ep' (case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv) s \<and> ((case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv) \<noteq> Structures_H.endpoint.IdleEP \<longrightarrow> ex_nonz_cap_to' epptr s) \<and> sym_refs ((state_refs_of' s)(epptr := ep_q_refs_of' (case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv), t := {r. snd r = TCBBound \<and> r \<in> state_refs_of' s t})) proof (prove)
goal (2 subgoals):
 1. \<And>epptr rv s. \<lbrakk>ct_idle_or_in_cur_domain' s; ct_not_inQ s; cur_tcb' s; if_live_then_nonz_cap' s; if_unsafe_then_cap' s; irqs_masked' s; pspace_domain_valid s; valid_arch_state' s; valid_global_refs' s; valid_idle' s; valid_irq_handlers' s; valid_machine_state' s; valid_pde_mappings' s; valid_pspace' s; Invariants_H.valid_queues s; valid_queues' s; sym_refs (state_refs_of' s); sch_act_wf (ksSchedulerAction s) s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; untyped_ranges_zero' s; valid_irq_node' (irq_node' s) s; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ko_at' rv epptr s; valid_irq_states' s; ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; st_tcb_at' (\<lambda>st. (\<exists>a. st = Structures_H.thread_state.BlockedOnReceive epptr a) \<or> (\<exists>a b c d. st = Structures_H.thread_state.BlockedOnSend epptr a b c d)) t s; \<not> (case rv of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False); valid_ep' rv s; \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)); t \<noteq> epptr\<rbrakk> \<Longrightarrow> valid_ep' (case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv) s
 2. \<And>epptr rv s. \<lbrakk>ct_idle_or_in_cur_domain' s; ct_not_inQ s; cur_tcb' s; if_live_then_nonz_cap' s; if_unsafe_then_cap' s; irqs_masked' s; pspace_domain_valid s; valid_arch_state' s; valid_global_refs' s; valid_idle' s; valid_irq_handlers' s; valid_machine_state' s; valid_pde_mappings' s; valid_pspace' s; Invariants_H.valid_queues s; valid_queues' s; sym_refs (state_refs_of' s); sch_act_wf (ksSchedulerAction s) s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; untyped_ranges_zero' s; valid_irq_node' (irq_node' s) s; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ko_at' rv epptr s; valid_irq_states' s; ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; st_tcb_at' (\<lambda>st. (\<exists>a. st = Structures_H.thread_state.BlockedOnReceive epptr a) \<or> (\<exists>a b c d. st = Structures_H.thread_state.BlockedOnSend epptr a b c d)) t s; \<not> (case rv of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False); valid_ep' rv s; \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)); t \<noteq> epptr\<rbrakk> \<Longrightarrow> ((case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv) \<noteq> Structures_H.endpoint.IdleEP \<longrightarrow> ex_nonz_cap_to' epptr s) \<and> sym_refs ((state_refs_of' s)(epptr := ep_q_refs_of' (case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv), t := {r. snd r = TCBBound \<and> r \<in> state_refs_of' s t})) proof (prove)
goal (3 subgoals):
 1. \<And>epptr s x1 x21 x22. \<lbrakk>\<forall>a b. t \<notin> set (ksReadyQueues s (a, b)); t \<noteq> epptr; ct_idle_or_in_cur_domain' s; ct_not_inQ s; cur_tcb' s; if_live_then_nonz_cap' s; if_unsafe_then_cap' s; irqs_masked' s; pspace_domain_valid s; valid_arch_state' s; valid_global_refs' s; valid_idle' s; valid_irq_handlers' s; valid_machine_state' s; valid_pde_mappings' s; valid_pspace' s; Invariants_H.valid_queues s; valid_queues' s; sym_refs (state_refs_of' s); sch_act_wf (ksSchedulerAction s) s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; untyped_ranges_zero' s; valid_irq_node' (irq_node' s) s; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ko_at' (Structures_H.endpoint.RecvEP x1) epptr s; valid_irq_states' s; ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; st_tcb_at' (\<lambda>st. (\<exists>a. st = Structures_H.thread_state.BlockedOnReceive epptr a) \<or> (\<exists>a b c d. st = Structures_H.thread_state.BlockedOnSend epptr a b c d)) t s; x1 \<noteq> []; \<forall>t\<in>set x1. tcb_at' t s; distinct x1; remove1 t x1 = x21 # x22\<rbrakk> \<Longrightarrow> tcb_at' x21 s \<and> (\<forall>t\<in>set x22. tcb_at' t s) \<and> x21 \<notin> set x22 \<and> distinct x22
 2. \<And>epptr s x3 x21 x22. \<lbrakk>\<forall>a b. t \<notin> set (ksReadyQueues s (a, b)); t \<noteq> epptr; ct_idle_or_in_cur_domain' s; ct_not_inQ s; cur_tcb' s; if_live_then_nonz_cap' s; if_unsafe_then_cap' s; irqs_masked' s; pspace_domain_valid s; valid_arch_state' s; valid_global_refs' s; valid_idle' s; valid_irq_handlers' s; valid_machine_state' s; valid_pde_mappings' s; valid_pspace' s; Invariants_H.valid_queues s; valid_queues' s; sym_refs (state_refs_of' s); sch_act_wf (ksSchedulerAction s) s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; untyped_ranges_zero' s; valid_irq_node' (irq_node' s) s; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ko_at' (Structures_H.endpoint.SendEP x3) epptr s; valid_irq_states' s; ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; st_tcb_at' (\<lambda>st. (\<exists>a. st = Structures_H.thread_state.BlockedOnReceive epptr a) \<or> (\<exists>a b c d. st = Structures_H.thread_state.BlockedOnSend epptr a b c d)) t s; x3 \<noteq> []; \<forall>t\<in>set x3. tcb_at' t s; distinct x3; remove1 t x3 = x21 # x22\<rbrakk> \<Longrightarrow> tcb_at' x21 s \<and> (\<forall>t\<in>set x22. tcb_at' t s) \<and> x21 \<notin> set x22 \<and> distinct x22
 3. \<And>epptr rv s. \<lbrakk>ct_idle_or_in_cur_domain' s; ct_not_inQ s; cur_tcb' s; if_live_then_nonz_cap' s; if_unsafe_then_cap' s; irqs_masked' s; pspace_domain_valid s; valid_arch_state' s; valid_global_refs' s; valid_idle' s; valid_irq_handlers' s; valid_machine_state' s; valid_pde_mappings' s; valid_pspace' s; Invariants_H.valid_queues s; valid_queues' s; sym_refs (state_refs_of' s); sch_act_wf (ksSchedulerAction s) s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; untyped_ranges_zero' s; valid_irq_node' (irq_node' s) s; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ko_at' rv epptr s; valid_irq_states' s; ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; st_tcb_at' (\<lambda>st. (\<exists>a. st = Structures_H.thread_state.BlockedOnReceive epptr a) \<or> (\<exists>a b c d. st = Structures_H.thread_state.BlockedOnSend epptr a b c d)) t s; \<not> (case rv of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False); valid_ep' rv s; \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)); t \<noteq> epptr\<rbrakk> \<Longrightarrow> ((case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv) \<noteq> Structures_H.endpoint.IdleEP \<longrightarrow> ex_nonz_cap_to' epptr s) \<and> sym_refs ((state_refs_of' s)(epptr := ep_q_refs_of' (case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv), t := {r. snd r = TCBBound \<and> r \<in> state_refs_of' s t})) proof (prove)
goal (3 subgoals):
 1. \<And>epptr s list x xs. \<lbrakk>\<forall>a b. t \<notin> set (ksReadyQueues s (a, b)); t \<noteq> epptr; ct_idle_or_in_cur_domain' s; ct_not_inQ s; cur_tcb' s; if_live_then_nonz_cap' s; if_unsafe_then_cap' s; irqs_masked' s; pspace_domain_valid s; valid_arch_state' s; valid_global_refs' s; valid_idle' s; valid_irq_handlers' s; valid_machine_state' s; valid_pde_mappings' s; valid_pspace' s; Invariants_H.valid_queues s; valid_queues' s; sym_refs (state_refs_of' s); sch_act_wf (ksSchedulerAction s) s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; untyped_ranges_zero' s; valid_irq_node' (irq_node' s) s; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ko_at' (Structures_H.endpoint.RecvEP list) epptr s; valid_irq_states' s; ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; st_tcb_at' (\<lambda>st. (\<exists>a. st = Structures_H.thread_state.BlockedOnReceive epptr a) \<or> (\<exists>a b c d. st = Structures_H.thread_state.BlockedOnSend epptr a b c d)) t s; list \<noteq> []; \<forall>t\<in>set list. tcb_at' t s; distinct list; remove1 t list = x # xs\<rbrakk> \<Longrightarrow> tcb_at' x s \<and> (\<forall>t\<in>set xs. tcb_at' t s) \<and> x \<notin> set xs \<and> distinct xs
 2. \<And>epptr s x3 x21 x22. \<lbrakk>\<forall>a b. t \<notin> set (ksReadyQueues s (a, b)); t \<noteq> epptr; ct_idle_or_in_cur_domain' s; ct_not_inQ s; cur_tcb' s; if_live_then_nonz_cap' s; if_unsafe_then_cap' s; irqs_masked' s; pspace_domain_valid s; valid_arch_state' s; valid_global_refs' s; valid_idle' s; valid_irq_handlers' s; valid_machine_state' s; valid_pde_mappings' s; valid_pspace' s; Invariants_H.valid_queues s; valid_queues' s; sym_refs (state_refs_of' s); sch_act_wf (ksSchedulerAction s) s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; untyped_ranges_zero' s; valid_irq_node' (irq_node' s) s; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ko_at' (Structures_H.endpoint.SendEP x3) epptr s; valid_irq_states' s; ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; st_tcb_at' (\<lambda>st. (\<exists>a. st = Structures_H.thread_state.BlockedOnReceive epptr a) \<or> (\<exists>a b c d. st = Structures_H.thread_state.BlockedOnSend epptr a b c d)) t s; x3 \<noteq> []; \<forall>t\<in>set x3. tcb_at' t s; distinct x3; remove1 t x3 = x21 # x22\<rbrakk> \<Longrightarrow> tcb_at' x21 s \<and> (\<forall>t\<in>set x22. tcb_at' t s) \<and> x21 \<notin> set x22 \<and> distinct x22
 3. \<And>epptr rv s. \<lbrakk>ct_idle_or_in_cur_domain' s; ct_not_inQ s; cur_tcb' s; if_live_then_nonz_cap' s; if_unsafe_then_cap' s; irqs_masked' s; pspace_domain_valid s; valid_arch_state' s; valid_global_refs' s; valid_idle' s; valid_irq_handlers' s; valid_machine_state' s; valid_pde_mappings' s; valid_pspace' s; Invariants_H.valid_queues s; valid_queues' s; sym_refs (state_refs_of' s); sch_act_wf (ksSchedulerAction s) s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; untyped_ranges_zero' s; valid_irq_node' (irq_node' s) s; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ko_at' rv epptr s; valid_irq_states' s; ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; st_tcb_at' (\<lambda>st. (\<exists>a. st = Structures_H.thread_state.BlockedOnReceive epptr a) \<or> (\<exists>a b c d. st = Structures_H.thread_state.BlockedOnSend epptr a b c d)) t s; \<not> (case rv of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False); valid_ep' rv s; \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)); t \<noteq> epptr\<rbrakk> \<Longrightarrow> ((case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv) \<noteq> Structures_H.endpoint.IdleEP \<longrightarrow> ex_nonz_cap_to' epptr s) \<and> sym_refs ((state_refs_of' s)(epptr := ep_q_refs_of' (case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv), t := {r. snd r = TCBBound \<and> r \<in> state_refs_of' s t})) proof (prove)
goal (3 subgoals):
 1. \<And>epptr s list x xs. \<lbrakk>\<forall>a b. t \<notin> set (ksReadyQueues s (a, b)); t \<noteq> epptr; ct_idle_or_in_cur_domain' s; ct_not_inQ s; cur_tcb' s; if_live_then_nonz_cap' s; if_unsafe_then_cap' s; irqs_masked' s; pspace_domain_valid s; valid_arch_state' s; valid_global_refs' s; valid_idle' s; valid_irq_handlers' s; valid_machine_state' s; valid_pde_mappings' s; valid_pspace' s; Invariants_H.valid_queues s; valid_queues' s; sym_refs (state_refs_of' s); sch_act_wf (ksSchedulerAction s) s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; untyped_ranges_zero' s; valid_irq_node' (irq_node' s) s; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ko_at' (Structures_H.endpoint.RecvEP list) epptr s; valid_irq_states' s; ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; st_tcb_at' (\<lambda>st. (\<exists>a. st = Structures_H.thread_state.BlockedOnReceive epptr a) \<or> (\<exists>a b c d. st = Structures_H.thread_state.BlockedOnSend epptr a b c d)) t s; list \<noteq> []; \<forall>t\<in>set list. tcb_at' t s; distinct list; remove1 t list = x # xs; distinct (remove1 t list)\<rbrakk> \<Longrightarrow> tcb_at' x s \<and> (\<forall>t\<in>set xs. tcb_at' t s) \<and> x \<notin> set xs \<and> distinct xs
 2. \<And>epptr s x3 x21 x22. \<lbrakk>\<forall>a b. t \<notin> set (ksReadyQueues s (a, b)); t \<noteq> epptr; ct_idle_or_in_cur_domain' s; ct_not_inQ s; cur_tcb' s; if_live_then_nonz_cap' s; if_unsafe_then_cap' s; irqs_masked' s; pspace_domain_valid s; valid_arch_state' s; valid_global_refs' s; valid_idle' s; valid_irq_handlers' s; valid_machine_state' s; valid_pde_mappings' s; valid_pspace' s; Invariants_H.valid_queues s; valid_queues' s; sym_refs (state_refs_of' s); sch_act_wf (ksSchedulerAction s) s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; untyped_ranges_zero' s; valid_irq_node' (irq_node' s) s; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ko_at' (Structures_H.endpoint.SendEP x3) epptr s; valid_irq_states' s; ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; st_tcb_at' (\<lambda>st. (\<exists>a. st = Structures_H.thread_state.BlockedOnReceive epptr a) \<or> (\<exists>a b c d. st = Structures_H.thread_state.BlockedOnSend epptr a b c d)) t s; x3 \<noteq> []; \<forall>t\<in>set x3. tcb_at' t s; distinct x3; remove1 t x3 = x21 # x22\<rbrakk> \<Longrightarrow> tcb_at' x21 s \<and> (\<forall>t\<in>set x22. tcb_at' t s) \<and> x21 \<notin> set x22 \<and> distinct x22
 3. \<And>epptr rv s. \<lbrakk>ct_idle_or_in_cur_domain' s; ct_not_inQ s; cur_tcb' s; if_live_then_nonz_cap' s; if_unsafe_then_cap' s; irqs_masked' s; pspace_domain_valid s; valid_arch_state' s; valid_global_refs' s; valid_idle' s; valid_irq_handlers' s; valid_machine_state' s; valid_pde_mappings' s; valid_pspace' s; Invariants_H.valid_queues s; valid_queues' s; sym_refs (state_refs_of' s); sch_act_wf (ksSchedulerAction s) s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; untyped_ranges_zero' s; valid_irq_node' (irq_node' s) s; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ko_at' rv epptr s; valid_irq_states' s; ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; st_tcb_at' (\<lambda>st. (\<exists>a. st = Structures_H.thread_state.BlockedOnReceive epptr a) \<or> (\<exists>a b c d. st = Structures_H.thread_state.BlockedOnSend epptr a b c d)) t s; \<not> (case rv of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False); valid_ep' rv s; \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)); t \<noteq> epptr\<rbrakk> \<Longrightarrow> ((case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv) \<noteq> Structures_H.endpoint.IdleEP \<longrightarrow> ex_nonz_cap_to' epptr s) \<and> sym_refs ((state_refs_of' s)(epptr := ep_q_refs_of' (case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv), t := {r. snd r = TCBBound \<and> r \<in> state_refs_of' s t})) proof (prove)
goal (3 subgoals):
 1. \<And>epptr s list x xs. \<lbrakk>\<forall>a b. t \<notin> set (ksReadyQueues s (a, b)); t \<noteq> epptr; ct_idle_or_in_cur_domain' s; ct_not_inQ s; cur_tcb' s; if_live_then_nonz_cap' s; if_unsafe_then_cap' s; irqs_masked' s; pspace_domain_valid s; valid_arch_state' s; valid_global_refs' s; valid_idle' s; valid_irq_handlers' s; valid_machine_state' s; valid_pde_mappings' s; valid_pspace' s; Invariants_H.valid_queues s; valid_queues' s; sym_refs (state_refs_of' s); sch_act_wf (ksSchedulerAction s) s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; untyped_ranges_zero' s; valid_irq_node' (irq_node' s) s; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ko_at' (Structures_H.endpoint.RecvEP list) epptr s; valid_irq_states' s; ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; st_tcb_at' (\<lambda>st. (\<exists>a. st = Structures_H.thread_state.BlockedOnReceive epptr a) \<or> (\<exists>a b c d. st = Structures_H.thread_state.BlockedOnSend epptr a b c d)) t s; list \<noteq> []; \<forall>t\<in>set list. tcb_at' t s; distinct list; remove1 t list = x # xs; distinct (remove1 t list); set (remove1 t list) \<subseteq> set list\<rbrakk> \<Longrightarrow> tcb_at' x s \<and> (\<forall>t\<in>set xs. tcb_at' t s) \<and> x \<notin> set xs \<and> distinct xs
 2. \<And>epptr s x3 x21 x22. \<lbrakk>\<forall>a b. t \<notin> set (ksReadyQueues s (a, b)); t \<noteq> epptr; ct_idle_or_in_cur_domain' s; ct_not_inQ s; cur_tcb' s; if_live_then_nonz_cap' s; if_unsafe_then_cap' s; irqs_masked' s; pspace_domain_valid s; valid_arch_state' s; valid_global_refs' s; valid_idle' s; valid_irq_handlers' s; valid_machine_state' s; valid_pde_mappings' s; valid_pspace' s; Invariants_H.valid_queues s; valid_queues' s; sym_refs (state_refs_of' s); sch_act_wf (ksSchedulerAction s) s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; untyped_ranges_zero' s; valid_irq_node' (irq_node' s) s; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ko_at' (Structures_H.endpoint.SendEP x3) epptr s; valid_irq_states' s; ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; st_tcb_at' (\<lambda>st. (\<exists>a. st = Structures_H.thread_state.BlockedOnReceive epptr a) \<or> (\<exists>a b c d. st = Structures_H.thread_state.BlockedOnSend epptr a b c d)) t s; x3 \<noteq> []; \<forall>t\<in>set x3. tcb_at' t s; distinct x3; remove1 t x3 = x21 # x22\<rbrakk> \<Longrightarrow> tcb_at' x21 s \<and> (\<forall>t\<in>set x22. tcb_at' t s) \<and> x21 \<notin> set x22 \<and> distinct x22
 3. \<And>epptr rv s. \<lbrakk>ct_idle_or_in_cur_domain' s; ct_not_inQ s; cur_tcb' s; if_live_then_nonz_cap' s; if_unsafe_then_cap' s; irqs_masked' s; pspace_domain_valid s; valid_arch_state' s; valid_global_refs' s; valid_idle' s; valid_irq_handlers' s; valid_machine_state' s; valid_pde_mappings' s; valid_pspace' s; Invariants_H.valid_queues s; valid_queues' s; sym_refs (state_refs_of' s); sch_act_wf (ksSchedulerAction s) s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; untyped_ranges_zero' s; valid_irq_node' (irq_node' s) s; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ko_at' rv epptr s; valid_irq_states' s; ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; st_tcb_at' (\<lambda>st. (\<exists>a. st = Structures_H.thread_state.BlockedOnReceive epptr a) \<or> (\<exists>a b c d. st = Structures_H.thread_state.BlockedOnSend epptr a b c d)) t s; \<not> (case rv of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False); valid_ep' rv s; \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)); t \<noteq> epptr\<rbrakk> \<Longrightarrow> ((case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv) \<noteq> Structures_H.endpoint.IdleEP \<longrightarrow> ex_nonz_cap_to' epptr s) \<and> sym_refs ((state_refs_of' s)(epptr := ep_q_refs_of' (case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv), t := {r. snd r = TCBBound \<and> r \<in> state_refs_of' s t})) proof (prove)
goal (2 subgoals):
 1. \<And>epptr s x3 x21 x22. \<lbrakk>\<forall>a b. t \<notin> set (ksReadyQueues s (a, b)); t \<noteq> epptr; ct_idle_or_in_cur_domain' s; ct_not_inQ s; cur_tcb' s; if_live_then_nonz_cap' s; if_unsafe_then_cap' s; irqs_masked' s; pspace_domain_valid s; valid_arch_state' s; valid_global_refs' s; valid_idle' s; valid_irq_handlers' s; valid_machine_state' s; valid_pde_mappings' s; valid_pspace' s; Invariants_H.valid_queues s; valid_queues' s; sym_refs (state_refs_of' s); sch_act_wf (ksSchedulerAction s) s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; untyped_ranges_zero' s; valid_irq_node' (irq_node' s) s; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ko_at' (Structures_H.endpoint.SendEP x3) epptr s; valid_irq_states' s; ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; st_tcb_at' (\<lambda>st. (\<exists>a. st = Structures_H.thread_state.BlockedOnReceive epptr a) \<or> (\<exists>a b c d. st = Structures_H.thread_state.BlockedOnSend epptr a b c d)) t s; x3 \<noteq> []; \<forall>t\<in>set x3. tcb_at' t s; distinct x3; remove1 t x3 = x21 # x22\<rbrakk> \<Longrightarrow> tcb_at' x21 s \<and> (\<forall>t\<in>set x22. tcb_at' t s) \<and> x21 \<notin> set x22 \<and> distinct x22
 2. \<And>epptr rv s. \<lbrakk>ct_idle_or_in_cur_domain' s; ct_not_inQ s; cur_tcb' s; if_live_then_nonz_cap' s; if_unsafe_then_cap' s; irqs_masked' s; pspace_domain_valid s; valid_arch_state' s; valid_global_refs' s; valid_idle' s; valid_irq_handlers' s; valid_machine_state' s; valid_pde_mappings' s; valid_pspace' s; Invariants_H.valid_queues s; valid_queues' s; sym_refs (state_refs_of' s); sch_act_wf (ksSchedulerAction s) s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; untyped_ranges_zero' s; valid_irq_node' (irq_node' s) s; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ko_at' rv epptr s; valid_irq_states' s; ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; st_tcb_at' (\<lambda>st. (\<exists>a. st = Structures_H.thread_state.BlockedOnReceive epptr a) \<or> (\<exists>a b c d. st = Structures_H.thread_state.BlockedOnSend epptr a b c d)) t s; \<not> (case rv of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False); valid_ep' rv s; \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)); t \<noteq> epptr\<rbrakk> \<Longrightarrow> ((case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv) \<noteq> Structures_H.endpoint.IdleEP \<longrightarrow> ex_nonz_cap_to' epptr s) \<and> sym_refs ((state_refs_of' s)(epptr := ep_q_refs_of' (case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv), t := {r. snd r = TCBBound \<and> r \<in> state_refs_of' s t})) proof (prove)
goal (2 subgoals):
 1. \<And>epptr s list x xs. \<lbrakk>\<forall>a b. t \<notin> set (ksReadyQueues s (a, b)); t \<noteq> epptr; ct_idle_or_in_cur_domain' s; ct_not_inQ s; cur_tcb' s; if_live_then_nonz_cap' s; if_unsafe_then_cap' s; irqs_masked' s; pspace_domain_valid s; valid_arch_state' s; valid_global_refs' s; valid_idle' s; valid_irq_handlers' s; valid_machine_state' s; valid_pde_mappings' s; valid_pspace' s; Invariants_H.valid_queues s; valid_queues' s; sym_refs (state_refs_of' s); sch_act_wf (ksSchedulerAction s) s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; untyped_ranges_zero' s; valid_irq_node' (irq_node' s) s; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ko_at' (Structures_H.endpoint.SendEP list) epptr s; valid_irq_states' s; ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; st_tcb_at' (\<lambda>st. (\<exists>a. st = Structures_H.thread_state.BlockedOnReceive epptr a) \<or> (\<exists>a b c d. st = Structures_H.thread_state.BlockedOnSend epptr a b c d)) t s; list \<noteq> []; \<forall>t\<in>set list. tcb_at' t s; distinct list; remove1 t list = x # xs\<rbrakk> \<Longrightarrow> tcb_at' x s \<and> (\<forall>t\<in>set xs. tcb_at' t s) \<and> x \<notin> set xs \<and> distinct xs
 2. \<And>epptr rv s. \<lbrakk>ct_idle_or_in_cur_domain' s; ct_not_inQ s; cur_tcb' s; if_live_then_nonz_cap' s; if_unsafe_then_cap' s; irqs_masked' s; pspace_domain_valid s; valid_arch_state' s; valid_global_refs' s; valid_idle' s; valid_irq_handlers' s; valid_machine_state' s; valid_pde_mappings' s; valid_pspace' s; Invariants_H.valid_queues s; valid_queues' s; sym_refs (state_refs_of' s); sch_act_wf (ksSchedulerAction s) s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; untyped_ranges_zero' s; valid_irq_node' (irq_node' s) s; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ko_at' rv epptr s; valid_irq_states' s; ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; st_tcb_at' (\<lambda>st. (\<exists>a. st = Structures_H.thread_state.BlockedOnReceive epptr a) \<or> (\<exists>a b c d. st = Structures_H.thread_state.BlockedOnSend epptr a b c d)) t s; \<not> (case rv of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False); valid_ep' rv s; \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)); t \<noteq> epptr\<rbrakk> \<Longrightarrow> ((case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv) \<noteq> Structures_H.endpoint.IdleEP \<longrightarrow> ex_nonz_cap_to' epptr s) \<and> sym_refs ((state_refs_of' s)(epptr := ep_q_refs_of' (case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv), t := {r. snd r = TCBBound \<and> r \<in> state_refs_of' s t})) proof (prove)
goal (2 subgoals):
 1. \<And>epptr s list x xs. \<lbrakk>\<forall>a b. t \<notin> set (ksReadyQueues s (a, b)); t \<noteq> epptr; ct_idle_or_in_cur_domain' s; ct_not_inQ s; cur_tcb' s; if_live_then_nonz_cap' s; if_unsafe_then_cap' s; irqs_masked' s; pspace_domain_valid s; valid_arch_state' s; valid_global_refs' s; valid_idle' s; valid_irq_handlers' s; valid_machine_state' s; valid_pde_mappings' s; valid_pspace' s; Invariants_H.valid_queues s; valid_queues' s; sym_refs (state_refs_of' s); sch_act_wf (ksSchedulerAction s) s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; untyped_ranges_zero' s; valid_irq_node' (irq_node' s) s; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ko_at' (Structures_H.endpoint.SendEP list) epptr s; valid_irq_states' s; ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; st_tcb_at' (\<lambda>st. (\<exists>a. st = Structures_H.thread_state.BlockedOnReceive epptr a) \<or> (\<exists>a b c d. st = Structures_H.thread_state.BlockedOnSend epptr a b c d)) t s; list \<noteq> []; \<forall>t\<in>set list. tcb_at' t s; distinct list; remove1 t list = x # xs; distinct (remove1 t list)\<rbrakk> \<Longrightarrow> tcb_at' x s \<and> (\<forall>t\<in>set xs. tcb_at' t s) \<and> x \<notin> set xs \<and> distinct xs
 2. \<And>epptr rv s. \<lbrakk>ct_idle_or_in_cur_domain' s; ct_not_inQ s; cur_tcb' s; if_live_then_nonz_cap' s; if_unsafe_then_cap' s; irqs_masked' s; pspace_domain_valid s; valid_arch_state' s; valid_global_refs' s; valid_idle' s; valid_irq_handlers' s; valid_machine_state' s; valid_pde_mappings' s; valid_pspace' s; Invariants_H.valid_queues s; valid_queues' s; sym_refs (state_refs_of' s); sch_act_wf (ksSchedulerAction s) s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; untyped_ranges_zero' s; valid_irq_node' (irq_node' s) s; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ko_at' rv epptr s; valid_irq_states' s; ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; st_tcb_at' (\<lambda>st. (\<exists>a. st = Structures_H.thread_state.BlockedOnReceive epptr a) \<or> (\<exists>a b c d. st = Structures_H.thread_state.BlockedOnSend epptr a b c d)) t s; \<not> (case rv of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False); valid_ep' rv s; \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)); t \<noteq> epptr\<rbrakk> \<Longrightarrow> ((case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv) \<noteq> Structures_H.endpoint.IdleEP \<longrightarrow> ex_nonz_cap_to' epptr s) \<and> sym_refs ((state_refs_of' s)(epptr := ep_q_refs_of' (case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv), t := {r. snd r = TCBBound \<and> r \<in> state_refs_of' s t})) proof (prove)
goal (2 subgoals):
 1. \<And>epptr s list x xs. \<lbrakk>\<forall>a b. t \<notin> set (ksReadyQueues s (a, b)); t \<noteq> epptr; ct_idle_or_in_cur_domain' s; ct_not_inQ s; cur_tcb' s; if_live_then_nonz_cap' s; if_unsafe_then_cap' s; irqs_masked' s; pspace_domain_valid s; valid_arch_state' s; valid_global_refs' s; valid_idle' s; valid_irq_handlers' s; valid_machine_state' s; valid_pde_mappings' s; valid_pspace' s; Invariants_H.valid_queues s; valid_queues' s; sym_refs (state_refs_of' s); sch_act_wf (ksSchedulerAction s) s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; untyped_ranges_zero' s; valid_irq_node' (irq_node' s) s; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ko_at' (Structures_H.endpoint.SendEP list) epptr s; valid_irq_states' s; ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; st_tcb_at' (\<lambda>st. (\<exists>a. st = Structures_H.thread_state.BlockedOnReceive epptr a) \<or> (\<exists>a b c d. st = Structures_H.thread_state.BlockedOnSend epptr a b c d)) t s; list \<noteq> []; \<forall>t\<in>set list. tcb_at' t s; distinct list; remove1 t list = x # xs; distinct (remove1 t list); set (remove1 t list) \<subseteq> set list\<rbrakk> \<Longrightarrow> tcb_at' x s \<and> (\<forall>t\<in>set xs. tcb_at' t s) \<and> x \<notin> set xs \<and> distinct xs
 2. \<And>epptr rv s. \<lbrakk>ct_idle_or_in_cur_domain' s; ct_not_inQ s; cur_tcb' s; if_live_then_nonz_cap' s; if_unsafe_then_cap' s; irqs_masked' s; pspace_domain_valid s; valid_arch_state' s; valid_global_refs' s; valid_idle' s; valid_irq_handlers' s; valid_machine_state' s; valid_pde_mappings' s; valid_pspace' s; Invariants_H.valid_queues s; valid_queues' s; sym_refs (state_refs_of' s); sch_act_wf (ksSchedulerAction s) s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; untyped_ranges_zero' s; valid_irq_node' (irq_node' s) s; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ko_at' rv epptr s; valid_irq_states' s; ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; st_tcb_at' (\<lambda>st. (\<exists>a. st = Structures_H.thread_state.BlockedOnReceive epptr a) \<or> (\<exists>a b c d. st = Structures_H.thread_state.BlockedOnSend epptr a b c d)) t s; \<not> (case rv of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False); valid_ep' rv s; \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)); t \<noteq> epptr\<rbrakk> \<Longrightarrow> ((case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv) \<noteq> Structures_H.endpoint.IdleEP \<longrightarrow> ex_nonz_cap_to' epptr s) \<and> sym_refs ((state_refs_of' s)(epptr := ep_q_refs_of' (case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv), t := {r. snd r = TCBBound \<and> r \<in> state_refs_of' s t})) proof (prove)
goal (1 subgoal):
 1. \<And>epptr rv s. \<lbrakk>ct_idle_or_in_cur_domain' s; ct_not_inQ s; cur_tcb' s; if_live_then_nonz_cap' s; if_unsafe_then_cap' s; irqs_masked' s; pspace_domain_valid s; valid_arch_state' s; valid_global_refs' s; valid_idle' s; valid_irq_handlers' s; valid_machine_state' s; valid_pde_mappings' s; valid_pspace' s; Invariants_H.valid_queues s; valid_queues' s; sym_refs (state_refs_of' s); sch_act_wf (ksSchedulerAction s) s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; untyped_ranges_zero' s; valid_irq_node' (irq_node' s) s; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ko_at' rv epptr s; valid_irq_states' s; ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; st_tcb_at' (\<lambda>st. (\<exists>a. st = Structures_H.thread_state.BlockedOnReceive epptr a) \<or> (\<exists>a b c d. st = Structures_H.thread_state.BlockedOnSend epptr a b c d)) t s; \<not> (case rv of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False); valid_ep' rv s; \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)); t \<noteq> epptr\<rbrakk> \<Longrightarrow> ((case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv) \<noteq> Structures_H.endpoint.IdleEP \<longrightarrow> ex_nonz_cap_to' epptr s) \<and> sym_refs ((state_refs_of' s)(epptr := ep_q_refs_of' (case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv), t := {r. snd r = TCBBound \<and> r \<in> state_refs_of' s t})) proof (prove)
goal (1 subgoal):
 1. \<And>epptr rv s. \<lbrakk>ct_idle_or_in_cur_domain' s; ct_not_inQ s; cur_tcb' s; if_live_then_nonz_cap' s; if_unsafe_then_cap' s; irqs_masked' s; pspace_domain_valid s; valid_arch_state' s; valid_global_refs' s; valid_idle' s; valid_irq_handlers' s; valid_machine_state' s; valid_pde_mappings' s; valid_pspace' s; Invariants_H.valid_queues s; valid_queues' s; sym_refs (state_refs_of' s); sch_act_wf (ksSchedulerAction s) s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; untyped_ranges_zero' s; valid_irq_node' (irq_node' s) s; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ko_at' rv epptr s; valid_irq_states' s; ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; st_tcb_at' (\<lambda>st. (\<exists>a. st = Structures_H.thread_state.BlockedOnReceive epptr a) \<or> (\<exists>a b c d. st = Structures_H.thread_state.BlockedOnSend epptr a b c d)) t s; \<not> (case rv of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False); valid_ep' rv s; \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)); t \<noteq> epptr; state_refs_of' s epptr = refs_of' (injectKO rv) \<and> (\<forall>(x, tp)\<in>refs_of' (injectKO rv). ko_wp_at' (\<lambda>ko. (epptr, symreftype tp) \<in> refs_of' ko) x s)\<rbrakk> \<Longrightarrow> ((case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv) \<noteq> Structures_H.endpoint.IdleEP \<longrightarrow> ex_nonz_cap_to' epptr s) \<and> sym_refs ((state_refs_of' s)(epptr := ep_q_refs_of' (case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv), t := {r. snd r = TCBBound \<and> r \<in> state_refs_of' s t})) proof (prove)
goal (2 subgoals):
 1. \<And>epptr rv s. \<lbrakk>ct_idle_or_in_cur_domain' s; ct_not_inQ s; cur_tcb' s; if_live_then_nonz_cap' s; if_unsafe_then_cap' s; irqs_masked' s; pspace_domain_valid s; valid_arch_state' s; valid_global_refs' s; valid_idle' s; valid_irq_handlers' s; valid_machine_state' s; valid_pde_mappings' s; valid_pspace' s; Invariants_H.valid_queues s; valid_queues' s; sym_refs (state_refs_of' s); sch_act_wf (ksSchedulerAction s) s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; untyped_ranges_zero' s; valid_irq_node' (irq_node' s) s; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ko_at' rv epptr s; valid_irq_states' s; ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; st_tcb_at' (\<lambda>st. (\<exists>a. st = Structures_H.thread_state.BlockedOnReceive epptr a) \<or> (\<exists>a b c d. st = Structures_H.thread_state.BlockedOnSend epptr a b c d)) t s; \<not> (case rv of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False); valid_ep' rv s; \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)); t \<noteq> epptr; state_refs_of' s epptr = refs_of' (injectKO rv) \<and> (\<forall>(x, tp)\<in>refs_of' (injectKO rv). ko_wp_at' (\<lambda>ko. (epptr, symreftype tp) \<in> refs_of' ko) x s)\<rbrakk> \<Longrightarrow> (case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv) \<noteq> Structures_H.endpoint.IdleEP \<longrightarrow> ex_nonz_cap_to' epptr s
 2. \<And>epptr rv s. \<lbrakk>ct_idle_or_in_cur_domain' s; ct_not_inQ s; cur_tcb' s; if_live_then_nonz_cap' s; if_unsafe_then_cap' s; irqs_masked' s; pspace_domain_valid s; valid_arch_state' s; valid_global_refs' s; valid_idle' s; valid_irq_handlers' s; valid_machine_state' s; valid_pde_mappings' s; valid_pspace' s; Invariants_H.valid_queues s; valid_queues' s; sym_refs (state_refs_of' s); sch_act_wf (ksSchedulerAction s) s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; untyped_ranges_zero' s; valid_irq_node' (irq_node' s) s; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ko_at' rv epptr s; valid_irq_states' s; ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; st_tcb_at' (\<lambda>st. (\<exists>a. st = Structures_H.thread_state.BlockedOnReceive epptr a) \<or> (\<exists>a b c d. st = Structures_H.thread_state.BlockedOnSend epptr a b c d)) t s; \<not> (case rv of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False); valid_ep' rv s; \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)); t \<noteq> epptr; state_refs_of' s epptr = refs_of' (injectKO rv) \<and> (\<forall>(x, tp)\<in>refs_of' (injectKO rv). ko_wp_at' (\<lambda>ko. (epptr, symreftype tp) \<in> refs_of' ko) x s)\<rbrakk> \<Longrightarrow> sym_refs ((state_refs_of' s)(epptr := ep_q_refs_of' (case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv), t := {r. snd r = TCBBound \<and> r \<in> state_refs_of' s t})) proof (prove)
goal (1 subgoal):
 1. \<And>epptr rv s. \<lbrakk>ct_idle_or_in_cur_domain' s; ct_not_inQ s; cur_tcb' s; if_live_then_nonz_cap' s; if_unsafe_then_cap' s; irqs_masked' s; pspace_domain_valid s; valid_arch_state' s; valid_global_refs' s; valid_idle' s; valid_irq_handlers' s; valid_machine_state' s; valid_pde_mappings' s; valid_pspace' s; Invariants_H.valid_queues s; valid_queues' s; sym_refs (state_refs_of' s); sch_act_wf (ksSchedulerAction s) s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; untyped_ranges_zero' s; valid_irq_node' (irq_node' s) s; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ko_at' rv epptr s; valid_irq_states' s; ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; st_tcb_at' (\<lambda>st. (\<exists>a. st = Structures_H.thread_state.BlockedOnReceive epptr a) \<or> (\<exists>a b c d. st = Structures_H.thread_state.BlockedOnSend epptr a b c d)) t s; \<not> (case rv of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False); valid_ep' rv s; \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)); t \<noteq> epptr; state_refs_of' s epptr = refs_of' (injectKO rv) \<and> (\<forall>(x, tp)\<in>refs_of' (injectKO rv). ko_wp_at' (\<lambda>ko. (epptr, symreftype tp) \<in> refs_of' ko) x s)\<rbrakk> \<Longrightarrow> sym_refs ((state_refs_of' s)(epptr := ep_q_refs_of' (case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv), t := {r. snd r = TCBBound \<and> r \<in> state_refs_of' s t})) proof (prove)
goal (1 subgoal):
 1. \<And>epptr rv s. \<lbrakk>ct_idle_or_in_cur_domain' s; ct_not_inQ s; cur_tcb' s; if_live_then_nonz_cap' s; if_unsafe_then_cap' s; irqs_masked' s; pspace_domain_valid s; valid_arch_state' s; valid_global_refs' s; valid_idle' s; valid_irq_handlers' s; valid_machine_state' s; valid_pde_mappings' s; valid_pspace' s; Invariants_H.valid_queues s; valid_queues' s; sym_refs (state_refs_of' s); sch_act_wf (ksSchedulerAction s) s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; untyped_ranges_zero' s; valid_irq_node' (irq_node' s) s; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ko_at' rv epptr s; valid_irq_states' s; ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; \<not> (case rv of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False); valid_ep' rv s; \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)); t \<noteq> epptr; state_refs_of' s epptr = refs_of' (injectKO rv) \<and> (\<forall>(x, tp)\<in>refs_of' (injectKO rv). ko_wp_at' (\<lambda>ko. (epptr, symreftype tp) \<in> refs_of' ko) x s); \<exists>ts ntfnptr. ((\<exists>a. ts = Structures_H.thread_state.BlockedOnReceive epptr a) \<or> (\<exists>a b c d. ts = Structures_H.thread_state.BlockedOnSend epptr a b c d)) \<and> obj_at' (tcb_ntfn_is_bound' ntfnptr) t s \<and> state_refs_of' s t = tcb_st_refs_of' ts \<union> tcb_bound_refs' ntfnptr\<rbrakk> \<Longrightarrow> sym_refs ((state_refs_of' s)(epptr := ep_q_refs_of' (case remove1 t (epQueue rv) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> epQueue_update (\<lambda>_. remove1 t (epQueue rv)) rv), t := {r. snd r = TCBBound \<and> r \<in> state_refs_of' s t})) proof (prove)
goal (2 subgoals):
 1. \<And>epptr s x1 ts ntfnptr. \<lbrakk>\<forall>a b. t \<notin> set (ksReadyQueues s (a, b)); t \<noteq> epptr; ct_idle_or_in_cur_domain' s; ct_not_inQ s; cur_tcb' s; if_live_then_nonz_cap' s; if_unsafe_then_cap' s; irqs_masked' s; pspace_domain_valid s; valid_arch_state' s; valid_global_refs' s; valid_idle' s; valid_irq_handlers' s; valid_machine_state' s; valid_pde_mappings' s; valid_pspace' s; Invariants_H.valid_queues s; valid_queues' s; sym_refs (state_refs_of' s); sch_act_wf (ksSchedulerAction s) s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; untyped_ranges_zero' s; valid_irq_node' (irq_node' s) s; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ko_at' (Structures_H.endpoint.RecvEP x1) epptr s; valid_irq_states' s; ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; state_refs_of' s epptr = set x1 \<times> {EPRecv}; \<forall>x\<in>set x1. ko_wp_at' (\<lambda>ko. (epptr, TCBBlockedRecv) \<in> refs_of' ko) x s; (\<exists>a. ts = Structures_H.thread_state.BlockedOnReceive epptr a) \<or> (\<exists>a b c d. ts = Structures_H.thread_state.BlockedOnSend epptr a b c d); obj_at' (tcb_ntfn_is_bound' ntfnptr) t s; state_refs_of' s t = tcb_st_refs_of' ts \<union> tcb_bound_refs' ntfnptr; x1 \<noteq> []; \<forall>t\<in>set x1. tcb_at' t s; distinct x1\<rbrakk> \<Longrightarrow> sym_refs ((state_refs_of' s)(epptr := (set x1 - {t}) \<times> {EPRecv}, t := {r. snd r = TCBBound \<and> (r \<in> tcb_st_refs_of' ts \<or> r \<in> tcb_bound_refs' ntfnptr)}))
 2. \<And>epptr s x3 ts ntfnptr. \<lbrakk>\<forall>a b. t \<notin> set (ksReadyQueues s (a, b)); t \<noteq> epptr; ct_idle_or_in_cur_domain' s; ct_not_inQ s; cur_tcb' s; if_live_then_nonz_cap' s; if_unsafe_then_cap' s; irqs_masked' s; pspace_domain_valid s; valid_arch_state' s; valid_global_refs' s; valid_idle' s; valid_irq_handlers' s; valid_machine_state' s; valid_pde_mappings' s; valid_pspace' s; Invariants_H.valid_queues s; valid_queues' s; sym_refs (state_refs_of' s); sch_act_wf (ksSchedulerAction s) s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; untyped_ranges_zero' s; valid_irq_node' (irq_node' s) s; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ko_at' (Structures_H.endpoint.SendEP x3) epptr s; valid_irq_states' s; ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; state_refs_of' s epptr = set x3 \<times> {EPSend}; \<forall>x\<in>set x3. ko_wp_at' (\<lambda>ko. (epptr, TCBBlockedSend) \<in> refs_of' ko) x s; (\<exists>a. ts = Structures_H.thread_state.BlockedOnReceive epptr a) \<or> (\<exists>a b c d. ts = Structures_H.thread_state.BlockedOnSend epptr a b c d); obj_at' (tcb_ntfn_is_bound' ntfnptr) t s; state_refs_of' s t = tcb_st_refs_of' ts \<union> tcb_bound_refs' ntfnptr; x3 \<noteq> []; \<forall>t\<in>set x3. tcb_at' t s; distinct x3\<rbrakk> \<Longrightarrow> sym_refs ((state_refs_of' s)(epptr := (set x3 - {t}) \<times> {EPSend}, t := {r. snd r = TCBBound \<and> (r \<in> tcb_st_refs_of' ts \<or> r \<in> tcb_bound_refs' ntfnptr)})) proof (prove)
goal (2 subgoals):
 1. \<And>epptr s x1 ts ntfnptr. \<lbrakk>\<forall>a b. t \<notin> set (ksReadyQueues s (a, b)); t \<noteq> epptr; ct_idle_or_in_cur_domain' s; ct_not_inQ s; cur_tcb' s; if_live_then_nonz_cap' s; if_unsafe_then_cap' s; irqs_masked' s; pspace_domain_valid s; valid_arch_state' s; valid_global_refs' s; valid_idle' s; valid_irq_handlers' s; valid_machine_state' s; valid_pde_mappings' s; valid_pspace' s; Invariants_H.valid_queues s; valid_queues' s; sym_refs (state_refs_of' s); sch_act_wf (ksSchedulerAction s) s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; untyped_ranges_zero' s; valid_irq_node' (irq_node' s) s; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ko_at' (Structures_H.endpoint.RecvEP x1) epptr s; valid_irq_states' s; ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; state_refs_of' s epptr = set x1 \<times> {EPRecv}; \<forall>x\<in>set x1. ko_wp_at' (\<lambda>ko. (epptr, TCBBlockedRecv) \<in> refs_of' ko) x s; (\<exists>a. ts = Structures_H.thread_state.BlockedOnReceive epptr a) \<or> (\<exists>a b c d. ts = Structures_H.thread_state.BlockedOnSend epptr a b c d); obj_at' (tcb_ntfn_is_bound' ntfnptr) t s; state_refs_of' s t = tcb_st_refs_of' ts \<union> tcb_bound_refs' ntfnptr; x1 \<noteq> []; \<forall>t\<in>set x1. tcb_at' t s; distinct x1; distinct (remove1 t x1)\<rbrakk> \<Longrightarrow> sym_refs ((state_refs_of' s)(epptr := (set x1 - {t}) \<times> {EPRecv}, t := {r. snd r = TCBBound \<and> (r \<in> tcb_st_refs_of' ts \<or> r \<in> tcb_bound_refs' ntfnptr)}))
 2. \<And>epptr s x3 ts ntfnptr. \<lbrakk>\<forall>a b. t \<notin> set (ksReadyQueues s (a, b)); t \<noteq> epptr; ct_idle_or_in_cur_domain' s; ct_not_inQ s; cur_tcb' s; if_live_then_nonz_cap' s; if_unsafe_then_cap' s; irqs_masked' s; pspace_domain_valid s; valid_arch_state' s; valid_global_refs' s; valid_idle' s; valid_irq_handlers' s; valid_machine_state' s; valid_pde_mappings' s; valid_pspace' s; Invariants_H.valid_queues s; valid_queues' s; sym_refs (state_refs_of' s); sch_act_wf (ksSchedulerAction s) s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; untyped_ranges_zero' s; valid_irq_node' (irq_node' s) s; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ko_at' (Structures_H.endpoint.SendEP x3) epptr s; valid_irq_states' s; ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; state_refs_of' s epptr = set x3 \<times> {EPSend}; \<forall>x\<in>set x3. ko_wp_at' (\<lambda>ko. (epptr, TCBBlockedSend) \<in> refs_of' ko) x s; (\<exists>a. ts = Structures_H.thread_state.BlockedOnReceive epptr a) \<or> (\<exists>a b c d. ts = Structures_H.thread_state.BlockedOnSend epptr a b c d); obj_at' (tcb_ntfn_is_bound' ntfnptr) t s; state_refs_of' s t = tcb_st_refs_of' ts \<union> tcb_bound_refs' ntfnptr; x3 \<noteq> []; \<forall>t\<in>set x3. tcb_at' t s; distinct x3\<rbrakk> \<Longrightarrow> sym_refs ((state_refs_of' s)(epptr := (set x3 - {t}) \<times> {EPSend}, t := {r. snd r = TCBBound \<and> (r \<in> tcb_st_refs_of' ts \<or> r \<in> tcb_bound_refs' ntfnptr)})) proof (prove)
goal (2 subgoals):
 1. \<And>epptr s x1 ts ntfnptr. \<lbrakk>\<forall>a b. t \<notin> set (ksReadyQueues s (a, b)); t \<noteq> epptr; ct_idle_or_in_cur_domain' s; ct_not_inQ s; cur_tcb' s; if_live_then_nonz_cap' s; if_unsafe_then_cap' s; irqs_masked' s; pspace_domain_valid s; valid_arch_state' s; valid_global_refs' s; valid_idle' s; valid_irq_handlers' s; valid_machine_state' s; valid_pde_mappings' s; valid_pspace' s; Invariants_H.valid_queues s; valid_queues' s; sym_refs (state_refs_of' s); sch_act_wf (ksSchedulerAction s) s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; untyped_ranges_zero' s; valid_irq_node' (irq_node' s) s; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ko_at' (Structures_H.endpoint.RecvEP x1) epptr s; valid_irq_states' s; ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; state_refs_of' s epptr = set x1 \<times> {EPRecv}; \<forall>x\<in>set x1. ko_wp_at' (\<lambda>ko. (epptr, TCBBlockedRecv) \<in> refs_of' ko) x s; (\<exists>a. ts = Structures_H.thread_state.BlockedOnReceive epptr a) \<or> (\<exists>a b c d. ts = Structures_H.thread_state.BlockedOnSend epptr a b c d); obj_at' (tcb_ntfn_is_bound' ntfnptr) t s; state_refs_of' s t = tcb_st_refs_of' ts \<union> tcb_bound_refs' ntfnptr; x1 \<noteq> []; \<forall>t\<in>set x1. tcb_at' t s; distinct x1; distinct (remove1 t x1); set (remove1 t x1) = set x1 - {t}\<rbrakk> \<Longrightarrow> sym_refs ((state_refs_of' s)(epptr := (set x1 - {t}) \<times> {EPRecv}, t := {r. snd r = TCBBound \<and> (r \<in> tcb_st_refs_of' ts \<or> r \<in> tcb_bound_refs' ntfnptr)}))
 2. \<And>epptr s x3 ts ntfnptr. \<lbrakk>\<forall>a b. t \<notin> set (ksReadyQueues s (a, b)); t \<noteq> epptr; ct_idle_or_in_cur_domain' s; ct_not_inQ s; cur_tcb' s; if_live_then_nonz_cap' s; if_unsafe_then_cap' s; irqs_masked' s; pspace_domain_valid s; valid_arch_state' s; valid_global_refs' s; valid_idle' s; valid_irq_handlers' s; valid_machine_state' s; valid_pde_mappings' s; valid_pspace' s; Invariants_H.valid_queues s; valid_queues' s; sym_refs (state_refs_of' s); sch_act_wf (ksSchedulerAction s) s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; untyped_ranges_zero' s; valid_irq_node' (irq_node' s) s; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ko_at' (Structures_H.endpoint.SendEP x3) epptr s; valid_irq_states' s; ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). 0 < dschLength x \<and> dschDomain x \<le> maxDomain; state_refs_of' s epptr = set x3 \<times> {EPSend}; \<forall>x\<in>set x3. ko_wp_at' (\<lambda>ko. (epptr, TCBBlockedSend) \<in> refs_of' ko) x s; (\<exists>a. ts = Structures_H.thread_state.BlockedOnReceive epptr a) \<or> (\<exists>a b c d. ts = Structures_H.thread_state.BlockedOnSend epptr a b c d); obj_at' (tcb_ntfn_is_bound' ntfnptr) t s; state_refs_of' s t = tcb_st_refs_of' ts \<union> tcb_bound_refs' ntfnptr; x3 \<noteq> []; \<forall>t\<in>set x3. tcb_at' t s; distinct x3\<rbrakk> \<Longrightarrow> sym_refs ((state_refs_of' s)(epptr := (set x3 - {t}) \<times> {EPSend}, t := {r. snd r = TCBBound \<and> (r \<in> tcb_st_refs_of' ts \<or> r \<in> tcb_bound_refs' ntfnptr)})) proof (state)
this:
\<lbrace>st_tcb_at' (\<lambda>st. \<exists>a. st = Structures_H.thread_state.BlockedOnReceive ?epptr1 a \<or> (\<exists>a b c d. st = Structures_H.thread_state.BlockedOnSend ?epptr1 a b c d)) t and invs'\<rbrace> do ep <- getEndpoint ?epptr1;
y <- assert (\<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False));
ep' <- case remove1 t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | x # xs \<Rightarrow> return (epQueue_update (\<lambda>_. x # xs) ep);
y <- setEndpoint ?epptr1 ep';
setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>rv. invs'\<rbrace>

goal (1 subgoal):
 1. \<lbrace>tcb_at' t and invs'\<rbrace> cancelIPC t \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and tcb_at' t\<rbrace> do y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
slot <- getThreadReplySlot t;
callerCap <- liftM (mdbNext \<circ> cteMDBNode) (getCTE slot);
when (callerCap \<noteq> nullPointer) (do y <- stateAssert (capHasProperty callerCap (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne callerCap
od)
od \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and tcb_at' t\<rbrace> do y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
slot <- locateSlotTCB t tcbReplySlot;
callerCap <- liftM (mdbNext \<circ> cteMDBNode) (getCTE slot);
when (callerCap \<noteq> nullPointer) (do y <- stateAssert (capHasProperty callerCap (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne callerCap
od)
od \<lbrace>\<lambda>rv. invs'\<rbrace> proof (state)
this:
\<lbrace>invs' and tcb_at' t\<rbrace> do y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
slot <- getThreadReplySlot t;
callerCap <- liftM (mdbNext \<circ> cteMDBNode) (getCTE slot);
when (callerCap \<noteq> nullPointer) (do y <- stateAssert (capHasProperty callerCap (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne callerCap
od)
od \<lbrace>\<lambda>rv. invs'\<rbrace>

goal (1 subgoal):
 1. \<lbrace>tcb_at' t and invs'\<rbrace> cancelIPC t \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at' t and invs'\<rbrace> cancelIPC t \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at' t and invs'\<rbrace> do state <- getThreadState t;
case state of Structures_H.thread_state.BlockedOnReceive x xa \<Rightarrow> do ep <- getEndpoint (blockingObject state);
y <- assert (\<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False));
ep' <- case remove1 t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return (epQueue_update (\<lambda>_. a # list) ep);
y <- setEndpoint (blockingObject state) ep';
setThreadState Structures_H.thread_state.Inactive t
od | Structures_H.thread_state.BlockedOnReply \<Rightarrow> do y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
slot <- getThreadReplySlot t;
callerCap <- liftM (mdbNext \<circ> cteMDBNode) (getCTE slot);
when (callerCap \<noteq> nullPointer) (do y <- stateAssert (capHasProperty callerCap (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne callerCap
od)
od | Structures_H.thread_state.BlockedOnNotification x \<Rightarrow> cancelSignal t (waitingOnNotification state) | Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<Rightarrow> do ep <- getEndpoint (blockingObject state);
y <- assert (\<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False));
ep' <- case remove1 t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return (epQueue_update (\<lambda>_. a # list) ep);
y <- setEndpoint (blockingObject state) ep';
setThreadState Structures_H.thread_state.Inactive t
od | _ \<Rightarrow> return ()
od \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>state. \<lbrace>st_tcb_at' (\<lambda>st. st = state) t and (tcb_at' t and invs')\<rbrace> case state of Structures_H.thread_state.BlockedOnReceive x xa \<Rightarrow> do ep <- getEndpoint (blockingObject state);
y <- assert (\<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False));
ep' <- case remove1 t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return (epQueue_update (\<lambda>_. a # list) ep);
y <- setEndpoint (blockingObject state) ep';
setThreadState Structures_H.thread_state.Inactive t
od | Structures_H.thread_state.BlockedOnReply \<Rightarrow> do y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
slot <- getThreadReplySlot t;
callerCap <- liftM (mdbNext \<circ> cteMDBNode) (getCTE slot);
when (callerCap \<noteq> nullPointer) (do y <- stateAssert (capHasProperty callerCap (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne callerCap
od)
od | Structures_H.thread_state.BlockedOnNotification x \<Rightarrow> cancelSignal t (waitingOnNotification state) | Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<Rightarrow> do ep <- getEndpoint (blockingObject state);
y <- assert (\<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False));
ep' <- case remove1 t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return (epQueue_update (\<lambda>_. a # list) ep);
y <- setEndpoint (blockingObject state) ep';
setThreadState Structures_H.thread_state.Inactive t
od | _ \<Rightarrow> return () \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>state x11 x12. state = Structures_H.thread_state.BlockedOnReceive x11 x12 \<Longrightarrow> \<lbrace>st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.BlockedOnReceive x11 x12) t and (tcb_at' t and invs')\<rbrace> do ep <- getEndpoint x11;
y <- assert (\<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False));
ep' <- case remove1 t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return (epQueue_update (\<lambda>_. a # list) ep);
y <- setEndpoint x11 ep';
setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>rv. invs'\<rbrace>
 2. \<lbrace>st_tcb_at' awaiting_reply' t and (tcb_at' t and invs')\<rbrace> do y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
slot <- getThreadReplySlot t;
callerCap <- liftM (mdbNext \<circ> cteMDBNode) (getCTE slot);
when (callerCap \<noteq> nullPointer) (do y <- stateAssert (capHasProperty callerCap (\<lambda>cap. isReplyCap cap \<and> \<not> capReplyMaster cap)) [];
cteDeleteOne callerCap
od)
od \<lbrace>\<lambda>rv. invs'\<rbrace>
 3. \<And>state x3. state = Structures_H.thread_state.BlockedOnNotification x3 \<Longrightarrow> \<lbrace>st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.BlockedOnNotification x3) t and (tcb_at' t and invs')\<rbrace> cancelSignal t x3 \<lbrace>\<lambda>rv. invs'\<rbrace>
 4. \<lbrace>st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Running) t and (tcb_at' t and invs')\<rbrace> return () \<lbrace>\<lambda>rv. invs'\<rbrace>
 5. \<lbrace>st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Inactive) t and (tcb_at' t and invs')\<rbrace> return () \<lbrace>\<lambda>rv. invs'\<rbrace>
 6. \<lbrace>st_tcb_at' idle' t and (tcb_at' t and invs')\<rbrace> return () \<lbrace>\<lambda>rv. invs'\<rbrace>
 7. \<And>state x71 x72 x73 x74 x75. state = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75 \<Longrightarrow> \<lbrace>st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75) t and (tcb_at' t and invs')\<rbrace> do ep <- getEndpoint x71;
y <- assert (\<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False));
ep' <- case remove1 t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return (epQueue_update (\<lambda>_. a # list) ep);
y <- setEndpoint x71 ep';
setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>rv. invs'\<rbrace>
 8. \<lbrace>st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Restart) t and (tcb_at' t and invs')\<rbrace> return () \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>state x11 x12 s st. \<lbrakk>tcb_at' t s; invs' s\<rbrakk> \<Longrightarrow> \<exists>a. Structures_H.thread_state.BlockedOnReceive x11 x12 = Structures_H.thread_state.BlockedOnReceive x11 a \<or> (\<exists>a b c d. Structures_H.thread_state.BlockedOnReceive x11 x12 = Structures_H.thread_state.BlockedOnSend x11 a b c d)
 2. \<And>state x3 s. \<lbrakk>st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.BlockedOnNotification x3) t s; tcb_at' t s; invs' s; ksSchedulerAction s = SwitchToThread t\<rbrakk> \<Longrightarrow> False
 3. \<And>state x71 x72 x73 x74 x75 s st. \<lbrakk>tcb_at' t s; invs' s\<rbrakk> \<Longrightarrow> \<exists>a. Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75 = Structures_H.thread_state.BlockedOnReceive x71 a \<or> (\<exists>a b c d. Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75 = Structures_H.thread_state.BlockedOnSend x71 a b c d) proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>tcb_at' t and invs'\<rbrace> cancelIPC t \<lbrace>\<lambda>rv. invs'\<rbrace>

goal:
No subgoals!