theory Finalise_C

lemma tcbSchedEnqueue_cslift_precond_discharge:
  "\<lbrakk> (s, s') \<in> rf_sr; obj_at' (P :: tcb \<Rightarrow> bool) x s;
        valid_queues s; valid_objs' s \<rbrakk> \<Longrightarrow>
   (\<exists>d v. option_map2 tcbPriority_C (cslift s') (tcb_ptr_to_ctcb_ptr x) = Some v
        \<and> unat v < numPriorities
        \<and> option_map2 tcbDomain_C (cslift s') (tcb_ptr_to_ctcb_ptr x) = Some d
        \<and> unat d < Kernel_Config.numDomains
        \<and> (end_C (index (ksReadyQueues_' (globals s')) (unat (d*0x100 + v))) \<noteq> NULL
                \<longrightarrow> option_map2 tcbPriority_C (cslift s')
                     (head_C (index (ksReadyQueues_' (globals s')) (unat (d*0x100 + v))))
                                    \<noteq> None
                  \<and> option_map2 tcbDomain_C (cslift s')
                     (head_C (index (ksReadyQueues_' (globals s')) (unat (d*0x100 + v))))
                                    \<noteq> None))" apply (drule(1) obj_at_cslift_tcb) apply (clarsimp simp: typ_heap_simps' option_map2_def) apply (frule_tac t=x in valid_objs'_maxPriority, fastforce simp: obj_at'_def) apply (frule_tac t=x in valid_objs'_maxDomain, fastforce simp: obj_at'_def) apply (drule_tac P="\<lambda>tcb. tcbPriority tcb \<le> maxPriority" in obj_at_ko_at2', simp) apply (drule_tac P="\<lambda>tcb. tcbDomain tcb \<le> maxDomain" in obj_at_ko_at2', simp) apply (simp add: ctcb_relation_tcbDomain_maxDomain_numDomains
                   ctcb_relation_tcbPriority_maxPriority_numPriorities) apply (frule_tac d="tcbDomain ko" and p="tcbPriority ko"
              in rf_sr_sched_queue_relation) apply (simp add: maxDom_to_H maxPrio_to_H)+ apply (simp add: cready_queues_index_to_C_def2 numPriorities_def le_maxDomain_eq_less_numDomains) apply (clarsimp simp: ctcb_relation_def) apply (frule arg_cong[where f=unat], subst(asm) unat_ucast_8_32) apply (frule tcb_queue'_head_end_NULL) apply (erule conjunct1[OF valid_queues_valid_q]) apply (frule(1) tcb_queue_relation_qhead_valid') apply (simp add: valid_queues_valid_q) apply (clarsimp simp: h_t_valid_clift_Some_iff) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> rf_sr; obj_at' P x s; Invariants_H.valid_queues s; valid_objs' s\<rbrakk> \<Longrightarrow> \<exists>d v. option_map2 tcbPriority_C (cslift s') (tcb_ptr_to_ctcb_ptr x) = Some v \<and> unat v < Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift s') (tcb_ptr_to_ctcb_ptr x) = Some d \<and> unat d < numDomains \<and> (StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> option_map2 tcbPriority_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) \<noteq> None \<and> option_map2 tcbDomain_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) \<noteq> None) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> rf_sr; Invariants_H.valid_queues s; valid_objs' s; \<exists>ko ko'. ko_at' ko x s \<and> P ko \<and> cslift s' (tcb_ptr_to_ctcb_ptr x) = Some ko' \<and> ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> \<exists>d v. option_map2 tcbPriority_C (cslift s') (tcb_ptr_to_ctcb_ptr x) = Some v \<and> unat v < Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift s') (tcb_ptr_to_ctcb_ptr x) = Some d \<and> unat d < numDomains \<and> (StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> option_map2 tcbPriority_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) \<noteq> None \<and> option_map2 tcbDomain_C (cslift s') (head_C (ksReadyQueues_' (globals s').[unat (d * 0x100 + v)])) \<noteq> None) proof (prove)
goal (1 subgoal):
 1. \<And>ko ko'. \<lbrakk>(s, s') \<in> rf_sr; Invariants_H.valid_queues s; valid_objs' s; ko_at' ko x s; P ko; cslift s' (tcb_ptr_to_ctcb_ptr x) = Some ko'; ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> unat (tcbPriority_C ko') < Config_H.numPriorities \<and> unat (tcbDomain_C ko') < numDomains \<and> (StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')]) \<noteq> NULL \<longrightarrow> (\<exists>y. cslift s' (head_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')])) = Some y)) proof (prove)
goal (1 subgoal):
 1. \<And>ko ko'. \<lbrakk>(s, s') \<in> rf_sr; Invariants_H.valid_queues s; valid_objs' s; ko_at' ko x s; P ko; cslift s' (tcb_ptr_to_ctcb_ptr x) = Some ko'; ctcb_relation ko ko'; obj_at' (\<lambda>tcb. tcbPriority tcb \<le> maxPriority) x s\<rbrakk> \<Longrightarrow> unat (tcbPriority_C ko') < Config_H.numPriorities \<and> unat (tcbDomain_C ko') < numDomains \<and> (StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')]) \<noteq> NULL \<longrightarrow> (\<exists>y. cslift s' (head_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')])) = Some y)) proof (prove)
goal (1 subgoal):
 1. \<And>ko ko'. \<lbrakk>(s, s') \<in> rf_sr; Invariants_H.valid_queues s; valid_objs' s; ko_at' ko x s; P ko; cslift s' (tcb_ptr_to_ctcb_ptr x) = Some ko'; ctcb_relation ko ko'; obj_at' (\<lambda>tcb. tcbPriority tcb \<le> maxPriority) x s; obj_at' (\<lambda>tcb. tcbDomain tcb \<le> maxDomain) x s\<rbrakk> \<Longrightarrow> unat (tcbPriority_C ko') < Config_H.numPriorities \<and> unat (tcbDomain_C ko') < numDomains \<and> (StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')]) \<noteq> NULL \<longrightarrow> (\<exists>y. cslift s' (head_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')])) = Some y)) proof (prove)
goal (1 subgoal):
 1. \<And>ko ko'. \<lbrakk>(s, s') \<in> rf_sr; Invariants_H.valid_queues s; valid_objs' s; ko_at' ko x s; P ko; cslift s' (tcb_ptr_to_ctcb_ptr x) = Some ko'; ctcb_relation ko ko'; obj_at' (\<lambda>tcb. tcbDomain tcb \<le> maxDomain) x s; tcbPriority ko \<le> maxPriority\<rbrakk> \<Longrightarrow> unat (tcbPriority_C ko') < Config_H.numPriorities \<and> unat (tcbDomain_C ko') < numDomains \<and> (StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')]) \<noteq> NULL \<longrightarrow> (\<exists>y. cslift s' (head_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')])) = Some y)) proof (prove)
goal (1 subgoal):
 1. \<And>ko ko'. \<lbrakk>(s, s') \<in> rf_sr; Invariants_H.valid_queues s; valid_objs' s; ko_at' ko x s; P ko; cslift s' (tcb_ptr_to_ctcb_ptr x) = Some ko'; ctcb_relation ko ko'; tcbPriority ko \<le> maxPriority; tcbDomain ko \<le> maxDomain\<rbrakk> \<Longrightarrow> unat (tcbPriority_C ko') < Config_H.numPriorities \<and> unat (tcbDomain_C ko') < numDomains \<and> (StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')]) \<noteq> NULL \<longrightarrow> (\<exists>y. cslift s' (head_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')])) = Some y)) proof (prove)
goal (1 subgoal):
 1. \<And>ko ko'. \<lbrakk>(s, s') \<in> rf_sr; Invariants_H.valid_queues s; valid_objs' s; ko_at' ko x s; P ko; cslift s' (tcb_ptr_to_ctcb_ptr x) = Some ko'; ctcb_relation ko ko'; tcbPriority ko \<le> maxPriority; tcbDomain ko \<le> maxDomain\<rbrakk> \<Longrightarrow> StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')]) \<noteq> NULL \<longrightarrow> (\<exists>y. cslift s' (head_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')])) = Some y) proof (prove)
goal (3 subgoals):
 1. \<And>ko ko'. \<lbrakk>(s, s') \<in> rf_sr; Invariants_H.valid_queues s; valid_objs' s; ko_at' ko x s; P ko; cslift s' (tcb_ptr_to_ctcb_ptr x) = Some ko'; ctcb_relation ko ko'; tcbPriority ko \<le> maxPriority; tcbDomain ko \<le> maxDomain\<rbrakk> \<Longrightarrow> tcbDomain ko \<le> UCAST(32 signed \<rightarrow> 8) maxDom
 2. \<And>ko ko'. \<lbrakk>(s, s') \<in> rf_sr; Invariants_H.valid_queues s; valid_objs' s; ko_at' ko x s; P ko; cslift s' (tcb_ptr_to_ctcb_ptr x) = Some ko'; ctcb_relation ko ko'; tcbPriority ko \<le> maxPriority; tcbDomain ko \<le> maxDomain\<rbrakk> \<Longrightarrow> tcbPriority ko \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio
 3. \<And>ko ko'. \<lbrakk>(s, s') \<in> rf_sr; Invariants_H.valid_queues s; valid_objs' s; ko_at' ko x s; P ko; cslift s' (tcb_ptr_to_ctcb_ptr x) = Some ko'; ctcb_relation ko ko'; tcbPriority ko \<le> maxPriority; tcbDomain ko \<le> maxDomain; sched_queue_relation' (cslift s') (ksReadyQueues s (tcbDomain ko, tcbPriority ko)) (head_C (ksReadyQueues_' (globals s').[cready_queues_index_to_C (tcbDomain ko) (tcbPriority ko)])) (StateRelation_C.end_C (ksReadyQueues_' (globals s').[cready_queues_index_to_C (tcbDomain ko) (tcbPriority ko)]))\<rbrakk> \<Longrightarrow> StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')]) \<noteq> NULL \<longrightarrow> (\<exists>y. cslift s' (head_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')])) = Some y) proof (prove)
goal (1 subgoal):
 1. \<And>ko ko'. \<lbrakk>(s, s') \<in> rf_sr; Invariants_H.valid_queues s; valid_objs' s; ko_at' ko x s; P ko; cslift s' (tcb_ptr_to_ctcb_ptr x) = Some ko'; ctcb_relation ko ko'; tcbPriority ko \<le> maxPriority; tcbDomain ko \<le> maxDomain; sched_queue_relation' (cslift s') (ksReadyQueues s (tcbDomain ko, tcbPriority ko)) (head_C (ksReadyQueues_' (globals s').[cready_queues_index_to_C (tcbDomain ko) (tcbPriority ko)])) (StateRelation_C.end_C (ksReadyQueues_' (globals s').[cready_queues_index_to_C (tcbDomain ko) (tcbPriority ko)]))\<rbrakk> \<Longrightarrow> StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')]) \<noteq> NULL \<longrightarrow> (\<exists>y. cslift s' (head_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')])) = Some y) proof (prove)
goal (1 subgoal):
 1. \<And>ko ko'. \<lbrakk>(s, s') \<in> rf_sr; Invariants_H.valid_queues s; valid_objs' s; ko_at' ko x s; P ko; cslift s' (tcb_ptr_to_ctcb_ptr x) = Some ko'; ctcb_relation ko ko'; tcbPriority ko \<le> maxPriority; unat (tcbDomain ko) < numDomains; sched_queue_relation' (cslift s') (ksReadyQueues s (tcbDomain ko, tcbPriority ko)) (head_C (ksReadyQueues_' (globals s').[unat (UCAST(8 \<rightarrow> 32) (tcbDomain ko) * 0x100 + UCAST(8 \<rightarrow> 32) (tcbPriority ko))])) (StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (UCAST(8 \<rightarrow> 32) (tcbDomain ko) * 0x100 + UCAST(8 \<rightarrow> 32) (tcbPriority ko))]))\<rbrakk> \<Longrightarrow> StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')]) \<noteq> NULL \<longrightarrow> (\<exists>y. cslift s' (head_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')])) = Some y) proof (prove)
goal (1 subgoal):
 1. \<And>ko ko'. \<lbrakk>(s, s') \<in> rf_sr; Invariants_H.valid_queues s; valid_objs' s; ko_at' ko x s; P ko; cslift s' (tcb_ptr_to_ctcb_ptr x) = Some ko'; tcbPriority ko \<le> maxPriority; unat (tcbDomain ko) < numDomains; sched_queue_relation' (cslift s') (ksReadyQueues s (tcbDomain ko, tcbPriority ko)) (head_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')])) (StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')])); tcbFaultHandler ko = tcbFaultHandler_C ko'; cthread_state_relation (tcbState ko) (tcbState_C ko', tcbFault_C ko'); tcbIPCBuffer ko = tcbIPCBuffer_C ko'; carch_tcb_relation (tcbArch ko) (tcbArch_C ko'); tcbQueued ko = to_bool (tcbQueued_CL (thread_state_lift (tcbState_C ko'))); UCAST(8 \<rightarrow> 32) (tcbDomain ko) = tcbDomain_C ko'; UCAST(8 \<rightarrow> 32) (tcbPriority ko) = tcbPriority_C ko'; UCAST(8 \<rightarrow> 32) (tcbMCP ko) = tcbMCP_C ko'; tcbTimeSlice ko = unat (tcbTimeSlice_C ko'); cfault_rel (tcbFault ko) (seL4_Fault_lift (tcbFault_C ko')) (lookup_fault_lift (tcbLookupFailure_C ko')); option_to_ptr (tcbBoundNotification ko) = tcbBoundNotification_C ko'; StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')]) \<noteq> NULL\<rbrakk> \<Longrightarrow> \<exists>y. cslift s' (head_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')])) = Some y proof (prove)
goal (1 subgoal):
 1. \<And>ko ko'. \<lbrakk>(s, s') \<in> rf_sr; Invariants_H.valid_queues s; valid_objs' s; ko_at' ko x s; P ko; cslift s' (tcb_ptr_to_ctcb_ptr x) = Some ko'; tcbPriority ko \<le> maxPriority; unat (tcbDomain ko) < numDomains; sched_queue_relation' (cslift s') (ksReadyQueues s (tcbDomain ko, tcbPriority ko)) (head_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')])) (StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')])); tcbFaultHandler ko = tcbFaultHandler_C ko'; cthread_state_relation (tcbState ko) (tcbState_C ko', tcbFault_C ko'); tcbIPCBuffer ko = tcbIPCBuffer_C ko'; carch_tcb_relation (tcbArch ko) (tcbArch_C ko'); tcbQueued ko = to_bool (tcbQueued_CL (thread_state_lift (tcbState_C ko'))); UCAST(8 \<rightarrow> 32) (tcbDomain ko) = tcbDomain_C ko'; UCAST(8 \<rightarrow> 32) (tcbPriority ko) = tcbPriority_C ko'; UCAST(8 \<rightarrow> 32) (tcbMCP ko) = tcbMCP_C ko'; tcbTimeSlice ko = unat (tcbTimeSlice_C ko'); cfault_rel (tcbFault ko) (seL4_Fault_lift (tcbFault_C ko')) (lookup_fault_lift (tcbLookupFailure_C ko')); option_to_ptr (tcbBoundNotification ko) = tcbBoundNotification_C ko'; StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')]) \<noteq> NULL; unat (tcbDomain ko) = unat (tcbDomain_C ko')\<rbrakk> \<Longrightarrow> \<exists>y. cslift s' (head_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')])) = Some y proof (prove)
goal (2 subgoals):
 1. \<And>ko ko'. \<lbrakk>(s, s') \<in> rf_sr; Invariants_H.valid_queues s; valid_objs' s; ko_at' ko x s; P ko; cslift s' (tcb_ptr_to_ctcb_ptr x) = Some ko'; tcbPriority ko \<le> maxPriority; unat (tcbDomain ko) < numDomains; sched_queue_relation' (cslift s') (ksReadyQueues s (tcbDomain ko, tcbPriority ko)) (head_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')])) (StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')])); tcbFaultHandler ko = tcbFaultHandler_C ko'; cthread_state_relation (tcbState ko) (tcbState_C ko', tcbFault_C ko'); tcbIPCBuffer ko = tcbIPCBuffer_C ko'; carch_tcb_relation (tcbArch ko) (tcbArch_C ko'); tcbQueued ko = to_bool (tcbQueued_CL (thread_state_lift (tcbState_C ko'))); UCAST(8 \<rightarrow> 32) (tcbDomain ko) = tcbDomain_C ko'; UCAST(8 \<rightarrow> 32) (tcbPriority ko) = tcbPriority_C ko'; UCAST(8 \<rightarrow> 32) (tcbMCP ko) = tcbMCP_C ko'; tcbTimeSlice ko = unat (tcbTimeSlice_C ko'); cfault_rel (tcbFault ko) (seL4_Fault_lift (tcbFault_C ko')) (lookup_fault_lift (tcbLookupFailure_C ko')); option_to_ptr (tcbBoundNotification ko) = tcbBoundNotification_C ko'; StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')]) \<noteq> NULL; unat (tcbDomain ko) = unat (tcbDomain_C ko')\<rbrakk> \<Longrightarrow> \<forall>t\<in>set (ksReadyQueues s (tcbDomain ko, tcbPriority ko)). tcb_at' t (?s50 ko ko')
 2. \<And>ko ko'. \<lbrakk>(s, s') \<in> rf_sr; Invariants_H.valid_queues s; valid_objs' s; ko_at' ko x s; P ko; cslift s' (tcb_ptr_to_ctcb_ptr x) = Some ko'; tcbPriority ko \<le> maxPriority; unat (tcbDomain ko) < numDomains; sched_queue_relation' (cslift s') (ksReadyQueues s (tcbDomain ko, tcbPriority ko)) (head_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')])) (StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')])); tcbFaultHandler ko = tcbFaultHandler_C ko'; cthread_state_relation (tcbState ko) (tcbState_C ko', tcbFault_C ko'); tcbIPCBuffer ko = tcbIPCBuffer_C ko'; carch_tcb_relation (tcbArch ko) (tcbArch_C ko'); tcbQueued ko = to_bool (tcbQueued_CL (thread_state_lift (tcbState_C ko'))); UCAST(8 \<rightarrow> 32) (tcbDomain ko) = tcbDomain_C ko'; UCAST(8 \<rightarrow> 32) (tcbPriority ko) = tcbPriority_C ko'; UCAST(8 \<rightarrow> 32) (tcbMCP ko) = tcbMCP_C ko'; tcbTimeSlice ko = unat (tcbTimeSlice_C ko'); cfault_rel (tcbFault ko) (seL4_Fault_lift (tcbFault_C ko')) (lookup_fault_lift (tcbLookupFailure_C ko')); option_to_ptr (tcbBoundNotification ko) = tcbBoundNotification_C ko'; StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')]) \<noteq> NULL; unat (tcbDomain ko) = unat (tcbDomain_C ko'); (StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')]) = NULL) = (head_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')]) = NULL)\<rbrakk> \<Longrightarrow> \<exists>y. cslift s' (head_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')])) = Some y proof (prove)
goal (1 subgoal):
 1. \<And>ko ko'. \<lbrakk>(s, s') \<in> rf_sr; Invariants_H.valid_queues s; valid_objs' s; ko_at' ko x s; P ko; cslift s' (tcb_ptr_to_ctcb_ptr x) = Some ko'; tcbPriority ko \<le> maxPriority; unat (tcbDomain ko) < numDomains; sched_queue_relation' (cslift s') (ksReadyQueues s (tcbDomain ko, tcbPriority ko)) (head_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')])) (StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')])); tcbFaultHandler ko = tcbFaultHandler_C ko'; cthread_state_relation (tcbState ko) (tcbState_C ko', tcbFault_C ko'); tcbIPCBuffer ko = tcbIPCBuffer_C ko'; carch_tcb_relation (tcbArch ko) (tcbArch_C ko'); tcbQueued ko = to_bool (tcbQueued_CL (thread_state_lift (tcbState_C ko'))); UCAST(8 \<rightarrow> 32) (tcbDomain ko) = tcbDomain_C ko'; UCAST(8 \<rightarrow> 32) (tcbPriority ko) = tcbPriority_C ko'; UCAST(8 \<rightarrow> 32) (tcbMCP ko) = tcbMCP_C ko'; tcbTimeSlice ko = unat (tcbTimeSlice_C ko'); cfault_rel (tcbFault ko) (seL4_Fault_lift (tcbFault_C ko')) (lookup_fault_lift (tcbLookupFailure_C ko')); option_to_ptr (tcbBoundNotification ko) = tcbBoundNotification_C ko'; StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')]) \<noteq> NULL; unat (tcbDomain ko) = unat (tcbDomain_C ko'); (StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')]) = NULL) = (head_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')]) = NULL)\<rbrakk> \<Longrightarrow> \<exists>y. cslift s' (head_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')])) = Some y proof (prove)
goal (2 subgoals):
 1. \<And>ko ko'. \<lbrakk>(s, s') \<in> rf_sr; Invariants_H.valid_queues s; valid_objs' s; ko_at' ko x s; P ko; cslift s' (tcb_ptr_to_ctcb_ptr x) = Some ko'; tcbPriority ko \<le> maxPriority; unat (tcbDomain ko) < numDomains; sched_queue_relation' (cslift s') (ksReadyQueues s (tcbDomain ko, tcbPriority ko)) (head_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')])) (StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')])); tcbFaultHandler ko = tcbFaultHandler_C ko'; cthread_state_relation (tcbState ko) (tcbState_C ko', tcbFault_C ko'); tcbIPCBuffer ko = tcbIPCBuffer_C ko'; carch_tcb_relation (tcbArch ko) (tcbArch_C ko'); tcbQueued ko = to_bool (tcbQueued_CL (thread_state_lift (tcbState_C ko'))); UCAST(8 \<rightarrow> 32) (tcbDomain ko) = tcbDomain_C ko'; UCAST(8 \<rightarrow> 32) (tcbPriority ko) = tcbPriority_C ko'; UCAST(8 \<rightarrow> 32) (tcbMCP ko) = tcbMCP_C ko'; tcbTimeSlice ko = unat (tcbTimeSlice_C ko'); cfault_rel (tcbFault ko) (seL4_Fault_lift (tcbFault_C ko')) (lookup_fault_lift (tcbLookupFailure_C ko')); option_to_ptr (tcbBoundNotification ko) = tcbBoundNotification_C ko'; StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')]) \<noteq> NULL; unat (tcbDomain ko) = unat (tcbDomain_C ko'); (StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')]) = NULL) = (head_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')]) = NULL)\<rbrakk> \<Longrightarrow> \<forall>tcb\<in>set (ksReadyQueues s (tcbDomain ko, tcbPriority ko)). tcb_at' tcb s
 2. \<And>ko ko'. \<lbrakk>(s, s') \<in> rf_sr; Invariants_H.valid_queues s; valid_objs' s; ko_at' ko x s; P ko; cslift s' (tcb_ptr_to_ctcb_ptr x) = Some ko'; tcbPriority ko \<le> maxPriority; unat (tcbDomain ko) < numDomains; sched_queue_relation' (cslift s') (ksReadyQueues s (tcbDomain ko, tcbPriority ko)) (head_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')])) (StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')])); tcbFaultHandler ko = tcbFaultHandler_C ko'; cthread_state_relation (tcbState ko) (tcbState_C ko', tcbFault_C ko'); tcbIPCBuffer ko = tcbIPCBuffer_C ko'; carch_tcb_relation (tcbArch ko) (tcbArch_C ko'); tcbQueued ko = to_bool (tcbQueued_CL (thread_state_lift (tcbState_C ko'))); UCAST(8 \<rightarrow> 32) (tcbDomain ko) = tcbDomain_C ko'; UCAST(8 \<rightarrow> 32) (tcbPriority ko) = tcbPriority_C ko'; UCAST(8 \<rightarrow> 32) (tcbMCP ko) = tcbMCP_C ko'; tcbTimeSlice ko = unat (tcbTimeSlice_C ko'); cfault_rel (tcbFault ko) (seL4_Fault_lift (tcbFault_C ko')) (lookup_fault_lift (tcbLookupFailure_C ko')); option_to_ptr (tcbBoundNotification ko) = tcbBoundNotification_C ko'; StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')]) \<noteq> NULL; unat (tcbDomain ko) = unat (tcbDomain_C ko'); (StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')]) = NULL) = (head_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')]) = NULL); head_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')]) \<noteq> NULL \<longrightarrow> s' \<Turnstile>\<^sub>c head_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')])\<rbrakk> \<Longrightarrow> \<exists>y. cslift s' (head_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')])) = Some y proof (prove)
goal (1 subgoal):
 1. \<And>ko ko'. \<lbrakk>(s, s') \<in> rf_sr; Invariants_H.valid_queues s; valid_objs' s; ko_at' ko x s; P ko; cslift s' (tcb_ptr_to_ctcb_ptr x) = Some ko'; tcbPriority ko \<le> maxPriority; unat (tcbDomain ko) < numDomains; sched_queue_relation' (cslift s') (ksReadyQueues s (tcbDomain ko, tcbPriority ko)) (head_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')])) (StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')])); tcbFaultHandler ko = tcbFaultHandler_C ko'; cthread_state_relation (tcbState ko) (tcbState_C ko', tcbFault_C ko'); tcbIPCBuffer ko = tcbIPCBuffer_C ko'; carch_tcb_relation (tcbArch ko) (tcbArch_C ko'); tcbQueued ko = to_bool (tcbQueued_CL (thread_state_lift (tcbState_C ko'))); UCAST(8 \<rightarrow> 32) (tcbDomain ko) = tcbDomain_C ko'; UCAST(8 \<rightarrow> 32) (tcbPriority ko) = tcbPriority_C ko'; UCAST(8 \<rightarrow> 32) (tcbMCP ko) = tcbMCP_C ko'; tcbTimeSlice ko = unat (tcbTimeSlice_C ko'); cfault_rel (tcbFault ko) (seL4_Fault_lift (tcbFault_C ko')) (lookup_fault_lift (tcbLookupFailure_C ko')); option_to_ptr (tcbBoundNotification ko) = tcbBoundNotification_C ko'; StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')]) \<noteq> NULL; unat (tcbDomain ko) = unat (tcbDomain_C ko'); (StateRelation_C.end_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')]) = NULL) = (head_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')]) = NULL); head_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')]) \<noteq> NULL \<longrightarrow> s' \<Turnstile>\<^sub>c head_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')])\<rbrakk> \<Longrightarrow> \<exists>y. cslift s' (head_C (ksReadyQueues_' (globals s').[unat (tcbDomain_C ko' * 0x100 + tcbPriority_C ko')])) = Some y proof (prove)
goal:
No subgoals!