theory IpcCancel_C

lemma state_relation_queue_update_helper:
  "\<lbrakk> (s, s') \<in> rf_sr; valid_queues s;
          globals t = ksReadyQueues_'_update
             (\<lambda>_. Arrays.update (ksReadyQueues_' (globals s')) prio' q')
             (t_hrs_'_update f (globals s'));
          sched_queue_relation' (cslift t) q (head_C q') (end_C q');
          cslift t |` ( - tcb_ptr_to_ctcb_ptr ` S )
             = cslift s' |` ( - tcb_ptr_to_ctcb_ptr ` S );
          option_map tcb_null_sched_ptrs \<circ> cslift t
            = option_map tcb_null_sched_ptrs \<circ> cslift s';
          cslift_all_but_tcb_C t s';
          zero_ranges_are_zero (gsUntypedZeroRanges s) (f (t_hrs_' (globals s')))
              = zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s'));
          hrs_htd (t_hrs_' (globals t)) = hrs_htd (t_hrs_' (globals s'));
          prio' = cready_queues_index_to_C qdom prio;
          \<forall>x \<in> S. obj_at' (inQ qdom prio) x s
                   \<or> (obj_at' (\<lambda>tcb. tcbPriority tcb = prio) x s
                       \<and> obj_at' (\<lambda>tcb. tcbDomain tcb = qdom) x s)
                   \<or> (tcb_at' x s \<and> (\<forall>d' p'. (d' \<noteq> qdom \<or> p' \<noteq> prio)
                                         \<longrightarrow> x \<notin> set (ksReadyQueues s (d', p'))));
          S \<noteq> {}; qdom \<le> ucast maxDom; prio \<le> ucast maxPrio \<rbrakk>
      \<Longrightarrow> (s \<lparr>ksReadyQueues := (ksReadyQueues s)((qdom, prio) := q)\<rparr>, t) \<in> rf_sr" apply (subgoal_tac "\<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). obj_at' (inQ d p) t s)
                           \<and> distinct(ksReadyQueues s (d, p))") apply (erule(5) state_relation_queue_update_helper', simp_all) apply (clarsimp simp: valid_queues_def valid_queues_no_bitmap_def) apply (drule_tac x=d in spec) apply (drule_tac x=p in spec) apply (clarsimp) apply (drule(1) bspec) apply (erule obj_at'_weakenE, clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> rf_sr; Invariants_H.valid_queues s; globals t = t_hrs_'_update f (globals s')\<lparr>ksReadyQueues_' := Arrays.update (ksReadyQueues_' (globals s')) prio' q'\<rparr>; sched_queue_relation' (cslift t) q (head_C q') (StateRelation_C.end_C q'); cslift t|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` S)\<^esub> = cslift s'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` S)\<^esub>; map_option tcb_null_sched_ptrs \<circ> cslift t = map_option tcb_null_sched_ptrs \<circ> cslift s'; cslift t = cslift s' \<and> cslift t = cslift s' \<and> cslift t = cslift s' \<and> cslift t = cslift s' \<and> cslift t = cslift s' \<and> cslift t = cslift s' \<and> cslift t = cslift s' \<and> cslift t = cslift s'; zero_ranges_are_zero (gsUntypedZeroRanges s) (f (t_hrs_' (globals s'))) = zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); hrs_htd (t_hrs_' (globals t)) = hrs_htd (t_hrs_' (globals s')); prio' = cready_queues_index_to_C qdom prio; \<forall>x\<in>S. obj_at' (inQ qdom prio) x s \<or> obj_at' (\<lambda>tcb. tcbPriority tcb = prio) x s \<and> obj_at' (\<lambda>tcb. tcbDomain tcb = qdom) x s \<or> tcb_at' x s \<and> (\<forall>d' p'. d' \<noteq> qdom \<or> p' \<noteq> prio \<longrightarrow> x \<notin> set (ksReadyQueues s (d', p'))); S \<noteq> {}; qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom; prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio\<rbrakk> \<Longrightarrow> (s\<lparr>ksReadyQueues := (ksReadyQueues s)((qdom, prio) := q)\<rparr>, t) \<in> rf_sr proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(s, s') \<in> rf_sr; Invariants_H.valid_queues s; globals t = t_hrs_'_update f (globals s')\<lparr>ksReadyQueues_' := Arrays.update (ksReadyQueues_' (globals s')) prio' q'\<rparr>; sched_queue_relation' (cslift t) q (head_C q') (StateRelation_C.end_C q'); cslift t|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` S)\<^esub> = cslift s'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` S)\<^esub>; map_option tcb_null_sched_ptrs \<circ> cslift t = map_option tcb_null_sched_ptrs \<circ> cslift s'; cslift t = cslift s' \<and> cslift t = cslift s' \<and> cslift t = cslift s' \<and> cslift t = cslift s' \<and> cslift t = cslift s' \<and> cslift t = cslift s' \<and> cslift t = cslift s' \<and> cslift t = cslift s'; zero_ranges_are_zero (gsUntypedZeroRanges s) (f (t_hrs_' (globals s'))) = zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); hrs_htd (t_hrs_' (globals t)) = hrs_htd (t_hrs_' (globals s')); prio' = cready_queues_index_to_C qdom prio; \<forall>x\<in>S. obj_at' (inQ qdom prio) x s \<or> obj_at' (\<lambda>tcb. tcbPriority tcb = prio) x s \<and> obj_at' (\<lambda>tcb. tcbDomain tcb = qdom) x s \<or> tcb_at' x s \<and> (\<forall>d' p'. d' \<noteq> qdom \<or> p' \<noteq> prio \<longrightarrow> x \<notin> set (ksReadyQueues s (d', p'))); S \<noteq> {}; qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom; prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio; \<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). obj_at' (inQ d p) t s) \<and> distinct (ksReadyQueues s (d, p))\<rbrakk> \<Longrightarrow> (s\<lparr>ksReadyQueues := (ksReadyQueues s)((qdom, prio) := q)\<rparr>, t) \<in> rf_sr
 2. \<lbrakk>(s, s') \<in> rf_sr; Invariants_H.valid_queues s; globals t = t_hrs_'_update f (globals s')\<lparr>ksReadyQueues_' := Arrays.update (ksReadyQueues_' (globals s')) prio' q'\<rparr>; sched_queue_relation' (cslift t) q (head_C q') (StateRelation_C.end_C q'); cslift t|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` S)\<^esub> = cslift s'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` S)\<^esub>; map_option tcb_null_sched_ptrs \<circ> cslift t = map_option tcb_null_sched_ptrs \<circ> cslift s'; cslift t = cslift s' \<and> cslift t = cslift s' \<and> cslift t = cslift s' \<and> cslift t = cslift s' \<and> cslift t = cslift s' \<and> cslift t = cslift s' \<and> cslift t = cslift s' \<and> cslift t = cslift s'; zero_ranges_are_zero (gsUntypedZeroRanges s) (f (t_hrs_' (globals s'))) = zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); hrs_htd (t_hrs_' (globals t)) = hrs_htd (t_hrs_' (globals s')); prio' = cready_queues_index_to_C qdom prio; \<forall>x\<in>S. obj_at' (inQ qdom prio) x s \<or> obj_at' (\<lambda>tcb. tcbPriority tcb = prio) x s \<and> obj_at' (\<lambda>tcb. tcbDomain tcb = qdom) x s \<or> tcb_at' x s \<and> (\<forall>d' p'. d' \<noteq> qdom \<or> p' \<noteq> prio \<longrightarrow> x \<notin> set (ksReadyQueues s (d', p'))); S \<noteq> {}; qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom; prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio\<rbrakk> \<Longrightarrow> \<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). obj_at' (inQ d p) t s) \<and> distinct (ksReadyQueues s (d, p)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> rf_sr; Invariants_H.valid_queues s; globals t = t_hrs_'_update f (globals s')\<lparr>ksReadyQueues_' := Arrays.update (ksReadyQueues_' (globals s')) (cready_queues_index_to_C qdom prio) q'\<rparr>; sched_queue_relation' (clift (f (t_hrs_' (globals s')))) q (head_C q') (StateRelation_C.end_C q'); clift (f (t_hrs_' (globals s')))|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` S)\<^esub> = cslift s'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` S)\<^esub>; map_option tcb_null_sched_ptrs \<circ> clift (f (t_hrs_' (globals s'))) = map_option tcb_null_sched_ptrs \<circ> cslift s'; clift (f (t_hrs_' (globals s'))) = cslift s' \<and> clift (f (t_hrs_' (globals s'))) = cslift s' \<and> clift (f (t_hrs_' (globals s'))) = cslift s' \<and> clift (f (t_hrs_' (globals s'))) = cslift s' \<and> clift (f (t_hrs_' (globals s'))) = cslift s' \<and> clift (f (t_hrs_' (globals s'))) = cslift s' \<and> clift (f (t_hrs_' (globals s'))) = cslift s' \<and> clift (f (t_hrs_' (globals s'))) = cslift s'; zero_ranges_are_zero (gsUntypedZeroRanges s) (f (t_hrs_' (globals s'))) = zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); hrs_htd (f (t_hrs_' (globals s'))) = hrs_htd (t_hrs_' (globals s')); prio' = cready_queues_index_to_C qdom prio; \<forall>x\<in>S. obj_at' (inQ qdom prio) x s \<or> obj_at' (\<lambda>tcb. tcbPriority tcb = prio) x s \<and> obj_at' (\<lambda>tcb. tcbDomain tcb = qdom) x s \<or> tcb_at' x s \<and> (\<forall>d' p'. (d' = qdom \<longrightarrow> p' \<noteq> prio) \<longrightarrow> x \<notin> set (ksReadyQueues s (d', p'))); S \<noteq> {}; qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom; prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio\<rbrakk> \<Longrightarrow> \<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). obj_at' (inQ d p) t s) \<and> distinct (ksReadyQueues s (d, p)) proof (prove)
goal (1 subgoal):
 1. \<And>d p ta. \<lbrakk>(s, s') \<in> rf_sr; globals t = t_hrs_'_update f (globals s')\<lparr>ksReadyQueues_' := Arrays.update (ksReadyQueues_' (globals s')) (cready_queues_index_to_C qdom prio) q'\<rparr>; sched_queue_relation' (clift (f (t_hrs_' (globals s')))) q (head_C q') (StateRelation_C.end_C q'); clift (f (t_hrs_' (globals s')))|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` S)\<^esub> = cslift s'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` S)\<^esub>; map_option tcb_null_sched_ptrs \<circ> clift (f (t_hrs_' (globals s'))) = map_option tcb_null_sched_ptrs \<circ> cslift s'; zero_ranges_are_zero (gsUntypedZeroRanges s) (f (t_hrs_' (globals s'))) = zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); hrs_htd (f (t_hrs_' (globals s'))) = hrs_htd (t_hrs_' (globals s')); prio' = cready_queues_index_to_C qdom prio; \<forall>x\<in>S. obj_at' (inQ qdom prio) x s \<or> obj_at' (\<lambda>tcb. tcbPriority tcb = prio) x s \<and> obj_at' (\<lambda>tcb. tcbDomain tcb = qdom) x s \<or> tcb_at' x s \<and> (\<forall>d' p'. (d' = qdom \<longrightarrow> p' \<noteq> prio) \<longrightarrow> x \<notin> set (ksReadyQueues s (d', p'))); S \<noteq> {}; qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom; prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio; ta \<in> set (ksReadyQueues s (d, p)); \<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) = []); clift (f (t_hrs_' (globals s'))) = cslift s'; valid_bitmapQ s; clift (f (t_hrs_' (globals s'))) = cslift s'; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; clift (f (t_hrs_' (globals s'))) = cslift s'; clift (f (t_hrs_' (globals s'))) = cslift s'; clift (f (t_hrs_' (globals s'))) = cslift s'; clift (f (t_hrs_' (globals s'))) = cslift s'; clift (f (t_hrs_' (globals s'))) = cslift s'; clift (f (t_hrs_' (globals s'))) = cslift s'\<rbrakk> \<Longrightarrow> obj_at' (inQ d p) ta s proof (prove)
goal (1 subgoal):
 1. \<And>d p ta. \<lbrakk>(s, s') \<in> rf_sr; globals t = t_hrs_'_update f (globals s')\<lparr>ksReadyQueues_' := Arrays.update (ksReadyQueues_' (globals s')) (cready_queues_index_to_C qdom prio) q'\<rparr>; sched_queue_relation' (clift (f (t_hrs_' (globals s')))) q (head_C q') (StateRelation_C.end_C q'); clift (f (t_hrs_' (globals s')))|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` S)\<^esub> = cslift s'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` S)\<^esub>; map_option tcb_null_sched_ptrs \<circ> clift (f (t_hrs_' (globals s'))) = map_option tcb_null_sched_ptrs \<circ> cslift s'; zero_ranges_are_zero (gsUntypedZeroRanges s) (f (t_hrs_' (globals s'))) = zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); hrs_htd (f (t_hrs_' (globals s'))) = hrs_htd (t_hrs_' (globals s')); prio' = cready_queues_index_to_C qdom prio; \<forall>x\<in>S. obj_at' (inQ qdom prio) x s \<or> obj_at' (\<lambda>tcb. tcbPriority tcb = prio) x s \<and> obj_at' (\<lambda>tcb. tcbDomain tcb = qdom) x s \<or> tcb_at' x s \<and> (\<forall>d' p'. (d' = qdom \<longrightarrow> p' \<noteq> prio) \<longrightarrow> x \<notin> set (ksReadyQueues s (d', p'))); S \<noteq> {}; qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom; prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio; ta \<in> set (ksReadyQueues s (d, p)); clift (f (t_hrs_' (globals s'))) = cslift s'; valid_bitmapQ s; clift (f (t_hrs_' (globals s'))) = cslift s'; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; clift (f (t_hrs_' (globals s'))) = cslift s'; clift (f (t_hrs_' (globals s'))) = cslift s'; clift (f (t_hrs_' (globals s'))) = cslift s'; clift (f (t_hrs_' (globals s'))) = cslift s'; clift (f (t_hrs_' (globals s'))) = cslift s'; clift (f (t_hrs_' (globals s'))) = cslift s'; \<forall>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) = [])\<rbrakk> \<Longrightarrow> obj_at' (inQ d p) ta s proof (prove)
goal (1 subgoal):
 1. \<And>d p ta. \<lbrakk>(s, s') \<in> rf_sr; globals t = t_hrs_'_update f (globals s')\<lparr>ksReadyQueues_' := Arrays.update (ksReadyQueues_' (globals s')) (cready_queues_index_to_C qdom prio) q'\<rparr>; sched_queue_relation' (clift (f (t_hrs_' (globals s')))) q (head_C q') (StateRelation_C.end_C q'); clift (f (t_hrs_' (globals s')))|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` S)\<^esub> = cslift s'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` S)\<^esub>; map_option tcb_null_sched_ptrs \<circ> clift (f (t_hrs_' (globals s'))) = map_option tcb_null_sched_ptrs \<circ> cslift s'; zero_ranges_are_zero (gsUntypedZeroRanges s) (f (t_hrs_' (globals s'))) = zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); hrs_htd (f (t_hrs_' (globals s'))) = hrs_htd (t_hrs_' (globals s')); prio' = cready_queues_index_to_C qdom prio; \<forall>x\<in>S. obj_at' (inQ qdom prio) x s \<or> obj_at' (\<lambda>tcb. tcbPriority tcb = prio) x s \<and> obj_at' (\<lambda>tcb. tcbDomain tcb = qdom) x s \<or> tcb_at' x s \<and> (\<forall>d' p'. (d' = qdom \<longrightarrow> p' \<noteq> prio) \<longrightarrow> x \<notin> set (ksReadyQueues s (d', p'))); S \<noteq> {}; qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom; prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio; ta \<in> set (ksReadyQueues s (d, p)); clift (f (t_hrs_' (globals s'))) = cslift s'; valid_bitmapQ s; clift (f (t_hrs_' (globals s'))) = cslift s'; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; clift (f (t_hrs_' (globals s'))) = cslift s'; clift (f (t_hrs_' (globals s'))) = cslift s'; clift (f (t_hrs_' (globals s'))) = cslift s'; clift (f (t_hrs_' (globals s'))) = cslift s'; clift (f (t_hrs_' (globals s'))) = cslift s'; clift (f (t_hrs_' (globals s'))) = cslift s'; (\<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) = [])\<rbrakk> \<Longrightarrow> obj_at' (inQ d p) ta s proof (prove)
goal (1 subgoal):
 1. \<And>d p ta. \<lbrakk>(s, s') \<in> rf_sr; globals t = t_hrs_'_update f (globals s')\<lparr>ksReadyQueues_' := Arrays.update (ksReadyQueues_' (globals s')) (cready_queues_index_to_C qdom prio) q'\<rparr>; sched_queue_relation' (clift (f (t_hrs_' (globals s')))) q (head_C q') (StateRelation_C.end_C q'); clift (f (t_hrs_' (globals s')))|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` S)\<^esub> = cslift s'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` S)\<^esub>; map_option tcb_null_sched_ptrs \<circ> clift (f (t_hrs_' (globals s'))) = map_option tcb_null_sched_ptrs \<circ> cslift s'; zero_ranges_are_zero (gsUntypedZeroRanges s) (f (t_hrs_' (globals s'))) = zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); hrs_htd (f (t_hrs_' (globals s'))) = hrs_htd (t_hrs_' (globals s')); prio' = cready_queues_index_to_C qdom prio; \<forall>x\<in>S. obj_at' (inQ qdom prio) x s \<or> obj_at' (\<lambda>tcb. tcbPriority tcb = prio) x s \<and> obj_at' (\<lambda>tcb. tcbDomain tcb = qdom) x s \<or> tcb_at' x s \<and> (\<forall>d' p'. (d' = qdom \<longrightarrow> p' \<noteq> prio) \<longrightarrow> x \<notin> set (ksReadyQueues s (d', p'))); S \<noteq> {}; qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom; prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio; ta \<in> set (ksReadyQueues s (d, p)); clift (f (t_hrs_' (globals s'))) = cslift s'; valid_bitmapQ s; clift (f (t_hrs_' (globals s'))) = cslift s'; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; clift (f (t_hrs_' (globals s'))) = cslift s'; clift (f (t_hrs_' (globals s'))) = cslift s'; clift (f (t_hrs_' (globals s'))) = cslift s'; clift (f (t_hrs_' (globals s'))) = cslift s'; clift (f (t_hrs_' (globals s'))) = cslift s'; clift (f (t_hrs_' (globals s'))) = cslift s'; \<forall>t\<in>set (ksReadyQueues s (d, p)). obj_at' (inQ d p and runnable' \<circ> tcbState) t s; distinct (ksReadyQueues s (d, p)); maxDomain < d \<longrightarrow> ksReadyQueues s (d, p) = []; maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = []\<rbrakk> \<Longrightarrow> obj_at' (inQ d p) ta s proof (prove)
goal (1 subgoal):
 1. \<And>d p ta. \<lbrakk>(s, s') \<in> rf_sr; globals t = t_hrs_'_update f (globals s')\<lparr>ksReadyQueues_' := Arrays.update (ksReadyQueues_' (globals s')) (cready_queues_index_to_C qdom prio) q'\<rparr>; sched_queue_relation' (clift (f (t_hrs_' (globals s')))) q (head_C q') (StateRelation_C.end_C q'); clift (f (t_hrs_' (globals s')))|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` S)\<^esub> = cslift s'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` S)\<^esub>; map_option tcb_null_sched_ptrs \<circ> clift (f (t_hrs_' (globals s'))) = map_option tcb_null_sched_ptrs \<circ> cslift s'; zero_ranges_are_zero (gsUntypedZeroRanges s) (f (t_hrs_' (globals s'))) = zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); hrs_htd (f (t_hrs_' (globals s'))) = hrs_htd (t_hrs_' (globals s')); prio' = cready_queues_index_to_C qdom prio; \<forall>x\<in>S. obj_at' (inQ qdom prio) x s \<or> obj_at' (\<lambda>tcb. tcbPriority tcb = prio) x s \<and> obj_at' (\<lambda>tcb. tcbDomain tcb = qdom) x s \<or> tcb_at' x s \<and> (\<forall>d' p'. (d' = qdom \<longrightarrow> p' \<noteq> prio) \<longrightarrow> x \<notin> set (ksReadyQueues s (d', p'))); S \<noteq> {}; qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom; prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio; ta \<in> set (ksReadyQueues s (d, p)); clift (f (t_hrs_' (globals s'))) = cslift s'; valid_bitmapQ s; clift (f (t_hrs_' (globals s'))) = cslift s'; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; clift (f (t_hrs_' (globals s'))) = cslift s'; clift (f (t_hrs_' (globals s'))) = cslift s'; clift (f (t_hrs_' (globals s'))) = cslift s'; clift (f (t_hrs_' (globals s'))) = cslift s'; clift (f (t_hrs_' (globals s'))) = cslift s'; clift (f (t_hrs_' (globals s'))) = cslift s'; distinct (ksReadyQueues s (d, p)); maxDomain < d \<longrightarrow> ksReadyQueues s (d, p) = []; maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = []; obj_at' (inQ d p and runnable' \<circ> tcbState) ta s\<rbrakk> \<Longrightarrow> obj_at' (inQ d p) ta s proof (prove)
goal:
No subgoals!