theory IpcCancel_R

lemma cancelAllIPC_invs'[wp]:
  "\<lbrace>invs'\<rbrace> cancelAllIPC ep_ptr \<lbrace>\<lambda>rv. invs'\<rbrace>" apply (simp add: cancelAllIPC_def ep'_Idle_case_helper cong del: if_cong) apply (wp rescheduleRequired_all_invs_but_ct_not_inQ
            cancel_all_invs'_helper hoare_vcg_const_Ball_lift
            valid_global_refs_lift' valid_arch_state_lift'
            valid_irq_node_lift ssa_invs' sts_sch_act'
            irqs_masked_lift
         | simp only: sch_act_wf.simps forM_x_def | simp)+ prefer 2 apply assumption apply (rule hoare_strengthen_post [OF get_ep_sp']) apply (rename_tac rv s) apply (clarsimp simp: invs'_def valid_state'_def valid_ep'_def) apply (frule obj_at_valid_objs', fastforce) apply (clarsimp simp: projectKOs valid_obj'_def) apply (rule conjI) apply (case_tac rv, simp_all add: valid_ep'_def)[1] apply (rule conjI[rotated]) apply (drule(1) sym_refs_ko_atD') apply (case_tac rv, simp_all add: st_tcb_at_refs_of_rev')[1] apply (clarsimp elim!: if_live_state_refsE
           | drule(1) bspec | drule st_tcb_at_state_refs_ofD')+ apply (drule(2) ep_q_refs_max) apply (erule delta_sym_refs) apply (clarsimp dest!: symreftype_inverse' split: if_split_asm | drule(1) bspec subsetD)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> cancelAllIPC ep_ptr \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> do ep <- getEndpoint ep_ptr;
if ep = Structures_H.endpoint.IdleEP then return () else do y <- setEndpoint ep_ptr Structures_H.endpoint.IdleEP;
y <- mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) (epQueue ep);
rescheduleRequired
od
od \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> getEndpoint ep_ptr \<lbrace>\<lambda>ep s. (ep = Structures_H.endpoint.IdleEP \<longrightarrow> invs' s) \<and> (ep \<noteq> Structures_H.endpoint.IdleEP \<longrightarrow> valid_pspace' s \<and> valid_ep' Structures_H.endpoint.IdleEP s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues 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> irqs_masked' s \<and> valid_machine_state' s \<and> cur_tcb' s \<and> valid_queues' 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> (\<forall>x\<in>set (epQueue ep). tcb_at' x s) \<and> sym_refs (\<lambda>x. if x \<in> set (epQueue ep) then {r \<in> ((state_refs_of' s)(ep_ptr := ep_q_refs_of' Structures_H.endpoint.IdleEP)) x. snd r = TCBBound} else ((state_refs_of' s)(ep_ptr := ep_q_refs_of' Structures_H.endpoint.IdleEP)) x) \<and> (\<forall>x\<in>set (epQueue ep). ex_nonz_cap_to' x s))\<rbrace>
 2. \<And>s. invs' s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>s. invs' s \<Longrightarrow> ?Q s
 2. \<lbrace>?Q\<rbrace> getEndpoint ep_ptr \<lbrace>\<lambda>ep s. (ep = Structures_H.endpoint.IdleEP \<longrightarrow> invs' s) \<and> (ep \<noteq> Structures_H.endpoint.IdleEP \<longrightarrow> valid_pspace' s \<and> valid_ep' Structures_H.endpoint.IdleEP s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues 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> irqs_masked' s \<and> valid_machine_state' s \<and> cur_tcb' s \<and> valid_queues' 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> (\<forall>x\<in>set (epQueue ep). tcb_at' x s) \<and> sym_refs (\<lambda>x. if x \<in> set (epQueue ep) then {r \<in> ((state_refs_of' s)(ep_ptr := ep_q_refs_of' Structures_H.endpoint.IdleEP)) x. snd r = TCBBound} else ((state_refs_of' s)(ep_ptr := ep_q_refs_of' Structures_H.endpoint.IdleEP)) x) \<and> (\<forall>x\<in>set (epQueue ep). ex_nonz_cap_to' x s))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> getEndpoint ep_ptr \<lbrace>\<lambda>ep s. (ep = Structures_H.endpoint.IdleEP \<longrightarrow> invs' s) \<and> (ep \<noteq> Structures_H.endpoint.IdleEP \<longrightarrow> valid_pspace' s \<and> valid_ep' Structures_H.endpoint.IdleEP s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues 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> irqs_masked' s \<and> valid_machine_state' s \<and> cur_tcb' s \<and> valid_queues' 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> (\<forall>x\<in>set (epQueue ep). tcb_at' x s) \<and> sym_refs (\<lambda>x. if x \<in> set (epQueue ep) then {r \<in> ((state_refs_of' s)(ep_ptr := ep_q_refs_of' Structures_H.endpoint.IdleEP)) x. snd r = TCBBound} else ((state_refs_of' s)(ep_ptr := ep_q_refs_of' Structures_H.endpoint.IdleEP)) x) \<and> (\<forall>x\<in>set (epQueue ep). ex_nonz_cap_to' x s))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>rv s. (invs' and ko_at' rv ep_ptr) s \<Longrightarrow> (rv = Structures_H.endpoint.IdleEP \<longrightarrow> invs' s) \<and> (rv \<noteq> Structures_H.endpoint.IdleEP \<longrightarrow> valid_pspace' s \<and> valid_ep' Structures_H.endpoint.IdleEP s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues 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> irqs_masked' s \<and> valid_machine_state' s \<and> cur_tcb' s \<and> valid_queues' 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> (\<forall>x\<in>set (epQueue rv). tcb_at' x s) \<and> sym_refs (\<lambda>x. if x \<in> set (epQueue rv) then {r \<in> ((state_refs_of' s)(ep_ptr := ep_q_refs_of' Structures_H.endpoint.IdleEP)) x. snd r = TCBBound} else ((state_refs_of' s)(ep_ptr := ep_q_refs_of' Structures_H.endpoint.IdleEP)) x) \<and> (\<forall>x\<in>set (epQueue rv). ex_nonz_cap_to' x s)) proof (prove)
goal (1 subgoal):
 1. \<And>rv s. (invs' and ko_at' rv ep_ptr) s \<Longrightarrow> (rv = Structures_H.endpoint.IdleEP \<longrightarrow> invs' s) \<and> (rv \<noteq> Structures_H.endpoint.IdleEP \<longrightarrow> valid_pspace' s \<and> valid_ep' Structures_H.endpoint.IdleEP s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues 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> irqs_masked' s \<and> valid_machine_state' s \<and> cur_tcb' s \<and> valid_queues' 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> (\<forall>x\<in>set (epQueue rv). tcb_at' x s) \<and> sym_refs (\<lambda>x. if x \<in> set (epQueue rv) then {r \<in> ((state_refs_of' s)(ep_ptr := ep_q_refs_of' Structures_H.endpoint.IdleEP)) x. snd r = TCBBound} else ((state_refs_of' s)(ep_ptr := ep_q_refs_of' Structures_H.endpoint.IdleEP)) x) \<and> (\<forall>x\<in>set (epQueue rv). ex_nonz_cap_to' x s)) proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ko_at' rv ep_ptr s; rv \<noteq> Structures_H.endpoint.IdleEP\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set (epQueue rv). tcb_at' x s) \<and> sym_refs (\<lambda>x. if x \<in> set (epQueue rv) then {r \<in> ((state_refs_of' s)(ep_ptr := ep_q_refs_of' Structures_H.endpoint.IdleEP)) x. snd r = TCBBound} else ((state_refs_of' s)(ep_ptr := ep_q_refs_of' Structures_H.endpoint.IdleEP)) x) \<and> (\<forall>x\<in>set (epQueue rv). ex_nonz_cap_to' x s) proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ko_at' rv ep_ptr s; rv \<noteq> Structures_H.endpoint.IdleEP; \<exists>k. k = rv \<and> ((\<forall>ko. projectKO_opt ko = Some k \<longrightarrow> injectKO k = ko) \<longrightarrow> valid_obj' (injectKO k) s)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set (epQueue rv). tcb_at' x s) \<and> sym_refs (\<lambda>x. if x \<in> set (epQueue rv) then {r \<in> ((state_refs_of' s)(ep_ptr := ep_q_refs_of' Structures_H.endpoint.IdleEP)) x. snd r = TCBBound} else ((state_refs_of' s)(ep_ptr := ep_q_refs_of' Structures_H.endpoint.IdleEP)) x) \<and> (\<forall>x\<in>set (epQueue rv). ex_nonz_cap_to' x s) proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ko_at' rv ep_ptr s; rv \<noteq> Structures_H.endpoint.IdleEP; valid_ep' rv s\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set (epQueue rv). tcb_at' x s) \<and> sym_refs (\<lambda>x. if x \<in> set (epQueue rv) then {r \<in> ((state_refs_of' s)(ep_ptr := ep_q_refs_of' Structures_H.endpoint.IdleEP)) x. snd r = TCBBound} else ((state_refs_of' s)(ep_ptr := ep_q_refs_of' Structures_H.endpoint.IdleEP)) x) \<and> (\<forall>x\<in>set (epQueue rv). ex_nonz_cap_to' x s) proof (prove)
goal (2 subgoals):
 1. \<And>rv s. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ko_at' rv ep_ptr s; rv \<noteq> Structures_H.endpoint.IdleEP; valid_ep' rv s\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (epQueue rv). tcb_at' x s
 2. \<And>rv s. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ko_at' rv ep_ptr s; rv \<noteq> Structures_H.endpoint.IdleEP; valid_ep' rv s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>x. if x \<in> set (epQueue rv) then {r \<in> ((state_refs_of' s)(ep_ptr := ep_q_refs_of' Structures_H.endpoint.IdleEP)) x. snd r = TCBBound} else ((state_refs_of' s)(ep_ptr := ep_q_refs_of' Structures_H.endpoint.IdleEP)) x) \<and> (\<forall>x\<in>set (epQueue rv). ex_nonz_cap_to' x s) proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ko_at' rv ep_ptr s; rv \<noteq> Structures_H.endpoint.IdleEP; valid_ep' rv s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>x. if x \<in> set (epQueue rv) then {r \<in> ((state_refs_of' s)(ep_ptr := ep_q_refs_of' Structures_H.endpoint.IdleEP)) x. snd r = TCBBound} else ((state_refs_of' s)(ep_ptr := ep_q_refs_of' Structures_H.endpoint.IdleEP)) x) \<and> (\<forall>x\<in>set (epQueue rv). ex_nonz_cap_to' x s) proof (prove)
goal (2 subgoals):
 1. \<And>rv s. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ko_at' rv ep_ptr s; rv \<noteq> Structures_H.endpoint.IdleEP; valid_ep' rv s\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (epQueue rv). ex_nonz_cap_to' x s
 2. \<And>rv s. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ko_at' rv ep_ptr s; rv \<noteq> Structures_H.endpoint.IdleEP; valid_ep' rv s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>x. if x \<in> set (epQueue rv) then {r \<in> ((state_refs_of' s)(ep_ptr := ep_q_refs_of' Structures_H.endpoint.IdleEP)) x. snd r = TCBBound} else ((state_refs_of' s)(ep_ptr := ep_q_refs_of' Structures_H.endpoint.IdleEP)) x) proof (prove)
goal (2 subgoals):
 1. \<And>rv s. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; rv \<noteq> Structures_H.endpoint.IdleEP; valid_ep' rv s; state_refs_of' s ep_ptr = refs_of' (injectKO rv) \<and> (\<forall>(x, tp)\<in>refs_of' (injectKO rv). ko_wp_at' (\<lambda>ko. (ep_ptr, symreftype tp) \<in> refs_of' ko) x s)\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (epQueue rv). ex_nonz_cap_to' x s
 2. \<And>rv s. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ko_at' rv ep_ptr s; rv \<noteq> Structures_H.endpoint.IdleEP; valid_ep' rv s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>x. if x \<in> set (epQueue rv) then {r \<in> ((state_refs_of' s)(ep_ptr := ep_q_refs_of' Structures_H.endpoint.IdleEP)) x. snd r = TCBBound} else ((state_refs_of' s)(ep_ptr := ep_q_refs_of' Structures_H.endpoint.IdleEP)) x) proof (prove)
goal (3 subgoals):
 1. \<And>rv s x1. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; valid_ep' (Structures_H.endpoint.RecvEP x1) s; state_refs_of' s ep_ptr = set x1 \<times> {EPRecv} \<and> (\<forall>x\<in>set x1. st_tcb_at' (\<lambda>ts. \<exists>a. ts = Structures_H.thread_state.BlockedOnReceive ep_ptr a) x s); rv = Structures_H.endpoint.RecvEP x1\<rbrakk> \<Longrightarrow> \<forall>x\<in>set x1. ex_nonz_cap_to' x s
 2. \<And>rv s x3. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; valid_ep' (Structures_H.endpoint.SendEP x3) s; state_refs_of' s ep_ptr = set x3 \<times> {EPSend} \<and> (\<forall>x\<in>set x3. st_tcb_at' (\<lambda>ts. \<exists>a b c d. ts = Structures_H.thread_state.BlockedOnSend ep_ptr a b c d) x s); rv = Structures_H.endpoint.SendEP x3\<rbrakk> \<Longrightarrow> \<forall>x\<in>set x3. ex_nonz_cap_to' x s
 3. \<And>rv s. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ko_at' rv ep_ptr s; rv \<noteq> Structures_H.endpoint.IdleEP; valid_ep' rv s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>x. if x \<in> set (epQueue rv) then {r \<in> ((state_refs_of' s)(ep_ptr := ep_q_refs_of' Structures_H.endpoint.IdleEP)) x. snd r = TCBBound} else ((state_refs_of' s)(ep_ptr := ep_q_refs_of' Structures_H.endpoint.IdleEP)) x) proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ko_at' rv ep_ptr s; rv \<noteq> Structures_H.endpoint.IdleEP; valid_ep' rv s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>x. if x \<in> set (epQueue rv) then {r \<in> ((state_refs_of' s)(ep_ptr := ep_q_refs_of' Structures_H.endpoint.IdleEP)) x. snd r = TCBBound} else ((state_refs_of' s)(ep_ptr := ep_q_refs_of' Structures_H.endpoint.IdleEP)) x) proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; rv \<noteq> Structures_H.endpoint.IdleEP; valid_ep' rv s; state_refs_of' s ep_ptr \<subseteq> set (epQueue rv) \<times> {EPSend, EPRecv} \<and> (\<forall>x\<in>set (epQueue rv). \<exists>ntfnptr. state_refs_of' s x \<subseteq> {(ep_ptr, TCBBlockedSend), (ep_ptr, TCBBlockedRecv), (ntfnptr, TCBBound)})\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>x. if x \<in> set (epQueue rv) then {r \<in> ((state_refs_of' s)(ep_ptr := ep_q_refs_of' Structures_H.endpoint.IdleEP)) x. snd r = TCBBound} else ((state_refs_of' s)(ep_ptr := ep_q_refs_of' Structures_H.endpoint.IdleEP)) x) proof (prove)
goal (2 subgoals):
 1. \<And>rv s x y tp. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; rv \<noteq> Structures_H.endpoint.IdleEP; valid_ep' rv s; state_refs_of' s ep_ptr \<subseteq> set (epQueue rv) \<times> {EPSend, EPRecv} \<and> (\<forall>x\<in>set (epQueue rv). \<exists>ntfnptr. state_refs_of' s x \<subseteq> {(ep_ptr, TCBBlockedSend), (ep_ptr, TCBBlockedRecv), (ntfnptr, TCBBound)}); (y, tp) \<in> (if x \<in> set (epQueue rv) then {r \<in> ((state_refs_of' s)(ep_ptr := ep_q_refs_of' Structures_H.endpoint.IdleEP)) x. snd r = TCBBound} else ((state_refs_of' s)(ep_ptr := ep_q_refs_of' Structures_H.endpoint.IdleEP)) x); (y, tp) \<notin> state_refs_of' s x\<rbrakk> \<Longrightarrow> (x, symreftype tp) \<in> (if y \<in> set (epQueue rv) then {r \<in> ((state_refs_of' s)(ep_ptr := ep_q_refs_of' Structures_H.endpoint.IdleEP)) y. snd r = TCBBound} else ((state_refs_of' s)(ep_ptr := ep_q_refs_of' Structures_H.endpoint.IdleEP)) y)
 2. \<And>rv s x y tp. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; rv \<noteq> Structures_H.endpoint.IdleEP; valid_ep' rv s; state_refs_of' s ep_ptr \<subseteq> set (epQueue rv) \<times> {EPSend, EPRecv} \<and> (\<forall>x\<in>set (epQueue rv). \<exists>ntfnptr. state_refs_of' s x \<subseteq> {(ep_ptr, TCBBlockedSend), (ep_ptr, TCBBlockedRecv), (ntfnptr, TCBBound)}); (y, tp) \<in> state_refs_of' s x; (y, tp) \<notin> (if x \<in> set (epQueue rv) then {r \<in> ((state_refs_of' s)(ep_ptr := ep_q_refs_of' Structures_H.endpoint.IdleEP)) x. snd r = TCBBound} else ((state_refs_of' s)(ep_ptr := ep_q_refs_of' Structures_H.endpoint.IdleEP)) x)\<rbrakk> \<Longrightarrow> (x, symreftype tp) \<notin> (if y \<in> set (epQueue rv) then {r \<in> ((state_refs_of' s)(ep_ptr := ep_q_refs_of' Structures_H.endpoint.IdleEP)) y. snd r = TCBBound} else ((state_refs_of' s)(ep_ptr := ep_q_refs_of' Structures_H.endpoint.IdleEP)) y) proof (prove)
goal:
No subgoals!