theory Fastpath_C

lemma setCTE_rf_sr:
  "\<lbrakk> (\<sigma>, s) \<in> rf_sr; ctes_of \<sigma> ptr = Some cte'';
     t_hrs_' (globals s') = hrs_mem_update
        (heap_update (cte_Ptr ptr) cte')
        (t_hrs_' (globals s));
     ccte_relation cte cte';
     (globals s')\<lparr> t_hrs_' := undefined \<rparr>
          = (globals s)\<lparr> t_hrs_' := undefined \<rparr> \<rbrakk>
      \<Longrightarrow>
   \<exists>x\<in>fst (setCTE ptr cte \<sigma>).
             (snd x, s') \<in> rf_sr" apply (rule fst_setCTE[OF ctes_of_cte_at], assumption) apply (erule rev_bexI) apply clarsimp apply (frule(1) rf_sr_ctes_of_clift) apply (subgoal_tac "\<exists>hrs. globals s' = globals s
                          \<lparr> t_hrs_' := hrs \<rparr>") apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
                         typ_heap_simps' cpspace_relation_def) apply (rule conjI) apply (erule(2) cmap_relation_updI, simp) apply (erule_tac t = s'a in ssubst) apply (simp add: heap_to_user_data_def) apply (rule conjI) apply (erule(1) setCTE_tcb_case) apply (simp add: carch_state_relation_def cmachine_state_relation_def
                    cvariable_array_map_const_add_map_option[where f="tcb_no_ctes_proj"]
                    typ_heap_simps' h_t_valid_clift_Some_iff) apply (cases "globals s", cases "globals s'") apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<sigma>, s) \<in> rf_sr; ctes_of \<sigma> ptr = Some cte''; t_hrs_' (globals s') = hrs_mem_update (heap_update (cte_Ptr ptr) cte') (t_hrs_' (globals s)); ccte_relation cte cte'; globals s'\<lparr>t_hrs_' := undefined\<rparr> = globals s\<lparr>t_hrs_' := undefined\<rparr>\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (setCTE ptr cte \<sigma>). (snd x, s') \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>s'a. \<lbrakk>(\<sigma>, s) \<in> rf_sr; ctes_of \<sigma> ptr = Some cte''; t_hrs_' (globals s') = hrs_mem_update (heap_update (cte_Ptr ptr) cte') (t_hrs_' (globals s)); ccte_relation cte cte'; globals s'\<lparr>t_hrs_' := undefined\<rparr> = globals s\<lparr>t_hrs_' := undefined\<rparr>; ((), s'a) \<in> fst (setCTE ptr ?cte \<sigma>); s'a = \<sigma>\<lparr>ksPSpace := ksPSpace s'a\<rparr>; ctes_of s'a = (ctes_of \<sigma>)(ptr \<mapsto> ?cte); map_to_eps (ksPSpace \<sigma>) = map_to_eps (ksPSpace s'a); map_to_ntfns (ksPSpace \<sigma>) = map_to_ntfns (ksPSpace s'a); map_to_pdes (ksPSpace \<sigma>) = map_to_pdes (ksPSpace s'a); map_to_ptes (ksPSpace \<sigma>) = map_to_ptes (ksPSpace s'a); map_to_asidpools (ksPSpace \<sigma>) = map_to_asidpools (ksPSpace s'a); map_to_user_data (ksPSpace \<sigma>) = map_to_user_data (ksPSpace s'a); map_to_user_data_device (ksPSpace \<sigma>) = map_to_user_data_device (ksPSpace s'a); map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace \<sigma>) = map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a); \<forall>T p. typ_at' T p \<sigma> = typ_at' T p s'a\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (setCTE ptr cte \<sigma>). (snd x, s') \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>s'a. \<lbrakk>(\<sigma>, s) \<in> rf_sr; ctes_of \<sigma> ptr = Some cte''; t_hrs_' (globals s') = hrs_mem_update (heap_update (cte_Ptr ptr) cte') (t_hrs_' (globals s)); ccte_relation cte cte'; globals s'\<lparr>t_hrs_' := undefined\<rparr> = globals s\<lparr>t_hrs_' := undefined\<rparr>; s'a = \<sigma>\<lparr>ksPSpace := ksPSpace s'a\<rparr>; ctes_of s'a = (ctes_of \<sigma>)(ptr \<mapsto> cte); map_to_eps (ksPSpace \<sigma>) = map_to_eps (ksPSpace s'a); map_to_ntfns (ksPSpace \<sigma>) = map_to_ntfns (ksPSpace s'a); map_to_pdes (ksPSpace \<sigma>) = map_to_pdes (ksPSpace s'a); map_to_ptes (ksPSpace \<sigma>) = map_to_ptes (ksPSpace s'a); map_to_asidpools (ksPSpace \<sigma>) = map_to_asidpools (ksPSpace s'a); map_to_user_data (ksPSpace \<sigma>) = map_to_user_data (ksPSpace s'a); map_to_user_data_device (ksPSpace \<sigma>) = map_to_user_data_device (ksPSpace s'a); map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace \<sigma>) = map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a); \<forall>T p. typ_at' T p \<sigma> = typ_at' T p s'a\<rbrakk> \<Longrightarrow> (snd ((), s'a), s') \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>s'a. \<lbrakk>(\<sigma>, s) \<in> rf_sr; ctes_of \<sigma> ptr = Some cte''; t_hrs_' (globals s') = hrs_mem_update (heap_update (cte_Ptr ptr) cte') (t_hrs_' (globals s)); ccte_relation cte cte'; globals s'\<lparr>t_hrs_' := undefined\<rparr> = globals s\<lparr>t_hrs_' := undefined\<rparr>; s'a = \<sigma>\<lparr>ksPSpace := ksPSpace s'a\<rparr>; ctes_of s'a = (ctes_of \<sigma>)(ptr \<mapsto> cte); map_to_eps (ksPSpace \<sigma>) = map_to_eps (ksPSpace s'a); map_to_ntfns (ksPSpace \<sigma>) = map_to_ntfns (ksPSpace s'a); map_to_pdes (ksPSpace \<sigma>) = map_to_pdes (ksPSpace s'a); map_to_ptes (ksPSpace \<sigma>) = map_to_ptes (ksPSpace s'a); map_to_asidpools (ksPSpace \<sigma>) = map_to_asidpools (ksPSpace s'a); map_to_user_data (ksPSpace \<sigma>) = map_to_user_data (ksPSpace s'a); map_to_user_data_device (ksPSpace \<sigma>) = map_to_user_data_device (ksPSpace s'a); map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace \<sigma>) = map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a); \<forall>T p. typ_at' T p \<sigma> = typ_at' T p s'a\<rbrakk> \<Longrightarrow> (s'a, s') \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>s'a. \<lbrakk>(\<sigma>, s) \<in> rf_sr; ctes_of \<sigma> ptr = Some cte''; t_hrs_' (globals s') = hrs_mem_update (heap_update (cte_Ptr ptr) cte') (t_hrs_' (globals s)); ccte_relation cte cte'; globals s'\<lparr>t_hrs_' := undefined\<rparr> = globals s\<lparr>t_hrs_' := undefined\<rparr>; s'a = \<sigma>\<lparr>ksPSpace := ksPSpace s'a\<rparr>; ctes_of s'a = (ctes_of \<sigma>)(ptr \<mapsto> cte); map_to_eps (ksPSpace \<sigma>) = map_to_eps (ksPSpace s'a); map_to_ntfns (ksPSpace \<sigma>) = map_to_ntfns (ksPSpace s'a); map_to_pdes (ksPSpace \<sigma>) = map_to_pdes (ksPSpace s'a); map_to_ptes (ksPSpace \<sigma>) = map_to_ptes (ksPSpace s'a); map_to_asidpools (ksPSpace \<sigma>) = map_to_asidpools (ksPSpace s'a); map_to_user_data (ksPSpace \<sigma>) = map_to_user_data (ksPSpace s'a); map_to_user_data_device (ksPSpace \<sigma>) = map_to_user_data_device (ksPSpace s'a); map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace \<sigma>) = map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a); \<forall>T p. typ_at' T p \<sigma> = typ_at' T p s'a; \<exists>cte'. cslift s (cte_Ptr ptr) = Some cte' \<and> cte_lift cte' \<noteq> None \<and> cte'' = cte_to_H (the (cte_lift cte')) \<and> c_valid_cte cte'\<rbrakk> \<Longrightarrow> (s'a, s') \<in> rf_sr proof (prove)
goal (2 subgoals):
 1. \<And>s'a. \<lbrakk>(\<sigma>, s) \<in> rf_sr; ctes_of \<sigma> ptr = Some cte''; t_hrs_' (globals s') = hrs_mem_update (heap_update (cte_Ptr ptr) cte') (t_hrs_' (globals s)); ccte_relation cte cte'; globals s'\<lparr>t_hrs_' := undefined\<rparr> = globals s\<lparr>t_hrs_' := undefined\<rparr>; s'a = \<sigma>\<lparr>ksPSpace := ksPSpace s'a\<rparr>; ctes_of s'a = (ctes_of \<sigma>)(ptr \<mapsto> cte); map_to_eps (ksPSpace \<sigma>) = map_to_eps (ksPSpace s'a); map_to_ntfns (ksPSpace \<sigma>) = map_to_ntfns (ksPSpace s'a); map_to_pdes (ksPSpace \<sigma>) = map_to_pdes (ksPSpace s'a); map_to_ptes (ksPSpace \<sigma>) = map_to_ptes (ksPSpace s'a); map_to_asidpools (ksPSpace \<sigma>) = map_to_asidpools (ksPSpace s'a); map_to_user_data (ksPSpace \<sigma>) = map_to_user_data (ksPSpace s'a); map_to_user_data_device (ksPSpace \<sigma>) = map_to_user_data_device (ksPSpace s'a); map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace \<sigma>) = map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a); \<forall>T p. typ_at' T p \<sigma> = typ_at' T p s'a; \<exists>cte'. cslift s (cte_Ptr ptr) = Some cte' \<and> cte_lift cte' \<noteq> None \<and> cte'' = cte_to_H (the (cte_lift cte')) \<and> c_valid_cte cte'; \<exists>hrs. globals s' = globals s\<lparr>t_hrs_' := hrs\<rparr>\<rbrakk> \<Longrightarrow> (s'a, s') \<in> rf_sr
 2. \<And>s'a. \<lbrakk>(\<sigma>, s) \<in> rf_sr; ctes_of \<sigma> ptr = Some cte''; t_hrs_' (globals s') = hrs_mem_update (heap_update (cte_Ptr ptr) cte') (t_hrs_' (globals s)); ccte_relation cte cte'; globals s'\<lparr>t_hrs_' := undefined\<rparr> = globals s\<lparr>t_hrs_' := undefined\<rparr>; s'a = \<sigma>\<lparr>ksPSpace := ksPSpace s'a\<rparr>; ctes_of s'a = (ctes_of \<sigma>)(ptr \<mapsto> cte); map_to_eps (ksPSpace \<sigma>) = map_to_eps (ksPSpace s'a); map_to_ntfns (ksPSpace \<sigma>) = map_to_ntfns (ksPSpace s'a); map_to_pdes (ksPSpace \<sigma>) = map_to_pdes (ksPSpace s'a); map_to_ptes (ksPSpace \<sigma>) = map_to_ptes (ksPSpace s'a); map_to_asidpools (ksPSpace \<sigma>) = map_to_asidpools (ksPSpace s'a); map_to_user_data (ksPSpace \<sigma>) = map_to_user_data (ksPSpace s'a); map_to_user_data_device (ksPSpace \<sigma>) = map_to_user_data_device (ksPSpace s'a); map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace \<sigma>) = map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a); \<forall>T p. typ_at' T p \<sigma> = typ_at' T p s'a; \<exists>cte'. cslift s (cte_Ptr ptr) = Some cte' \<and> cte_lift cte' \<noteq> None \<and> cte'' = cte_to_H (the (cte_lift cte')) \<and> c_valid_cte cte'\<rbrakk> \<Longrightarrow> \<exists>hrs. globals s' = globals s\<lparr>t_hrs_' := hrs\<rparr> proof (prove)
goal (2 subgoals):
 1. \<And>s'a cte'a a b y. \<lbrakk>ctes_of \<sigma> ptr = Some (cte_to_H y); (a, b) = hrs_mem_update (heap_update (cte_Ptr ptr) cte') (t_hrs_' (globals s)); ccte_relation cte cte'; s'a = \<sigma>\<lparr>ksPSpace := ksPSpace s'a\<rparr>; ctes_of s'a = (ctes_of \<sigma>)(ptr \<mapsto> cte); map_to_eps (ksPSpace \<sigma>) = map_to_eps (ksPSpace s'a); map_to_ntfns (ksPSpace \<sigma>) = map_to_ntfns (ksPSpace s'a); map_to_pdes (ksPSpace \<sigma>) = map_to_pdes (ksPSpace s'a); map_to_ptes (ksPSpace \<sigma>) = map_to_ptes (ksPSpace s'a); map_to_asidpools (ksPSpace \<sigma>) = map_to_asidpools (ksPSpace s'a); map_to_user_data (ksPSpace \<sigma>) = map_to_user_data (ksPSpace s'a); map_to_user_data_device (ksPSpace \<sigma>) = map_to_user_data_device (ksPSpace s'a); map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace \<sigma>) = map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a); \<forall>T p. typ_at' T p \<sigma> = typ_at' T p s'a; globals s' = globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr ptr) cte') (t_hrs_' (globals s))\<rparr>; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cslift s (cte_Ptr ptr) = Some cte'a; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cte_lift cte'a = Some y; cmap_relation (map_to_eps (ksPSpace s'a)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); c_valid_cte cte'a; cte'' = cte_to_H y; cmap_relation (map_to_ntfns (ksPSpace s'a)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace s'a)) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s'a)) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s'a)) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s'a) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s'a) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s'a)) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s'a)) (c_h_t_valid s) pt_Ptr; cready_queues_relation (cslift s) (ksReadyQueues_' (globals s)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals s)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals s) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals s)); carch_state_relation (ksArchState \<sigma>) (globals s); cmachine_state_relation (ksMachineState \<sigma>) (globals s); cte_array_relation \<sigma> (globals s); tcb_cte_array_relation \<sigma> (globals s); apsnd fst (ghost'state_' (globals s)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals s)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals s) = ksWorkUnitsCompleted \<sigma>; 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 \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals s) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals s) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> cmap_relation ((ctes_of \<sigma>)(ptr \<mapsto> cte)) ((cslift s)(cte_Ptr ptr \<mapsto> cte')) cte_Ptr ccte_relation \<and> cmap_relation (map_to_tcbs (ksPSpace s'a)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation \<and> cmap_relation (heap_to_user_data (ksPSpace s'a) (underlying_memory (ksMachineState s'a))) (cslift s) PTR(user_data_C) cuser_user_data_relation \<and> cmap_relation (heap_to_device_data (ksPSpace s'a) (underlying_memory (ksMachineState s'a))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation \<and> cready_queues_relation (cslift s) (ksReadyQueues_' (globals s)) (ksReadyQueues s'a) \<and> zero_ranges_are_zero (gsUntypedZeroRanges s'a) (t_hrs_' (globals s)) \<and> cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s)) (ksReadyQueuesL1Bitmap s'a) \<and> cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s)) (ksReadyQueuesL2Bitmap s'a) \<and> ksCurThread \<sigma> = ksCurThread s'a \<and> ksIdleThread \<sigma> = ksIdleThread s'a \<and> cinterrupt_relation (ksInterruptState s'a) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s)) \<and> cscheduler_action_relation (ksSchedulerAction s'a) (ksSchedulerAction_' (globals s)) \<and> carch_state_relation (ksArchState s'a) (globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr ptr) cte') (t_hrs_' (globals s))\<rparr>) \<and> cmachine_state_relation (ksMachineState s'a) (globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr ptr) cte') (t_hrs_' (globals s))\<rparr>) \<and> cte_array_relation s'a (globals s) \<and> tcb_cte_array_relation s'a (globals s) \<and> gsUserPages \<sigma> = gsUserPages s'a \<and> gsCNodes \<sigma> = gsCNodes s'a \<and> ghost_size_rel (ghost'state_' (globals s)) (gsMaxObjectSize s'a) \<and> ksWorkUnitsCompleted \<sigma> = ksWorkUnitsCompleted s'a \<and> cdom_schedule_relation (kernel_state.ksDomSchedule s'a) kernel_all_global_addresses.ksDomSchedule \<and> word_of_nat (ksDomScheduleIdx \<sigma>) = word_of_nat (ksDomScheduleIdx s'a) \<and> ksCurDomain \<sigma> = ksCurDomain s'a \<and> ksDomainTime \<sigma> = ksDomainTime s'a
 2. \<And>s'a. \<lbrakk>(\<sigma>, s) \<in> rf_sr; ctes_of \<sigma> ptr = Some cte''; t_hrs_' (globals s') = hrs_mem_update (heap_update (cte_Ptr ptr) cte') (t_hrs_' (globals s)); ccte_relation cte cte'; globals s'\<lparr>t_hrs_' := undefined\<rparr> = globals s\<lparr>t_hrs_' := undefined\<rparr>; s'a = \<sigma>\<lparr>ksPSpace := ksPSpace s'a\<rparr>; ctes_of s'a = (ctes_of \<sigma>)(ptr \<mapsto> cte); map_to_eps (ksPSpace \<sigma>) = map_to_eps (ksPSpace s'a); map_to_ntfns (ksPSpace \<sigma>) = map_to_ntfns (ksPSpace s'a); map_to_pdes (ksPSpace \<sigma>) = map_to_pdes (ksPSpace s'a); map_to_ptes (ksPSpace \<sigma>) = map_to_ptes (ksPSpace s'a); map_to_asidpools (ksPSpace \<sigma>) = map_to_asidpools (ksPSpace s'a); map_to_user_data (ksPSpace \<sigma>) = map_to_user_data (ksPSpace s'a); map_to_user_data_device (ksPSpace \<sigma>) = map_to_user_data_device (ksPSpace s'a); map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace \<sigma>) = map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a); \<forall>T p. typ_at' T p \<sigma> = typ_at' T p s'a; \<exists>cte'. cslift s (cte_Ptr ptr) = Some cte' \<and> cte_lift cte' \<noteq> None \<and> cte'' = cte_to_H (the (cte_lift cte')) \<and> c_valid_cte cte'\<rbrakk> \<Longrightarrow> \<exists>hrs. globals s' = globals s\<lparr>t_hrs_' := hrs\<rparr> proof (prove)
goal (3 subgoals):
 1. \<And>s'a cte'a a b y. \<lbrakk>ctes_of \<sigma> ptr = Some (cte_to_H y); (a, b) = hrs_mem_update (heap_update (cte_Ptr ptr) cte') (t_hrs_' (globals s)); ccte_relation cte cte'; s'a = \<sigma>\<lparr>ksPSpace := ksPSpace s'a\<rparr>; ctes_of s'a = (ctes_of \<sigma>)(ptr \<mapsto> cte); map_to_eps (ksPSpace \<sigma>) = map_to_eps (ksPSpace s'a); map_to_ntfns (ksPSpace \<sigma>) = map_to_ntfns (ksPSpace s'a); map_to_pdes (ksPSpace \<sigma>) = map_to_pdes (ksPSpace s'a); map_to_ptes (ksPSpace \<sigma>) = map_to_ptes (ksPSpace s'a); map_to_asidpools (ksPSpace \<sigma>) = map_to_asidpools (ksPSpace s'a); map_to_user_data (ksPSpace \<sigma>) = map_to_user_data (ksPSpace s'a); map_to_user_data_device (ksPSpace \<sigma>) = map_to_user_data_device (ksPSpace s'a); map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace \<sigma>) = map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a); \<forall>T p. typ_at' T p \<sigma> = typ_at' T p s'a; globals s' = globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr ptr) cte') (t_hrs_' (globals s))\<rparr>; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cslift s (cte_Ptr ptr) = Some cte'a; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cte_lift cte'a = Some y; cmap_relation (map_to_eps (ksPSpace s'a)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); c_valid_cte cte'a; cte'' = cte_to_H y; cmap_relation (map_to_ntfns (ksPSpace s'a)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace s'a)) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s'a)) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s'a)) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s'a) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s'a) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s'a)) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s'a)) (c_h_t_valid s) pt_Ptr; cready_queues_relation (cslift s) (ksReadyQueues_' (globals s)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals s)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals s) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals s)); carch_state_relation (ksArchState \<sigma>) (globals s); cmachine_state_relation (ksMachineState \<sigma>) (globals s); cte_array_relation \<sigma> (globals s); tcb_cte_array_relation \<sigma> (globals s); apsnd fst (ghost'state_' (globals s)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals s)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals s) = ksWorkUnitsCompleted \<sigma>; 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 \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals s) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals s) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> cmap_relation ((ctes_of \<sigma>)(ptr \<mapsto> cte)) ((cslift s)(cte_Ptr ptr \<mapsto> cte')) cte_Ptr ccte_relation
 2. \<And>s'a cte'a a b y. \<lbrakk>ctes_of \<sigma> ptr = Some (cte_to_H y); (a, b) = hrs_mem_update (heap_update (cte_Ptr ptr) cte') (t_hrs_' (globals s)); ccte_relation cte cte'; s'a = \<sigma>\<lparr>ksPSpace := ksPSpace s'a\<rparr>; ctes_of s'a = (ctes_of \<sigma>)(ptr \<mapsto> cte); map_to_eps (ksPSpace \<sigma>) = map_to_eps (ksPSpace s'a); map_to_ntfns (ksPSpace \<sigma>) = map_to_ntfns (ksPSpace s'a); map_to_pdes (ksPSpace \<sigma>) = map_to_pdes (ksPSpace s'a); map_to_ptes (ksPSpace \<sigma>) = map_to_ptes (ksPSpace s'a); map_to_asidpools (ksPSpace \<sigma>) = map_to_asidpools (ksPSpace s'a); map_to_user_data (ksPSpace \<sigma>) = map_to_user_data (ksPSpace s'a); map_to_user_data_device (ksPSpace \<sigma>) = map_to_user_data_device (ksPSpace s'a); map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace \<sigma>) = map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a); \<forall>T p. typ_at' T p \<sigma> = typ_at' T p s'a; globals s' = globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr ptr) cte') (t_hrs_' (globals s))\<rparr>; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cslift s (cte_Ptr ptr) = Some cte'a; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cte_lift cte'a = Some y; cmap_relation (map_to_eps (ksPSpace s'a)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); c_valid_cte cte'a; cte'' = cte_to_H y; cmap_relation (map_to_ntfns (ksPSpace s'a)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace s'a)) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s'a)) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s'a)) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s'a) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s'a) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s'a)) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s'a)) (c_h_t_valid s) pt_Ptr; cready_queues_relation (cslift s) (ksReadyQueues_' (globals s)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals s)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals s) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals s)); carch_state_relation (ksArchState \<sigma>) (globals s); cmachine_state_relation (ksMachineState \<sigma>) (globals s); cte_array_relation \<sigma> (globals s); tcb_cte_array_relation \<sigma> (globals s); apsnd fst (ghost'state_' (globals s)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals s)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals s) = ksWorkUnitsCompleted \<sigma>; 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 \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals s) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals s) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> cmap_relation (map_to_tcbs (ksPSpace s'a)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation \<and> cmap_relation (heap_to_user_data (ksPSpace s'a) (underlying_memory (ksMachineState s'a))) (cslift s) PTR(user_data_C) cuser_user_data_relation \<and> cmap_relation (heap_to_device_data (ksPSpace s'a) (underlying_memory (ksMachineState s'a))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation \<and> cready_queues_relation (cslift s) (ksReadyQueues_' (globals s)) (ksReadyQueues s'a) \<and> zero_ranges_are_zero (gsUntypedZeroRanges s'a) (t_hrs_' (globals s)) \<and> cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s)) (ksReadyQueuesL1Bitmap s'a) \<and> cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s)) (ksReadyQueuesL2Bitmap s'a) \<and> ksCurThread \<sigma> = ksCurThread s'a \<and> ksIdleThread \<sigma> = ksIdleThread s'a \<and> cinterrupt_relation (ksInterruptState s'a) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s)) \<and> cscheduler_action_relation (ksSchedulerAction s'a) (ksSchedulerAction_' (globals s)) \<and> carch_state_relation (ksArchState s'a) (globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr ptr) cte') (t_hrs_' (globals s))\<rparr>) \<and> cmachine_state_relation (ksMachineState s'a) (globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr ptr) cte') (t_hrs_' (globals s))\<rparr>) \<and> cte_array_relation s'a (globals s) \<and> tcb_cte_array_relation s'a (globals s) \<and> gsUserPages \<sigma> = gsUserPages s'a \<and> gsCNodes \<sigma> = gsCNodes s'a \<and> ghost_size_rel (ghost'state_' (globals s)) (gsMaxObjectSize s'a) \<and> ksWorkUnitsCompleted \<sigma> = ksWorkUnitsCompleted s'a \<and> cdom_schedule_relation (kernel_state.ksDomSchedule s'a) kernel_all_global_addresses.ksDomSchedule \<and> word_of_nat (ksDomScheduleIdx \<sigma>) = word_of_nat (ksDomScheduleIdx s'a) \<and> ksCurDomain \<sigma> = ksCurDomain s'a \<and> ksDomainTime \<sigma> = ksDomainTime s'a
 3. \<And>s'a. \<lbrakk>(\<sigma>, s) \<in> rf_sr; ctes_of \<sigma> ptr = Some cte''; t_hrs_' (globals s') = hrs_mem_update (heap_update (cte_Ptr ptr) cte') (t_hrs_' (globals s)); ccte_relation cte cte'; globals s'\<lparr>t_hrs_' := undefined\<rparr> = globals s\<lparr>t_hrs_' := undefined\<rparr>; s'a = \<sigma>\<lparr>ksPSpace := ksPSpace s'a\<rparr>; ctes_of s'a = (ctes_of \<sigma>)(ptr \<mapsto> cte); map_to_eps (ksPSpace \<sigma>) = map_to_eps (ksPSpace s'a); map_to_ntfns (ksPSpace \<sigma>) = map_to_ntfns (ksPSpace s'a); map_to_pdes (ksPSpace \<sigma>) = map_to_pdes (ksPSpace s'a); map_to_ptes (ksPSpace \<sigma>) = map_to_ptes (ksPSpace s'a); map_to_asidpools (ksPSpace \<sigma>) = map_to_asidpools (ksPSpace s'a); map_to_user_data (ksPSpace \<sigma>) = map_to_user_data (ksPSpace s'a); map_to_user_data_device (ksPSpace \<sigma>) = map_to_user_data_device (ksPSpace s'a); map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace \<sigma>) = map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a); \<forall>T p. typ_at' T p \<sigma> = typ_at' T p s'a; \<exists>cte'. cslift s (cte_Ptr ptr) = Some cte' \<and> cte_lift cte' \<noteq> None \<and> cte'' = cte_to_H (the (cte_lift cte')) \<and> c_valid_cte cte'\<rbrakk> \<Longrightarrow> \<exists>hrs. globals s' = globals s\<lparr>t_hrs_' := hrs\<rparr> proof (prove)
goal (2 subgoals):
 1. \<And>s'a cte'a a b y. \<lbrakk>ctes_of \<sigma> ptr = Some (cte_to_H y); (a, b) = hrs_mem_update (heap_update (cte_Ptr ptr) cte') (t_hrs_' (globals s)); ccte_relation cte cte'; s'a = \<sigma>\<lparr>ksPSpace := ksPSpace s'a\<rparr>; ctes_of s'a = (ctes_of \<sigma>)(ptr \<mapsto> cte); map_to_eps (ksPSpace \<sigma>) = map_to_eps (ksPSpace s'a); map_to_ntfns (ksPSpace \<sigma>) = map_to_ntfns (ksPSpace s'a); map_to_pdes (ksPSpace \<sigma>) = map_to_pdes (ksPSpace s'a); map_to_ptes (ksPSpace \<sigma>) = map_to_ptes (ksPSpace s'a); map_to_asidpools (ksPSpace \<sigma>) = map_to_asidpools (ksPSpace s'a); map_to_user_data (ksPSpace \<sigma>) = map_to_user_data (ksPSpace s'a); map_to_user_data_device (ksPSpace \<sigma>) = map_to_user_data_device (ksPSpace s'a); map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace \<sigma>) = map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a); \<forall>T p. typ_at' T p \<sigma> = typ_at' T p s'a; globals s' = globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr ptr) cte') (t_hrs_' (globals s))\<rparr>; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cslift s (cte_Ptr ptr) = Some cte'a; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cte_lift cte'a = Some y; cmap_relation (map_to_eps (ksPSpace s'a)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); c_valid_cte cte'a; cte'' = cte_to_H y; cmap_relation (map_to_ntfns (ksPSpace s'a)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace s'a)) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s'a)) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s'a)) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s'a) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s'a) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s'a)) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s'a)) (c_h_t_valid s) pt_Ptr; cready_queues_relation (cslift s) (ksReadyQueues_' (globals s)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals s)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals s) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals s)); carch_state_relation (ksArchState \<sigma>) (globals s); cmachine_state_relation (ksMachineState \<sigma>) (globals s); cte_array_relation \<sigma> (globals s); tcb_cte_array_relation \<sigma> (globals s); apsnd fst (ghost'state_' (globals s)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals s)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals s) = ksWorkUnitsCompleted \<sigma>; 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 \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals s) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals s) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> cmap_relation (map_to_tcbs (ksPSpace s'a)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation \<and> cmap_relation (heap_to_user_data (ksPSpace s'a) (underlying_memory (ksMachineState s'a))) (cslift s) PTR(user_data_C) cuser_user_data_relation \<and> cmap_relation (heap_to_device_data (ksPSpace s'a) (underlying_memory (ksMachineState s'a))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation \<and> cready_queues_relation (cslift s) (ksReadyQueues_' (globals s)) (ksReadyQueues s'a) \<and> zero_ranges_are_zero (gsUntypedZeroRanges s'a) (t_hrs_' (globals s)) \<and> cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s)) (ksReadyQueuesL1Bitmap s'a) \<and> cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s)) (ksReadyQueuesL2Bitmap s'a) \<and> ksCurThread \<sigma> = ksCurThread s'a \<and> ksIdleThread \<sigma> = ksIdleThread s'a \<and> cinterrupt_relation (ksInterruptState s'a) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s)) \<and> cscheduler_action_relation (ksSchedulerAction s'a) (ksSchedulerAction_' (globals s)) \<and> carch_state_relation (ksArchState s'a) (globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr ptr) cte') (t_hrs_' (globals s))\<rparr>) \<and> cmachine_state_relation (ksMachineState s'a) (globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr ptr) cte') (t_hrs_' (globals s))\<rparr>) \<and> cte_array_relation s'a (globals s) \<and> tcb_cte_array_relation s'a (globals s) \<and> gsUserPages \<sigma> = gsUserPages s'a \<and> gsCNodes \<sigma> = gsCNodes s'a \<and> ghost_size_rel (ghost'state_' (globals s)) (gsMaxObjectSize s'a) \<and> ksWorkUnitsCompleted \<sigma> = ksWorkUnitsCompleted s'a \<and> cdom_schedule_relation (kernel_state.ksDomSchedule s'a) kernel_all_global_addresses.ksDomSchedule \<and> word_of_nat (ksDomScheduleIdx \<sigma>) = word_of_nat (ksDomScheduleIdx s'a) \<and> ksCurDomain \<sigma> = ksCurDomain s'a \<and> ksDomainTime \<sigma> = ksDomainTime s'a
 2. \<And>s'a. \<lbrakk>(\<sigma>, s) \<in> rf_sr; ctes_of \<sigma> ptr = Some cte''; t_hrs_' (globals s') = hrs_mem_update (heap_update (cte_Ptr ptr) cte') (t_hrs_' (globals s)); ccte_relation cte cte'; globals s'\<lparr>t_hrs_' := undefined\<rparr> = globals s\<lparr>t_hrs_' := undefined\<rparr>; s'a = \<sigma>\<lparr>ksPSpace := ksPSpace s'a\<rparr>; ctes_of s'a = (ctes_of \<sigma>)(ptr \<mapsto> cte); map_to_eps (ksPSpace \<sigma>) = map_to_eps (ksPSpace s'a); map_to_ntfns (ksPSpace \<sigma>) = map_to_ntfns (ksPSpace s'a); map_to_pdes (ksPSpace \<sigma>) = map_to_pdes (ksPSpace s'a); map_to_ptes (ksPSpace \<sigma>) = map_to_ptes (ksPSpace s'a); map_to_asidpools (ksPSpace \<sigma>) = map_to_asidpools (ksPSpace s'a); map_to_user_data (ksPSpace \<sigma>) = map_to_user_data (ksPSpace s'a); map_to_user_data_device (ksPSpace \<sigma>) = map_to_user_data_device (ksPSpace s'a); map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace \<sigma>) = map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a); \<forall>T p. typ_at' T p \<sigma> = typ_at' T p s'a; \<exists>cte'. cslift s (cte_Ptr ptr) = Some cte' \<and> cte_lift cte' \<noteq> None \<and> cte'' = cte_to_H (the (cte_lift cte')) \<and> c_valid_cte cte'\<rbrakk> \<Longrightarrow> \<exists>hrs. globals s' = globals s\<lparr>t_hrs_' := hrs\<rparr> proof (prove)
goal (2 subgoals):
 1. \<And>s'a cte'a a b y. \<lbrakk>ctes_of \<sigma> ptr = Some (cte_to_H y); (a, b) = hrs_mem_update (heap_update (cte_Ptr ptr) cte') (t_hrs_' (globals s)); ccte_relation cte cte'; ctes_of s'a = (ctes_of \<sigma>)(ptr \<mapsto> cte); map_to_eps (ksPSpace \<sigma>) = map_to_eps (ksPSpace s'a); map_to_ntfns (ksPSpace \<sigma>) = map_to_ntfns (ksPSpace s'a); map_to_pdes (ksPSpace \<sigma>) = map_to_pdes (ksPSpace s'a); map_to_ptes (ksPSpace \<sigma>) = map_to_ptes (ksPSpace s'a); map_to_asidpools (ksPSpace \<sigma>) = map_to_asidpools (ksPSpace s'a); map_to_user_data (ksPSpace \<sigma>) = map_to_user_data (ksPSpace s'a); map_to_user_data_device (ksPSpace \<sigma>) = map_to_user_data_device (ksPSpace s'a); map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace \<sigma>) = map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a); \<forall>T p. typ_at' T p \<sigma> = typ_at' T p s'a; globals s' = globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr ptr) cte') (t_hrs_' (globals s))\<rparr>; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cslift s (cte_Ptr ptr) = Some cte'a; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cte_lift cte'a = Some y; cmap_relation (map_to_eps (ksPSpace s'a)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); c_valid_cte cte'a; cte'' = cte_to_H y; cmap_relation (map_to_ntfns (ksPSpace s'a)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace s'a)) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s'a)) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s'a)) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s'a) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s'a) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s'a)) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s'a)) (c_h_t_valid s) pt_Ptr; cready_queues_relation (cslift s) (ksReadyQueues_' (globals s)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals s)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals s) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals s)); carch_state_relation (ksArchState \<sigma>) (globals s); cmachine_state_relation (ksMachineState \<sigma>) (globals s); cte_array_relation \<sigma> (globals s); tcb_cte_array_relation \<sigma> (globals s); apsnd fst (ghost'state_' (globals s)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals s)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals s) = ksWorkUnitsCompleted \<sigma>; 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 \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals s) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals s) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> cmap_relation (map_to_tcbs (ksPSpace (\<sigma>\<lparr>ksPSpace := ksPSpace s'a\<rparr>))) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation \<and> cmap_relation (heap_to_user_data (ksPSpace (\<sigma>\<lparr>ksPSpace := ksPSpace s'a\<rparr>)) (underlying_memory (ksMachineState (\<sigma>\<lparr>ksPSpace := ksPSpace s'a\<rparr>)))) (cslift s) PTR(user_data_C) cuser_user_data_relation \<and> cmap_relation (heap_to_device_data (ksPSpace (\<sigma>\<lparr>ksPSpace := ksPSpace s'a\<rparr>)) (underlying_memory (ksMachineState (\<sigma>\<lparr>ksPSpace := ksPSpace s'a\<rparr>)))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation \<and> cready_queues_relation (cslift s) (ksReadyQueues_' (globals s)) (ksReadyQueues (\<sigma>\<lparr>ksPSpace := ksPSpace s'a\<rparr>)) \<and> zero_ranges_are_zero (gsUntypedZeroRanges (\<sigma>\<lparr>ksPSpace := ksPSpace s'a\<rparr>)) (t_hrs_' (globals s)) \<and> cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s)) (ksReadyQueuesL1Bitmap (\<sigma>\<lparr>ksPSpace := ksPSpace s'a\<rparr>)) \<and> cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s)) (ksReadyQueuesL2Bitmap (\<sigma>\<lparr>ksPSpace := ksPSpace s'a\<rparr>)) \<and> ksCurThread \<sigma> = ksCurThread (\<sigma>\<lparr>ksPSpace := ksPSpace s'a\<rparr>) \<and> ksIdleThread \<sigma> = ksIdleThread (\<sigma>\<lparr>ksPSpace := ksPSpace s'a\<rparr>) \<and> cinterrupt_relation (ksInterruptState (\<sigma>\<lparr>ksPSpace := ksPSpace s'a\<rparr>)) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s)) \<and> cscheduler_action_relation (ksSchedulerAction (\<sigma>\<lparr>ksPSpace := ksPSpace s'a\<rparr>)) (ksSchedulerAction_' (globals s)) \<and> carch_state_relation (ksArchState (\<sigma>\<lparr>ksPSpace := ksPSpace s'a\<rparr>)) (globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr ptr) cte') (t_hrs_' (globals s))\<rparr>) \<and> cmachine_state_relation (ksMachineState (\<sigma>\<lparr>ksPSpace := ksPSpace s'a\<rparr>)) (globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr ptr) cte') (t_hrs_' (globals s))\<rparr>) \<and> cte_array_relation (\<sigma>\<lparr>ksPSpace := ksPSpace s'a\<rparr>) (globals s) \<and> tcb_cte_array_relation (\<sigma>\<lparr>ksPSpace := ksPSpace s'a\<rparr>) (globals s) \<and> gsUserPages \<sigma> = gsUserPages (\<sigma>\<lparr>ksPSpace := ksPSpace s'a\<rparr>) \<and> gsCNodes \<sigma> = gsCNodes (\<sigma>\<lparr>ksPSpace := ksPSpace s'a\<rparr>) \<and> ghost_size_rel (ghost'state_' (globals s)) (gsMaxObjectSize (\<sigma>\<lparr>ksPSpace := ksPSpace s'a\<rparr>)) \<and> ksWorkUnitsCompleted \<sigma> = ksWorkUnitsCompleted (\<sigma>\<lparr>ksPSpace := ksPSpace s'a\<rparr>) \<and> cdom_schedule_relation (kernel_state.ksDomSchedule (\<sigma>\<lparr>ksPSpace := ksPSpace s'a\<rparr>)) kernel_all_global_addresses.ksDomSchedule \<and> word_of_nat (ksDomScheduleIdx \<sigma>) = word_of_nat (ksDomScheduleIdx (\<sigma>\<lparr>ksPSpace := ksPSpace s'a\<rparr>)) \<and> ksCurDomain \<sigma> = ksCurDomain (\<sigma>\<lparr>ksPSpace := ksPSpace s'a\<rparr>) \<and> ksDomainTime \<sigma> = ksDomainTime (\<sigma>\<lparr>ksPSpace := ksPSpace s'a\<rparr>)
 2. \<And>s'a. \<lbrakk>(\<sigma>, s) \<in> rf_sr; ctes_of \<sigma> ptr = Some cte''; t_hrs_' (globals s') = hrs_mem_update (heap_update (cte_Ptr ptr) cte') (t_hrs_' (globals s)); ccte_relation cte cte'; globals s'\<lparr>t_hrs_' := undefined\<rparr> = globals s\<lparr>t_hrs_' := undefined\<rparr>; s'a = \<sigma>\<lparr>ksPSpace := ksPSpace s'a\<rparr>; ctes_of s'a = (ctes_of \<sigma>)(ptr \<mapsto> cte); map_to_eps (ksPSpace \<sigma>) = map_to_eps (ksPSpace s'a); map_to_ntfns (ksPSpace \<sigma>) = map_to_ntfns (ksPSpace s'a); map_to_pdes (ksPSpace \<sigma>) = map_to_pdes (ksPSpace s'a); map_to_ptes (ksPSpace \<sigma>) = map_to_ptes (ksPSpace s'a); map_to_asidpools (ksPSpace \<sigma>) = map_to_asidpools (ksPSpace s'a); map_to_user_data (ksPSpace \<sigma>) = map_to_user_data (ksPSpace s'a); map_to_user_data_device (ksPSpace \<sigma>) = map_to_user_data_device (ksPSpace s'a); map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace \<sigma>) = map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a); \<forall>T p. typ_at' T p \<sigma> = typ_at' T p s'a; \<exists>cte'. cslift s (cte_Ptr ptr) = Some cte' \<and> cte_lift cte' \<noteq> None \<and> cte'' = cte_to_H (the (cte_lift cte')) \<and> c_valid_cte cte'\<rbrakk> \<Longrightarrow> \<exists>hrs. globals s' = globals s\<lparr>t_hrs_' := hrs\<rparr> proof (prove)
goal (2 subgoals):
 1. \<And>s'a cte'a a b y. \<lbrakk>ctes_of \<sigma> ptr = Some (cte_to_H y); (a, b) = hrs_mem_update (heap_update (cte_Ptr ptr) cte') (t_hrs_' (globals s)); ccte_relation cte cte'; ctes_of s'a = (ctes_of \<sigma>)(ptr \<mapsto> cte); map_to_eps (ksPSpace \<sigma>) = map_to_eps (ksPSpace s'a); map_to_ntfns (ksPSpace \<sigma>) = map_to_ntfns (ksPSpace s'a); map_to_pdes (ksPSpace \<sigma>) = map_to_pdes (ksPSpace s'a); map_to_ptes (ksPSpace \<sigma>) = map_to_ptes (ksPSpace s'a); map_to_asidpools (ksPSpace \<sigma>) = map_to_asidpools (ksPSpace s'a); map_to_user_data (ksPSpace \<sigma>) = map_to_user_data (ksPSpace s'a); map_to_user_data_device (ksPSpace \<sigma>) = map_to_user_data_device (ksPSpace s'a); map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace \<sigma>) = map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a); \<forall>T p. typ_at' T p \<sigma> = typ_at' T p s'a; globals s' = globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr ptr) cte') (t_hrs_' (globals s))\<rparr>; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cslift s (cte_Ptr ptr) = Some cte'a; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cte_lift cte'a = Some y; cmap_relation (map_to_eps (ksPSpace s'a)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); c_valid_cte cte'a; cte'' = cte_to_H y; cmap_relation (map_to_ntfns (ksPSpace s'a)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace s'a)) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s'a)) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s'a)) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) p) (map_to_user_data (ksPSpace s'a) p)) (cslift s) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s'a) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s'a)) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s'a)) (c_h_t_valid s) pt_Ptr; cready_queues_relation (cslift s) (ksReadyQueues_' (globals s)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals s)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals s) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals s)); carch_state_relation (ksArchState \<sigma>) (globals s); cmachine_state_relation (ksMachineState \<sigma>) (globals s); cte_array_relation \<sigma> (globals s); tcb_cte_array_relation \<sigma> (globals s); apsnd fst (ghost'state_' (globals s)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals s)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals s) = ksWorkUnitsCompleted \<sigma>; 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 \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals s) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals s) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> cmap_relation (map_to_tcbs (ksPSpace s'a)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation \<and> carch_state_relation (ksArchState \<sigma>) (globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr ptr) cte') (t_hrs_' (globals s))\<rparr>) \<and> cmachine_state_relation (ksMachineState \<sigma>) (globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr ptr) cte') (t_hrs_' (globals s))\<rparr>) \<and> tcb_cte_array_relation s'a (globals s)
 2. \<And>s'a. \<lbrakk>(\<sigma>, s) \<in> rf_sr; ctes_of \<sigma> ptr = Some cte''; t_hrs_' (globals s') = hrs_mem_update (heap_update (cte_Ptr ptr) cte') (t_hrs_' (globals s)); ccte_relation cte cte'; globals s'\<lparr>t_hrs_' := undefined\<rparr> = globals s\<lparr>t_hrs_' := undefined\<rparr>; s'a = \<sigma>\<lparr>ksPSpace := ksPSpace s'a\<rparr>; ctes_of s'a = (ctes_of \<sigma>)(ptr \<mapsto> cte); map_to_eps (ksPSpace \<sigma>) = map_to_eps (ksPSpace s'a); map_to_ntfns (ksPSpace \<sigma>) = map_to_ntfns (ksPSpace s'a); map_to_pdes (ksPSpace \<sigma>) = map_to_pdes (ksPSpace s'a); map_to_ptes (ksPSpace \<sigma>) = map_to_ptes (ksPSpace s'a); map_to_asidpools (ksPSpace \<sigma>) = map_to_asidpools (ksPSpace s'a); map_to_user_data (ksPSpace \<sigma>) = map_to_user_data (ksPSpace s'a); map_to_user_data_device (ksPSpace \<sigma>) = map_to_user_data_device (ksPSpace s'a); map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace \<sigma>) = map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a); \<forall>T p. typ_at' T p \<sigma> = typ_at' T p s'a; \<exists>cte'. cslift s (cte_Ptr ptr) = Some cte' \<and> cte_lift cte' \<noteq> None \<and> cte'' = cte_to_H (the (cte_lift cte')) \<and> c_valid_cte cte'\<rbrakk> \<Longrightarrow> \<exists>hrs. globals s' = globals s\<lparr>t_hrs_' := hrs\<rparr> proof (prove)
goal (3 subgoals):
 1. \<And>s'a cte'a a b y. \<lbrakk>ctes_of \<sigma> ptr = Some (cte_to_H y); (a, b) = hrs_mem_update (heap_update (cte_Ptr ptr) cte') (t_hrs_' (globals s)); ccte_relation cte cte'; ctes_of s'a = (ctes_of \<sigma>)(ptr \<mapsto> cte); map_to_eps (ksPSpace \<sigma>) = map_to_eps (ksPSpace s'a); map_to_ntfns (ksPSpace \<sigma>) = map_to_ntfns (ksPSpace s'a); map_to_pdes (ksPSpace \<sigma>) = map_to_pdes (ksPSpace s'a); map_to_ptes (ksPSpace \<sigma>) = map_to_ptes (ksPSpace s'a); map_to_asidpools (ksPSpace \<sigma>) = map_to_asidpools (ksPSpace s'a); map_to_user_data (ksPSpace \<sigma>) = map_to_user_data (ksPSpace s'a); map_to_user_data_device (ksPSpace \<sigma>) = map_to_user_data_device (ksPSpace s'a); map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace \<sigma>) = map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a); \<forall>T p. typ_at' T p \<sigma> = typ_at' T p s'a; globals s' = globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr ptr) cte') (t_hrs_' (globals s))\<rparr>; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cslift s (cte_Ptr ptr) = Some cte'a; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cte_lift cte'a = Some y; cmap_relation (map_to_eps (ksPSpace s'a)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); c_valid_cte cte'a; cte'' = cte_to_H y; cmap_relation (map_to_ntfns (ksPSpace s'a)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace s'a)) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s'a)) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s'a)) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) p) (map_to_user_data (ksPSpace s'a) p)) (cslift s) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s'a) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s'a)) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s'a)) (c_h_t_valid s) pt_Ptr; cready_queues_relation (cslift s) (ksReadyQueues_' (globals s)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals s)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals s) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals s)); carch_state_relation (ksArchState \<sigma>) (globals s); cmachine_state_relation (ksMachineState \<sigma>) (globals s); cte_array_relation \<sigma> (globals s); tcb_cte_array_relation \<sigma> (globals s); apsnd fst (ghost'state_' (globals s)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals s)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals s) = ksWorkUnitsCompleted \<sigma>; 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 \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals s) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals s) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> cmap_relation (map_to_tcbs (ksPSpace s'a)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation
 2. \<And>s'a cte'a a b y. \<lbrakk>ctes_of \<sigma> ptr = Some (cte_to_H y); (a, b) = hrs_mem_update (heap_update (cte_Ptr ptr) cte') (t_hrs_' (globals s)); ccte_relation cte cte'; ctes_of s'a = (ctes_of \<sigma>)(ptr \<mapsto> cte); map_to_eps (ksPSpace \<sigma>) = map_to_eps (ksPSpace s'a); map_to_ntfns (ksPSpace \<sigma>) = map_to_ntfns (ksPSpace s'a); map_to_pdes (ksPSpace \<sigma>) = map_to_pdes (ksPSpace s'a); map_to_ptes (ksPSpace \<sigma>) = map_to_ptes (ksPSpace s'a); map_to_asidpools (ksPSpace \<sigma>) = map_to_asidpools (ksPSpace s'a); map_to_user_data (ksPSpace \<sigma>) = map_to_user_data (ksPSpace s'a); map_to_user_data_device (ksPSpace \<sigma>) = map_to_user_data_device (ksPSpace s'a); map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace \<sigma>) = map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a); \<forall>T p. typ_at' T p \<sigma> = typ_at' T p s'a; globals s' = globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr ptr) cte') (t_hrs_' (globals s))\<rparr>; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cslift s (cte_Ptr ptr) = Some cte'a; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cte_lift cte'a = Some y; cmap_relation (map_to_eps (ksPSpace s'a)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); c_valid_cte cte'a; cte'' = cte_to_H y; cmap_relation (map_to_ntfns (ksPSpace s'a)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace s'a)) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s'a)) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s'a)) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) p) (map_to_user_data (ksPSpace s'a) p)) (cslift s) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s'a) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s'a)) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s'a)) (c_h_t_valid s) pt_Ptr; cready_queues_relation (cslift s) (ksReadyQueues_' (globals s)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals s)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals s) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals s)); carch_state_relation (ksArchState \<sigma>) (globals s); cmachine_state_relation (ksMachineState \<sigma>) (globals s); cte_array_relation \<sigma> (globals s); tcb_cte_array_relation \<sigma> (globals s); apsnd fst (ghost'state_' (globals s)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals s)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals s) = ksWorkUnitsCompleted \<sigma>; 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 \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals s) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals s) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> carch_state_relation (ksArchState \<sigma>) (globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr ptr) cte') (t_hrs_' (globals s))\<rparr>) \<and> cmachine_state_relation (ksMachineState \<sigma>) (globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr ptr) cte') (t_hrs_' (globals s))\<rparr>) \<and> tcb_cte_array_relation s'a (globals s)
 3. \<And>s'a. \<lbrakk>(\<sigma>, s) \<in> rf_sr; ctes_of \<sigma> ptr = Some cte''; t_hrs_' (globals s') = hrs_mem_update (heap_update (cte_Ptr ptr) cte') (t_hrs_' (globals s)); ccte_relation cte cte'; globals s'\<lparr>t_hrs_' := undefined\<rparr> = globals s\<lparr>t_hrs_' := undefined\<rparr>; s'a = \<sigma>\<lparr>ksPSpace := ksPSpace s'a\<rparr>; ctes_of s'a = (ctes_of \<sigma>)(ptr \<mapsto> cte); map_to_eps (ksPSpace \<sigma>) = map_to_eps (ksPSpace s'a); map_to_ntfns (ksPSpace \<sigma>) = map_to_ntfns (ksPSpace s'a); map_to_pdes (ksPSpace \<sigma>) = map_to_pdes (ksPSpace s'a); map_to_ptes (ksPSpace \<sigma>) = map_to_ptes (ksPSpace s'a); map_to_asidpools (ksPSpace \<sigma>) = map_to_asidpools (ksPSpace s'a); map_to_user_data (ksPSpace \<sigma>) = map_to_user_data (ksPSpace s'a); map_to_user_data_device (ksPSpace \<sigma>) = map_to_user_data_device (ksPSpace s'a); map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace \<sigma>) = map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a); \<forall>T p. typ_at' T p \<sigma> = typ_at' T p s'a; \<exists>cte'. cslift s (cte_Ptr ptr) = Some cte' \<and> cte_lift cte' \<noteq> None \<and> cte'' = cte_to_H (the (cte_lift cte')) \<and> c_valid_cte cte'\<rbrakk> \<Longrightarrow> \<exists>hrs. globals s' = globals s\<lparr>t_hrs_' := hrs\<rparr> proof (prove)
goal (2 subgoals):
 1. \<And>s'a cte'a a b y. \<lbrakk>ctes_of \<sigma> ptr = Some (cte_to_H y); (a, b) = hrs_mem_update (heap_update (cte_Ptr ptr) cte') (t_hrs_' (globals s)); ccte_relation cte cte'; ctes_of s'a = (ctes_of \<sigma>)(ptr \<mapsto> cte); map_to_eps (ksPSpace \<sigma>) = map_to_eps (ksPSpace s'a); map_to_ntfns (ksPSpace \<sigma>) = map_to_ntfns (ksPSpace s'a); map_to_pdes (ksPSpace \<sigma>) = map_to_pdes (ksPSpace s'a); map_to_ptes (ksPSpace \<sigma>) = map_to_ptes (ksPSpace s'a); map_to_asidpools (ksPSpace \<sigma>) = map_to_asidpools (ksPSpace s'a); map_to_user_data (ksPSpace \<sigma>) = map_to_user_data (ksPSpace s'a); map_to_user_data_device (ksPSpace \<sigma>) = map_to_user_data_device (ksPSpace s'a); map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace \<sigma>) = map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a); \<forall>T p. typ_at' T p \<sigma> = typ_at' T p s'a; globals s' = globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr ptr) cte') (t_hrs_' (globals s))\<rparr>; cmap_relation (ctes_of \<sigma>) (cslift s) cte_Ptr ccte_relation; cslift s (cte_Ptr ptr) = Some cte'a; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift s) tcb_ptr_to_ctcb_ptr ctcb_relation; cte_lift cte'a = Some y; cmap_relation (map_to_eps (ksPSpace s'a)) (cslift s) ep_Ptr (cendpoint_relation (cslift s)); c_valid_cte cte'a; cte'' = cte_to_H y; cmap_relation (map_to_ntfns (ksPSpace s'a)) (cslift s) ntfn_Ptr (cnotification_relation (cslift s)); cmap_relation (map_to_pdes (ksPSpace s'a)) (cslift s) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s'a)) (cslift s) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s'a)) (cslift s) ap_Ptr casid_pool_relation; cmap_relation (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) p) (map_to_user_data (ksPSpace s'a) p)) (cslift s) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s'a) (underlying_memory (ksMachineState \<sigma>))) (cslift s) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s'a)) (c_h_t_valid s) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s'a)) (c_h_t_valid s) pt_Ptr; cready_queues_relation (cslift s) (ksReadyQueues_' (globals s)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals s)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals s) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals s)); carch_state_relation (ksArchState \<sigma>) (globals s); cmachine_state_relation (ksMachineState \<sigma>) (globals s); cte_array_relation \<sigma> (globals s); tcb_cte_array_relation \<sigma> (globals s); apsnd fst (ghost'state_' (globals s)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals s)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals s) = ksWorkUnitsCompleted \<sigma>; 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 \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals s) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals s) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> carch_state_relation (ksArchState \<sigma>) (globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr ptr) cte') (t_hrs_' (globals s))\<rparr>) \<and> cmachine_state_relation (ksMachineState \<sigma>) (globals s\<lparr>t_hrs_' := hrs_mem_update (heap_update (cte_Ptr ptr) cte') (t_hrs_' (globals s))\<rparr>) \<and> tcb_cte_array_relation s'a (globals s)
 2. \<And>s'a. \<lbrakk>(\<sigma>, s) \<in> rf_sr; ctes_of \<sigma> ptr = Some cte''; t_hrs_' (globals s') = hrs_mem_update (heap_update (cte_Ptr ptr) cte') (t_hrs_' (globals s)); ccte_relation cte cte'; globals s'\<lparr>t_hrs_' := undefined\<rparr> = globals s\<lparr>t_hrs_' := undefined\<rparr>; s'a = \<sigma>\<lparr>ksPSpace := ksPSpace s'a\<rparr>; ctes_of s'a = (ctes_of \<sigma>)(ptr \<mapsto> cte); map_to_eps (ksPSpace \<sigma>) = map_to_eps (ksPSpace s'a); map_to_ntfns (ksPSpace \<sigma>) = map_to_ntfns (ksPSpace s'a); map_to_pdes (ksPSpace \<sigma>) = map_to_pdes (ksPSpace s'a); map_to_ptes (ksPSpace \<sigma>) = map_to_ptes (ksPSpace s'a); map_to_asidpools (ksPSpace \<sigma>) = map_to_asidpools (ksPSpace s'a); map_to_user_data (ksPSpace \<sigma>) = map_to_user_data (ksPSpace s'a); map_to_user_data_device (ksPSpace \<sigma>) = map_to_user_data_device (ksPSpace s'a); map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace \<sigma>) = map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a); \<forall>T p. typ_at' T p \<sigma> = typ_at' T p s'a; \<exists>cte'. cslift s (cte_Ptr ptr) = Some cte' \<and> cte_lift cte' \<noteq> None \<and> cte'' = cte_to_H (the (cte_lift cte')) \<and> c_valid_cte cte'\<rbrakk> \<Longrightarrow> \<exists>hrs. globals s' = globals s\<lparr>t_hrs_' := hrs\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>s'a. \<lbrakk>(\<sigma>, s) \<in> rf_sr; ctes_of \<sigma> ptr = Some cte''; t_hrs_' (globals s') = hrs_mem_update (heap_update (cte_Ptr ptr) cte') (t_hrs_' (globals s)); ccte_relation cte cte'; globals s'\<lparr>t_hrs_' := undefined\<rparr> = globals s\<lparr>t_hrs_' := undefined\<rparr>; s'a = \<sigma>\<lparr>ksPSpace := ksPSpace s'a\<rparr>; ctes_of s'a = (ctes_of \<sigma>)(ptr \<mapsto> cte); map_to_eps (ksPSpace \<sigma>) = map_to_eps (ksPSpace s'a); map_to_ntfns (ksPSpace \<sigma>) = map_to_ntfns (ksPSpace s'a); map_to_pdes (ksPSpace \<sigma>) = map_to_pdes (ksPSpace s'a); map_to_ptes (ksPSpace \<sigma>) = map_to_ptes (ksPSpace s'a); map_to_asidpools (ksPSpace \<sigma>) = map_to_asidpools (ksPSpace s'a); map_to_user_data (ksPSpace \<sigma>) = map_to_user_data (ksPSpace s'a); map_to_user_data_device (ksPSpace \<sigma>) = map_to_user_data_device (ksPSpace s'a); map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace \<sigma>) = map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a); \<forall>T p. typ_at' T p \<sigma> = typ_at' T p s'a; \<exists>cte'. cslift s (cte_Ptr ptr) = Some cte' \<and> cte_lift cte' \<noteq> None \<and> cte'' = cte_to_H (the (cte_lift cte')) \<and> c_valid_cte cte'\<rbrakk> \<Longrightarrow> \<exists>hrs. globals s' = globals s\<lparr>t_hrs_' := hrs\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>s'a t_hrs_'a phantom_machine_state_' ghost'state_' avail_reg_' ksNumCPUs_' ndks_boot_' active_irq_' rootserver_' ksCurDomain_' ksCurThread_' ksDomainTime_' ksIdleThread_' tlbLockCount_' armKSNextASID_' current_fault_' ksReadyQueues_' armKSASIDTable_' rootserver_mem_' armKSHWASIDTable_' intStateIRQTable_' ksDomScheduleIdx_' ksSchedulerAction_' current_extra_caps_' isFPUEnabledCached_' current_lookup_fault_' ksWorkUnitsCompleted_' current_syscall_error_' ksReadyQueuesL1Bitmap_' ksReadyQueuesL2Bitmap_' t_hrs_'aa phantom_machine_state_'a ghost'state_'a avail_reg_'a ksNumCPUs_'a ndks_boot_'a active_irq_'a rootserver_'a ksCurDomain_'a ksCurThread_'a ksDomainTime_'a ksIdleThread_'a tlbLockCount_'a armKSNextASID_'a current_fault_'a ksReadyQueues_'a armKSASIDTable_'a rootserver_mem_'a armKSHWASIDTable_'a intStateIRQTable_'a ksDomScheduleIdx_'a ksSchedulerAction_'a current_extra_caps_'a isFPUEnabledCached_'a current_lookup_fault_'a ksWorkUnitsCompleted_'a current_syscall_error_'a ksReadyQueuesL1Bitmap_'a ksReadyQueuesL2Bitmap_'a. \<lbrakk>(\<sigma>, s) \<in> rf_sr; ctes_of \<sigma> ptr = Some cte''; t_hrs_' (globals s') = hrs_mem_update (heap_update (cte_Ptr ptr) cte') (t_hrs_' (globals s)); ccte_relation cte cte'; globals s'\<lparr>t_hrs_' := undefined\<rparr> = globals s\<lparr>t_hrs_' := undefined\<rparr>; s'a = \<sigma>\<lparr>ksPSpace := ksPSpace s'a\<rparr>; ctes_of s'a = (ctes_of \<sigma>)(ptr \<mapsto> cte); map_to_eps (ksPSpace \<sigma>) = map_to_eps (ksPSpace s'a); map_to_ntfns (ksPSpace \<sigma>) = map_to_ntfns (ksPSpace s'a); map_to_pdes (ksPSpace \<sigma>) = map_to_pdes (ksPSpace s'a); map_to_ptes (ksPSpace \<sigma>) = map_to_ptes (ksPSpace s'a); map_to_asidpools (ksPSpace \<sigma>) = map_to_asidpools (ksPSpace s'a); map_to_user_data (ksPSpace \<sigma>) = map_to_user_data (ksPSpace s'a); map_to_user_data_device (ksPSpace \<sigma>) = map_to_user_data_device (ksPSpace s'a); map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace \<sigma>) = map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s'a); \<forall>T p. typ_at' T p \<sigma> = typ_at' T p s'a; \<exists>cte'. cslift s (cte_Ptr ptr) = Some cte' \<and> cte_lift cte' \<noteq> None \<and> cte'' = cte_to_H (the (cte_lift cte')) \<and> c_valid_cte cte'; globals s = \<lparr>t_hrs_' = t_hrs_'a, phantom_machine_state_' = phantom_machine_state_', ghost'state_' = ghost'state_', avail_reg_' = avail_reg_', ksNumCPUs_' = ksNumCPUs_', ndks_boot_' = ndks_boot_', active_irq_' = active_irq_', rootserver_' = rootserver_', ksCurDomain_' = ksCurDomain_', ksCurThread_' = ksCurThread_', ksDomainTime_' = ksDomainTime_', ksIdleThread_' = ksIdleThread_', tlbLockCount_' = tlbLockCount_', armKSNextASID_' = armKSNextASID_', current_fault_' = current_fault_', ksReadyQueues_' = ksReadyQueues_', armKSASIDTable_' = armKSASIDTable_', rootserver_mem_' = rootserver_mem_', armKSHWASIDTable_' = armKSHWASIDTable_', intStateIRQTable_' = intStateIRQTable_', ksDomScheduleIdx_' = ksDomScheduleIdx_', ksSchedulerAction_' = ksSchedulerAction_', current_extra_caps_' = current_extra_caps_', isFPUEnabledCached_' = isFPUEnabledCached_', current_lookup_fault_' = current_lookup_fault_', ksWorkUnitsCompleted_' = ksWorkUnitsCompleted_', current_syscall_error_' = current_syscall_error_', ksReadyQueuesL1Bitmap_' = ksReadyQueuesL1Bitmap_', ksReadyQueuesL2Bitmap_' = ksReadyQueuesL2Bitmap_'\<rparr>; globals s' = \<lparr>t_hrs_' = t_hrs_'aa, phantom_machine_state_' = phantom_machine_state_'a, ghost'state_' = ghost'state_'a, avail_reg_' = avail_reg_'a, ksNumCPUs_' = ksNumCPUs_'a, ndks_boot_' = ndks_boot_'a, active_irq_' = active_irq_'a, rootserver_' = rootserver_'a, ksCurDomain_' = ksCurDomain_'a, ksCurThread_' = ksCurThread_'a, ksDomainTime_' = ksDomainTime_'a, ksIdleThread_' = ksIdleThread_'a, tlbLockCount_' = tlbLockCount_'a, armKSNextASID_' = armKSNextASID_'a, current_fault_' = current_fault_'a, ksReadyQueues_' = ksReadyQueues_'a, armKSASIDTable_' = armKSASIDTable_'a, rootserver_mem_' = rootserver_mem_'a, armKSHWASIDTable_' = armKSHWASIDTable_'a, intStateIRQTable_' = intStateIRQTable_'a, ksDomScheduleIdx_' = ksDomScheduleIdx_'a, ksSchedulerAction_' = ksSchedulerAction_'a, current_extra_caps_' = current_extra_caps_'a, isFPUEnabledCached_' = isFPUEnabledCached_'a, current_lookup_fault_' = current_lookup_fault_'a, ksWorkUnitsCompleted_' = ksWorkUnitsCompleted_'a, current_syscall_error_' = current_syscall_error_'a, ksReadyQueuesL1Bitmap_' = ksReadyQueuesL1Bitmap_'a, ksReadyQueuesL2Bitmap_' = ksReadyQueuesL2Bitmap_'a\<rparr>\<rbrakk> \<Longrightarrow> \<exists>hrs. globals s' = globals s\<lparr>t_hrs_' := hrs\<rparr> proof (prove)
goal:
No subgoals!