theory Fastpath_Equiv

lemma st_tcb_at_is_Reply_imp_not_tcbQueued: "\<And>s t.\<lbrakk> invs' s; st_tcb_at' isReply t s\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>a. \<not> tcbQueued a) t s" apply (clarsimp simp: invs'_def valid_state'_def valid_queues_def st_tcb_at'_def valid_queues_no_bitmap_def) apply (rule all_prio_not_inQ_not_tcbQueued) apply (clarsimp simp: obj_at'_def) apply (erule_tac x="d" in allE) apply (erule_tac x="p" in allE) apply (erule conjE) apply (erule_tac x="t" in ballE) apply (clarsimp simp: obj_at'_def runnable'_def isReply_def) apply (case_tac "tcbState obj") apply ((clarsimp simp: inQ_def)+)[8] apply (clarsimp simp: valid_queues'_def obj_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>invs' s; st_tcb_at' isReply t s\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>a. \<not> tcbQueued a) t s proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>obj_at' (isReply \<circ> tcbState) t s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) 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; 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 (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>a. \<not> tcbQueued a) t s proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>obj_at' (isReply \<circ> tcbState) t s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) 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; 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 (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>a. \<forall>d p. \<not> inQ d p a) t s proof (prove)
goal (1 subgoal):
 1. \<And>s t ko obj d p. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; \<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). \<exists>ko. ksPSpace s t = Some ko \<and> is_aligned t (objBitsKO ko) \<and> (\<exists>obj. fst (projectKO ko s) = {(obj, s)} \<and> inQ d p obj \<and> runnable' (tcbState obj) \<and> ps_clear t (objBitsKO ko) 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; 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 (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ksPSpace s t = Some ko; is_aligned t (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; isReply (tcbState obj); ps_clear t (objBitsKO ko) s; inQ d p obj\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s t ko obj d p. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans 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 (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ksPSpace s t = Some ko; is_aligned t (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; isReply (tcbState obj); ps_clear t (objBitsKO ko) s; inQ d p obj; \<forall>p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). \<exists>ko. ksPSpace s t = Some ko \<and> is_aligned t (objBitsKO ko) \<and> (\<exists>obj. fst (projectKO ko s) = {(obj, s)} \<and> inQ d p obj \<and> runnable' (tcbState obj) \<and> ps_clear t (objBitsKO ko) s)) \<and> distinct (ksReadyQueues s (d, p)) \<and> (maxDomain < d \<longrightarrow> ksReadyQueues s (d, p) = []) \<and> (maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = [])\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s t ko obj d p. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans 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 (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ksPSpace s t = Some ko; is_aligned t (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; isReply (tcbState obj); ps_clear t (objBitsKO ko) s; inQ d p obj; (\<forall>t\<in>set (ksReadyQueues s (d, p)). \<exists>ko. ksPSpace s t = Some ko \<and> is_aligned t (objBitsKO ko) \<and> (\<exists>obj. fst (projectKO ko s) = {(obj, s)} \<and> inQ d p obj \<and> runnable' (tcbState obj) \<and> ps_clear t (objBitsKO ko) s)) \<and> distinct (ksReadyQueues s (d, p)) \<and> (maxDomain < d \<longrightarrow> ksReadyQueues s (d, p) = []) \<and> (maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = [])\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s t ko obj d p. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans 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 (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ksPSpace s t = Some ko; is_aligned t (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; isReply (tcbState obj); ps_clear t (objBitsKO ko) s; inQ d p obj; \<forall>t\<in>set (ksReadyQueues s (d, p)). \<exists>ko. ksPSpace s t = Some ko \<and> is_aligned t (objBitsKO ko) \<and> (\<exists>obj. fst (projectKO ko s) = {(obj, s)} \<and> inQ d p obj \<and> runnable' (tcbState obj) \<and> ps_clear t (objBitsKO ko) s); distinct (ksReadyQueues s (d, p)) \<and> (maxDomain < d \<longrightarrow> ksReadyQueues s (d, p) = []) \<and> (maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = [])\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s t ko obj d p. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans 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 (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ksPSpace s t = Some ko; is_aligned t (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; isReply (tcbState obj); ps_clear t (objBitsKO ko) s; inQ d p obj; distinct (ksReadyQueues s (d, p)) \<and> (maxDomain < d \<longrightarrow> ksReadyQueues s (d, p) = []) \<and> (maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = []); \<exists>ko. ksPSpace s t = Some ko \<and> is_aligned t (objBitsKO ko) \<and> (\<exists>obj. fst (projectKO ko s) = {(obj, s)} \<and> inQ d p obj \<and> runnable' (tcbState obj) \<and> ps_clear t (objBitsKO ko) s)\<rbrakk> \<Longrightarrow> False
 2. \<And>s t ko obj d p. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans 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 (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ksPSpace s t = Some ko; is_aligned t (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; isReply (tcbState obj); ps_clear t (objBitsKO ko) s; inQ d p obj; distinct (ksReadyQueues s (d, p)) \<and> (maxDomain < d \<longrightarrow> ksReadyQueues s (d, p) = []) \<and> (maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = []); t \<notin> set (ksReadyQueues s (d, p))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s t ko obj d p. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans 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 (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ksPSpace s t = Some ko; is_aligned t (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; case tcbState obj of Structures_H.thread_state.BlockedOnReply \<Rightarrow> True | _ \<Rightarrow> False; ps_clear t (objBitsKO ko) s; inQ d p obj; Structures_H.thread_state.rec_thread_state (\<lambda>a b. False) False (\<lambda>x. False) True False False (\<lambda>a b c d e. False) True (tcbState obj); distinct (ksReadyQueues s (d, p)); maxDomain < d \<longrightarrow> ksReadyQueues s (d, p) = []; maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = []\<rbrakk> \<Longrightarrow> False
 2. \<And>s t ko obj d p. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans 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 (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ksPSpace s t = Some ko; is_aligned t (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; isReply (tcbState obj); ps_clear t (objBitsKO ko) s; inQ d p obj; distinct (ksReadyQueues s (d, p)) \<and> (maxDomain < d \<longrightarrow> ksReadyQueues s (d, p) = []) \<and> (maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = []); t \<notin> set (ksReadyQueues s (d, p))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (9 subgoals):
 1. \<And>s t ko obj d p x11 x12. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans 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 (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ksPSpace s t = Some ko; is_aligned t (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; case tcbState obj of Structures_H.thread_state.BlockedOnReply \<Rightarrow> True | _ \<Rightarrow> False; ps_clear t (objBitsKO ko) s; inQ d p obj; Structures_H.thread_state.rec_thread_state (\<lambda>a b. False) False (\<lambda>x. False) True False False (\<lambda>a b c d e. False) True (tcbState obj); distinct (ksReadyQueues s (d, p)); maxDomain < d \<longrightarrow> ksReadyQueues s (d, p) = []; maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = []; tcbState obj = Structures_H.thread_state.BlockedOnReceive x11 x12\<rbrakk> \<Longrightarrow> False
 2. \<And>s t ko obj d p. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans 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 (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ksPSpace s t = Some ko; is_aligned t (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; case tcbState obj of Structures_H.thread_state.BlockedOnReply \<Rightarrow> True | _ \<Rightarrow> False; ps_clear t (objBitsKO ko) s; inQ d p obj; Structures_H.thread_state.rec_thread_state (\<lambda>a b. False) False (\<lambda>x. False) True False False (\<lambda>a b c d e. False) True (tcbState obj); distinct (ksReadyQueues s (d, p)); maxDomain < d \<longrightarrow> ksReadyQueues s (d, p) = []; maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = []; awaiting_reply' (tcbState obj)\<rbrakk> \<Longrightarrow> False
 3. \<And>s t ko obj d p x3. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans 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 (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ksPSpace s t = Some ko; is_aligned t (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; case tcbState obj of Structures_H.thread_state.BlockedOnReply \<Rightarrow> True | _ \<Rightarrow> False; ps_clear t (objBitsKO ko) s; inQ d p obj; Structures_H.thread_state.rec_thread_state (\<lambda>a b. False) False (\<lambda>x. False) True False False (\<lambda>a b c d e. False) True (tcbState obj); distinct (ksReadyQueues s (d, p)); maxDomain < d \<longrightarrow> ksReadyQueues s (d, p) = []; maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = []; tcbState obj = Structures_H.thread_state.BlockedOnNotification x3\<rbrakk> \<Longrightarrow> False
 4. \<And>s t ko obj d p. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans 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 (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ksPSpace s t = Some ko; is_aligned t (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; case tcbState obj of Structures_H.thread_state.BlockedOnReply \<Rightarrow> True | _ \<Rightarrow> False; ps_clear t (objBitsKO ko) s; inQ d p obj; Structures_H.thread_state.rec_thread_state (\<lambda>a b. False) False (\<lambda>x. False) True False False (\<lambda>a b c d e. False) True (tcbState obj); distinct (ksReadyQueues s (d, p)); maxDomain < d \<longrightarrow> ksReadyQueues s (d, p) = []; maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = []; tcbState obj = Structures_H.thread_state.Running\<rbrakk> \<Longrightarrow> False
 5. \<And>s t ko obj d p. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans 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 (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ksPSpace s t = Some ko; is_aligned t (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; case tcbState obj of Structures_H.thread_state.BlockedOnReply \<Rightarrow> True | _ \<Rightarrow> False; ps_clear t (objBitsKO ko) s; inQ d p obj; Structures_H.thread_state.rec_thread_state (\<lambda>a b. False) False (\<lambda>x. False) True False False (\<lambda>a b c d e. False) True (tcbState obj); distinct (ksReadyQueues s (d, p)); maxDomain < d \<longrightarrow> ksReadyQueues s (d, p) = []; maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = []; tcbState obj = Structures_H.thread_state.Inactive\<rbrakk> \<Longrightarrow> False
 6. \<And>s t ko obj d p. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans 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 (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ksPSpace s t = Some ko; is_aligned t (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; case tcbState obj of Structures_H.thread_state.BlockedOnReply \<Rightarrow> True | _ \<Rightarrow> False; ps_clear t (objBitsKO ko) s; inQ d p obj; Structures_H.thread_state.rec_thread_state (\<lambda>a b. False) False (\<lambda>x. False) True False False (\<lambda>a b c d e. False) True (tcbState obj); distinct (ksReadyQueues s (d, p)); maxDomain < d \<longrightarrow> ksReadyQueues s (d, p) = []; maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = []; idle' (tcbState obj)\<rbrakk> \<Longrightarrow> False
 7. \<And>s t ko obj d p x71 x72 x73 x74 x75. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans 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 (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ksPSpace s t = Some ko; is_aligned t (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; case tcbState obj of Structures_H.thread_state.BlockedOnReply \<Rightarrow> True | _ \<Rightarrow> False; ps_clear t (objBitsKO ko) s; inQ d p obj; Structures_H.thread_state.rec_thread_state (\<lambda>a b. False) False (\<lambda>x. False) True False False (\<lambda>a b c d e. False) True (tcbState obj); distinct (ksReadyQueues s (d, p)); maxDomain < d \<longrightarrow> ksReadyQueues s (d, p) = []; maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = []; tcbState obj = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75\<rbrakk> \<Longrightarrow> False
 8. \<And>s t ko obj d p. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans 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 (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ksPSpace s t = Some ko; is_aligned t (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; case tcbState obj of Structures_H.thread_state.BlockedOnReply \<Rightarrow> True | _ \<Rightarrow> False; ps_clear t (objBitsKO ko) s; inQ d p obj; Structures_H.thread_state.rec_thread_state (\<lambda>a b. False) False (\<lambda>x. False) True False False (\<lambda>a b c d e. False) True (tcbState obj); distinct (ksReadyQueues s (d, p)); maxDomain < d \<longrightarrow> ksReadyQueues s (d, p) = []; maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = []; tcbState obj = Structures_H.thread_state.Restart\<rbrakk> \<Longrightarrow> False
 9. \<And>s t ko obj d p. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans 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 (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ksPSpace s t = Some ko; is_aligned t (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; isReply (tcbState obj); ps_clear t (objBitsKO ko) s; inQ d p obj; distinct (ksReadyQueues s (d, p)) \<and> (maxDomain < d \<longrightarrow> ksReadyQueues s (d, p) = []) \<and> (maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = []); t \<notin> set (ksReadyQueues s (d, p))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s t ko obj d p. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans 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 (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ksPSpace s t = Some ko; is_aligned t (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; isReply (tcbState obj); ps_clear t (objBitsKO ko) s; inQ d p obj; distinct (ksReadyQueues s (d, p)) \<and> (maxDomain < d \<longrightarrow> ksReadyQueues s (d, p) = []) \<and> (maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = []); t \<notin> set (ksReadyQueues s (d, p))\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!