theory IpcCancel_C

lemma rf_sr_sched_queue_relation:
  "\<lbrakk> (s, s') \<in> rf_sr; d \<le> ucast maxDom; p \<le> ucast maxPrio \<rbrakk>
  \<Longrightarrow> sched_queue_relation' (cslift s') (ksReadyQueues s (d, p))
                                        (head_C (index (ksReadyQueues_' (globals s'))
                                                       (cready_queues_index_to_C d p)))
                                        (end_C (index (ksReadyQueues_' (globals s'))
                                                      (cready_queues_index_to_C d p)))" unfolding rf_sr_def cstate_relation_def cready_queues_relation_def apply (clarsimp simp: Let_def seL4_MinPrio_def minDom_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> rf_sr; d \<le> UCAST(32 signed \<rightarrow> 8) maxDom; p \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio\<rbrakk> \<Longrightarrow> sched_queue_relation' (cslift s') (ksReadyQueues s (d, p)) (head_C (ksReadyQueues_' (globals s').[cready_queues_index_to_C d p])) (StateRelation_C.end_C (ksReadyQueues_' (globals s').[cready_queues_index_to_C d p])) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> {(s, s'). let cheap = t_hrs_' (globals s') in cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) cheap \<and> (\<forall>qdom prio. (UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom \<and> qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom \<and> UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio \<and> prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio \<longrightarrow> (let cqueue = ksReadyQueues_' (globals s').[cready_queues_index_to_C qdom prio] in sched_queue_relation' (clift cheap) (ksReadyQueues s (qdom, prio)) (head_C cqueue) (StateRelation_C.end_C cqueue))) \<and> (\<not> (UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom \<and> qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom \<and> UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio \<and> prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio) \<longrightarrow> ksReadyQueues s (qdom, prio) = [])) \<and> zero_ranges_are_zero (gsUntypedZeroRanges s) cheap \<and> cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s) \<and> cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s) \<and> ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s) \<and> ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s) \<and> cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')) \<and> cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')) \<and> carch_state_relation (ksArchState s) (globals s') \<and> cmachine_state_relation (ksMachineState s) (globals s') \<and> cte_array_relation s (globals s') \<and> tcb_cte_array_relation s (globals s') \<and> apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s) \<and> ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s) \<and> ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s \<and> s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr \<and> ptr_span intStateIRQNode_array_Ptr \<subseteq> kernel_data_refs \<and> s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr \<and> ptr_span armKSGlobalPD_Ptr \<subseteq> kernel_data_refs \<and> htd_safe domain (hrs_htd (t_hrs_' (globals s'))) \<and> - domain \<subseteq> kernel_data_refs \<and> globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list \<and> cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule \<and> ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s) \<and> ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s) \<and> ksDomainTime_' (globals s') = ksDomainTime s}; d \<le> UCAST(32 signed \<rightarrow> 8) maxDom; p \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio\<rbrakk> \<Longrightarrow> sched_queue_relation' (cslift s') (ksReadyQueues s (d, p)) (head_C (ksReadyQueues_' (globals s').[cready_queues_index_to_C d p])) (StateRelation_C.end_C (ksReadyQueues_' (globals s').[cready_queues_index_to_C d p])) proof (prove)
goal:
No subgoals!