theory Finalise_C

lemma tcbSchedEnqueue_cslift_spec:
  "\<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> \<lbrace>s. \<exists>d v. option_map2 tcbPriority_C (cslift s) \<acute>tcb = Some v
                       \<and> unat v \<le> numPriorities
                       \<and> option_map2 tcbDomain_C (cslift s) \<acute>tcb = Some d
                       \<and> unat d < Kernel_Config.numDomains
                       \<and> (end_C (index \<acute>ksReadyQueues (unat (d*0x100 + v))) \<noteq> NULL
                           \<longrightarrow> option_map2 tcbPriority_C (cslift s)
                                   (head_C (index \<acute>ksReadyQueues (unat (d*0x100 + v))))
                                           \<noteq> None
                             \<and> option_map2 tcbDomain_C (cslift s)
                                   (head_C (index \<acute>ksReadyQueues (unat (d*0x100 + v))))
                                           \<noteq> None)\<rbrace>
       Call tcbSchedEnqueue_'proc
      {s'. option_map2 tcbEPNext_C (cslift s') = option_map2 tcbEPNext_C (cslift s)
           \<and> option_map2 tcbEPPrev_C (cslift s') = option_map2 tcbEPPrev_C (cslift s)
           \<and> option_map2 tcbPriority_C (cslift s') = option_map2 tcbPriority_C (cslift s)
           \<and> option_map2 tcbDomain_C (cslift s') = option_map2 tcbDomain_C (cslift s)}" apply (hoare_rule HoarePartial.ProcNoRec1) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: option_map2_def fun_eq_iff h_t_valid_clift
                        h_t_valid_field[OF h_t_valid_clift]) apply (rule conjI) apply (clarsimp simp: typ_heap_simps le_maxDomain_eq_less_numDomains) apply unat_arith apply clarsimp apply (rule conjI) apply (clarsimp simp: typ_heap_simps cong: if_cong) apply (simp split: if_split) apply (clarsimp simp: typ_heap_simps if_Some_helper cong: if_cong) by (simp split: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> \<lbrace>s. \<exists>d v. option_map2 tcbPriority_C (cslift s) \<acute>tcb = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift s) \<acute>tcb = Some d \<and> unat d < numDomains \<and> (StateRelation_C.end_C (\<acute>ksReadyQueues.[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> option_map2 tcbPriority_C (cslift s) (head_C (\<acute>ksReadyQueues.[unat (d * 0x100 + v)])) \<noteq> None \<and> option_map2 tcbDomain_C (cslift s) (head_C (\<acute>ksReadyQueues.[unat (d * 0x100 + v)])) \<noteq> None)\<rbrace> Call tcbSchedEnqueue_'proc {s'. option_map2 tcbEPNext_C (cslift s') = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift s') = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift s') = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift s') = option_map2 tcbDomain_C (cslift s)} proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> \<lbrace>s. \<exists>d v. option_map2 tcbPriority_C (cslift s) \<acute>tcb = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift s) \<acute>tcb = Some d \<and> unat d < numDomains \<and> (StateRelation_C.end_C (\<acute>ksReadyQueues.[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> option_map2 tcbPriority_C (cslift s) (head_C (\<acute>ksReadyQueues.[unat (d * 0x100 + v)])) \<noteq> None \<and> option_map2 tcbDomain_C (cslift s) (head_C (\<acute>ksReadyQueues.[unat (d * 0x100 + v)])) \<noteq> None)\<rbrace> TRY
  Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_' s} (\<acute>ret__unsigned :== CALL thread_state_get_tcbQueued_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(\<acute>tcb\<rightarrow>[''tcbState_C'']))));;
IF \<not> \<acute>ret__unsigned \<noteq> 0 THEN
  lvar_nondet_init queue_' queue_'_update;;
lvar_nondet_init dom_' dom_'_update;;
lvar_nondet_init prio_' prio_'_update;;
lvar_nondet_init idx_' idx_'_update;;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_' s} (\<acute>dom :== h_val (hrs_mem \<acute>t_hrs) (PTR(32 word) &(\<acute>tcb\<rightarrow>[''tcbDomain_C''])));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_' s} (\<acute>prio :== h_val (hrs_mem \<acute>t_hrs) (PTR(32 word) &(\<acute>tcb\<rightarrow>[''tcbPriority_C''])));;
\<acute>idx :== CALL ready_queues_index_'proc(\<acute>dom,\<acute>prio);;
Guard ArrayBounds \<lbrace>\<acute>idx < SCAST(32 signed \<rightarrow> 32) 0x1000\<rbrace> (\<acute>queue :== \<acute>ksReadyQueues.[unat \<acute>idx]);;
IF \<not> StateRelation_C.end_C \<acute>queue \<noteq> NULL THEN
  \<acute>queue :== tcb_queue_C.end_C_update (\<lambda>_. \<acute>tcb) \<acute>queue;;
CALL addToBitmap_'proc(SCAST(32 signed \<rightarrow> 32) 0,\<acute>dom,\<acute>prio)
ELSE
  Guard C_Guard {s. s \<Turnstile>\<^sub>c head_C (queue_' s)} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(head_C \<acute>queue\<rightarrow>[''tcbSchedPrev_C''])) \<acute>tcb)))
FI;;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_' s} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(\<acute>tcb\<rightarrow>[''tcbSchedPrev_C''])) (PTR_COERCE(unit \<rightarrow> tcb_C) (PTR(unit) (SCAST(32 signed \<rightarrow> 32) 0))))));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_' s} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(\<acute>tcb\<rightarrow>[''tcbSchedNext_C''])) (head_C \<acute>queue))));;
\<acute>queue :== head_C_update (\<lambda>_. \<acute>tcb) \<acute>queue;;
Guard ArrayBounds \<lbrace>\<acute>idx < SCAST(32 signed \<rightarrow> 32) 0x1000\<rbrace> (\<acute>ksReadyQueues :== Arrays.update \<acute>ksReadyQueues (unat \<acute>idx) \<acute>queue);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_' s} (CALL thread_state_ptr_set_tcbQueued_'proc(PTR(thread_state_C) &(\<acute>tcb\<rightarrow>[''tcbState_C'']),SCAST(32 signed \<rightarrow> 32) true))
FI
CATCH SKIP
END {s'. option_map2 tcbEPNext_C (cslift s') = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift s') = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift s') = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift s') = option_map2 tcbDomain_C (cslift s)} proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrace>s. \<exists>d v. option_map2 tcbPriority_C (cslift s) \<acute>tcb = Some v \<and> unat v \<le> Config_H.numPriorities \<and> option_map2 tcbDomain_C (cslift s) \<acute>tcb = Some d \<and> unat d < numDomains \<and> (StateRelation_C.end_C (\<acute>ksReadyQueues.[unat (d * 0x100 + v)]) \<noteq> NULL \<longrightarrow> option_map2 tcbPriority_C (cslift s) (head_C (\<acute>ksReadyQueues.[unat (d * 0x100 + v)])) \<noteq> None \<and> option_map2 tcbDomain_C (cslift s) (head_C (\<acute>ksReadyQueues.[unat (d * 0x100 + v)])) \<noteq> None)\<rbrace> \<subseteq> {sa. sa \<Turnstile>\<^sub>c tcb_' sa \<longrightarrow> (\<forall>t. ret__unsigned_' t = tcbQueued_CL (thread_state_lift (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(thread_state_C) &(tcb_' sa\<rightarrow>[''tcbState_C''])))) \<longrightarrow> (tcbQueued_CL (thread_state_lift (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(thread_state_C) &(tcb_' sa\<rightarrow>[''tcbState_C''])))) = 0 \<longrightarrow> (numDomains \<le> 1 \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word) &(tcb_' sa\<rightarrow>[''tcbDomain_C''])) = 0) \<and> (\<forall>t. ret__unsigned_long_' t = h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word) &(tcb_' sa\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word) &(tcb_' sa\<rightarrow>[''tcbPriority_C''])) \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word) &(tcb_' sa\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word) &(tcb_' sa\<rightarrow>[''tcbPriority_C''])) < SCAST(32 signed \<rightarrow> 32) 0x1000 \<longrightarrow> (StateRelation_C.end_C (ksReadyQueues_' (globals sa).[unat (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word) &(tcb_' sa\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word) &(tcb_' sa\<rightarrow>[''tcbPriority_C''])))]) = NULL \<longrightarrow> (\<forall>t. ret__unsigned_long_' t = h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word) &(tcb_' sa\<rightarrow>[''tcbPriority_C''])) >> wordRadix \<longrightarrow> (\<forall>t. ret__unsigned_long_' t = word_of_nat l2BitmapSize - 1 - (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word) &(tcb_' sa\<rightarrow>[''tcbPriority_C''])) >> wordRadix) \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word) &(tcb_' sa\<rightarrow>[''tcbDomain_C''])) < SCAST(32 signed \<rightarrow> 32) 0x10 \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word) &(tcb_' sa\<rightarrow>[''tcbPriority_C''])) >> wordRadix < SCAST(32 signed \<rightarrow> 32) 0x20 \<longrightarrow> word_of_nat l2BitmapSize - 1 - (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word) &(tcb_' sa\<rightarrow>[''tcbPriority_C''])) >> wordRadix) < SCAST(32 signed \<rightarrow> 32) 8 \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word) &(tcb_' sa\<rightarrow>[''tcbPriority_C''])) && (1 << unat 5) - 1 < SCAST(32 signed \<rightarrow> 32) 0x20 \<longrightarrow> 0 \<le>s 5 \<longrightarrow> 5 <s 0x20 \<longrightarrow> hrs_htd (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' sa\<rightarrow>[''tcbSchedPrev_C''])) (PTR_COERCE(unit \<rightarrow> tcb_C) (PTR(unit) (SCAST(32 signed \<rightarrow> 32) 0)))) (t_hrs_' (globals sa))) \<Turnstile>\<^sub>t tcb_' sa \<longrightarrow> hrs_htd (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' sa\<rightarrow>[''tcbSchedNext_C''])) (head_C (tcb_queue_C.end_C_update (\<lambda>_. tcb_' sa) (ksReadyQueues_' (globals sa).[unat (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word) &(tcb_' sa\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word) &(tcb_' sa\<rightarrow>[''tcbPriority_C''])))])))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' sa\<rightarrow>[''tcbSchedPrev_C''])) (PTR_COERCE(unit \<rightarrow> tcb_C) (PTR(unit) (SCAST(32 signed \<rightarrow> 32) 0)))) (t_hrs_' (globals sa)))) \<Turnstile>\<^sub>t tcb_' sa \<longrightarrow> hrs_htd (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' sa\<rightarrow>[''tcbSchedNext_C''])) (head_C (tcb_queue_C.end_C_update (\<lambda>_. tcb_' sa) (ksReadyQueues_' (globals sa).[unat (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word) &(tcb_' sa\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word) &(tcb_' sa\<rightarrow>[''tcbPriority_C''])))])))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' sa\<rightarrow>[''tcbSchedPrev_C''])) (PTR_COERCE(unit \<rightarrow> tcb_C) (PTR(unit) (SCAST(32 signed \<rightarrow> 32) 0)))) (t_hrs_' (globals sa)))) \<Turnstile>\<^sub>t cparent (PTR(thread_state_C) &(tcb_' sa\<rightarrow>[''tcbState_C''])) [''tcbState_C''] \<and> (\<forall>t. (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (clift (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' sa\<rightarrow>[''tcbSchedNext_C''])) (head_C (tcb_queue_C.end_C_update (\<lambda>_. tcb_' sa) (ksReadyQueues_' (globals sa).[unat (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word) &(tcb_' sa\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word) &(tcb_' sa\<rightarrow>[''tcbPriority_C''])))])))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' sa\<rightarrow>[''tcbSchedPrev_C''])) (PTR_COERCE(unit \<rightarrow> tcb_C) (PTR(unit) (SCAST(32 signed \<rightarrow> 32) 0)))) (t_hrs_' (globals sa)))) (cparent (PTR(thread_state_C) &(tcb_' sa\<rightarrow>[''tcbState_C''])) [''tcbState_C'']))))\<lparr>tcbQueued_CL := SCAST(32 signed \<rightarrow> 32) true && mask 1\<rparr> \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cparent (PTR(thread_state_C) &(tcb_' sa\<rightarrow>[''tcbState_C''])) [''tcbState_C'']) (tcbState_C_update (\<lambda>_. thread_state) (the (clift (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' sa\<rightarrow>[''tcbSchedNext_C''])) (head_C (tcb_queue_C.end_C_update (\<lambda>_. tcb_' sa) (ksReadyQueues_' (globals sa).[unat (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word) &(tcb_' sa\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word) &(tcb_' sa\<rightarrow>[''tcbPriority_C''])))])))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' sa\<rightarrow>[''tcbSchedPrev_C''])) (PTR_COERCE(unit \<rightarrow> tcb_C) (PTR(unit) (SCAST(32 signed \<rightarrow> 32) 0)))) (t_hrs_' (globals sa)))) (cparent (PTR(thread_state_C) &(tcb_' sa\<rightarrow>[''tcbState_C''])) [''tcbState_C'']))))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' sa\<rightarrow>[''tcbSchedNext_C''])) (head_C (tcb_queue_C.end_C_update (\<lambda>_. tcb_' sa) (ksReadyQueues_' (globals sa).[unat (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word) &(tcb_' sa\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word) &(tcb_' sa\<rightarrow>[''tcbPriority_C''])))])))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' sa\<rightarrow>[''tcbSchedPrev_C''])) (PTR_COERCE(unit \<rightarrow> tcb_C) (PTR(unit) (SCAST(32 signed \<rightarrow> 32) 0)))) (t_hrs_' (globals sa))))) \<longrightarrow> option_map2 tcbEPNext_C (cslift t) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift t) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift t) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift t) = option_map2 tcbDomain_C (cslift s))))) \<and> (StateRelation_C.end_C (ksReadyQueues_' (globals sa).[unat (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word) &(tcb_' sa\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word) &(tcb_' sa\<rightarrow>[''tcbPriority_C''])))]) \<noteq> NULL \<longrightarrow> sa \<Turnstile>\<^sub>c head_C (ksReadyQueues_' (globals sa).[unat (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word) &(tcb_' sa\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word) &(tcb_' sa\<rightarrow>[''tcbPriority_C''])))]) \<longrightarrow> hrs_htd (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(head_C (ksReadyQueues_' (globals sa).[unat (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word) &(tcb_' sa\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word) &(tcb_' sa\<rightarrow>[''tcbPriority_C''])))])\<rightarrow>[''tcbSchedPrev_C''])) (tcb_' sa)) (t_hrs_' (globals sa))) \<Turnstile>\<^sub>t tcb_' sa \<longrightarrow> hrs_htd (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' sa\<rightarrow>[''tcbSchedPrev_C''])) (PTR_COERCE(unit \<rightarrow> tcb_C) (PTR(unit) (SCAST(32 signed \<rightarrow> 32) 0)))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(head_C (ksReadyQueues_' (globals sa).[unat (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word) &(tcb_' sa\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word) &(tcb_' sa\<rightarrow>[''tcbPriority_C''])))])\<rightarrow>[''tcbSchedPrev_C''])) (tcb_' sa)) (t_hrs_' (globals sa)))) \<Turnstile>\<^sub>t tcb_' sa \<longrightarrow> hrs_htd (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' sa\<rightarrow>[''tcbSchedNext_C''])) (head_C (ksReadyQueues_' (globals sa).[unat (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word) &(tcb_' sa\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word) &(tcb_' sa\<rightarrow>[''tcbPriority_C''])))]))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' sa\<rightarrow>[''tcbSchedPrev_C''])) (PTR_COERCE(unit \<rightarrow> tcb_C) (PTR(unit) (SCAST(32 signed \<rightarrow> 32) 0)))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(head_C (ksReadyQueues_' (globals sa).[unat (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word) &(tcb_' sa\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word) &(tcb_' sa\<rightarrow>[''tcbPriority_C''])))])\<rightarrow>[''tcbSchedPrev_C''])) (tcb_' sa)) (t_hrs_' (globals sa))))) \<Turnstile>\<^sub>t tcb_' sa \<longrightarrow> hrs_htd (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' sa\<rightarrow>[''tcbSchedNext_C''])) (head_C (ksReadyQueues_' (globals sa).[unat (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word) &(tcb_' sa\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word) &(tcb_' sa\<rightarrow>[''tcbPriority_C''])))]))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' sa\<rightarrow>[''tcbSchedPrev_C''])) (PTR_COERCE(unit \<rightarrow> tcb_C) (PTR(unit) (SCAST(32 signed \<rightarrow> 32) 0)))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(head_C (ksReadyQueues_' (globals sa).[unat (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word) &(tcb_' sa\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word) &(tcb_' sa\<rightarrow>[''tcbPriority_C''])))])\<rightarrow>[''tcbSchedPrev_C''])) (tcb_' sa)) (t_hrs_' (globals sa))))) \<Turnstile>\<^sub>t cparent (PTR(thread_state_C) &(tcb_' sa\<rightarrow>[''tcbState_C''])) [''tcbState_C''] \<and> (\<forall>t. (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (clift (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' sa\<rightarrow>[''tcbSchedNext_C''])) (head_C (ksReadyQueues_' (globals sa).[unat (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word) &(tcb_' sa\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word) &(tcb_' sa\<rightarrow>[''tcbPriority_C''])))]))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' sa\<rightarrow>[''tcbSchedPrev_C''])) (PTR_COERCE(unit \<rightarrow> tcb_C) (PTR(unit) (SCAST(32 signed \<rightarrow> 32) 0)))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(head_C (ksReadyQueues_' (globals sa).[unat (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word) &(tcb_' sa\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word) &(tcb_' sa\<rightarrow>[''tcbPriority_C''])))])\<rightarrow>[''tcbSchedPrev_C''])) (tcb_' sa)) (t_hrs_' (globals sa))))) (cparent (PTR(thread_state_C) &(tcb_' sa\<rightarrow>[''tcbState_C''])) [''tcbState_C'']))))\<lparr>tcbQueued_CL := SCAST(32 signed \<rightarrow> 32) true && mask 1\<rparr> \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cparent (PTR(thread_state_C) &(tcb_' sa\<rightarrow>[''tcbState_C''])) [''tcbState_C'']) (tcbState_C_update (\<lambda>_. thread_state) (the (clift (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' sa\<rightarrow>[''tcbSchedNext_C''])) (head_C (ksReadyQueues_' (globals sa).[unat (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word) &(tcb_' sa\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word) &(tcb_' sa\<rightarrow>[''tcbPriority_C''])))]))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' sa\<rightarrow>[''tcbSchedPrev_C''])) (PTR_COERCE(unit \<rightarrow> tcb_C) (PTR(unit) (SCAST(32 signed \<rightarrow> 32) 0)))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(head_C (ksReadyQueues_' (globals sa).[unat (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word) &(tcb_' sa\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word) &(tcb_' sa\<rightarrow>[''tcbPriority_C''])))])\<rightarrow>[''tcbSchedPrev_C''])) (tcb_' sa)) (t_hrs_' (globals sa))))) (cparent (PTR(thread_state_C) &(tcb_' sa\<rightarrow>[''tcbState_C''])) [''tcbState_C'']))))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' sa\<rightarrow>[''tcbSchedNext_C''])) (head_C (ksReadyQueues_' (globals sa).[unat (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word) &(tcb_' sa\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word) &(tcb_' sa\<rightarrow>[''tcbPriority_C''])))]))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' sa\<rightarrow>[''tcbSchedPrev_C''])) (PTR_COERCE(unit \<rightarrow> tcb_C) (PTR(unit) (SCAST(32 signed \<rightarrow> 32) 0)))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(head_C (ksReadyQueues_' (globals sa).[unat (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word) &(tcb_' sa\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word) &(tcb_' sa\<rightarrow>[''tcbPriority_C''])))])\<rightarrow>[''tcbSchedPrev_C''])) (tcb_' sa)) (t_hrs_' (globals sa)))))) \<longrightarrow> option_map2 tcbEPNext_C (cslift t) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift t) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift t) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift t) = option_map2 tcbDomain_C (cslift s))))) \<and> (tcbQueued_CL (thread_state_lift (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(thread_state_C) &(tcb_' sa\<rightarrow>[''tcbState_C''])))) \<noteq> 0 \<longrightarrow> option_map2 tcbEPNext_C (cslift sa) = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift sa) = option_map2 tcbEPPrev_C (cslift s) \<and> option_map2 tcbPriority_C (cslift sa) = option_map2 tcbPriority_C (cslift s) \<and> option_map2 tcbDomain_C (cslift sa) = option_map2 tcbDomain_C (cslift s)))} proof (prove)
goal (1 subgoal):
 1. \<And>x z t. \<lbrakk>unat (tcbPriority_C z) \<le> Config_H.numPriorities; unat (tcbDomain_C z) < numDomains; StateRelation_C.end_C (ksReadyQueues_' (globals x).[unat (tcbDomain_C z * 0x100 + tcbPriority_C z)]) \<noteq> NULL \<longrightarrow> (\<exists>y. cslift x (head_C (ksReadyQueues_' (globals x).[unat (tcbDomain_C z * 0x100 + tcbPriority_C z)])) = Some y); cslift x (tcb_' x) = Some z; ret__unsigned_' t = 0; tcbQueued_CL (thread_state_lift (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(thread_state_C) &(tcb_' x\<rightarrow>[''tcbState_C''])))) = 0\<rbrakk> \<Longrightarrow> (numDomains \<le> Suc 0 \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) = 0) \<and> ((\<exists>t. ret__unsigned_long_' t = h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C'']))) \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])) < 0x1000 \<longrightarrow> (StateRelation_C.end_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]) = NULL \<longrightarrow> (\<exists>t. ret__unsigned_long_' t = h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])) >> wordRadix) \<longrightarrow> (\<exists>t. ret__unsigned_long_' t = word_of_nat l2BitmapSize - 1 - (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])) >> wordRadix)) \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) < 0x10 \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])) >> wordRadix < 0x20 \<longrightarrow> word_of_nat l2BitmapSize - 1 - (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])) >> wordRadix) < 8 \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])) && 0x1F < 0x20 \<longrightarrow> (\<forall>t. (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (clift (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedNext_C''])) (head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedPrev_C''])) NULL) (t_hrs_' (globals x)))) (tcb_' x))))\<lparr>tcbQueued_CL := SCAST(32 signed \<rightarrow> 32) true\<rparr> \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (tcb_' x) (tcbState_C_update (\<lambda>_. thread_state) (the (clift (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedNext_C''])) (head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedPrev_C''])) NULL) (t_hrs_' (globals x)))) (tcb_' x))))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedNext_C''])) (head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedPrev_C''])) NULL) (t_hrs_' (globals x))))) \<longrightarrow> (\<forall>xa. map_option tcbEPNext_C (cslift t xa) = map_option tcbEPNext_C (cslift x xa)) \<and> (\<forall>xa. map_option tcbEPPrev_C (cslift t xa) = map_option tcbEPPrev_C (cslift x xa)) \<and> (\<forall>xa. map_option tcbPriority_C (cslift t xa) = map_option tcbPriority_C (cslift x xa)) \<and> (\<forall>xa. map_option tcbDomain_C (cslift t xa) = map_option tcbDomain_C (cslift x xa)))) \<and> (StateRelation_C.end_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]) \<noteq> NULL \<longrightarrow> x \<Turnstile>\<^sub>c head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]) \<longrightarrow> (\<forall>t. (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (clift (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedNext_C''])) (head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedPrev_C''])) NULL) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))])\<rightarrow>[''tcbSchedPrev_C''])) (tcb_' x)) (t_hrs_' (globals x))))) (tcb_' x))))\<lparr>tcbQueued_CL := SCAST(32 signed \<rightarrow> 32) true\<rparr> \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (tcb_' x) (tcbState_C_update (\<lambda>_. thread_state) (the (clift (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedNext_C''])) (head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedPrev_C''])) NULL) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))])\<rightarrow>[''tcbSchedPrev_C''])) (tcb_' x)) (t_hrs_' (globals x))))) (tcb_' x))))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedNext_C''])) (head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedPrev_C''])) NULL) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))])\<rightarrow>[''tcbSchedPrev_C''])) (tcb_' x)) (t_hrs_' (globals x)))))) \<longrightarrow> (\<forall>xa. map_option tcbEPNext_C (cslift t xa) = map_option tcbEPNext_C (cslift x xa)) \<and> (\<forall>xa. map_option tcbEPPrev_C (cslift t xa) = map_option tcbEPPrev_C (cslift x xa)) \<and> (\<forall>xa. map_option tcbPriority_C (cslift t xa) = map_option tcbPriority_C (cslift x xa)) \<and> (\<forall>xa. map_option tcbDomain_C (cslift t xa) = map_option tcbDomain_C (cslift x xa))))) proof (prove)
goal (2 subgoals):
 1. \<And>x z t. \<lbrakk>unat (tcbPriority_C z) \<le> Config_H.numPriorities; unat (tcbDomain_C z) < numDomains; StateRelation_C.end_C (ksReadyQueues_' (globals x).[unat (tcbDomain_C z * 0x100 + tcbPriority_C z)]) \<noteq> NULL \<longrightarrow> (\<exists>y. cslift x (head_C (ksReadyQueues_' (globals x).[unat (tcbDomain_C z * 0x100 + tcbPriority_C z)])) = Some y); cslift x (tcb_' x) = Some z; ret__unsigned_' t = 0; tcbQueued_CL (thread_state_lift (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(thread_state_C) &(tcb_' x\<rightarrow>[''tcbState_C''])))) = 0\<rbrakk> \<Longrightarrow> numDomains \<le> Suc 0 \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) = 0
 2. \<And>x z t. \<lbrakk>unat (tcbPriority_C z) \<le> Config_H.numPriorities; unat (tcbDomain_C z) < numDomains; StateRelation_C.end_C (ksReadyQueues_' (globals x).[unat (tcbDomain_C z * 0x100 + tcbPriority_C z)]) \<noteq> NULL \<longrightarrow> (\<exists>y. cslift x (head_C (ksReadyQueues_' (globals x).[unat (tcbDomain_C z * 0x100 + tcbPriority_C z)])) = Some y); cslift x (tcb_' x) = Some z; ret__unsigned_' t = 0; tcbQueued_CL (thread_state_lift (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(thread_state_C) &(tcb_' x\<rightarrow>[''tcbState_C''])))) = 0\<rbrakk> \<Longrightarrow> (\<exists>t. ret__unsigned_long_' t = h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C'']))) \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])) < 0x1000 \<longrightarrow> (StateRelation_C.end_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]) = NULL \<longrightarrow> (\<exists>t. ret__unsigned_long_' t = h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])) >> wordRadix) \<longrightarrow> (\<exists>t. ret__unsigned_long_' t = word_of_nat l2BitmapSize - 1 - (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])) >> wordRadix)) \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) < 0x10 \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])) >> wordRadix < 0x20 \<longrightarrow> word_of_nat l2BitmapSize - 1 - (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])) >> wordRadix) < 8 \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])) && 0x1F < 0x20 \<longrightarrow> (\<forall>t. (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (clift (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedNext_C''])) (head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedPrev_C''])) NULL) (t_hrs_' (globals x)))) (tcb_' x))))\<lparr>tcbQueued_CL := SCAST(32 signed \<rightarrow> 32) true\<rparr> \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (tcb_' x) (tcbState_C_update (\<lambda>_. thread_state) (the (clift (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedNext_C''])) (head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedPrev_C''])) NULL) (t_hrs_' (globals x)))) (tcb_' x))))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedNext_C''])) (head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedPrev_C''])) NULL) (t_hrs_' (globals x))))) \<longrightarrow> (\<forall>xa. map_option tcbEPNext_C (cslift t xa) = map_option tcbEPNext_C (cslift x xa)) \<and> (\<forall>xa. map_option tcbEPPrev_C (cslift t xa) = map_option tcbEPPrev_C (cslift x xa)) \<and> (\<forall>xa. map_option tcbPriority_C (cslift t xa) = map_option tcbPriority_C (cslift x xa)) \<and> (\<forall>xa. map_option tcbDomain_C (cslift t xa) = map_option tcbDomain_C (cslift x xa)))) \<and> (StateRelation_C.end_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]) \<noteq> NULL \<longrightarrow> x \<Turnstile>\<^sub>c head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]) \<longrightarrow> (\<forall>t. (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (clift (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedNext_C''])) (head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedPrev_C''])) NULL) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))])\<rightarrow>[''tcbSchedPrev_C''])) (tcb_' x)) (t_hrs_' (globals x))))) (tcb_' x))))\<lparr>tcbQueued_CL := SCAST(32 signed \<rightarrow> 32) true\<rparr> \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (tcb_' x) (tcbState_C_update (\<lambda>_. thread_state) (the (clift (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedNext_C''])) (head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedPrev_C''])) NULL) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))])\<rightarrow>[''tcbSchedPrev_C''])) (tcb_' x)) (t_hrs_' (globals x))))) (tcb_' x))))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedNext_C''])) (head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedPrev_C''])) NULL) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))])\<rightarrow>[''tcbSchedPrev_C''])) (tcb_' x)) (t_hrs_' (globals x)))))) \<longrightarrow> (\<forall>xa. map_option tcbEPNext_C (cslift t xa) = map_option tcbEPNext_C (cslift x xa)) \<and> (\<forall>xa. map_option tcbEPPrev_C (cslift t xa) = map_option tcbEPPrev_C (cslift x xa)) \<and> (\<forall>xa. map_option tcbPriority_C (cslift t xa) = map_option tcbPriority_C (cslift x xa)) \<and> (\<forall>xa. map_option tcbDomain_C (cslift t xa) = map_option tcbDomain_C (cslift x xa)))) proof (prove)
goal (2 subgoals):
 1. \<And>x z t. \<lbrakk>unat (tcbPriority_C z) \<le> Config_H.numPriorities; unat (tcbDomain_C z) < numDomains; StateRelation_C.end_C (ksReadyQueues_' (globals x).[unat (tcbDomain_C z * 0x100 + tcbPriority_C z)]) \<noteq> NULL \<longrightarrow> (\<exists>y. cslift x (head_C (ksReadyQueues_' (globals x).[unat (tcbDomain_C z * 0x100 + tcbPriority_C z)])) = Some y); cslift x (tcb_' x) = Some z; ret__unsigned_' t = 0; tcbQueued_CL (thread_state_lift (tcbState_C z)) = 0; numDomains \<le> Suc 0\<rbrakk> \<Longrightarrow> tcbDomain_C z = 0
 2. \<And>x z t. \<lbrakk>unat (tcbPriority_C z) \<le> Config_H.numPriorities; unat (tcbDomain_C z) < numDomains; StateRelation_C.end_C (ksReadyQueues_' (globals x).[unat (tcbDomain_C z * 0x100 + tcbPriority_C z)]) \<noteq> NULL \<longrightarrow> (\<exists>y. cslift x (head_C (ksReadyQueues_' (globals x).[unat (tcbDomain_C z * 0x100 + tcbPriority_C z)])) = Some y); cslift x (tcb_' x) = Some z; ret__unsigned_' t = 0; tcbQueued_CL (thread_state_lift (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(thread_state_C) &(tcb_' x\<rightarrow>[''tcbState_C''])))) = 0\<rbrakk> \<Longrightarrow> (\<exists>t. ret__unsigned_long_' t = h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C'']))) \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])) < 0x1000 \<longrightarrow> (StateRelation_C.end_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]) = NULL \<longrightarrow> (\<exists>t. ret__unsigned_long_' t = h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])) >> wordRadix) \<longrightarrow> (\<exists>t. ret__unsigned_long_' t = word_of_nat l2BitmapSize - 1 - (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])) >> wordRadix)) \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) < 0x10 \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])) >> wordRadix < 0x20 \<longrightarrow> word_of_nat l2BitmapSize - 1 - (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])) >> wordRadix) < 8 \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])) && 0x1F < 0x20 \<longrightarrow> (\<forall>t. (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (clift (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedNext_C''])) (head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedPrev_C''])) NULL) (t_hrs_' (globals x)))) (tcb_' x))))\<lparr>tcbQueued_CL := SCAST(32 signed \<rightarrow> 32) true\<rparr> \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (tcb_' x) (tcbState_C_update (\<lambda>_. thread_state) (the (clift (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedNext_C''])) (head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedPrev_C''])) NULL) (t_hrs_' (globals x)))) (tcb_' x))))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedNext_C''])) (head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedPrev_C''])) NULL) (t_hrs_' (globals x))))) \<longrightarrow> (\<forall>xa. map_option tcbEPNext_C (cslift t xa) = map_option tcbEPNext_C (cslift x xa)) \<and> (\<forall>xa. map_option tcbEPPrev_C (cslift t xa) = map_option tcbEPPrev_C (cslift x xa)) \<and> (\<forall>xa. map_option tcbPriority_C (cslift t xa) = map_option tcbPriority_C (cslift x xa)) \<and> (\<forall>xa. map_option tcbDomain_C (cslift t xa) = map_option tcbDomain_C (cslift x xa)))) \<and> (StateRelation_C.end_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]) \<noteq> NULL \<longrightarrow> x \<Turnstile>\<^sub>c head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]) \<longrightarrow> (\<forall>t. (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (clift (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedNext_C''])) (head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedPrev_C''])) NULL) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))])\<rightarrow>[''tcbSchedPrev_C''])) (tcb_' x)) (t_hrs_' (globals x))))) (tcb_' x))))\<lparr>tcbQueued_CL := SCAST(32 signed \<rightarrow> 32) true\<rparr> \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (tcb_' x) (tcbState_C_update (\<lambda>_. thread_state) (the (clift (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedNext_C''])) (head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedPrev_C''])) NULL) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))])\<rightarrow>[''tcbSchedPrev_C''])) (tcb_' x)) (t_hrs_' (globals x))))) (tcb_' x))))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedNext_C''])) (head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedPrev_C''])) NULL) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))])\<rightarrow>[''tcbSchedPrev_C''])) (tcb_' x)) (t_hrs_' (globals x)))))) \<longrightarrow> (\<forall>xa. map_option tcbEPNext_C (cslift t xa) = map_option tcbEPNext_C (cslift x xa)) \<and> (\<forall>xa. map_option tcbEPPrev_C (cslift t xa) = map_option tcbEPPrev_C (cslift x xa)) \<and> (\<forall>xa. map_option tcbPriority_C (cslift t xa) = map_option tcbPriority_C (cslift x xa)) \<and> (\<forall>xa. map_option tcbDomain_C (cslift t xa) = map_option tcbDomain_C (cslift x xa)))) proof (prove)
goal (1 subgoal):
 1. \<And>x z t. \<lbrakk>unat (tcbPriority_C z) \<le> Config_H.numPriorities; unat (tcbDomain_C z) < numDomains; StateRelation_C.end_C (ksReadyQueues_' (globals x).[unat (tcbDomain_C z * 0x100 + tcbPriority_C z)]) \<noteq> NULL \<longrightarrow> (\<exists>y. cslift x (head_C (ksReadyQueues_' (globals x).[unat (tcbDomain_C z * 0x100 + tcbPriority_C z)])) = Some y); cslift x (tcb_' x) = Some z; ret__unsigned_' t = 0; tcbQueued_CL (thread_state_lift (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(thread_state_C) &(tcb_' x\<rightarrow>[''tcbState_C''])))) = 0\<rbrakk> \<Longrightarrow> (\<exists>t. ret__unsigned_long_' t = h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C'']))) \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])) < 0x1000 \<longrightarrow> (StateRelation_C.end_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]) = NULL \<longrightarrow> (\<exists>t. ret__unsigned_long_' t = h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])) >> wordRadix) \<longrightarrow> (\<exists>t. ret__unsigned_long_' t = word_of_nat l2BitmapSize - 1 - (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])) >> wordRadix)) \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) < 0x10 \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])) >> wordRadix < 0x20 \<longrightarrow> word_of_nat l2BitmapSize - 1 - (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])) >> wordRadix) < 8 \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])) && 0x1F < 0x20 \<longrightarrow> (\<forall>t. (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (clift (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedNext_C''])) (head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedPrev_C''])) NULL) (t_hrs_' (globals x)))) (tcb_' x))))\<lparr>tcbQueued_CL := SCAST(32 signed \<rightarrow> 32) true\<rparr> \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (tcb_' x) (tcbState_C_update (\<lambda>_. thread_state) (the (clift (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedNext_C''])) (head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedPrev_C''])) NULL) (t_hrs_' (globals x)))) (tcb_' x))))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedNext_C''])) (head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedPrev_C''])) NULL) (t_hrs_' (globals x))))) \<longrightarrow> (\<forall>xa. map_option tcbEPNext_C (cslift t xa) = map_option tcbEPNext_C (cslift x xa)) \<and> (\<forall>xa. map_option tcbEPPrev_C (cslift t xa) = map_option tcbEPPrev_C (cslift x xa)) \<and> (\<forall>xa. map_option tcbPriority_C (cslift t xa) = map_option tcbPriority_C (cslift x xa)) \<and> (\<forall>xa. map_option tcbDomain_C (cslift t xa) = map_option tcbDomain_C (cslift x xa)))) \<and> (StateRelation_C.end_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]) \<noteq> NULL \<longrightarrow> x \<Turnstile>\<^sub>c head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]) \<longrightarrow> (\<forall>t. (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (clift (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedNext_C''])) (head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedPrev_C''])) NULL) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))])\<rightarrow>[''tcbSchedPrev_C''])) (tcb_' x)) (t_hrs_' (globals x))))) (tcb_' x))))\<lparr>tcbQueued_CL := SCAST(32 signed \<rightarrow> 32) true\<rparr> \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (tcb_' x) (tcbState_C_update (\<lambda>_. thread_state) (the (clift (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedNext_C''])) (head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedPrev_C''])) NULL) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))])\<rightarrow>[''tcbSchedPrev_C''])) (tcb_' x)) (t_hrs_' (globals x))))) (tcb_' x))))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedNext_C''])) (head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedPrev_C''])) NULL) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))])\<rightarrow>[''tcbSchedPrev_C''])) (tcb_' x)) (t_hrs_' (globals x)))))) \<longrightarrow> (\<forall>xa. map_option tcbEPNext_C (cslift t xa) = map_option tcbEPNext_C (cslift x xa)) \<and> (\<forall>xa. map_option tcbEPPrev_C (cslift t xa) = map_option tcbEPPrev_C (cslift x xa)) \<and> (\<forall>xa. map_option tcbPriority_C (cslift t xa) = map_option tcbPriority_C (cslift x xa)) \<and> (\<forall>xa. map_option tcbDomain_C (cslift t xa) = map_option tcbDomain_C (cslift x xa)))) proof (prove)
goal (1 subgoal):
 1. \<And>x z t ta. \<lbrakk>unat (tcbPriority_C z) \<le> Config_H.numPriorities; unat (tcbDomain_C z) < numDomains; StateRelation_C.end_C (ksReadyQueues_' (globals x).[unat (tcbDomain_C z * 0x100 + tcbPriority_C z)]) \<noteq> NULL \<longrightarrow> (\<exists>y. cslift x (head_C (ksReadyQueues_' (globals x).[unat (tcbDomain_C z * 0x100 + tcbPriority_C z)])) = Some y); cslift x (tcb_' x) = Some z; ret__unsigned_' t = 0; tcbQueued_CL (thread_state_lift (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(thread_state_C) &(tcb_' x\<rightarrow>[''tcbState_C''])))) = 0; ret__unsigned_long_' ta = h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])); h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])) < 0x1000\<rbrakk> \<Longrightarrow> (StateRelation_C.end_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]) = NULL \<longrightarrow> (\<exists>t. ret__unsigned_long_' t = h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])) >> wordRadix) \<longrightarrow> (\<exists>t. ret__unsigned_long_' t = word_of_nat l2BitmapSize - 1 - (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])) >> wordRadix)) \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) < 0x10 \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])) >> wordRadix < 0x20 \<longrightarrow> word_of_nat l2BitmapSize - 1 - (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])) >> wordRadix) < 8 \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])) && 0x1F < 0x20 \<longrightarrow> (\<forall>t. (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (clift (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedNext_C''])) (head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedPrev_C''])) NULL) (t_hrs_' (globals x)))) (tcb_' x))))\<lparr>tcbQueued_CL := SCAST(32 signed \<rightarrow> 32) true\<rparr> \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (tcb_' x) (tcbState_C_update (\<lambda>_. thread_state) (the (clift (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedNext_C''])) (head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedPrev_C''])) NULL) (t_hrs_' (globals x)))) (tcb_' x))))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedNext_C''])) (head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedPrev_C''])) NULL) (t_hrs_' (globals x))))) \<longrightarrow> (\<forall>xa. map_option tcbEPNext_C (cslift t xa) = map_option tcbEPNext_C (cslift x xa)) \<and> (\<forall>xa. map_option tcbEPPrev_C (cslift t xa) = map_option tcbEPPrev_C (cslift x xa)) \<and> (\<forall>xa. map_option tcbPriority_C (cslift t xa) = map_option tcbPriority_C (cslift x xa)) \<and> (\<forall>xa. map_option tcbDomain_C (cslift t xa) = map_option tcbDomain_C (cslift x xa)))) \<and> (StateRelation_C.end_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]) \<noteq> NULL \<longrightarrow> x \<Turnstile>\<^sub>c head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]) \<longrightarrow> (\<forall>t. (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (clift (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedNext_C''])) (head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedPrev_C''])) NULL) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))])\<rightarrow>[''tcbSchedPrev_C''])) (tcb_' x)) (t_hrs_' (globals x))))) (tcb_' x))))\<lparr>tcbQueued_CL := SCAST(32 signed \<rightarrow> 32) true\<rparr> \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (tcb_' x) (tcbState_C_update (\<lambda>_. thread_state) (the (clift (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedNext_C''])) (head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedPrev_C''])) NULL) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))])\<rightarrow>[''tcbSchedPrev_C''])) (tcb_' x)) (t_hrs_' (globals x))))) (tcb_' x))))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedNext_C''])) (head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedPrev_C''])) NULL) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))])\<rightarrow>[''tcbSchedPrev_C''])) (tcb_' x)) (t_hrs_' (globals x)))))) \<longrightarrow> (\<forall>xa. map_option tcbEPNext_C (cslift t xa) = map_option tcbEPNext_C (cslift x xa)) \<and> (\<forall>xa. map_option tcbEPPrev_C (cslift t xa) = map_option tcbEPPrev_C (cslift x xa)) \<and> (\<forall>xa. map_option tcbPriority_C (cslift t xa) = map_option tcbPriority_C (cslift x xa)) \<and> (\<forall>xa. map_option tcbDomain_C (cslift t xa) = map_option tcbDomain_C (cslift x xa)))) proof (prove)
goal (2 subgoals):
 1. \<And>x z t ta. \<lbrakk>unat (tcbPriority_C z) \<le> Config_H.numPriorities; unat (tcbDomain_C z) < numDomains; StateRelation_C.end_C (ksReadyQueues_' (globals x).[unat (tcbDomain_C z * 0x100 + tcbPriority_C z)]) \<noteq> NULL \<longrightarrow> (\<exists>y. cslift x (head_C (ksReadyQueues_' (globals x).[unat (tcbDomain_C z * 0x100 + tcbPriority_C z)])) = Some y); cslift x (tcb_' x) = Some z; ret__unsigned_' t = 0; tcbQueued_CL (thread_state_lift (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(thread_state_C) &(tcb_' x\<rightarrow>[''tcbState_C''])))) = 0; ret__unsigned_long_' ta = h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])); h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])) < 0x1000\<rbrakk> \<Longrightarrow> StateRelation_C.end_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]) = NULL \<longrightarrow> (\<exists>t. ret__unsigned_long_' t = h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])) >> wordRadix) \<longrightarrow> (\<exists>t. ret__unsigned_long_' t = word_of_nat l2BitmapSize - 1 - (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])) >> wordRadix)) \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) < 0x10 \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])) >> wordRadix < 0x20 \<longrightarrow> word_of_nat l2BitmapSize - 1 - (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])) >> wordRadix) < 8 \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])) && 0x1F < 0x20 \<longrightarrow> (\<forall>t. (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (clift (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedNext_C''])) (head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedPrev_C''])) NULL) (t_hrs_' (globals x)))) (tcb_' x))))\<lparr>tcbQueued_CL := SCAST(32 signed \<rightarrow> 32) true\<rparr> \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (tcb_' x) (tcbState_C_update (\<lambda>_. thread_state) (the (clift (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedNext_C''])) (head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedPrev_C''])) NULL) (t_hrs_' (globals x)))) (tcb_' x))))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedNext_C''])) (head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedPrev_C''])) NULL) (t_hrs_' (globals x))))) \<longrightarrow> (\<forall>xa. map_option tcbEPNext_C (cslift t xa) = map_option tcbEPNext_C (cslift x xa)) \<and> (\<forall>xa. map_option tcbEPPrev_C (cslift t xa) = map_option tcbEPPrev_C (cslift x xa)) \<and> (\<forall>xa. map_option tcbPriority_C (cslift t xa) = map_option tcbPriority_C (cslift x xa)) \<and> (\<forall>xa. map_option tcbDomain_C (cslift t xa) = map_option tcbDomain_C (cslift x xa)))
 2. \<And>x z t ta. \<lbrakk>unat (tcbPriority_C z) \<le> Config_H.numPriorities; unat (tcbDomain_C z) < numDomains; StateRelation_C.end_C (ksReadyQueues_' (globals x).[unat (tcbDomain_C z * 0x100 + tcbPriority_C z)]) \<noteq> NULL \<longrightarrow> (\<exists>y. cslift x (head_C (ksReadyQueues_' (globals x).[unat (tcbDomain_C z * 0x100 + tcbPriority_C z)])) = Some y); cslift x (tcb_' x) = Some z; ret__unsigned_' t = 0; tcbQueued_CL (thread_state_lift (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(thread_state_C) &(tcb_' x\<rightarrow>[''tcbState_C''])))) = 0; ret__unsigned_long_' ta = h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])); h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])) < 0x1000\<rbrakk> \<Longrightarrow> StateRelation_C.end_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]) \<noteq> NULL \<longrightarrow> x \<Turnstile>\<^sub>c head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]) \<longrightarrow> (\<forall>t. (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (clift (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedNext_C''])) (head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedPrev_C''])) NULL) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))])\<rightarrow>[''tcbSchedPrev_C''])) (tcb_' x)) (t_hrs_' (globals x))))) (tcb_' x))))\<lparr>tcbQueued_CL := SCAST(32 signed \<rightarrow> 32) true\<rparr> \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (tcb_' x) (tcbState_C_update (\<lambda>_. thread_state) (the (clift (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedNext_C''])) (head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedPrev_C''])) NULL) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))])\<rightarrow>[''tcbSchedPrev_C''])) (tcb_' x)) (t_hrs_' (globals x))))) (tcb_' x))))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedNext_C''])) (head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedPrev_C''])) NULL) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))])\<rightarrow>[''tcbSchedPrev_C''])) (tcb_' x)) (t_hrs_' (globals x)))))) \<longrightarrow> (\<forall>xa. map_option tcbEPNext_C (cslift t xa) = map_option tcbEPNext_C (cslift x xa)) \<and> (\<forall>xa. map_option tcbEPPrev_C (cslift t xa) = map_option tcbEPPrev_C (cslift x xa)) \<and> (\<forall>xa. map_option tcbPriority_C (cslift t xa) = map_option tcbPriority_C (cslift x xa)) \<and> (\<forall>xa. map_option tcbDomain_C (cslift t xa) = map_option tcbDomain_C (cslift x xa))) proof (prove)
goal (2 subgoals):
 1. \<And>x z t ta tb tc td thread_state. \<lbrakk>unat (tcbPriority_C z) \<le> Config_H.numPriorities; unat (tcbDomain_C z) < numDomains; cslift x (tcb_' x) = Some z; ret__unsigned_' t = 0; tcbQueued_CL (thread_state_lift (tcbState_C z)) = 0; ret__unsigned_long_' ta = tcbDomain_C z * 0x100 + tcbPriority_C z; tcbDomain_C z * 0x100 + tcbPriority_C z < 0x1000; StateRelation_C.end_C (ksReadyQueues_' (globals x).[unat (tcbDomain_C z * 0x100 + tcbPriority_C z)]) = NULL; ret__unsigned_long_' tb = tcbPriority_C z >> wordRadix; ret__unsigned_long_' tc = word_of_nat l2BitmapSize - 1 - (tcbPriority_C z >> wordRadix); tcbDomain_C z < 0x10; tcbPriority_C z >> wordRadix < 0x20; word_of_nat l2BitmapSize - 1 - (tcbPriority_C z >> wordRadix) < 8; tcbPriority_C z && 0x1F < 0x20; thread_state_lift thread_state = thread_state_lift (tcbState_C z)\<lparr>tcbQueued_CL := SCAST(32 signed \<rightarrow> 32) true\<rparr>; t_hrs_' (globals td) = hrs_mem_update (heap_update (tcb_' x) (tcbSchedPrev_C_update (\<lambda>_. NULL) (tcbSchedNext_C_update (\<lambda>_. head_C (ksReadyQueues_' (globals x).[unat (tcbDomain_C z * 0x100 + tcbPriority_C z)])) (tcbState_C_update (\<lambda>_. thread_state) z)))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedNext_C''])) (head_C (ksReadyQueues_' (globals x).[unat (tcbDomain_C z * 0x100 + tcbPriority_C z)]))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedPrev_C''])) NULL) (t_hrs_' (globals x))))\<rbrakk> \<Longrightarrow> (\<forall>xa. map_option tcbEPNext_C (if xa = tcb_' x then Some (tcbSchedPrev_C_update (\<lambda>_. NULL) (tcbSchedNext_C_update (\<lambda>_. head_C (ksReadyQueues_' (globals x).[unat (tcbDomain_C z * 0x100 + tcbPriority_C z)])) (tcbState_C_update (\<lambda>_. thread_state) z))) else cslift x xa) = map_option tcbEPNext_C (cslift x xa)) \<and> (\<forall>xa. map_option tcbEPPrev_C (if xa = tcb_' x then Some (tcbSchedPrev_C_update (\<lambda>_. NULL) (tcbSchedNext_C_update (\<lambda>_. head_C (ksReadyQueues_' (globals x).[unat (tcbDomain_C z * 0x100 + tcbPriority_C z)])) (tcbState_C_update (\<lambda>_. thread_state) z))) else cslift x xa) = map_option tcbEPPrev_C (cslift x xa)) \<and> (\<forall>xa. map_option tcbPriority_C (if xa = tcb_' x then Some (tcbSchedPrev_C_update (\<lambda>_. NULL) (tcbSchedNext_C_update (\<lambda>_. head_C (ksReadyQueues_' (globals x).[unat (tcbDomain_C z * 0x100 + tcbPriority_C z)])) (tcbState_C_update (\<lambda>_. thread_state) z))) else cslift x xa) = map_option tcbPriority_C (cslift x xa)) \<and> (\<forall>xa. map_option tcbDomain_C (if xa = tcb_' x then Some (tcbSchedPrev_C_update (\<lambda>_. NULL) (tcbSchedNext_C_update (\<lambda>_. head_C (ksReadyQueues_' (globals x).[unat (tcbDomain_C z * 0x100 + tcbPriority_C z)])) (tcbState_C_update (\<lambda>_. thread_state) z))) else cslift x xa) = map_option tcbDomain_C (cslift x xa))
 2. \<And>x z t ta. \<lbrakk>unat (tcbPriority_C z) \<le> Config_H.numPriorities; unat (tcbDomain_C z) < numDomains; StateRelation_C.end_C (ksReadyQueues_' (globals x).[unat (tcbDomain_C z * 0x100 + tcbPriority_C z)]) \<noteq> NULL \<longrightarrow> (\<exists>y. cslift x (head_C (ksReadyQueues_' (globals x).[unat (tcbDomain_C z * 0x100 + tcbPriority_C z)])) = Some y); cslift x (tcb_' x) = Some z; ret__unsigned_' t = 0; tcbQueued_CL (thread_state_lift (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(thread_state_C) &(tcb_' x\<rightarrow>[''tcbState_C''])))) = 0; ret__unsigned_long_' ta = h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])); h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])) < 0x1000\<rbrakk> \<Longrightarrow> StateRelation_C.end_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]) \<noteq> NULL \<longrightarrow> x \<Turnstile>\<^sub>c head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]) \<longrightarrow> (\<forall>t. (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (clift (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedNext_C''])) (head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedPrev_C''])) NULL) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))])\<rightarrow>[''tcbSchedPrev_C''])) (tcb_' x)) (t_hrs_' (globals x))))) (tcb_' x))))\<lparr>tcbQueued_CL := SCAST(32 signed \<rightarrow> 32) true\<rparr> \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (tcb_' x) (tcbState_C_update (\<lambda>_. thread_state) (the (clift (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedNext_C''])) (head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedPrev_C''])) NULL) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))])\<rightarrow>[''tcbSchedPrev_C''])) (tcb_' x)) (t_hrs_' (globals x))))) (tcb_' x))))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedNext_C''])) (head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedPrev_C''])) NULL) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))])\<rightarrow>[''tcbSchedPrev_C''])) (tcb_' x)) (t_hrs_' (globals x)))))) \<longrightarrow> (\<forall>xa. map_option tcbEPNext_C (cslift t xa) = map_option tcbEPNext_C (cslift x xa)) \<and> (\<forall>xa. map_option tcbEPPrev_C (cslift t xa) = map_option tcbEPPrev_C (cslift x xa)) \<and> (\<forall>xa. map_option tcbPriority_C (cslift t xa) = map_option tcbPriority_C (cslift x xa)) \<and> (\<forall>xa. map_option tcbDomain_C (cslift t xa) = map_option tcbDomain_C (cslift x xa))) proof (prove)
goal (1 subgoal):
 1. \<And>x z t ta. \<lbrakk>unat (tcbPriority_C z) \<le> Config_H.numPriorities; unat (tcbDomain_C z) < numDomains; StateRelation_C.end_C (ksReadyQueues_' (globals x).[unat (tcbDomain_C z * 0x100 + tcbPriority_C z)]) \<noteq> NULL \<longrightarrow> (\<exists>y. cslift x (head_C (ksReadyQueues_' (globals x).[unat (tcbDomain_C z * 0x100 + tcbPriority_C z)])) = Some y); cslift x (tcb_' x) = Some z; ret__unsigned_' t = 0; tcbQueued_CL (thread_state_lift (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(thread_state_C) &(tcb_' x\<rightarrow>[''tcbState_C''])))) = 0; ret__unsigned_long_' ta = h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])); h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])) < 0x1000\<rbrakk> \<Longrightarrow> StateRelation_C.end_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]) \<noteq> NULL \<longrightarrow> x \<Turnstile>\<^sub>c head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]) \<longrightarrow> (\<forall>t. (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (clift (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedNext_C''])) (head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedPrev_C''])) NULL) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))])\<rightarrow>[''tcbSchedPrev_C''])) (tcb_' x)) (t_hrs_' (globals x))))) (tcb_' x))))\<lparr>tcbQueued_CL := SCAST(32 signed \<rightarrow> 32) true\<rparr> \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (tcb_' x) (tcbState_C_update (\<lambda>_. thread_state) (the (clift (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedNext_C''])) (head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedPrev_C''])) NULL) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))])\<rightarrow>[''tcbSchedPrev_C''])) (tcb_' x)) (t_hrs_' (globals x))))) (tcb_' x))))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedNext_C''])) (head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))]))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedPrev_C''])) NULL) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(head_C (ksReadyQueues_' (globals x).[unat (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbDomain_C''])) * 0x100 + h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word) &(tcb_' x\<rightarrow>[''tcbPriority_C''])))])\<rightarrow>[''tcbSchedPrev_C''])) (tcb_' x)) (t_hrs_' (globals x)))))) \<longrightarrow> (\<forall>xa. map_option tcbEPNext_C (cslift t xa) = map_option tcbEPNext_C (cslift x xa)) \<and> (\<forall>xa. map_option tcbEPPrev_C (cslift t xa) = map_option tcbEPPrev_C (cslift x xa)) \<and> (\<forall>xa. map_option tcbPriority_C (cslift t xa) = map_option tcbPriority_C (cslift x xa)) \<and> (\<forall>xa. map_option tcbDomain_C (cslift t xa) = map_option tcbDomain_C (cslift x xa))) proof (prove)
goal (1 subgoal):
 1. \<And>x z t ta tb thread_state y. \<lbrakk>unat (tcbPriority_C z) \<le> Config_H.numPriorities; unat (tcbDomain_C z) < numDomains; cslift x (tcb_' x) = Some z; ret__unsigned_' t = 0; tcbQueued_CL (thread_state_lift (tcbState_C z)) = 0; ret__unsigned_long_' ta = tcbDomain_C z * 0x100 + tcbPriority_C z; tcbDomain_C z * 0x100 + tcbPriority_C z < 0x1000; StateRelation_C.end_C (ksReadyQueues_' (globals x).[unat (tcbDomain_C z * 0x100 + tcbPriority_C z)]) \<noteq> NULL; thread_state_lift thread_state = thread_state_lift (tcbState_C (if tcb_' x = head_C (ksReadyQueues_' (globals x).[unat (tcbDomain_C z * 0x100 + tcbPriority_C z)]) then tcbSchedPrev_C_update (\<lambda>_. head_C (ksReadyQueues_' (globals x).[unat (tcbDomain_C z * 0x100 + tcbPriority_C z)])) y else z))\<lparr>tcbQueued_CL := SCAST(32 signed \<rightarrow> 32) true\<rparr>; t_hrs_' (globals tb) = hrs_mem_update (heap_update (tcb_' x) (tcbSchedPrev_C_update (\<lambda>_. NULL) (tcbSchedNext_C_update (\<lambda>_. head_C (ksReadyQueues_' (globals x).[unat (tcbDomain_C z * 0x100 + tcbPriority_C z)])) (tcbState_C_update (\<lambda>_. thread_state) (if tcb_' x = head_C (ksReadyQueues_' (globals x).[unat (tcbDomain_C z * 0x100 + tcbPriority_C z)]) then tcbSchedPrev_C_update (\<lambda>_. head_C (ksReadyQueues_' (globals x).[unat (tcbDomain_C z * 0x100 + tcbPriority_C z)])) y else z))))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedNext_C''])) (head_C (ksReadyQueues_' (globals x).[unat (tcbDomain_C z * 0x100 + tcbPriority_C z)]))) (hrs_mem_update (heap_update (PTR(tcb_C ptr) &(tcb_' x\<rightarrow>[''tcbSchedPrev_C''])) NULL) (hrs_mem_update (heap_update (head_C (ksReadyQueues_' (globals x).[unat (tcbDomain_C z * 0x100 + tcbPriority_C z)])) (tcbSchedPrev_C_update (\<lambda>_. tcb_' x) y)) (t_hrs_' (globals x))))); cslift x (head_C (ksReadyQueues_' (globals x).[unat (tcbDomain_C z * 0x100 + tcbPriority_C z)])) = Some y\<rbrakk> \<Longrightarrow> (\<forall>xa. map_option tcbEPNext_C (if xa = tcb_' x then Some (tcbSchedPrev_C_update (\<lambda>_. NULL) (tcbSchedNext_C_update (\<lambda>_. head_C (ksReadyQueues_' (globals x).[unat (tcbDomain_C z * 0x100 + tcbPriority_C z)])) (tcbState_C_update (\<lambda>_. thread_state) (if tcb_' x = head_C (ksReadyQueues_' (globals x).[unat (tcbDomain_C z * 0x100 + tcbPriority_C z)]) then tcbSchedPrev_C_update (\<lambda>_. head_C (ksReadyQueues_' (globals x).[unat (tcbDomain_C z * 0x100 + tcbPriority_C z)])) y else z)))) else if xa = head_C (ksReadyQueues_' (globals x).[unat (tcbDomain_C z * 0x100 + tcbPriority_C z)]) then Some (tcbSchedPrev_C_update (\<lambda>_. tcb_' x) y) else cslift x xa) = map_option tcbEPNext_C (cslift x xa)) \<and> (\<forall>xa. map_option tcbEPPrev_C (if xa = tcb_' x then Some (tcbSchedPrev_C_update (\<lambda>_. NULL) (tcbSchedNext_C_update (\<lambda>_. head_C (ksReadyQueues_' (globals x).[unat (tcbDomain_C z * 0x100 + tcbPriority_C z)])) (tcbState_C_update (\<lambda>_. thread_state) (if tcb_' x = head_C (ksReadyQueues_' (globals x).[unat (tcbDomain_C z * 0x100 + tcbPriority_C z)]) then tcbSchedPrev_C_update (\<lambda>_. head_C (ksReadyQueues_' (globals x).[unat (tcbDomain_C z * 0x100 + tcbPriority_C z)])) y else z)))) else if xa = head_C (ksReadyQueues_' (globals x).[unat (tcbDomain_C z * 0x100 + tcbPriority_C z)]) then Some (tcbSchedPrev_C_update (\<lambda>_. tcb_' x) y) else cslift x xa) = map_option tcbEPPrev_C (cslift x xa)) \<and> (\<forall>xa. map_option tcbPriority_C (if xa = tcb_' x then Some (tcbSchedPrev_C_update (\<lambda>_. NULL) (tcbSchedNext_C_update (\<lambda>_. head_C (ksReadyQueues_' (globals x).[unat (tcbDomain_C z * 0x100 + tcbPriority_C z)])) (tcbState_C_update (\<lambda>_. thread_state) (if tcb_' x = head_C (ksReadyQueues_' (globals x).[unat (tcbDomain_C z * 0x100 + tcbPriority_C z)]) then tcbSchedPrev_C_update (\<lambda>_. head_C (ksReadyQueues_' (globals x).[unat (tcbDomain_C z * 0x100 + tcbPriority_C z)])) y else z)))) else if xa = head_C (ksReadyQueues_' (globals x).[unat (tcbDomain_C z * 0x100 + tcbPriority_C z)]) then Some (tcbSchedPrev_C_update (\<lambda>_. tcb_' x) y) else cslift x xa) = map_option tcbPriority_C (cslift x xa)) \<and> (\<forall>xa. map_option tcbDomain_C (if xa = tcb_' x then Some (tcbSchedPrev_C_update (\<lambda>_. NULL) (tcbSchedNext_C_update (\<lambda>_. head_C (ksReadyQueues_' (globals x).[unat (tcbDomain_C z * 0x100 + tcbPriority_C z)])) (tcbState_C_update (\<lambda>_. thread_state) (if tcb_' x = head_C (ksReadyQueues_' (globals x).[unat (tcbDomain_C z * 0x100 + tcbPriority_C z)]) then tcbSchedPrev_C_update (\<lambda>_. head_C (ksReadyQueues_' (globals x).[unat (tcbDomain_C z * 0x100 + tcbPriority_C z)])) y else z)))) else if xa = head_C (ksReadyQueues_' (globals x).[unat (tcbDomain_C z * 0x100 + tcbPriority_C z)]) then Some (tcbSchedPrev_C_update (\<lambda>_. tcb_' x) y) else cslift x xa) = map_option tcbDomain_C (cslift x xa))