theory Refine_C

lemma ct_running'_C:
  "\<lbrakk> (s, t) \<in> rf_sr; invs' s \<rbrakk> \<Longrightarrow> ct_running' s = ct_running_C t" apply (simp add: ct_running_C_def Let_def ct_in_state'_def st_tcb_at'_def) apply (clarsimp simp: rf_sr_def cstate_relation_def cpspace_relation_def Let_def) apply (rule iffI) apply (drule obj_at_ko_at') apply clarsimp apply (erule (1) cmap_relation_ko_atE) apply (clarsimp simp: ctcb_relation_def cthread_state_relation_def) apply clarsimp apply (drule (1) cmap_relation_cs_atD [where addr_fun=tcb_ptr_to_ctcb_ptr]) apply simp apply clarsimp apply (frule (1) map_to_ko_atI') apply (erule obj_at'_weakenE) apply (clarsimp simp: ctcb_relation_def cthread_state_relation_def) apply (case_tac "tcbState ko", simp_all add:
    ThreadState_Running_def
    ThreadState_BlockedOnReceive_def
    ThreadState_BlockedOnSend_def
    ThreadState_BlockedOnReply_def
    ThreadState_BlockedOnNotification_def
    ThreadState_Inactive_def
    ThreadState_IdleThreadState_def
    ThreadState_Restart_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, t) \<in> rf_sr; invs' s\<rbrakk> \<Longrightarrow> ct_running' s = ct_running_C t proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, t) \<in> rf_sr; invs' s\<rbrakk> \<Longrightarrow> obj_at' ((\<lambda>st. st = Structures_H.thread_state.Running) \<circ> tcbState) (ksCurThread s) s = (\<exists>tcb. cslift t (ksCurThread_' (globals t)) = Some tcb \<and> tsType_CL (thread_state_lift (tcbState_C tcb)) = SCAST(32 signed \<rightarrow> 32) ThreadState_Running) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs' s; cmap_relation (ctes_of s) (cslift t) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace s)) (cslift t) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace s)) (cslift t) ep_Ptr (cendpoint_relation (cslift t)); cmap_relation (map_to_ntfns (ksPSpace s)) (cslift t) ntfn_Ptr (cnotification_relation (cslift t)); cmap_relation (map_to_pdes (ksPSpace s)) (cslift t) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s)) (cslift t) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (cslift t) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift t) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift t) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s)) (c_h_t_valid t) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s)) (c_h_t_valid t) pt_Ptr; cready_queues_relation (cslift t) (ksReadyQueues_' (globals t)) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals t)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals t)) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals t)) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals t) = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals t) = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals t)); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals t)); carch_state_relation (ksArchState s) (globals t); cmachine_state_relation (ksMachineState s) (globals t); cte_array_relation s (globals t); tcb_cte_array_relation s (globals t); apsnd fst (ghost'state_' (globals t)) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals t)) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals t) = ksWorkUnitsCompleted s; t \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; t \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals t))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals t) = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals t) = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals t) = ksDomainTime s\<rbrakk> \<Longrightarrow> obj_at' ((\<lambda>st. st = Structures_H.thread_state.Running) \<circ> tcbState) (ksCurThread s) s = (\<exists>tcb. cslift t (tcb_ptr_to_ctcb_ptr (ksCurThread s)) = Some tcb \<and> tsType_CL (thread_state_lift (tcbState_C tcb)) = SCAST(32 signed \<rightarrow> 32) ThreadState_Running) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invs' s; cmap_relation (ctes_of s) (cslift t) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace s)) (cslift t) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace s)) (cslift t) ep_Ptr (cendpoint_relation (cslift t)); cmap_relation (map_to_ntfns (ksPSpace s)) (cslift t) ntfn_Ptr (cnotification_relation (cslift t)); cmap_relation (map_to_pdes (ksPSpace s)) (cslift t) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s)) (cslift t) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (cslift t) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift t) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift t) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s)) (c_h_t_valid t) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s)) (c_h_t_valid t) pt_Ptr; cready_queues_relation (cslift t) (ksReadyQueues_' (globals t)) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals t)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals t)) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals t)) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals t) = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals t) = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals t)); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals t)); carch_state_relation (ksArchState s) (globals t); cmachine_state_relation (ksMachineState s) (globals t); cte_array_relation s (globals t); tcb_cte_array_relation s (globals t); apsnd fst (ghost'state_' (globals t)) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals t)) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals t) = ksWorkUnitsCompleted s; t \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; t \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals t))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals t) = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals t) = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals t) = ksDomainTime s; obj_at' ((\<lambda>st. st = Structures_H.thread_state.Running) \<circ> tcbState) (ksCurThread s) s\<rbrakk> \<Longrightarrow> \<exists>tcb. cslift t (tcb_ptr_to_ctcb_ptr (ksCurThread s)) = Some tcb \<and> tsType_CL (thread_state_lift (tcbState_C tcb)) = SCAST(32 signed \<rightarrow> 32) ThreadState_Running
 2. \<lbrakk>invs' s; cmap_relation (ctes_of s) (cslift t) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace s)) (cslift t) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace s)) (cslift t) ep_Ptr (cendpoint_relation (cslift t)); cmap_relation (map_to_ntfns (ksPSpace s)) (cslift t) ntfn_Ptr (cnotification_relation (cslift t)); cmap_relation (map_to_pdes (ksPSpace s)) (cslift t) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s)) (cslift t) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (cslift t) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift t) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift t) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s)) (c_h_t_valid t) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s)) (c_h_t_valid t) pt_Ptr; cready_queues_relation (cslift t) (ksReadyQueues_' (globals t)) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals t)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals t)) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals t)) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals t) = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals t) = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals t)); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals t)); carch_state_relation (ksArchState s) (globals t); cmachine_state_relation (ksMachineState s) (globals t); cte_array_relation s (globals t); tcb_cte_array_relation s (globals t); apsnd fst (ghost'state_' (globals t)) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals t)) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals t) = ksWorkUnitsCompleted s; t \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; t \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals t))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals t) = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals t) = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals t) = ksDomainTime s; \<exists>tcb. cslift t (tcb_ptr_to_ctcb_ptr (ksCurThread s)) = Some tcb \<and> tsType_CL (thread_state_lift (tcbState_C tcb)) = SCAST(32 signed \<rightarrow> 32) ThreadState_Running\<rbrakk> \<Longrightarrow> obj_at' ((\<lambda>st. st = Structures_H.thread_state.Running) \<circ> tcbState) (ksCurThread s) s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invs' s; cmap_relation (ctes_of s) (cslift t) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace s)) (cslift t) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace s)) (cslift t) ep_Ptr (cendpoint_relation (cslift t)); cmap_relation (map_to_ntfns (ksPSpace s)) (cslift t) ntfn_Ptr (cnotification_relation (cslift t)); cmap_relation (map_to_pdes (ksPSpace s)) (cslift t) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s)) (cslift t) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (cslift t) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift t) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift t) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s)) (c_h_t_valid t) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s)) (c_h_t_valid t) pt_Ptr; cready_queues_relation (cslift t) (ksReadyQueues_' (globals t)) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals t)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals t)) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals t)) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals t) = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals t) = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals t)); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals t)); carch_state_relation (ksArchState s) (globals t); cmachine_state_relation (ksMachineState s) (globals t); cte_array_relation s (globals t); tcb_cte_array_relation s (globals t); apsnd fst (ghost'state_' (globals t)) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals t)) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals t) = ksWorkUnitsCompleted s; t \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; t \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals t))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals t) = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals t) = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals t) = ksDomainTime s; \<exists>ko. ko_at' ko (ksCurThread s) s \<and> ((\<lambda>st. st = Structures_H.thread_state.Running) \<circ> tcbState) ko\<rbrakk> \<Longrightarrow> \<exists>tcb. cslift t (tcb_ptr_to_ctcb_ptr (ksCurThread s)) = Some tcb \<and> tsType_CL (thread_state_lift (tcbState_C tcb)) = SCAST(32 signed \<rightarrow> 32) ThreadState_Running
 2. \<lbrakk>invs' s; cmap_relation (ctes_of s) (cslift t) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace s)) (cslift t) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace s)) (cslift t) ep_Ptr (cendpoint_relation (cslift t)); cmap_relation (map_to_ntfns (ksPSpace s)) (cslift t) ntfn_Ptr (cnotification_relation (cslift t)); cmap_relation (map_to_pdes (ksPSpace s)) (cslift t) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s)) (cslift t) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (cslift t) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift t) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift t) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s)) (c_h_t_valid t) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s)) (c_h_t_valid t) pt_Ptr; cready_queues_relation (cslift t) (ksReadyQueues_' (globals t)) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals t)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals t)) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals t)) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals t) = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals t) = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals t)); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals t)); carch_state_relation (ksArchState s) (globals t); cmachine_state_relation (ksMachineState s) (globals t); cte_array_relation s (globals t); tcb_cte_array_relation s (globals t); apsnd fst (ghost'state_' (globals t)) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals t)) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals t) = ksWorkUnitsCompleted s; t \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; t \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals t))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals t) = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals t) = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals t) = ksDomainTime s; \<exists>tcb. cslift t (tcb_ptr_to_ctcb_ptr (ksCurThread s)) = Some tcb \<and> tsType_CL (thread_state_lift (tcbState_C tcb)) = SCAST(32 signed \<rightarrow> 32) ThreadState_Running\<rbrakk> \<Longrightarrow> obj_at' ((\<lambda>st. st = Structures_H.thread_state.Running) \<circ> tcbState) (ksCurThread s) s proof (prove)
goal (2 subgoals):
 1. \<And>ko. \<lbrakk>invs' s; cmap_relation (ctes_of s) (cslift t) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace s)) (cslift t) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace s)) (cslift t) ep_Ptr (cendpoint_relation (cslift t)); cmap_relation (map_to_ntfns (ksPSpace s)) (cslift t) ntfn_Ptr (cnotification_relation (cslift t)); cmap_relation (map_to_pdes (ksPSpace s)) (cslift t) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s)) (cslift t) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (cslift t) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift t) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift t) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s)) (c_h_t_valid t) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s)) (c_h_t_valid t) pt_Ptr; cready_queues_relation (cslift t) (ksReadyQueues_' (globals t)) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals t)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals t)) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals t)) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals t) = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals t) = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals t)); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals t)); carch_state_relation (ksArchState s) (globals t); cmachine_state_relation (ksMachineState s) (globals t); cte_array_relation s (globals t); tcb_cte_array_relation s (globals t); apsnd fst (ghost'state_' (globals t)) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals t)) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals t) = ksWorkUnitsCompleted s; t \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; t \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals t))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals t) = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals t) = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals t) = ksDomainTime s; ko_at' ko (ksCurThread s) s; tcbState ko = Structures_H.thread_state.Running\<rbrakk> \<Longrightarrow> \<exists>tcb. cslift t (tcb_ptr_to_ctcb_ptr (ksCurThread s)) = Some tcb \<and> tsType_CL (thread_state_lift (tcbState_C tcb)) = SCAST(32 signed \<rightarrow> 32) ThreadState_Running
 2. \<lbrakk>invs' s; cmap_relation (ctes_of s) (cslift t) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace s)) (cslift t) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace s)) (cslift t) ep_Ptr (cendpoint_relation (cslift t)); cmap_relation (map_to_ntfns (ksPSpace s)) (cslift t) ntfn_Ptr (cnotification_relation (cslift t)); cmap_relation (map_to_pdes (ksPSpace s)) (cslift t) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s)) (cslift t) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (cslift t) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift t) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift t) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s)) (c_h_t_valid t) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s)) (c_h_t_valid t) pt_Ptr; cready_queues_relation (cslift t) (ksReadyQueues_' (globals t)) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals t)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals t)) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals t)) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals t) = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals t) = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals t)); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals t)); carch_state_relation (ksArchState s) (globals t); cmachine_state_relation (ksMachineState s) (globals t); cte_array_relation s (globals t); tcb_cte_array_relation s (globals t); apsnd fst (ghost'state_' (globals t)) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals t)) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals t) = ksWorkUnitsCompleted s; t \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; t \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals t))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals t) = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals t) = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals t) = ksDomainTime s; \<exists>tcb. cslift t (tcb_ptr_to_ctcb_ptr (ksCurThread s)) = Some tcb \<and> tsType_CL (thread_state_lift (tcbState_C tcb)) = SCAST(32 signed \<rightarrow> 32) ThreadState_Running\<rbrakk> \<Longrightarrow> obj_at' ((\<lambda>st. st = Structures_H.thread_state.Running) \<circ> tcbState) (ksCurThread s) s proof (prove)
goal (2 subgoals):
 1. \<And>ko ko'. \<lbrakk>invs' s; cmap_relation (ctes_of s) (cslift t) cte_Ptr ccte_relation; cmap_relation (map_to_eps (ksPSpace s)) (cslift t) ep_Ptr (cendpoint_relation (cslift t)); cmap_relation (map_to_ntfns (ksPSpace s)) (cslift t) ntfn_Ptr (cnotification_relation (cslift t)); cmap_relation (map_to_pdes (ksPSpace s)) (cslift t) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s)) (cslift t) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (cslift t) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift t) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift t) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s)) (c_h_t_valid t) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s)) (c_h_t_valid t) pt_Ptr; cready_queues_relation (cslift t) (ksReadyQueues_' (globals t)) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals t)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals t)) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals t)) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals t) = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals t) = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals t)); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals t)); carch_state_relation (ksArchState s) (globals t); cmachine_state_relation (ksMachineState s) (globals t); cte_array_relation s (globals t); tcb_cte_array_relation s (globals t); apsnd fst (ghost'state_' (globals t)) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals t)) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals t) = ksWorkUnitsCompleted s; t \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; t \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals t))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals t) = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals t) = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals t) = ksDomainTime s; ko_at' ko (ksCurThread s) s; tcbState ko = Structures_H.thread_state.Running; cslift t (tcb_ptr_to_ctcb_ptr (ksCurThread s)) = Some ko'; ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> \<exists>tcb. cslift t (tcb_ptr_to_ctcb_ptr (ksCurThread s)) = Some tcb \<and> tsType_CL (thread_state_lift (tcbState_C tcb)) = SCAST(32 signed \<rightarrow> 32) ThreadState_Running
 2. \<lbrakk>invs' s; cmap_relation (ctes_of s) (cslift t) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace s)) (cslift t) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace s)) (cslift t) ep_Ptr (cendpoint_relation (cslift t)); cmap_relation (map_to_ntfns (ksPSpace s)) (cslift t) ntfn_Ptr (cnotification_relation (cslift t)); cmap_relation (map_to_pdes (ksPSpace s)) (cslift t) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s)) (cslift t) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (cslift t) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift t) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift t) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s)) (c_h_t_valid t) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s)) (c_h_t_valid t) pt_Ptr; cready_queues_relation (cslift t) (ksReadyQueues_' (globals t)) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals t)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals t)) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals t)) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals t) = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals t) = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals t)); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals t)); carch_state_relation (ksArchState s) (globals t); cmachine_state_relation (ksMachineState s) (globals t); cte_array_relation s (globals t); tcb_cte_array_relation s (globals t); apsnd fst (ghost'state_' (globals t)) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals t)) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals t) = ksWorkUnitsCompleted s; t \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; t \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals t))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals t) = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals t) = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals t) = ksDomainTime s; \<exists>tcb. cslift t (tcb_ptr_to_ctcb_ptr (ksCurThread s)) = Some tcb \<and> tsType_CL (thread_state_lift (tcbState_C tcb)) = SCAST(32 signed \<rightarrow> 32) ThreadState_Running\<rbrakk> \<Longrightarrow> obj_at' ((\<lambda>st. st = Structures_H.thread_state.Running) \<circ> tcbState) (ksCurThread s) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs' s; cmap_relation (ctes_of s) (cslift t) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace s)) (cslift t) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace s)) (cslift t) ep_Ptr (cendpoint_relation (cslift t)); cmap_relation (map_to_ntfns (ksPSpace s)) (cslift t) ntfn_Ptr (cnotification_relation (cslift t)); cmap_relation (map_to_pdes (ksPSpace s)) (cslift t) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s)) (cslift t) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (cslift t) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift t) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift t) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s)) (c_h_t_valid t) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s)) (c_h_t_valid t) pt_Ptr; cready_queues_relation (cslift t) (ksReadyQueues_' (globals t)) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals t)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals t)) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals t)) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals t) = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals t) = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals t)); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals t)); carch_state_relation (ksArchState s) (globals t); cmachine_state_relation (ksMachineState s) (globals t); cte_array_relation s (globals t); tcb_cte_array_relation s (globals t); apsnd fst (ghost'state_' (globals t)) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals t)) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals t) = ksWorkUnitsCompleted s; t \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; t \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals t))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals t) = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals t) = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals t) = ksDomainTime s; \<exists>tcb. cslift t (tcb_ptr_to_ctcb_ptr (ksCurThread s)) = Some tcb \<and> tsType_CL (thread_state_lift (tcbState_C tcb)) = SCAST(32 signed \<rightarrow> 32) ThreadState_Running\<rbrakk> \<Longrightarrow> obj_at' ((\<lambda>st. st = Structures_H.thread_state.Running) \<circ> tcbState) (ksCurThread s) s proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>invs' s; cmap_relation (ctes_of s) (cslift t) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace s)) (cslift t) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace s)) (cslift t) ep_Ptr (cendpoint_relation (cslift t)); cmap_relation (map_to_ntfns (ksPSpace s)) (cslift t) ntfn_Ptr (cnotification_relation (cslift t)); cmap_relation (map_to_pdes (ksPSpace s)) (cslift t) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s)) (cslift t) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (cslift t) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift t) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift t) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s)) (c_h_t_valid t) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s)) (c_h_t_valid t) pt_Ptr; cready_queues_relation (cslift t) (ksReadyQueues_' (globals t)) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals t)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals t)) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals t)) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals t) = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals t) = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals t)); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals t)); carch_state_relation (ksArchState s) (globals t); cmachine_state_relation (ksMachineState s) (globals t); cte_array_relation s (globals t); tcb_cte_array_relation s (globals t); apsnd fst (ghost'state_' (globals t)) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals t)) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals t) = ksWorkUnitsCompleted s; t \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; t \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals t))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals t) = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals t) = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals t) = ksDomainTime s; cslift t (tcb_ptr_to_ctcb_ptr (ksCurThread s)) = Some tcb; tsType_CL (thread_state_lift (tcbState_C tcb)) = SCAST(32 signed \<rightarrow> 32) ThreadState_Running\<rbrakk> \<Longrightarrow> obj_at' ((\<lambda>st. st = Structures_H.thread_state.Running) \<circ> tcbState) (ksCurThread s) s proof (prove)
goal (2 subgoals):
 1. \<And>tcb. \<lbrakk>invs' s; cmap_relation (ctes_of s) (cslift t) cte_Ptr ccte_relation; cmap_relation (map_to_eps (ksPSpace s)) (cslift t) ep_Ptr (cendpoint_relation (cslift t)); cmap_relation (map_to_ntfns (ksPSpace s)) (cslift t) ntfn_Ptr (cnotification_relation (cslift t)); cmap_relation (map_to_pdes (ksPSpace s)) (cslift t) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s)) (cslift t) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (cslift t) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift t) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift t) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s)) (c_h_t_valid t) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s)) (c_h_t_valid t) pt_Ptr; cready_queues_relation (cslift t) (ksReadyQueues_' (globals t)) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals t)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals t)) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals t)) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals t) = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals t) = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals t)); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals t)); carch_state_relation (ksArchState s) (globals t); cmachine_state_relation (ksMachineState s) (globals t); cte_array_relation s (globals t); tcb_cte_array_relation s (globals t); apsnd fst (ghost'state_' (globals t)) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals t)) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals t) = ksWorkUnitsCompleted s; t \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; t \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals t))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals t) = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals t) = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals t) = ksDomainTime s; cslift t (tcb_ptr_to_ctcb_ptr (ksCurThread s)) = Some tcb; tsType_CL (thread_state_lift (tcbState_C tcb)) = SCAST(32 signed \<rightarrow> 32) ThreadState_Running\<rbrakk> \<Longrightarrow> inj tcb_ptr_to_ctcb_ptr
 2. \<And>tcb. \<lbrakk>invs' s; cmap_relation (ctes_of s) (cslift t) cte_Ptr ccte_relation; cmap_relation (map_to_eps (ksPSpace s)) (cslift t) ep_Ptr (cendpoint_relation (cslift t)); cmap_relation (map_to_ntfns (ksPSpace s)) (cslift t) ntfn_Ptr (cnotification_relation (cslift t)); cmap_relation (map_to_pdes (ksPSpace s)) (cslift t) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s)) (cslift t) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (cslift t) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift t) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift t) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s)) (c_h_t_valid t) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s)) (c_h_t_valid t) pt_Ptr; cready_queues_relation (cslift t) (ksReadyQueues_' (globals t)) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals t)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals t)) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals t)) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals t) = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals t) = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals t)); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals t)); carch_state_relation (ksArchState s) (globals t); cmachine_state_relation (ksMachineState s) (globals t); cte_array_relation s (globals t); tcb_cte_array_relation s (globals t); apsnd fst (ghost'state_' (globals t)) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals t)) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals t) = ksWorkUnitsCompleted s; t \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; t \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals t))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals t) = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals t) = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals t) = ksDomainTime s; cslift t (tcb_ptr_to_ctcb_ptr (ksCurThread s)) = Some tcb; tsType_CL (thread_state_lift (tcbState_C tcb)) = SCAST(32 signed \<rightarrow> 32) ThreadState_Running; \<exists>ko. map_to_tcbs (ksPSpace s) (ksCurThread s) = Some ko \<and> ctcb_relation ko tcb\<rbrakk> \<Longrightarrow> obj_at' ((\<lambda>st. st = Structures_H.thread_state.Running) \<circ> tcbState) (ksCurThread s) s proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>invs' s; cmap_relation (ctes_of s) (cslift t) cte_Ptr ccte_relation; cmap_relation (map_to_eps (ksPSpace s)) (cslift t) ep_Ptr (cendpoint_relation (cslift t)); cmap_relation (map_to_ntfns (ksPSpace s)) (cslift t) ntfn_Ptr (cnotification_relation (cslift t)); cmap_relation (map_to_pdes (ksPSpace s)) (cslift t) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s)) (cslift t) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (cslift t) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift t) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift t) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s)) (c_h_t_valid t) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s)) (c_h_t_valid t) pt_Ptr; cready_queues_relation (cslift t) (ksReadyQueues_' (globals t)) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals t)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals t)) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals t)) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals t) = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals t) = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals t)); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals t)); carch_state_relation (ksArchState s) (globals t); cmachine_state_relation (ksMachineState s) (globals t); cte_array_relation s (globals t); tcb_cte_array_relation s (globals t); apsnd fst (ghost'state_' (globals t)) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals t)) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals t) = ksWorkUnitsCompleted s; t \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; t \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals t))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals t) = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals t) = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals t) = ksDomainTime s; cslift t (tcb_ptr_to_ctcb_ptr (ksCurThread s)) = Some tcb; tsType_CL (thread_state_lift (tcbState_C tcb)) = SCAST(32 signed \<rightarrow> 32) ThreadState_Running; \<exists>ko. map_to_tcbs (ksPSpace s) (ksCurThread s) = Some ko \<and> ctcb_relation ko tcb\<rbrakk> \<Longrightarrow> obj_at' ((\<lambda>st. st = Structures_H.thread_state.Running) \<circ> tcbState) (ksCurThread s) s proof (prove)
goal (1 subgoal):
 1. \<And>tcb ko. \<lbrakk>invs' s; cmap_relation (ctes_of s) (cslift t) cte_Ptr ccte_relation; cmap_relation (map_to_eps (ksPSpace s)) (cslift t) ep_Ptr (cendpoint_relation (cslift t)); cmap_relation (map_to_ntfns (ksPSpace s)) (cslift t) ntfn_Ptr (cnotification_relation (cslift t)); cmap_relation (map_to_pdes (ksPSpace s)) (cslift t) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s)) (cslift t) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (cslift t) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift t) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift t) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s)) (c_h_t_valid t) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s)) (c_h_t_valid t) pt_Ptr; cready_queues_relation (cslift t) (ksReadyQueues_' (globals t)) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals t)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals t)) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals t)) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals t) = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals t) = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals t)); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals t)); carch_state_relation (ksArchState s) (globals t); cmachine_state_relation (ksMachineState s) (globals t); cte_array_relation s (globals t); tcb_cte_array_relation s (globals t); apsnd fst (ghost'state_' (globals t)) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals t)) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals t) = ksWorkUnitsCompleted s; t \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; t \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals t))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals t) = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals t) = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals t) = ksDomainTime s; cslift t (tcb_ptr_to_ctcb_ptr (ksCurThread s)) = Some tcb; tsType_CL (thread_state_lift (tcbState_C tcb)) = SCAST(32 signed \<rightarrow> 32) ThreadState_Running; map_to_tcbs (ksPSpace s) (ksCurThread s) = Some ko; ctcb_relation ko tcb\<rbrakk> \<Longrightarrow> obj_at' ((\<lambda>st. st = Structures_H.thread_state.Running) \<circ> tcbState) (ksCurThread s) s proof (prove)
goal (1 subgoal):
 1. \<And>tcb ko. \<lbrakk>invs' s; cmap_relation (ctes_of s) (cslift t) cte_Ptr ccte_relation; cmap_relation (map_to_eps (ksPSpace s)) (cslift t) ep_Ptr (cendpoint_relation (cslift t)); cmap_relation (map_to_ntfns (ksPSpace s)) (cslift t) ntfn_Ptr (cnotification_relation (cslift t)); cmap_relation (map_to_pdes (ksPSpace s)) (cslift t) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s)) (cslift t) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (cslift t) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift t) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift t) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s)) (c_h_t_valid t) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s)) (c_h_t_valid t) pt_Ptr; cready_queues_relation (cslift t) (ksReadyQueues_' (globals t)) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals t)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals t)) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals t)) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals t) = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals t) = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals t)); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals t)); carch_state_relation (ksArchState s) (globals t); cmachine_state_relation (ksMachineState s) (globals t); cte_array_relation s (globals t); tcb_cte_array_relation s (globals t); apsnd fst (ghost'state_' (globals t)) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals t)) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals t) = ksWorkUnitsCompleted s; t \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; t \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals t))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals t) = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals t) = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals t) = ksDomainTime s; cslift t (tcb_ptr_to_ctcb_ptr (ksCurThread s)) = Some tcb; tsType_CL (thread_state_lift (tcbState_C tcb)) = SCAST(32 signed \<rightarrow> 32) ThreadState_Running; map_to_tcbs (ksPSpace s) (ksCurThread s) = Some ko; ctcb_relation ko tcb; ko_at' ko (ksCurThread s) s\<rbrakk> \<Longrightarrow> obj_at' ((\<lambda>st. st = Structures_H.thread_state.Running) \<circ> tcbState) (ksCurThread s) s proof (prove)
goal (1 subgoal):
 1. \<And>tcb ko k. \<lbrakk>invs' s; cmap_relation (ctes_of s) (cslift t) cte_Ptr ccte_relation; cmap_relation (map_to_eps (ksPSpace s)) (cslift t) ep_Ptr (cendpoint_relation (cslift t)); cmap_relation (map_to_ntfns (ksPSpace s)) (cslift t) ntfn_Ptr (cnotification_relation (cslift t)); cmap_relation (map_to_pdes (ksPSpace s)) (cslift t) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s)) (cslift t) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (cslift t) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift t) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift t) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s)) (c_h_t_valid t) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s)) (c_h_t_valid t) pt_Ptr; cready_queues_relation (cslift t) (ksReadyQueues_' (globals t)) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals t)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals t)) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals t)) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals t) = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals t) = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals t)); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals t)); carch_state_relation (ksArchState s) (globals t); cmachine_state_relation (ksMachineState s) (globals t); cte_array_relation s (globals t); tcb_cte_array_relation s (globals t); apsnd fst (ghost'state_' (globals t)) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals t)) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals t) = ksWorkUnitsCompleted s; t \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; t \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals t))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals t) = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals t) = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals t) = ksDomainTime s; cslift t (tcb_ptr_to_ctcb_ptr (ksCurThread s)) = Some tcb; tsType_CL (thread_state_lift (tcbState_C tcb)) = SCAST(32 signed \<rightarrow> 32) ThreadState_Running; map_to_tcbs (ksPSpace s) (ksCurThread s) = Some ko; ctcb_relation ko tcb; k = ko\<rbrakk> \<Longrightarrow> ((\<lambda>st. st = Structures_H.thread_state.Running) \<circ> tcbState) k proof (prove)
goal (1 subgoal):
 1. \<And>tcb ko. \<lbrakk>invs' s; cmap_relation (ctes_of s) (cslift t) cte_Ptr ccte_relation; cmap_relation (map_to_eps (ksPSpace s)) (cslift t) ep_Ptr (cendpoint_relation (cslift t)); cmap_relation (map_to_ntfns (ksPSpace s)) (cslift t) ntfn_Ptr (cnotification_relation (cslift t)); cmap_relation (map_to_pdes (ksPSpace s)) (cslift t) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s)) (cslift t) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (cslift t) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift t) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift t) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s)) (c_h_t_valid t) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s)) (c_h_t_valid t) pt_Ptr; cready_queues_relation (cslift t) (ksReadyQueues_' (globals t)) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals t)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals t)) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals t)) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals t) = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals t) = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals t)); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals t)); carch_state_relation (ksArchState s) (globals t); cmachine_state_relation (ksMachineState s) (globals t); cte_array_relation s (globals t); tcb_cte_array_relation s (globals t); apsnd fst (ghost'state_' (globals t)) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals t)) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals t) = ksWorkUnitsCompleted s; t \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; t \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals t))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals t) = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals t) = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals t) = ksDomainTime s; cslift t (tcb_ptr_to_ctcb_ptr (ksCurThread s)) = Some tcb; tsType_CL (thread_state_lift (tcbState_C tcb)) = SCAST(32 signed \<rightarrow> 32) ThreadState_Running; map_to_tcbs (ksPSpace s) (ksCurThread s) = Some ko; tcbFaultHandler ko = tcbFaultHandler_C tcb; cthread_state_relation_lifted (tcbState ko) (thread_state_lift (tcbState_C tcb), seL4_Fault_lift (tcbFault_C tcb)); tcbIPCBuffer ko = tcbIPCBuffer_C tcb; carch_tcb_relation (tcbArch ko) (tcbArch_C tcb); tcbQueued ko = to_bool (tcbQueued_CL (thread_state_lift (tcbState_C tcb))); UCAST(8 \<rightarrow> 32) (tcbDomain ko) = tcbDomain_C tcb; UCAST(8 \<rightarrow> 32) (tcbPriority ko) = tcbPriority_C tcb; UCAST(8 \<rightarrow> 32) (tcbMCP ko) = tcbMCP_C tcb; tcbTimeSlice ko = unat (tcbTimeSlice_C tcb); cfault_rel (tcbFault ko) (seL4_Fault_lift (tcbFault_C tcb)) (lookup_fault_lift (tcbLookupFailure_C tcb)); option_to_ptr (tcbBoundNotification ko) = tcbBoundNotification_C tcb\<rbrakk> \<Longrightarrow> tcbState ko = Structures_H.thread_state.Running proof (prove)
goal:
No subgoals!