theory VSpace_C

lemma setObjectASID_Basic_ccorres:
  "ccorres dc xfdc \<top> {s. f s = p \<and> casid_pool_relation pool (asid_pool_C.asid_pool_C (pool' s))} hs
     (setObject p pool)
     ((Basic (\<lambda>s. globals_update( t_hrs_'_update
            (hrs_mem_update (heap_update (Ptr &(ap_Ptr (f s)\<rightarrow>[''array_C''])) (pool' s)))) s)))" apply (rule setObject_ccorres_helper) apply (simp_all add: objBits_simps archObjSize_def pageBits_def) apply (rule conseqPre, vcg) apply (rule subsetI, clarsimp simp: Collect_const_mem) apply (rule cmap_relationE1, erule rf_sr_cpspace_asidpool_relation,
         erule ko_at_projectKO_opt) apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def) apply (rule conjI) apply (clarsimp simp: cpspace_relation_def typ_heap_simps
                         update_asidpool_map_to_asidpools
                         update_asidpool_map_tos) apply (case_tac y') apply clarsimp apply (erule cmap_relation_updI,
          erule ko_at_projectKO_opt, simp+) apply (simp add: cready_queues_relation_def
                   carch_state_relation_def
                   cmachine_state_relation_def
                   Let_def typ_heap_simps
                   update_asidpool_map_tos) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (\<lambda>_. True) {s. f s = p \<and> casid_pool_relation pool (asid_pool_C.asid_pool_C (pool' s))} hs (setObject p pool) (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(pde_C ptr[1024]) &(ap_Ptr \<acute>f\<rightarrow>[''array_C''])) \<acute>pool'))) proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma> ko'. \<Gamma>\<turnstile> {s. (\<sigma>, s) \<in> rf_sr \<and> True \<and> s \<in> {s. f s = p \<and> casid_pool_relation pool (asid_pool_C.asid_pool_C (pool' s))} \<and> ko_at' ko' p \<sigma>} \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(pde_C ptr[1024]) &(ap_Ptr \<acute>f\<rightarrow>[''array_C''])) \<acute>pool')) {s. (\<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(p \<mapsto> injectKOS pool)\<rparr>, s) \<in> rf_sr}
 2. \<And>ko. updateObject ko = updateObject_default ko
 3. \<And>ko. 1 < 2 ^ objBits ko proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> ko'. \<Gamma>\<turnstile> {s. (\<sigma>, s) \<in> rf_sr \<and> f s = p \<and> casid_pool_relation pool (asid_pool_C.asid_pool_C (pool' s)) \<and> ko_at' ko' p \<sigma>} \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(pde_C ptr[1024]) &(ap_Ptr \<acute>f\<rightarrow>[''array_C''])) \<acute>pool')) {s. (\<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(p \<mapsto> KOArch (KOASIDPool pool))\<rparr>, s) \<in> rf_sr} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> ko'. {s. (\<sigma>, s) \<in> rf_sr \<and> f s = p \<and> casid_pool_relation pool (asid_pool_C.asid_pool_C (pool' s)) \<and> ko_at' ko' p \<sigma>} \<subseteq> {s. (\<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(p \<mapsto> KOArch (KOASIDPool pool))\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(pde_C ptr[1024]) &(ap_Ptr (f s)\<rightarrow>[''array_C''])) (pool' s)))) s) \<in> rf_sr} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> ko' x. \<lbrakk>(\<sigma>, x) \<in> rf_sr; p = f x; casid_pool_relation pool (asid_pool_C.asid_pool_C (pool' x)); ko_at' ko' (f x) \<sigma>\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(f x \<mapsto> KOArch (KOASIDPool pool))\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(pde_C ptr[1024]) &(ap_Ptr (f x)\<rightarrow>[''array_C''])) (pool' x)))) x) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> ko' x y'. \<lbrakk>(\<sigma>, x) \<in> rf_sr; p = f x; casid_pool_relation pool (asid_pool_C.asid_pool_C (pool' x)); ko_at' ko' (f x) \<sigma>; map_to_asidpools (ksPSpace \<sigma>) (f x) = Some ko'; casid_pool_relation ko' y'; cslift x (ap_Ptr (f x)) = Some y'\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(f x \<mapsto> KOArch (KOASIDPool pool))\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(pde_C ptr[1024]) &(ap_Ptr (f x)\<rightarrow>[''array_C''])) (pool' x)))) x) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> ko' x y'. \<lbrakk>p = f x; casid_pool_relation pool (asid_pool_C.asid_pool_C (pool' x)); ko_at' ko' (f x) \<sigma>; map_to_asidpools (ksPSpace \<sigma>) (f x) = Some ko'; casid_pool_relation ko' y'; cslift x (ap_Ptr (f x)) = Some y'; cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); carch_state_relation (ksArchState \<sigma>) (globals x); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - 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 x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> cpspace_relation ((ksPSpace \<sigma>)(f x \<mapsto> KOArch (KOASIDPool pool))) (underlying_memory (ksMachineState \<sigma>)) (hrs_mem_update (heap_update (PTR(pde_C ptr[1024]) &(ap_Ptr (f x)\<rightarrow>[''array_C''])) (pool' x)) (t_hrs_' (globals x))) \<and> cready_queues_relation (clift (hrs_mem_update (heap_update (PTR(pde_C ptr[1024]) &(ap_Ptr (f x)\<rightarrow>[''array_C''])) (pool' x)) (t_hrs_' (globals x)))) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>) \<and> zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (hrs_mem_update (heap_update (PTR(pde_C ptr[1024]) &(ap_Ptr (f x)\<rightarrow>[''array_C''])) (pool' x)) (t_hrs_' (globals x))) \<and> carch_state_relation (ksArchState \<sigma>) (t_hrs_'_update (hrs_mem_update (heap_update (PTR(pde_C ptr[1024]) &(ap_Ptr (f x)\<rightarrow>[''array_C''])) (pool' x))) (globals x)) \<and> cmachine_state_relation (ksMachineState \<sigma>) (t_hrs_'_update (hrs_mem_update (heap_update (PTR(pde_C ptr[1024]) &(ap_Ptr (f x)\<rightarrow>[''array_C''])) (pool' x))) (globals x)) \<and> cvariable_array_map_relation (map_to_tcbs ((ksPSpace \<sigma>)(f x \<mapsto> KOArch (KOASIDPool pool)))) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals x))) proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> ko' x y'. \<lbrakk>p = f x; casid_pool_relation pool (asid_pool_C.asid_pool_C (pool' x)); ko_at' ko' (f x) \<sigma>; map_to_asidpools (ksPSpace \<sigma>) (f x) = Some ko'; casid_pool_relation ko' y'; cslift x (ap_Ptr (f x)) = Some y'; cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); carch_state_relation (ksArchState \<sigma>) (globals x); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - 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 x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> cpspace_relation ((ksPSpace \<sigma>)(f x \<mapsto> KOArch (KOASIDPool pool))) (underlying_memory (ksMachineState \<sigma>)) (hrs_mem_update (heap_update (PTR(pde_C ptr[1024]) &(ap_Ptr (f x)\<rightarrow>[''array_C''])) (pool' x)) (t_hrs_' (globals x)))
 2. \<And>\<sigma> ko' x y'. \<lbrakk>p = f x; casid_pool_relation pool (asid_pool_C.asid_pool_C (pool' x)); ko_at' ko' (f x) \<sigma>; map_to_asidpools (ksPSpace \<sigma>) (f x) = Some ko'; casid_pool_relation ko' y'; cslift x (ap_Ptr (f x)) = Some y'; cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); carch_state_relation (ksArchState \<sigma>) (globals x); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - 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 x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> cready_queues_relation (clift (hrs_mem_update (heap_update (PTR(pde_C ptr[1024]) &(ap_Ptr (f x)\<rightarrow>[''array_C''])) (pool' x)) (t_hrs_' (globals x)))) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>) \<and> zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (hrs_mem_update (heap_update (PTR(pde_C ptr[1024]) &(ap_Ptr (f x)\<rightarrow>[''array_C''])) (pool' x)) (t_hrs_' (globals x))) \<and> carch_state_relation (ksArchState \<sigma>) (t_hrs_'_update (hrs_mem_update (heap_update (PTR(pde_C ptr[1024]) &(ap_Ptr (f x)\<rightarrow>[''array_C''])) (pool' x))) (globals x)) \<and> cmachine_state_relation (ksMachineState \<sigma>) (t_hrs_'_update (hrs_mem_update (heap_update (PTR(pde_C ptr[1024]) &(ap_Ptr (f x)\<rightarrow>[''array_C''])) (pool' x))) (globals x)) \<and> cvariable_array_map_relation (map_to_tcbs ((ksPSpace \<sigma>)(f x \<mapsto> KOArch (KOASIDPool pool)))) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals x))) proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> ko' x y'. \<lbrakk>p = f x; casid_pool_relation pool (asid_pool_C.asid_pool_C (pool' x)); ko_at' ko' (f x) \<sigma>; map_to_asidpools (ksPSpace \<sigma>) (f x) = Some ko'; casid_pool_relation ko' y'; cslift x (ap_Ptr (f x)) = Some y'; cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); carch_state_relation (ksArchState \<sigma>) (globals x); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - 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 x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>; cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr\<rbrakk> \<Longrightarrow> cmap_relation ((map_to_asidpools (ksPSpace \<sigma>))(f x \<mapsto> pool)) ((cslift x)(ap_Ptr (f x) \<mapsto> array_C_update (\<lambda>_. pool' x) y')) ap_Ptr casid_pool_relation
 2. \<And>\<sigma> ko' x y'. \<lbrakk>p = f x; casid_pool_relation pool (asid_pool_C.asid_pool_C (pool' x)); ko_at' ko' (f x) \<sigma>; map_to_asidpools (ksPSpace \<sigma>) (f x) = Some ko'; casid_pool_relation ko' y'; cslift x (ap_Ptr (f x)) = Some y'; cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); carch_state_relation (ksArchState \<sigma>) (globals x); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - 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 x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> cready_queues_relation (clift (hrs_mem_update (heap_update (PTR(pde_C ptr[1024]) &(ap_Ptr (f x)\<rightarrow>[''array_C''])) (pool' x)) (t_hrs_' (globals x)))) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>) \<and> zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (hrs_mem_update (heap_update (PTR(pde_C ptr[1024]) &(ap_Ptr (f x)\<rightarrow>[''array_C''])) (pool' x)) (t_hrs_' (globals x))) \<and> carch_state_relation (ksArchState \<sigma>) (t_hrs_'_update (hrs_mem_update (heap_update (PTR(pde_C ptr[1024]) &(ap_Ptr (f x)\<rightarrow>[''array_C''])) (pool' x))) (globals x)) \<and> cmachine_state_relation (ksMachineState \<sigma>) (t_hrs_'_update (hrs_mem_update (heap_update (PTR(pde_C ptr[1024]) &(ap_Ptr (f x)\<rightarrow>[''array_C''])) (pool' x))) (globals x)) \<and> cvariable_array_map_relation (map_to_tcbs ((ksPSpace \<sigma>)(f x \<mapsto> KOArch (KOASIDPool pool)))) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals x))) proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> ko' x y' xa. \<lbrakk>p = f x; casid_pool_relation pool (asid_pool_C.asid_pool_C (pool' x)); ko_at' ko' (f x) \<sigma>; map_to_asidpools (ksPSpace \<sigma>) (f x) = Some ko'; casid_pool_relation ko' y'; cslift x (ap_Ptr (f x)) = Some y'; cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); carch_state_relation (ksArchState \<sigma>) (globals x); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - 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 x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>; cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr; y' = asid_pool_C.asid_pool_C xa\<rbrakk> \<Longrightarrow> cmap_relation ((map_to_asidpools (ksPSpace \<sigma>))(f x \<mapsto> pool)) ((cslift x)(ap_Ptr (f x) \<mapsto> array_C_update (\<lambda>_. pool' x) y')) ap_Ptr casid_pool_relation
 2. \<And>\<sigma> ko' x y'. \<lbrakk>p = f x; casid_pool_relation pool (asid_pool_C.asid_pool_C (pool' x)); ko_at' ko' (f x) \<sigma>; map_to_asidpools (ksPSpace \<sigma>) (f x) = Some ko'; casid_pool_relation ko' y'; cslift x (ap_Ptr (f x)) = Some y'; cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); carch_state_relation (ksArchState \<sigma>) (globals x); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - 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 x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> cready_queues_relation (clift (hrs_mem_update (heap_update (PTR(pde_C ptr[1024]) &(ap_Ptr (f x)\<rightarrow>[''array_C''])) (pool' x)) (t_hrs_' (globals x)))) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>) \<and> zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (hrs_mem_update (heap_update (PTR(pde_C ptr[1024]) &(ap_Ptr (f x)\<rightarrow>[''array_C''])) (pool' x)) (t_hrs_' (globals x))) \<and> carch_state_relation (ksArchState \<sigma>) (t_hrs_'_update (hrs_mem_update (heap_update (PTR(pde_C ptr[1024]) &(ap_Ptr (f x)\<rightarrow>[''array_C''])) (pool' x))) (globals x)) \<and> cmachine_state_relation (ksMachineState \<sigma>) (t_hrs_'_update (hrs_mem_update (heap_update (PTR(pde_C ptr[1024]) &(ap_Ptr (f x)\<rightarrow>[''array_C''])) (pool' x))) (globals x)) \<and> cvariable_array_map_relation (map_to_tcbs ((ksPSpace \<sigma>)(f x \<mapsto> KOArch (KOASIDPool pool)))) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals x))) proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> ko' x xa. \<lbrakk>p = f x; casid_pool_relation pool (asid_pool_C.asid_pool_C (pool' x)); ko_at' ko' (f x) \<sigma>; map_to_asidpools (ksPSpace \<sigma>) (f x) = Some ko'; casid_pool_relation ko' (asid_pool_C.asid_pool_C xa); cslift x (ap_Ptr (f x)) = Some (asid_pool_C.asid_pool_C xa); cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); carch_state_relation (ksArchState \<sigma>) (globals x); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - 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 x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>; cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr\<rbrakk> \<Longrightarrow> cmap_relation ((map_to_asidpools (ksPSpace \<sigma>))(f x \<mapsto> pool)) ((cslift x)(ap_Ptr (f x) \<mapsto> asid_pool_C.asid_pool_C (pool' x))) ap_Ptr casid_pool_relation
 2. \<And>\<sigma> ko' x y'. \<lbrakk>p = f x; casid_pool_relation pool (asid_pool_C.asid_pool_C (pool' x)); ko_at' ko' (f x) \<sigma>; map_to_asidpools (ksPSpace \<sigma>) (f x) = Some ko'; casid_pool_relation ko' y'; cslift x (ap_Ptr (f x)) = Some y'; cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); carch_state_relation (ksArchState \<sigma>) (globals x); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - 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 x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> cready_queues_relation (clift (hrs_mem_update (heap_update (PTR(pde_C ptr[1024]) &(ap_Ptr (f x)\<rightarrow>[''array_C''])) (pool' x)) (t_hrs_' (globals x)))) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>) \<and> zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (hrs_mem_update (heap_update (PTR(pde_C ptr[1024]) &(ap_Ptr (f x)\<rightarrow>[''array_C''])) (pool' x)) (t_hrs_' (globals x))) \<and> carch_state_relation (ksArchState \<sigma>) (t_hrs_'_update (hrs_mem_update (heap_update (PTR(pde_C ptr[1024]) &(ap_Ptr (f x)\<rightarrow>[''array_C''])) (pool' x))) (globals x)) \<and> cmachine_state_relation (ksMachineState \<sigma>) (t_hrs_'_update (hrs_mem_update (heap_update (PTR(pde_C ptr[1024]) &(ap_Ptr (f x)\<rightarrow>[''array_C''])) (pool' x))) (globals x)) \<and> cvariable_array_map_relation (map_to_tcbs ((ksPSpace \<sigma>)(f x \<mapsto> KOArch (KOASIDPool pool)))) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals x))) proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> ko' x y'. \<lbrakk>p = f x; casid_pool_relation pool (asid_pool_C.asid_pool_C (pool' x)); ko_at' ko' (f x) \<sigma>; map_to_asidpools (ksPSpace \<sigma>) (f x) = Some ko'; casid_pool_relation ko' y'; cslift x (ap_Ptr (f x)) = Some y'; cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); carch_state_relation (ksArchState \<sigma>) (globals x); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - 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 x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> cready_queues_relation (clift (hrs_mem_update (heap_update (PTR(pde_C ptr[1024]) &(ap_Ptr (f x)\<rightarrow>[''array_C''])) (pool' x)) (t_hrs_' (globals x)))) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>) \<and> zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (hrs_mem_update (heap_update (PTR(pde_C ptr[1024]) &(ap_Ptr (f x)\<rightarrow>[''array_C''])) (pool' x)) (t_hrs_' (globals x))) \<and> carch_state_relation (ksArchState \<sigma>) (t_hrs_'_update (hrs_mem_update (heap_update (PTR(pde_C ptr[1024]) &(ap_Ptr (f x)\<rightarrow>[''array_C''])) (pool' x))) (globals x)) \<and> cmachine_state_relation (ksMachineState \<sigma>) (t_hrs_'_update (hrs_mem_update (heap_update (PTR(pde_C ptr[1024]) &(ap_Ptr (f x)\<rightarrow>[''array_C''])) (pool' x))) (globals x)) \<and> cvariable_array_map_relation (map_to_tcbs ((ksPSpace \<sigma>)(f x \<mapsto> KOArch (KOASIDPool pool)))) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals x))) proof (prove)
goal:
No subgoals!