theory Retype_C

lemma threadSet_domain_ccorres [corres]:
  "ccorres dc xfdc (tcb_at' thread) {s. thread' s = tcb_ptr_to_ctcb_ptr thread \<and> d' s = ucast d} hs
           (threadSet (tcbDomain_update (\<lambda>_. d)) thread)
           (Basic (\<lambda>s. globals_update (t_hrs_'_update (hrs_mem_update (heap_update (Ptr &(thread' s\<rightarrow>[''tcbDomain_C''])::word32 ptr) (d' s)))) s))" apply (rule ccorres_guard_imp2) apply (rule threadSet_ccorres_lemma4 [where P=\<top> and P'=\<top>]) apply vcg prefer 2 apply (rule conjI, simp) apply assumption apply clarsimp apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def) apply (clarsimp simp: cmachine_state_relation_def carch_state_relation_def cpspace_relation_def) apply (clarsimp simp: update_tcb_map_tos typ_heap_simps') apply (simp add: map_to_ctes_upd_tcb_no_ctes map_to_tcbs_upd tcb_cte_cases_def) apply (simp add: cep_relations_drop_fun_upd
                   cvariable_relation_upd_const ko_at_projectKO_opt) apply (rule conjI) defer apply (erule cready_queues_relation_not_queue_ptrs) apply (rule ext, simp split: if_split) apply (rule ext, simp split: if_split) apply (drule ko_at_projectKO_opt) apply (erule (2) cmap_relation_upd_relI) subgoal by (simp add: ctcb_relation_def) apply assumption by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (tcb_at' thread) {s. thread' s = tcb_ptr_to_ctcb_ptr thread \<and> d' s = UCAST(8 \<rightarrow> 32) d} hs (threadSet (tcbDomain_update (\<lambda>_. d)) thread) (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) &(\<acute>thread'\<rightarrow>[''tcbDomain_C''])) \<acute>d'))) proof (prove)
goal (2 subgoals):
 1. ccorres dc xfdc ?Q ?Q' hs (threadSet (tcbDomain_update (\<lambda>_. d)) thread) (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) &(\<acute>thread'\<rightarrow>[''tcbDomain_C''])) \<acute>d')))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; tcb_at' thread s; s' \<in> {s. thread' s = tcb_ptr_to_ctcb_ptr thread \<and> d' s = UCAST(8 \<rightarrow> 32) d}\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?Q' proof (prove)
goal (3 subgoals):
 1. \<And>s tcb. \<Gamma>\<turnstile> (?Q3 s tcb) \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) &(\<acute>thread'\<rightarrow>[''tcbDomain_C''])) \<acute>d')) {s'. (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> injectKOS (tcbDomain_update (\<lambda>_. d) tcb))\<rparr>, s') \<in> rf_sr}
 2. \<And>s s' tcb tcb'. \<lbrakk>(s, s') \<in> rf_sr; True; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; True; s' \<in> ?Q'\<rbrakk> \<Longrightarrow> s' \<in> ?Q3 s tcb
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; tcb_at' thread s; s' \<in> {s. thread' s = tcb_ptr_to_ctcb_ptr thread \<and> d' s = UCAST(8 \<rightarrow> 32) d}\<rbrakk> \<Longrightarrow> (tcb_at' thread and (\<lambda>_. True)) s \<and> s' \<in> ?Q' proof (prove)
goal (2 subgoals):
 1. \<And>s s' tcb tcb'. \<lbrakk>(s, s') \<in> rf_sr; True; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; True; s' \<in> ?Q'\<rbrakk> \<Longrightarrow> s' \<in> {sa. (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> injectKOS (tcbDomain_update (\<lambda>_. d) tcb))\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) &(thread' sa\<rightarrow>[''tcbDomain_C''])) (d' sa)))) sa) \<in> rf_sr}
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; tcb_at' thread s; s' \<in> {s. thread' s = tcb_ptr_to_ctcb_ptr thread \<and> d' s = UCAST(8 \<rightarrow> 32) d}\<rbrakk> \<Longrightarrow> (tcb_at' thread and (\<lambda>_. True)) s \<and> s' \<in> ?Q' proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; tcb_at' thread s; s' \<in> {s. thread' s = tcb_ptr_to_ctcb_ptr thread \<and> d' s = UCAST(8 \<rightarrow> 32) d}\<rbrakk> \<Longrightarrow> (tcb_at' thread and (\<lambda>_. True)) s \<and> s' \<in> ?Q'
 2. \<And>s s' tcb tcb'. \<lbrakk>(s, s') \<in> rf_sr; True; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; True; s' \<in> ?Q'\<rbrakk> \<Longrightarrow> s' \<in> {sa. (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> injectKOS (tcbDomain_update (\<lambda>_. d) tcb))\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) &(thread' sa\<rightarrow>[''tcbDomain_C''])) (d' sa)))) sa) \<in> rf_sr} proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; tcb_at' thread s; s' \<in> {s. thread' s = tcb_ptr_to_ctcb_ptr thread \<and> d' s = UCAST(8 \<rightarrow> 32) d}\<rbrakk> \<Longrightarrow> s' \<in> ?Q'
 2. \<And>s s' tcb tcb'. \<lbrakk>(s, s') \<in> rf_sr; True; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; True; s' \<in> ?Q'\<rbrakk> \<Longrightarrow> s' \<in> {sa. (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> injectKOS (tcbDomain_update (\<lambda>_. d) tcb))\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) &(thread' sa\<rightarrow>[''tcbDomain_C''])) (d' sa)))) sa) \<in> rf_sr} proof (prove)
goal (1 subgoal):
 1. \<And>s s' tcb tcb'. \<lbrakk>(s, s') \<in> rf_sr; True; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; True; s' \<in> {s. thread' s = tcb_ptr_to_ctcb_ptr thread \<and> d' s = UCAST(8 \<rightarrow> 32) d}\<rbrakk> \<Longrightarrow> s' \<in> {sa. (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> injectKOS (tcbDomain_update (\<lambda>_. d) tcb))\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) &(thread' sa\<rightarrow>[''tcbDomain_C''])) (d' sa)))) sa) \<in> rf_sr} proof (prove)
goal (1 subgoal):
 1. \<And>s s' tcb tcb'. \<lbrakk>(s, s') \<in> rf_sr; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; thread' s' = tcb_ptr_to_ctcb_ptr thread; d' s' = UCAST(8 \<rightarrow> 32) d\<rbrakk> \<Longrightarrow> (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> KOTCB (tcbDomain_update (\<lambda>_. d) tcb))\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbDomain_C''])) (UCAST(8 \<rightarrow> 32) d)))) s') \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>s s' tcb tcb'. \<lbrakk>ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; thread' s' = tcb_ptr_to_ctcb_ptr thread; d' s' = UCAST(8 \<rightarrow> 32) d; cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) (t_hrs_' (globals s')); cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')); carch_state_relation (ksArchState s) (globals s'); cmachine_state_relation (ksMachineState s) (globals s'); cte_array_relation s (globals s'); tcb_cte_array_relation s (globals s'); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s\<rbrakk> \<Longrightarrow> cpspace_relation ((ksPSpace s)(thread \<mapsto> KOTCB (tcbDomain_update (\<lambda>_. d) tcb))) (underlying_memory (ksMachineState s)) (hrs_mem_update (heap_update (PTR(32 word) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbDomain_C''])) (UCAST(8 \<rightarrow> 32) d)) (t_hrs_' (globals s'))) \<and> cready_queues_relation (clift (hrs_mem_update (heap_update (PTR(32 word) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbDomain_C''])) (UCAST(8 \<rightarrow> 32) d)) (t_hrs_' (globals s')))) (ksReadyQueues_' (globals s')) (ksReadyQueues s) \<and> zero_ranges_are_zero (gsUntypedZeroRanges s) (hrs_mem_update (heap_update (PTR(32 word) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbDomain_C''])) (UCAST(8 \<rightarrow> 32) d)) (t_hrs_' (globals s'))) \<and> carch_state_relation (ksArchState s) (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbDomain_C''])) (UCAST(8 \<rightarrow> 32) d))) (globals s')) \<and> cmachine_state_relation (ksMachineState s) (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbDomain_C''])) (UCAST(8 \<rightarrow> 32) d))) (globals s')) \<and> cvariable_array_map_relation (map_to_tcbs ((ksPSpace s)(thread \<mapsto> KOTCB (tcbDomain_update (\<lambda>_. d) tcb)))) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (1 subgoal):
 1. \<And>s s' tcb tcb'. \<lbrakk>ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; thread' s' = tcb_ptr_to_ctcb_ptr thread; d' s' = UCAST(8 \<rightarrow> 32) d; cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')); cte_array_relation s (globals s'); tcb_cte_array_relation s (globals s'); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s; cmap_relation (ctes_of s) (cslift s') cte_Ptr ccte_relation; armKSNextASID_' (globals s') = armKSNextASID (ksArchState s); irq_masks (ksMachineState s) = irq_masks (phantom_machine_state_' (globals s')); cmap_relation (map_to_tcbs (ksPSpace s)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation; armKSKernelVSpace_C = armKSKernelVSpace (ksArchState s); irq_state (ksMachineState s) = irq_state (phantom_machine_state_' (globals s')); cmap_relation (map_to_eps (ksPSpace s)) (cslift s') ep_Ptr (cendpoint_relation (cslift s')); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState s)) (armKSHWASIDTable_' (globals s')); device_state (ksMachineState s) = device_state (phantom_machine_state_' (globals s')); cmap_relation (map_to_ntfns (ksPSpace s)) (cslift s') ntfn_Ptr (cnotification_relation (cslift s')); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState s)) (armKSASIDTable_' (globals s')); exclusive_state (ksMachineState s) = exclusive_state (phantom_machine_state_' (globals s')); machine_state_rest (ksMachineState s) = machine_state_rest (phantom_machine_state_' (globals s')); cmap_relation (map_to_pdes (ksPSpace s)) (cslift s') pde_Ptr cpde_relation; asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift s' \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState s); cmap_relation (map_to_ptes (ksPSpace s)) (cslift s') pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (cslift s') ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s)) (c_h_t_valid s') pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s)) (c_h_t_valid s') pt_Ptr\<rbrakk> \<Longrightarrow> cmap_relation (map_to_ctes ((ksPSpace s)(thread \<mapsto> KOTCB (tcbDomain_update (\<lambda>_. d) tcb)))) (clift (hrs_mem_update (heap_update (PTR(32 word) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbDomain_C''])) (UCAST(8 \<rightarrow> 32) d)) (t_hrs_' (globals s')))) cte_Ptr ccte_relation \<and> cpspace_tcb_relation ((ksPSpace s)(thread \<mapsto> KOTCB (tcbDomain_update (\<lambda>_. d) tcb))) (hrs_mem_update (heap_update (PTR(32 word) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbDomain_C''])) (UCAST(8 \<rightarrow> 32) d)) (t_hrs_' (globals s'))) \<and> cmap_relation (map_to_eps ((ksPSpace s)(thread \<mapsto> KOTCB (tcbDomain_update (\<lambda>_. d) tcb)))) (clift (hrs_mem_update (heap_update (PTR(32 word) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbDomain_C''])) (UCAST(8 \<rightarrow> 32) d)) (t_hrs_' (globals s')))) ep_Ptr (cendpoint_relation (clift (hrs_mem_update (heap_update (PTR(32 word) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbDomain_C''])) (UCAST(8 \<rightarrow> 32) d)) (t_hrs_' (globals s'))))) \<and> cmap_relation (map_to_ntfns ((ksPSpace s)(thread \<mapsto> KOTCB (tcbDomain_update (\<lambda>_. d) tcb)))) (clift (hrs_mem_update (heap_update (PTR(32 word) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbDomain_C''])) (UCAST(8 \<rightarrow> 32) d)) (t_hrs_' (globals s')))) ntfn_Ptr (cnotification_relation (clift (hrs_mem_update (heap_update (PTR(32 word) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbDomain_C''])) (UCAST(8 \<rightarrow> 32) d)) (t_hrs_' (globals s'))))) \<and> cmap_relation (map_to_pdes ((ksPSpace s)(thread \<mapsto> KOTCB (tcbDomain_update (\<lambda>_. d) tcb)))) (clift (hrs_mem_update (heap_update (PTR(32 word) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbDomain_C''])) (UCAST(8 \<rightarrow> 32) d)) (t_hrs_' (globals s')))) pde_Ptr cpde_relation \<and> cmap_relation (map_to_ptes ((ksPSpace s)(thread \<mapsto> KOTCB (tcbDomain_update (\<lambda>_. d) tcb)))) (clift (hrs_mem_update (heap_update (PTR(32 word) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbDomain_C''])) (UCAST(8 \<rightarrow> 32) d)) (t_hrs_' (globals s')))) pte_Ptr cpte_relation \<and> cmap_relation (map_to_asidpools ((ksPSpace s)(thread \<mapsto> KOTCB (tcbDomain_update (\<lambda>_. d) tcb)))) (clift (hrs_mem_update (heap_update (PTR(32 word) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbDomain_C''])) (UCAST(8 \<rightarrow> 32) d)) (t_hrs_' (globals s')))) ap_Ptr casid_pool_relation \<and> cpspace_user_data_relation ((ksPSpace s)(thread \<mapsto> KOTCB (tcbDomain_update (\<lambda>_. d) tcb))) (underlying_memory (ksMachineState s)) (hrs_mem_update (heap_update (PTR(32 word) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbDomain_C''])) (UCAST(8 \<rightarrow> 32) d)) (t_hrs_' (globals s'))) \<and> cpspace_device_data_relation ((ksPSpace s)(thread \<mapsto> KOTCB (tcbDomain_update (\<lambda>_. d) tcb))) (underlying_memory (ksMachineState s)) (hrs_mem_update (heap_update (PTR(32 word) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbDomain_C''])) (UCAST(8 \<rightarrow> 32) d)) (t_hrs_' (globals s'))) \<and> carray_map_relation pdBits (map_to_pdes ((ksPSpace s)(thread \<mapsto> KOTCB (tcbDomain_update (\<lambda>_. d) tcb)))) (c_h_t_valid s') pd_Ptr \<and> carray_map_relation ptBits (map_to_ptes ((ksPSpace s)(thread \<mapsto> KOTCB (tcbDomain_update (\<lambda>_. d) tcb)))) (c_h_t_valid s') pt_Ptr \<and> cready_queues_relation (clift (hrs_mem_update (heap_update (PTR(32 word) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbDomain_C''])) (UCAST(8 \<rightarrow> 32) d)) (t_hrs_' (globals s')))) (ksReadyQueues_' (globals s')) (ksReadyQueues s) \<and> zero_ranges_are_zero (gsUntypedZeroRanges s) (hrs_mem_update (heap_update (PTR(32 word) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbDomain_C''])) (UCAST(8 \<rightarrow> 32) d)) (t_hrs_' (globals s'))) \<and> set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift s' \<circ>\<^sub>m pd_pointer_to_asid_slot) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (hrs_mem_update (heap_update (PTR(32 word) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbDomain_C''])) (UCAST(8 \<rightarrow> 32) d)) (t_hrs_' (globals s'))) \<circ>\<^sub>m pd_pointer_to_asid_slot) \<and> cvariable_array_map_relation (map_to_tcbs ((ksPSpace s)(thread \<mapsto> KOTCB (tcbDomain_update (\<lambda>_. d) tcb)))) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (1 subgoal):
 1. \<And>s s' tcb tcb'. \<lbrakk>ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; thread' s' = tcb_ptr_to_ctcb_ptr thread; d' s' = UCAST(8 \<rightarrow> 32) d; cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')); cte_array_relation s (globals s'); tcb_cte_array_relation s (globals s'); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s; cmap_relation (ctes_of s) (cslift s') cte_Ptr ccte_relation; armKSNextASID_' (globals s') = armKSNextASID (ksArchState s); irq_masks (ksMachineState s) = irq_masks (phantom_machine_state_' (globals s')); cmap_relation (map_to_tcbs (ksPSpace s)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation; armKSKernelVSpace_C = armKSKernelVSpace (ksArchState s); irq_state (ksMachineState s) = irq_state (phantom_machine_state_' (globals s')); cmap_relation (map_to_eps (ksPSpace s)) (cslift s') ep_Ptr (cendpoint_relation (cslift s')); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState s)) (armKSHWASIDTable_' (globals s')); device_state (ksMachineState s) = device_state (phantom_machine_state_' (globals s')); cmap_relation (map_to_ntfns (ksPSpace s)) (cslift s') ntfn_Ptr (cnotification_relation (cslift s')); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState s)) (armKSASIDTable_' (globals s')); exclusive_state (ksMachineState s) = exclusive_state (phantom_machine_state_' (globals s')); machine_state_rest (ksMachineState s) = machine_state_rest (phantom_machine_state_' (globals s')); cmap_relation (map_to_pdes (ksPSpace s)) (cslift s') pde_Ptr cpde_relation; asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift s' \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState s); cmap_relation (map_to_ptes (ksPSpace s)) (cslift s') pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (cslift s') ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s)) (c_h_t_valid s') pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s)) (c_h_t_valid s') pt_Ptr\<rbrakk> \<Longrightarrow> cmap_relation (map_to_ctes ((ksPSpace s)(thread \<mapsto> KOTCB (tcbDomain_update (\<lambda>_. d) tcb)))) (cslift s') cte_Ptr ccte_relation \<and> cmap_relation (map_to_tcbs ((ksPSpace s)(thread \<mapsto> KOTCB (tcbDomain_update (\<lambda>_. d) tcb)))) ((cslift s')(tcb_ptr_to_ctcb_ptr thread \<mapsto> tcbDomain_C_update (\<lambda>_. UCAST(8 \<rightarrow> 32) d) tcb')) tcb_ptr_to_ctcb_ptr ctcb_relation \<and> cmap_relation (map_to_eps (ksPSpace s)) (cslift s') ep_Ptr (cendpoint_relation ((cslift s')(tcb_ptr_to_ctcb_ptr thread \<mapsto> tcbDomain_C_update (\<lambda>_. UCAST(8 \<rightarrow> 32) d) tcb'))) \<and> cmap_relation (map_to_ntfns (ksPSpace s)) (cslift s') ntfn_Ptr (cnotification_relation ((cslift s')(tcb_ptr_to_ctcb_ptr thread \<mapsto> tcbDomain_C_update (\<lambda>_. UCAST(8 \<rightarrow> 32) d) tcb'))) \<and> cready_queues_relation ((cslift s')(tcb_ptr_to_ctcb_ptr thread \<mapsto> tcbDomain_C_update (\<lambda>_. UCAST(8 \<rightarrow> 32) d) tcb')) (ksReadyQueues_' (globals s')) (ksReadyQueues s) \<and> cvariable_array_map_relation (map_to_tcbs ((ksPSpace s)(thread \<mapsto> KOTCB (tcbDomain_update (\<lambda>_. d) tcb)))) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (1 subgoal):
 1. \<And>s s' tcb tcb'. \<lbrakk>ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; thread' s' = tcb_ptr_to_ctcb_ptr thread; d' s' = UCAST(8 \<rightarrow> 32) d; cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')); cte_array_relation s (globals s'); tcb_cte_array_relation s (globals s'); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s; cmap_relation (ctes_of s) (cslift s') cte_Ptr ccte_relation; armKSNextASID_' (globals s') = armKSNextASID (ksArchState s); irq_masks (ksMachineState s) = irq_masks (phantom_machine_state_' (globals s')); cmap_relation (map_to_tcbs (ksPSpace s)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation; armKSKernelVSpace_C = armKSKernelVSpace (ksArchState s); irq_state (ksMachineState s) = irq_state (phantom_machine_state_' (globals s')); cmap_relation (map_to_eps (ksPSpace s)) (cslift s') ep_Ptr (cendpoint_relation (cslift s')); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState s)) (armKSHWASIDTable_' (globals s')); device_state (ksMachineState s) = device_state (phantom_machine_state_' (globals s')); cmap_relation (map_to_ntfns (ksPSpace s)) (cslift s') ntfn_Ptr (cnotification_relation (cslift s')); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState s)) (armKSASIDTable_' (globals s')); exclusive_state (ksMachineState s) = exclusive_state (phantom_machine_state_' (globals s')); machine_state_rest (ksMachineState s) = machine_state_rest (phantom_machine_state_' (globals s')); cmap_relation (map_to_pdes (ksPSpace s)) (cslift s') pde_Ptr cpde_relation; asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift s' \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState s); cmap_relation (map_to_ptes (ksPSpace s)) (cslift s') pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (cslift s') ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s)) (c_h_t_valid s') pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s)) (c_h_t_valid s') pt_Ptr\<rbrakk> \<Longrightarrow> cmap_relation ((map_to_tcbs (ksPSpace s))(thread \<mapsto> tcbDomain_update (\<lambda>_. d) tcb)) ((cslift s')(tcb_ptr_to_ctcb_ptr thread \<mapsto> tcbDomain_C_update (\<lambda>_. UCAST(8 \<rightarrow> 32) d) tcb')) tcb_ptr_to_ctcb_ptr ctcb_relation \<and> cmap_relation (map_to_eps (ksPSpace s)) (cslift s') ep_Ptr (cendpoint_relation ((cslift s')(tcb_ptr_to_ctcb_ptr thread \<mapsto> tcbDomain_C_update (\<lambda>_. UCAST(8 \<rightarrow> 32) d) tcb'))) \<and> cmap_relation (map_to_ntfns (ksPSpace s)) (cslift s') ntfn_Ptr (cnotification_relation ((cslift s')(tcb_ptr_to_ctcb_ptr thread \<mapsto> tcbDomain_C_update (\<lambda>_. UCAST(8 \<rightarrow> 32) d) tcb'))) \<and> cready_queues_relation ((cslift s')(tcb_ptr_to_ctcb_ptr thread \<mapsto> tcbDomain_C_update (\<lambda>_. UCAST(8 \<rightarrow> 32) d) tcb')) (ksReadyQueues_' (globals s')) (ksReadyQueues s) \<and> cvariable_array_map_relation ((map_to_tcbs (ksPSpace s))(thread \<mapsto> tcbDomain_update (\<lambda>_. d) tcb)) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (1 subgoal):
 1. \<And>s s' tcb tcb'. \<lbrakk>ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; thread' s' = tcb_ptr_to_ctcb_ptr thread; d' s' = UCAST(8 \<rightarrow> 32) d; cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')); cte_array_relation s (globals s'); tcb_cte_array_relation s (globals s'); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s; cmap_relation (ctes_of s) (cslift s') cte_Ptr ccte_relation; armKSNextASID_' (globals s') = armKSNextASID (ksArchState s); irq_masks (ksMachineState s) = irq_masks (phantom_machine_state_' (globals s')); cmap_relation (map_to_tcbs (ksPSpace s)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation; armKSKernelVSpace_C = armKSKernelVSpace (ksArchState s); irq_state (ksMachineState s) = irq_state (phantom_machine_state_' (globals s')); cmap_relation (map_to_eps (ksPSpace s)) (cslift s') ep_Ptr (cendpoint_relation (cslift s')); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState s)) (armKSHWASIDTable_' (globals s')); device_state (ksMachineState s) = device_state (phantom_machine_state_' (globals s')); cmap_relation (map_to_ntfns (ksPSpace s)) (cslift s') ntfn_Ptr (cnotification_relation (cslift s')); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState s)) (armKSASIDTable_' (globals s')); exclusive_state (ksMachineState s) = exclusive_state (phantom_machine_state_' (globals s')); machine_state_rest (ksMachineState s) = machine_state_rest (phantom_machine_state_' (globals s')); cmap_relation (map_to_pdes (ksPSpace s)) (cslift s') pde_Ptr cpde_relation; asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift s' \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState s); cmap_relation (map_to_ptes (ksPSpace s)) (cslift s') pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (cslift s') ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s)) (c_h_t_valid s') pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s)) (c_h_t_valid s') pt_Ptr\<rbrakk> \<Longrightarrow> cmap_relation ((map_to_tcbs (ksPSpace s))(thread \<mapsto> tcbDomain_update (\<lambda>_. d) tcb)) ((cslift s')(tcb_ptr_to_ctcb_ptr thread \<mapsto> tcbDomain_C_update (\<lambda>_. UCAST(8 \<rightarrow> 32) d) tcb')) tcb_ptr_to_ctcb_ptr ctcb_relation \<and> cready_queues_relation ((cslift s')(tcb_ptr_to_ctcb_ptr thread \<mapsto> tcbDomain_C_update (\<lambda>_. UCAST(8 \<rightarrow> 32) d) tcb')) (ksReadyQueues_' (globals s')) (ksReadyQueues s) proof (prove)
goal (2 subgoals):
 1. \<And>s s' tcb tcb'. \<lbrakk>ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; thread' s' = tcb_ptr_to_ctcb_ptr thread; d' s' = UCAST(8 \<rightarrow> 32) d; cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')); cte_array_relation s (globals s'); tcb_cte_array_relation s (globals s'); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s; cmap_relation (ctes_of s) (cslift s') cte_Ptr ccte_relation; armKSNextASID_' (globals s') = armKSNextASID (ksArchState s); irq_masks (ksMachineState s) = irq_masks (phantom_machine_state_' (globals s')); cmap_relation (map_to_tcbs (ksPSpace s)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation; armKSKernelVSpace_C = armKSKernelVSpace (ksArchState s); irq_state (ksMachineState s) = irq_state (phantom_machine_state_' (globals s')); cmap_relation (map_to_eps (ksPSpace s)) (cslift s') ep_Ptr (cendpoint_relation (cslift s')); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState s)) (armKSHWASIDTable_' (globals s')); device_state (ksMachineState s) = device_state (phantom_machine_state_' (globals s')); cmap_relation (map_to_ntfns (ksPSpace s)) (cslift s') ntfn_Ptr (cnotification_relation (cslift s')); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState s)) (armKSASIDTable_' (globals s')); exclusive_state (ksMachineState s) = exclusive_state (phantom_machine_state_' (globals s')); machine_state_rest (ksMachineState s) = machine_state_rest (phantom_machine_state_' (globals s')); cmap_relation (map_to_pdes (ksPSpace s)) (cslift s') pde_Ptr cpde_relation; asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift s' \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState s); cmap_relation (map_to_ptes (ksPSpace s)) (cslift s') pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (cslift s') ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s)) (c_h_t_valid s') pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s)) (c_h_t_valid s') pt_Ptr\<rbrakk> \<Longrightarrow> cmap_relation ((map_to_tcbs (ksPSpace s))(thread \<mapsto> tcbDomain_update (\<lambda>_. d) tcb)) ((cslift s')(tcb_ptr_to_ctcb_ptr thread \<mapsto> tcbDomain_C_update (\<lambda>_. UCAST(8 \<rightarrow> 32) d) tcb')) tcb_ptr_to_ctcb_ptr ctcb_relation
 2. \<And>s s' tcb tcb'. \<lbrakk>ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; thread' s' = tcb_ptr_to_ctcb_ptr thread; d' s' = UCAST(8 \<rightarrow> 32) d; cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')); cte_array_relation s (globals s'); tcb_cte_array_relation s (globals s'); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s; cmap_relation (ctes_of s) (cslift s') cte_Ptr ccte_relation; armKSNextASID_' (globals s') = armKSNextASID (ksArchState s); irq_masks (ksMachineState s) = irq_masks (phantom_machine_state_' (globals s')); cmap_relation (map_to_tcbs (ksPSpace s)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation; armKSKernelVSpace_C = armKSKernelVSpace (ksArchState s); irq_state (ksMachineState s) = irq_state (phantom_machine_state_' (globals s')); cmap_relation (map_to_eps (ksPSpace s)) (cslift s') ep_Ptr (cendpoint_relation (cslift s')); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState s)) (armKSHWASIDTable_' (globals s')); device_state (ksMachineState s) = device_state (phantom_machine_state_' (globals s')); cmap_relation (map_to_ntfns (ksPSpace s)) (cslift s') ntfn_Ptr (cnotification_relation (cslift s')); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState s)) (armKSASIDTable_' (globals s')); exclusive_state (ksMachineState s) = exclusive_state (phantom_machine_state_' (globals s')); machine_state_rest (ksMachineState s) = machine_state_rest (phantom_machine_state_' (globals s')); cmap_relation (map_to_pdes (ksPSpace s)) (cslift s') pde_Ptr cpde_relation; asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift s' \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState s); cmap_relation (map_to_ptes (ksPSpace s)) (cslift s') pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (cslift s') ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s)) (c_h_t_valid s') pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s)) (c_h_t_valid s') pt_Ptr\<rbrakk> \<Longrightarrow> cready_queues_relation ((cslift s')(tcb_ptr_to_ctcb_ptr thread \<mapsto> tcbDomain_C_update (\<lambda>_. UCAST(8 \<rightarrow> 32) d) tcb')) (ksReadyQueues_' (globals s')) (ksReadyQueues s) proof (prove)
goal (2 subgoals):
 1. \<And>s s' tcb tcb'. \<lbrakk>ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; thread' s' = tcb_ptr_to_ctcb_ptr thread; d' s' = UCAST(8 \<rightarrow> 32) d; cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')); cte_array_relation s (globals s'); tcb_cte_array_relation s (globals s'); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s; cmap_relation (ctes_of s) (cslift s') cte_Ptr ccte_relation; armKSNextASID_' (globals s') = armKSNextASID (ksArchState s); irq_masks (ksMachineState s) = irq_masks (phantom_machine_state_' (globals s')); cmap_relation (map_to_tcbs (ksPSpace s)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation; armKSKernelVSpace_C = armKSKernelVSpace (ksArchState s); irq_state (ksMachineState s) = irq_state (phantom_machine_state_' (globals s')); cmap_relation (map_to_eps (ksPSpace s)) (cslift s') ep_Ptr (cendpoint_relation (cslift s')); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState s)) (armKSHWASIDTable_' (globals s')); device_state (ksMachineState s) = device_state (phantom_machine_state_' (globals s')); cmap_relation (map_to_ntfns (ksPSpace s)) (cslift s') ntfn_Ptr (cnotification_relation (cslift s')); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState s)) (armKSASIDTable_' (globals s')); exclusive_state (ksMachineState s) = exclusive_state (phantom_machine_state_' (globals s')); machine_state_rest (ksMachineState s) = machine_state_rest (phantom_machine_state_' (globals s')); cmap_relation (map_to_pdes (ksPSpace s)) (cslift s') pde_Ptr cpde_relation; asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift s' \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState s); cmap_relation (map_to_ptes (ksPSpace s)) (cslift s') pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (cslift s') ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s)) (c_h_t_valid s') pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s)) (c_h_t_valid s') pt_Ptr\<rbrakk> \<Longrightarrow> cready_queues_relation ((cslift s')(tcb_ptr_to_ctcb_ptr thread \<mapsto> tcbDomain_C_update (\<lambda>_. UCAST(8 \<rightarrow> 32) d) tcb')) (ksReadyQueues_' (globals s')) (ksReadyQueues s)
 2. \<And>s s' tcb tcb'. \<lbrakk>ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; thread' s' = tcb_ptr_to_ctcb_ptr thread; d' s' = UCAST(8 \<rightarrow> 32) d; cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')); cte_array_relation s (globals s'); tcb_cte_array_relation s (globals s'); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s; cmap_relation (ctes_of s) (cslift s') cte_Ptr ccte_relation; armKSNextASID_' (globals s') = armKSNextASID (ksArchState s); irq_masks (ksMachineState s) = irq_masks (phantom_machine_state_' (globals s')); cmap_relation (map_to_tcbs (ksPSpace s)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation; armKSKernelVSpace_C = armKSKernelVSpace (ksArchState s); irq_state (ksMachineState s) = irq_state (phantom_machine_state_' (globals s')); cmap_relation (map_to_eps (ksPSpace s)) (cslift s') ep_Ptr (cendpoint_relation (cslift s')); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState s)) (armKSHWASIDTable_' (globals s')); device_state (ksMachineState s) = device_state (phantom_machine_state_' (globals s')); cmap_relation (map_to_ntfns (ksPSpace s)) (cslift s') ntfn_Ptr (cnotification_relation (cslift s')); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState s)) (armKSASIDTable_' (globals s')); exclusive_state (ksMachineState s) = exclusive_state (phantom_machine_state_' (globals s')); machine_state_rest (ksMachineState s) = machine_state_rest (phantom_machine_state_' (globals s')); cmap_relation (map_to_pdes (ksPSpace s)) (cslift s') pde_Ptr cpde_relation; asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift s' \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState s); cmap_relation (map_to_ptes (ksPSpace s)) (cslift s') pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (cslift s') ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s)) (c_h_t_valid s') pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s)) (c_h_t_valid s') pt_Ptr\<rbrakk> \<Longrightarrow> cmap_relation ((map_to_tcbs (ksPSpace s))(thread \<mapsto> tcbDomain_update (\<lambda>_. d) tcb)) ((cslift s')(tcb_ptr_to_ctcb_ptr thread \<mapsto> tcbDomain_C_update (\<lambda>_. UCAST(8 \<rightarrow> 32) d) tcb')) tcb_ptr_to_ctcb_ptr ctcb_relation proof (prove)
goal (3 subgoals):
 1. \<And>s s' tcb tcb'. \<lbrakk>ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; thread' s' = tcb_ptr_to_ctcb_ptr thread; d' s' = UCAST(8 \<rightarrow> 32) d; zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')); cte_array_relation s (globals s'); tcb_cte_array_relation s (globals s'); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s; cmap_relation (ctes_of s) (cslift s') cte_Ptr ccte_relation; armKSNextASID_' (globals s') = armKSNextASID (ksArchState s); irq_masks (ksMachineState s) = irq_masks (phantom_machine_state_' (globals s')); cmap_relation (map_to_tcbs (ksPSpace s)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation; armKSKernelVSpace_C = armKSKernelVSpace (ksArchState s); irq_state (ksMachineState s) = irq_state (phantom_machine_state_' (globals s')); cmap_relation (map_to_eps (ksPSpace s)) (cslift s') ep_Ptr (cendpoint_relation (cslift s')); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState s)) (armKSHWASIDTable_' (globals s')); device_state (ksMachineState s) = device_state (phantom_machine_state_' (globals s')); cmap_relation (map_to_ntfns (ksPSpace s)) (cslift s') ntfn_Ptr (cnotification_relation (cslift s')); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState s)) (armKSASIDTable_' (globals s')); exclusive_state (ksMachineState s) = exclusive_state (phantom_machine_state_' (globals s')); machine_state_rest (ksMachineState s) = machine_state_rest (phantom_machine_state_' (globals s')); cmap_relation (map_to_pdes (ksPSpace s)) (cslift s') pde_Ptr cpde_relation; asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift s' \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState s); cmap_relation (map_to_ptes (ksPSpace s)) (cslift s') pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (cslift s') ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s)) (c_h_t_valid s') pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s)) (c_h_t_valid s') pt_Ptr\<rbrakk> \<Longrightarrow> map_option tcbSchedNext_C \<circ> (cslift s')(tcb_ptr_to_ctcb_ptr thread \<mapsto> tcbDomain_C_update (\<lambda>_. UCAST(8 \<rightarrow> 32) d) tcb') = map_option tcbSchedNext_C \<circ> cslift s'
 2. \<And>s s' tcb tcb'. \<lbrakk>ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; thread' s' = tcb_ptr_to_ctcb_ptr thread; d' s' = UCAST(8 \<rightarrow> 32) d; zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')); cte_array_relation s (globals s'); tcb_cte_array_relation s (globals s'); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s; cmap_relation (ctes_of s) (cslift s') cte_Ptr ccte_relation; armKSNextASID_' (globals s') = armKSNextASID (ksArchState s); irq_masks (ksMachineState s) = irq_masks (phantom_machine_state_' (globals s')); cmap_relation (map_to_tcbs (ksPSpace s)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation; armKSKernelVSpace_C = armKSKernelVSpace (ksArchState s); irq_state (ksMachineState s) = irq_state (phantom_machine_state_' (globals s')); cmap_relation (map_to_eps (ksPSpace s)) (cslift s') ep_Ptr (cendpoint_relation (cslift s')); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState s)) (armKSHWASIDTable_' (globals s')); device_state (ksMachineState s) = device_state (phantom_machine_state_' (globals s')); cmap_relation (map_to_ntfns (ksPSpace s)) (cslift s') ntfn_Ptr (cnotification_relation (cslift s')); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState s)) (armKSASIDTable_' (globals s')); exclusive_state (ksMachineState s) = exclusive_state (phantom_machine_state_' (globals s')); machine_state_rest (ksMachineState s) = machine_state_rest (phantom_machine_state_' (globals s')); cmap_relation (map_to_pdes (ksPSpace s)) (cslift s') pde_Ptr cpde_relation; asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift s' \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState s); cmap_relation (map_to_ptes (ksPSpace s)) (cslift s') pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (cslift s') ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s)) (c_h_t_valid s') pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s)) (c_h_t_valid s') pt_Ptr\<rbrakk> \<Longrightarrow> map_option tcbSchedPrev_C \<circ> (cslift s')(tcb_ptr_to_ctcb_ptr thread \<mapsto> tcbDomain_C_update (\<lambda>_. UCAST(8 \<rightarrow> 32) d) tcb') = map_option tcbSchedPrev_C \<circ> cslift s'
 3. \<And>s s' tcb tcb'. \<lbrakk>ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; thread' s' = tcb_ptr_to_ctcb_ptr thread; d' s' = UCAST(8 \<rightarrow> 32) d; cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')); cte_array_relation s (globals s'); tcb_cte_array_relation s (globals s'); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s; cmap_relation (ctes_of s) (cslift s') cte_Ptr ccte_relation; armKSNextASID_' (globals s') = armKSNextASID (ksArchState s); irq_masks (ksMachineState s) = irq_masks (phantom_machine_state_' (globals s')); cmap_relation (map_to_tcbs (ksPSpace s)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation; armKSKernelVSpace_C = armKSKernelVSpace (ksArchState s); irq_state (ksMachineState s) = irq_state (phantom_machine_state_' (globals s')); cmap_relation (map_to_eps (ksPSpace s)) (cslift s') ep_Ptr (cendpoint_relation (cslift s')); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState s)) (armKSHWASIDTable_' (globals s')); device_state (ksMachineState s) = device_state (phantom_machine_state_' (globals s')); cmap_relation (map_to_ntfns (ksPSpace s)) (cslift s') ntfn_Ptr (cnotification_relation (cslift s')); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState s)) (armKSASIDTable_' (globals s')); exclusive_state (ksMachineState s) = exclusive_state (phantom_machine_state_' (globals s')); machine_state_rest (ksMachineState s) = machine_state_rest (phantom_machine_state_' (globals s')); cmap_relation (map_to_pdes (ksPSpace s)) (cslift s') pde_Ptr cpde_relation; asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift s' \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState s); cmap_relation (map_to_ptes (ksPSpace s)) (cslift s') pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (cslift s') ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s)) (c_h_t_valid s') pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s)) (c_h_t_valid s') pt_Ptr\<rbrakk> \<Longrightarrow> cmap_relation ((map_to_tcbs (ksPSpace s))(thread \<mapsto> tcbDomain_update (\<lambda>_. d) tcb)) ((cslift s')(tcb_ptr_to_ctcb_ptr thread \<mapsto> tcbDomain_C_update (\<lambda>_. UCAST(8 \<rightarrow> 32) d) tcb')) tcb_ptr_to_ctcb_ptr ctcb_relation proof (prove)
goal (2 subgoals):
 1. \<And>s s' tcb tcb'. \<lbrakk>ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; thread' s' = tcb_ptr_to_ctcb_ptr thread; d' s' = UCAST(8 \<rightarrow> 32) d; zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')); cte_array_relation s (globals s'); tcb_cte_array_relation s (globals s'); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s; cmap_relation (ctes_of s) (cslift s') cte_Ptr ccte_relation; armKSNextASID_' (globals s') = armKSNextASID (ksArchState s); irq_masks (ksMachineState s) = irq_masks (phantom_machine_state_' (globals s')); cmap_relation (map_to_tcbs (ksPSpace s)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation; armKSKernelVSpace_C = armKSKernelVSpace (ksArchState s); irq_state (ksMachineState s) = irq_state (phantom_machine_state_' (globals s')); cmap_relation (map_to_eps (ksPSpace s)) (cslift s') ep_Ptr (cendpoint_relation (cslift s')); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState s)) (armKSHWASIDTable_' (globals s')); device_state (ksMachineState s) = device_state (phantom_machine_state_' (globals s')); cmap_relation (map_to_ntfns (ksPSpace s)) (cslift s') ntfn_Ptr (cnotification_relation (cslift s')); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState s)) (armKSASIDTable_' (globals s')); exclusive_state (ksMachineState s) = exclusive_state (phantom_machine_state_' (globals s')); machine_state_rest (ksMachineState s) = machine_state_rest (phantom_machine_state_' (globals s')); cmap_relation (map_to_pdes (ksPSpace s)) (cslift s') pde_Ptr cpde_relation; asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift s' \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState s); cmap_relation (map_to_ptes (ksPSpace s)) (cslift s') pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (cslift s') ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s)) (c_h_t_valid s') pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s)) (c_h_t_valid s') pt_Ptr\<rbrakk> \<Longrightarrow> map_option tcbSchedPrev_C \<circ> (cslift s')(tcb_ptr_to_ctcb_ptr thread \<mapsto> tcbDomain_C_update (\<lambda>_. UCAST(8 \<rightarrow> 32) d) tcb') = map_option tcbSchedPrev_C \<circ> cslift s'
 2. \<And>s s' tcb tcb'. \<lbrakk>ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; thread' s' = tcb_ptr_to_ctcb_ptr thread; d' s' = UCAST(8 \<rightarrow> 32) d; cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')); cte_array_relation s (globals s'); tcb_cte_array_relation s (globals s'); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s; cmap_relation (ctes_of s) (cslift s') cte_Ptr ccte_relation; armKSNextASID_' (globals s') = armKSNextASID (ksArchState s); irq_masks (ksMachineState s) = irq_masks (phantom_machine_state_' (globals s')); cmap_relation (map_to_tcbs (ksPSpace s)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation; armKSKernelVSpace_C = armKSKernelVSpace (ksArchState s); irq_state (ksMachineState s) = irq_state (phantom_machine_state_' (globals s')); cmap_relation (map_to_eps (ksPSpace s)) (cslift s') ep_Ptr (cendpoint_relation (cslift s')); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState s)) (armKSHWASIDTable_' (globals s')); device_state (ksMachineState s) = device_state (phantom_machine_state_' (globals s')); cmap_relation (map_to_ntfns (ksPSpace s)) (cslift s') ntfn_Ptr (cnotification_relation (cslift s')); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState s)) (armKSASIDTable_' (globals s')); exclusive_state (ksMachineState s) = exclusive_state (phantom_machine_state_' (globals s')); machine_state_rest (ksMachineState s) = machine_state_rest (phantom_machine_state_' (globals s')); cmap_relation (map_to_pdes (ksPSpace s)) (cslift s') pde_Ptr cpde_relation; asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift s' \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState s); cmap_relation (map_to_ptes (ksPSpace s)) (cslift s') pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (cslift s') ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s)) (c_h_t_valid s') pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s)) (c_h_t_valid s') pt_Ptr\<rbrakk> \<Longrightarrow> cmap_relation ((map_to_tcbs (ksPSpace s))(thread \<mapsto> tcbDomain_update (\<lambda>_. d) tcb)) ((cslift s')(tcb_ptr_to_ctcb_ptr thread \<mapsto> tcbDomain_C_update (\<lambda>_. UCAST(8 \<rightarrow> 32) d) tcb')) tcb_ptr_to_ctcb_ptr ctcb_relation proof (prove)
goal (1 subgoal):
 1. \<And>s s' tcb tcb'. \<lbrakk>ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; thread' s' = tcb_ptr_to_ctcb_ptr thread; d' s' = UCAST(8 \<rightarrow> 32) d; cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')); cte_array_relation s (globals s'); tcb_cte_array_relation s (globals s'); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s; cmap_relation (ctes_of s) (cslift s') cte_Ptr ccte_relation; armKSNextASID_' (globals s') = armKSNextASID (ksArchState s); irq_masks (ksMachineState s) = irq_masks (phantom_machine_state_' (globals s')); cmap_relation (map_to_tcbs (ksPSpace s)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation; armKSKernelVSpace_C = armKSKernelVSpace (ksArchState s); irq_state (ksMachineState s) = irq_state (phantom_machine_state_' (globals s')); cmap_relation (map_to_eps (ksPSpace s)) (cslift s') ep_Ptr (cendpoint_relation (cslift s')); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState s)) (armKSHWASIDTable_' (globals s')); device_state (ksMachineState s) = device_state (phantom_machine_state_' (globals s')); cmap_relation (map_to_ntfns (ksPSpace s)) (cslift s') ntfn_Ptr (cnotification_relation (cslift s')); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState s)) (armKSASIDTable_' (globals s')); exclusive_state (ksMachineState s) = exclusive_state (phantom_machine_state_' (globals s')); machine_state_rest (ksMachineState s) = machine_state_rest (phantom_machine_state_' (globals s')); cmap_relation (map_to_pdes (ksPSpace s)) (cslift s') pde_Ptr cpde_relation; asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift s' \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState s); cmap_relation (map_to_ptes (ksPSpace s)) (cslift s') pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (cslift s') ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s)) (c_h_t_valid s') pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s)) (c_h_t_valid s') pt_Ptr\<rbrakk> \<Longrightarrow> cmap_relation ((map_to_tcbs (ksPSpace s))(thread \<mapsto> tcbDomain_update (\<lambda>_. d) tcb)) ((cslift s')(tcb_ptr_to_ctcb_ptr thread \<mapsto> tcbDomain_C_update (\<lambda>_. UCAST(8 \<rightarrow> 32) d) tcb')) tcb_ptr_to_ctcb_ptr ctcb_relation proof (prove)
goal (1 subgoal):
 1. \<And>s s' tcb tcb'. \<lbrakk>cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; thread' s' = tcb_ptr_to_ctcb_ptr thread; d' s' = UCAST(8 \<rightarrow> 32) d; cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')); cte_array_relation s (globals s'); tcb_cte_array_relation s (globals s'); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s; cmap_relation (ctes_of s) (cslift s') cte_Ptr ccte_relation; armKSNextASID_' (globals s') = armKSNextASID (ksArchState s); irq_masks (ksMachineState s) = irq_masks (phantom_machine_state_' (globals s')); cmap_relation (map_to_tcbs (ksPSpace s)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation; armKSKernelVSpace_C = armKSKernelVSpace (ksArchState s); irq_state (ksMachineState s) = irq_state (phantom_machine_state_' (globals s')); cmap_relation (map_to_eps (ksPSpace s)) (cslift s') ep_Ptr (cendpoint_relation (cslift s')); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState s)) (armKSHWASIDTable_' (globals s')); device_state (ksMachineState s) = device_state (phantom_machine_state_' (globals s')); cmap_relation (map_to_ntfns (ksPSpace s)) (cslift s') ntfn_Ptr (cnotification_relation (cslift s')); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState s)) (armKSASIDTable_' (globals s')); exclusive_state (ksMachineState s) = exclusive_state (phantom_machine_state_' (globals s')); machine_state_rest (ksMachineState s) = machine_state_rest (phantom_machine_state_' (globals s')); cmap_relation (map_to_pdes (ksPSpace s)) (cslift s') pde_Ptr cpde_relation; asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift s' \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState s); cmap_relation (map_to_ptes (ksPSpace s)) (cslift s') pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (cslift s') ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s)) (c_h_t_valid s') pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s)) (c_h_t_valid s') pt_Ptr; map_to_tcbs (ksPSpace s) thread = Some tcb\<rbrakk> \<Longrightarrow> cmap_relation ((map_to_tcbs (ksPSpace s))(thread \<mapsto> tcbDomain_update (\<lambda>_. d) tcb)) ((cslift s')(tcb_ptr_to_ctcb_ptr thread \<mapsto> tcbDomain_C_update (\<lambda>_. UCAST(8 \<rightarrow> 32) d) tcb')) tcb_ptr_to_ctcb_ptr ctcb_relation proof (prove)
goal (3 subgoals):
 1. \<And>s s' tcb tcb'. \<lbrakk>cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; thread' s' = tcb_ptr_to_ctcb_ptr thread; d' s' = UCAST(8 \<rightarrow> 32) d; cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')); cte_array_relation s (globals s'); tcb_cte_array_relation s (globals s'); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s; cmap_relation (ctes_of s) (cslift s') cte_Ptr ccte_relation; armKSNextASID_' (globals s') = armKSNextASID (ksArchState s); irq_masks (ksMachineState s) = irq_masks (phantom_machine_state_' (globals s')); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState s); irq_state (ksMachineState s) = irq_state (phantom_machine_state_' (globals s')); cmap_relation (map_to_eps (ksPSpace s)) (cslift s') ep_Ptr (cendpoint_relation (cslift s')); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState s)) (armKSHWASIDTable_' (globals s')); device_state (ksMachineState s) = device_state (phantom_machine_state_' (globals s')); cmap_relation (map_to_ntfns (ksPSpace s)) (cslift s') ntfn_Ptr (cnotification_relation (cslift s')); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState s)) (armKSASIDTable_' (globals s')); exclusive_state (ksMachineState s) = exclusive_state (phantom_machine_state_' (globals s')); machine_state_rest (ksMachineState s) = machine_state_rest (phantom_machine_state_' (globals s')); cmap_relation (map_to_pdes (ksPSpace s)) (cslift s') pde_Ptr cpde_relation; asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift s' \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState s); cmap_relation (map_to_ptes (ksPSpace s)) (cslift s') pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (cslift s') ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s)) (c_h_t_valid s') pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s)) (c_h_t_valid s') pt_Ptr; map_to_tcbs (ksPSpace s) thread = Some tcb\<rbrakk> \<Longrightarrow> ctcb_relation (tcbDomain_update (\<lambda>_. d) tcb) (tcbDomain_C_update (\<lambda>_. UCAST(8 \<rightarrow> 32) d) tcb')
 2. \<And>s s' tcb tcb' x ov ov'. \<lbrakk>cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; thread' s' = tcb_ptr_to_ctcb_ptr thread; d' s' = UCAST(8 \<rightarrow> 32) d; cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')); cte_array_relation s (globals s'); tcb_cte_array_relation s (globals s'); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s; cmap_relation (ctes_of s) (cslift s') cte_Ptr ccte_relation; armKSNextASID_' (globals s') = armKSNextASID (ksArchState s); irq_masks (ksMachineState s) = irq_masks (phantom_machine_state_' (globals s')); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState s); irq_state (ksMachineState s) = irq_state (phantom_machine_state_' (globals s')); cmap_relation (map_to_eps (ksPSpace s)) (cslift s') ep_Ptr (cendpoint_relation (cslift s')); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState s)) (armKSHWASIDTable_' (globals s')); device_state (ksMachineState s) = device_state (phantom_machine_state_' (globals s')); cmap_relation (map_to_ntfns (ksPSpace s)) (cslift s') ntfn_Ptr (cnotification_relation (cslift s')); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState s)) (armKSASIDTable_' (globals s')); exclusive_state (ksMachineState s) = exclusive_state (phantom_machine_state_' (globals s')); machine_state_rest (ksMachineState s) = machine_state_rest (phantom_machine_state_' (globals s')); cmap_relation (map_to_pdes (ksPSpace s)) (cslift s') pde_Ptr cpde_relation; asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift s' \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState s); cmap_relation (map_to_ptes (ksPSpace s)) (cslift s') pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (cslift s') ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s)) (c_h_t_valid s') pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s)) (c_h_t_valid s') pt_Ptr; map_to_tcbs (ksPSpace s) thread = Some tcb; x \<noteq> thread; map_to_tcbs (ksPSpace s) x = Some ov; cslift s' (tcb_ptr_to_ctcb_ptr x) = Some ov'; ctcb_relation ov ov'\<rbrakk> \<Longrightarrow> ctcb_relation ov ov'
 3. \<And>s s' tcb tcb'. \<lbrakk>cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; thread' s' = tcb_ptr_to_ctcb_ptr thread; d' s' = UCAST(8 \<rightarrow> 32) d; cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')); cte_array_relation s (globals s'); tcb_cte_array_relation s (globals s'); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s; cmap_relation (ctes_of s) (cslift s') cte_Ptr ccte_relation; armKSNextASID_' (globals s') = armKSNextASID (ksArchState s); irq_masks (ksMachineState s) = irq_masks (phantom_machine_state_' (globals s')); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState s); irq_state (ksMachineState s) = irq_state (phantom_machine_state_' (globals s')); cmap_relation (map_to_eps (ksPSpace s)) (cslift s') ep_Ptr (cendpoint_relation (cslift s')); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState s)) (armKSHWASIDTable_' (globals s')); device_state (ksMachineState s) = device_state (phantom_machine_state_' (globals s')); cmap_relation (map_to_ntfns (ksPSpace s)) (cslift s') ntfn_Ptr (cnotification_relation (cslift s')); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState s)) (armKSASIDTable_' (globals s')); exclusive_state (ksMachineState s) = exclusive_state (phantom_machine_state_' (globals s')); machine_state_rest (ksMachineState s) = machine_state_rest (phantom_machine_state_' (globals s')); cmap_relation (map_to_pdes (ksPSpace s)) (cslift s') pde_Ptr cpde_relation; asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift s' \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState s); cmap_relation (map_to_ptes (ksPSpace s)) (cslift s') pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (cslift s') ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s)) (c_h_t_valid s') pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s)) (c_h_t_valid s') pt_Ptr; map_to_tcbs (ksPSpace s) thread = Some tcb\<rbrakk> \<Longrightarrow> inj tcb_ptr_to_ctcb_ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cslift s'_ (tcb_ptr_to_ctcb_ptr thread) = Some tcb'_; ctcb_relation tcb_ tcb'_; thread' s'_ = tcb_ptr_to_ctcb_ptr thread; d' s'_ = UCAST(8 \<rightarrow> 32) d; cready_queues_relation (cslift s'_) (ksReadyQueues_' (globals s'_)) (ksReadyQueues s_); zero_ranges_are_zero (gsUntypedZeroRanges s_) (t_hrs_' (globals s'_)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s'_)) (ksReadyQueuesL1Bitmap s_); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s'_)) (ksReadyQueuesL2Bitmap s_); ksCurThread_' (globals s'_) = tcb_ptr_to_ctcb_ptr (ksCurThread s_); ksIdleThread_' (globals s'_) = tcb_ptr_to_ctcb_ptr (ksIdleThread s_); cinterrupt_relation (ksInterruptState s_) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s'_)); cscheduler_action_relation (ksSchedulerAction s_) (ksSchedulerAction_' (globals s'_)); cte_array_relation s_ (globals s'_); tcb_cte_array_relation s_ (globals s'_); apsnd fst (ghost'state_' (globals s'_)) = (gsUserPages s_, gsCNodes s_); ghost_size_rel (ghost'state_' (globals s'_)) (gsMaxObjectSize s_); ksWorkUnitsCompleted_' (globals s'_) = ksWorkUnitsCompleted s_; s'_ \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; s'_ \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s'_))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s_) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s'_) = word_of_nat (ksDomScheduleIdx s_); ksCurDomain_' (globals s'_) = UCAST(8 \<rightarrow> 32) (ksCurDomain s_); ksDomainTime_' (globals s'_) = ksDomainTime s_; cmap_relation (ctes_of s_) (cslift s'_) cte_Ptr ccte_relation; armKSNextASID_' (globals s'_) = armKSNextASID (ksArchState s_); irq_masks (ksMachineState s_) = irq_masks (phantom_machine_state_' (globals s'_)); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState s_); irq_state (ksMachineState s_) = irq_state (phantom_machine_state_' (globals s'_)); cmap_relation (map_to_eps (ksPSpace s_)) (cslift s'_) ep_Ptr (cendpoint_relation (cslift s'_)); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState s_)) (armKSHWASIDTable_' (globals s'_)); device_state (ksMachineState s_) = device_state (phantom_machine_state_' (globals s'_)); cmap_relation (map_to_ntfns (ksPSpace s_)) (cslift s'_) ntfn_Ptr (cnotification_relation (cslift s'_)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState s_)) (armKSASIDTable_' (globals s'_)); exclusive_state (ksMachineState s_) = exclusive_state (phantom_machine_state_' (globals s'_)); machine_state_rest (ksMachineState s_) = machine_state_rest (phantom_machine_state_' (globals s'_)); cmap_relation (map_to_pdes (ksPSpace s_)) (cslift s'_) pde_Ptr cpde_relation; asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s_)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift s'_ \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState s_); cmap_relation (map_to_ptes (ksPSpace s_)) (cslift s'_) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s_)) (cslift s'_) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s_) (underlying_memory (ksMachineState s_))) (cslift s'_) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s_) (underlying_memory (ksMachineState s_))) (cslift s'_) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s_)) (c_h_t_valid s'_) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s_)) (c_h_t_valid s'_) pt_Ptr; map_to_tcbs (ksPSpace s_) thread = Some tcb_\<rbrakk> \<Longrightarrow> ctcb_relation (tcbDomain_update (\<lambda>_. d) tcb_) (tcbDomain_C_update (\<lambda>_. UCAST(8 \<rightarrow> 32) d) tcb'_) proof (prove)
goal (2 subgoals):
 1. \<And>s s' tcb tcb' x ov ov'. \<lbrakk>cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; thread' s' = tcb_ptr_to_ctcb_ptr thread; d' s' = UCAST(8 \<rightarrow> 32) d; cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')); cte_array_relation s (globals s'); tcb_cte_array_relation s (globals s'); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s; cmap_relation (ctes_of s) (cslift s') cte_Ptr ccte_relation; armKSNextASID_' (globals s') = armKSNextASID (ksArchState s); irq_masks (ksMachineState s) = irq_masks (phantom_machine_state_' (globals s')); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState s); irq_state (ksMachineState s) = irq_state (phantom_machine_state_' (globals s')); cmap_relation (map_to_eps (ksPSpace s)) (cslift s') ep_Ptr (cendpoint_relation (cslift s')); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState s)) (armKSHWASIDTable_' (globals s')); device_state (ksMachineState s) = device_state (phantom_machine_state_' (globals s')); cmap_relation (map_to_ntfns (ksPSpace s)) (cslift s') ntfn_Ptr (cnotification_relation (cslift s')); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState s)) (armKSASIDTable_' (globals s')); exclusive_state (ksMachineState s) = exclusive_state (phantom_machine_state_' (globals s')); machine_state_rest (ksMachineState s) = machine_state_rest (phantom_machine_state_' (globals s')); cmap_relation (map_to_pdes (ksPSpace s)) (cslift s') pde_Ptr cpde_relation; asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift s' \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState s); cmap_relation (map_to_ptes (ksPSpace s)) (cslift s') pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (cslift s') ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s)) (c_h_t_valid s') pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s)) (c_h_t_valid s') pt_Ptr; map_to_tcbs (ksPSpace s) thread = Some tcb; x \<noteq> thread; map_to_tcbs (ksPSpace s) x = Some ov; cslift s' (tcb_ptr_to_ctcb_ptr x) = Some ov'; ctcb_relation ov ov'\<rbrakk> \<Longrightarrow> ctcb_relation ov ov'
 2. \<And>s s' tcb tcb'. \<lbrakk>cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; thread' s' = tcb_ptr_to_ctcb_ptr thread; d' s' = UCAST(8 \<rightarrow> 32) d; cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')); cte_array_relation s (globals s'); tcb_cte_array_relation s (globals s'); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s; cmap_relation (ctes_of s) (cslift s') cte_Ptr ccte_relation; armKSNextASID_' (globals s') = armKSNextASID (ksArchState s); irq_masks (ksMachineState s) = irq_masks (phantom_machine_state_' (globals s')); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState s); irq_state (ksMachineState s) = irq_state (phantom_machine_state_' (globals s')); cmap_relation (map_to_eps (ksPSpace s)) (cslift s') ep_Ptr (cendpoint_relation (cslift s')); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState s)) (armKSHWASIDTable_' (globals s')); device_state (ksMachineState s) = device_state (phantom_machine_state_' (globals s')); cmap_relation (map_to_ntfns (ksPSpace s)) (cslift s') ntfn_Ptr (cnotification_relation (cslift s')); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState s)) (armKSASIDTable_' (globals s')); exclusive_state (ksMachineState s) = exclusive_state (phantom_machine_state_' (globals s')); machine_state_rest (ksMachineState s) = machine_state_rest (phantom_machine_state_' (globals s')); cmap_relation (map_to_pdes (ksPSpace s)) (cslift s') pde_Ptr cpde_relation; asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift s' \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState s); cmap_relation (map_to_ptes (ksPSpace s)) (cslift s') pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (cslift s') ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s)) (c_h_t_valid s') pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s)) (c_h_t_valid s') pt_Ptr; map_to_tcbs (ksPSpace s) thread = Some tcb\<rbrakk> \<Longrightarrow> inj tcb_ptr_to_ctcb_ptr proof (prove)
goal (1 subgoal):
 1. \<And>s s' tcb tcb'. \<lbrakk>cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; thread' s' = tcb_ptr_to_ctcb_ptr thread; d' s' = UCAST(8 \<rightarrow> 32) d; cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')); cte_array_relation s (globals s'); tcb_cte_array_relation s (globals s'); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s; cmap_relation (ctes_of s) (cslift s') cte_Ptr ccte_relation; armKSNextASID_' (globals s') = armKSNextASID (ksArchState s); irq_masks (ksMachineState s) = irq_masks (phantom_machine_state_' (globals s')); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState s); irq_state (ksMachineState s) = irq_state (phantom_machine_state_' (globals s')); cmap_relation (map_to_eps (ksPSpace s)) (cslift s') ep_Ptr (cendpoint_relation (cslift s')); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState s)) (armKSHWASIDTable_' (globals s')); device_state (ksMachineState s) = device_state (phantom_machine_state_' (globals s')); cmap_relation (map_to_ntfns (ksPSpace s)) (cslift s') ntfn_Ptr (cnotification_relation (cslift s')); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState s)) (armKSASIDTable_' (globals s')); exclusive_state (ksMachineState s) = exclusive_state (phantom_machine_state_' (globals s')); machine_state_rest (ksMachineState s) = machine_state_rest (phantom_machine_state_' (globals s')); cmap_relation (map_to_pdes (ksPSpace s)) (cslift s') pde_Ptr cpde_relation; asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift s' \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState s); cmap_relation (map_to_ptes (ksPSpace s)) (cslift s') pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (cslift s') ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s)) (c_h_t_valid s') pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s)) (c_h_t_valid s') pt_Ptr; map_to_tcbs (ksPSpace s) thread = Some tcb\<rbrakk> \<Longrightarrow> inj tcb_ptr_to_ctcb_ptr