theory PSpace_C

lemma storePTE_Basic_ccorres':
  "\<lbrakk> cpte_relation pte pte' \<rbrakk> \<Longrightarrow>
   ccorres dc xfdc \<top> {s. ptr_val (f s) = p} hs
     (storePTE p pte)
     (Guard C_Guard {s. s \<Turnstile>\<^sub>c f s}
        (Basic (\<lambda>s. globals_update( t_hrs_'_update
            (hrs_mem_update (heap_update (f s) pte'))) s)))" apply (simp add: storePTE_def) apply (rule setObject_ccorres_helper) apply (simp_all add: objBits_simps archObjSize_def) apply (rule conseqPre, vcg) apply (rule subsetI, clarsimp simp: Collect_const_mem) apply (rule cmap_relationE1, erule rf_sr_cpte_relation,
         erule ko_at_projectKO_opt) apply (rule conjI, fastforce intro: typ_heap_simps) apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def) apply (rule conjI) apply (clarsimp simp: cpspace_relation_def typ_heap_simps
                         update_pte_map_to_ptes
                         update_pte_map_tos
                         carray_map_relation_upd_triv) apply (case_tac "f x", simp) 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
                   cteCaps_of_def update_pte_map_tos
                   ) apply (simp add: pteBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cpte_relation pte pte' \<Longrightarrow> ccorres dc xfdc (\<lambda>_. True) {s. ptr_val (f s) = p} hs (storePTE p pte) (Guard C_Guard {s. s \<Turnstile>\<^sub>c f s} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update \<acute>f pte')))) proof (prove)
goal (1 subgoal):
 1. cpte_relation pte pte' \<Longrightarrow> ccorres dc xfdc (\<lambda>_. True) {s. ptr_val (f s) = p} hs (setObject p pte) (Guard C_Guard {s. s \<Turnstile>\<^sub>c f s} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update \<acute>f pte')))) proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma> ko'. cpte_relation pte pte' \<Longrightarrow> \<Gamma>\<turnstile> {s. (\<sigma>, s) \<in> rf_sr \<and> True \<and> s \<in> {s. ptr_val (f s) = p} \<and> ko_at' ko' p \<sigma>} Guard C_Guard {s. s \<Turnstile>\<^sub>c f s} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update \<acute>f pte'))) {s. (\<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(p \<mapsto> injectKOS pte)\<rparr>, s) \<in> rf_sr}
 2. \<And>ko. cpte_relation pte pte' \<Longrightarrow> updateObject ko = updateObject_default ko
 3. \<And>ko. cpte_relation pte pte' \<Longrightarrow> 1 < 2 ^ objBits ko proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> ko'. cpte_relation pte pte' \<Longrightarrow> \<Gamma>\<turnstile> {s. (\<sigma>, s) \<in> rf_sr \<and> ptr_val (f s) = p \<and> ko_at' ko' p \<sigma>} Guard C_Guard {s. s \<Turnstile>\<^sub>c f s} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update \<acute>f pte'))) {s. (\<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(p \<mapsto> KOArch (KOPTE pte))\<rparr>, s) \<in> rf_sr}
 2. cpte_relation pte pte' \<Longrightarrow> 1 < 2 ^ pteBits proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> ko'. cpte_relation pte pte' \<Longrightarrow> {s. (\<sigma>, s) \<in> rf_sr \<and> ptr_val (f s) = p \<and> ko_at' ko' p \<sigma>} \<subseteq> {s. s \<Turnstile>\<^sub>c f s \<and> (\<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(p \<mapsto> KOArch (KOPTE pte))\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (f s) pte'))) s) \<in> rf_sr}
 2. cpte_relation pte pte' \<Longrightarrow> 1 < 2 ^ pteBits proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> ko' x. \<lbrakk>cpte_relation pte pte'; (\<sigma>, x) \<in> rf_sr; ko_at' ko' (ptr_val (f x)) \<sigma>; p = ptr_val (f x)\<rbrakk> \<Longrightarrow> x \<Turnstile>\<^sub>c f x \<and> (\<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(ptr_val (f x) \<mapsto> KOArch (KOPTE pte))\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (f x) pte'))) x) \<in> rf_sr
 2. cpte_relation pte pte' \<Longrightarrow> 1 < 2 ^ pteBits proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> ko' x y'. \<lbrakk>cpte_relation pte pte'; (\<sigma>, x) \<in> rf_sr; ko_at' ko' (ptr_val (f x)) \<sigma>; p = ptr_val (f x); map_to_ptes (ksPSpace \<sigma>) (ptr_val (f x)) = Some ko'; cpte_relation ko' y'; cslift x (pte_Ptr (ptr_val (f x))) = Some y'\<rbrakk> \<Longrightarrow> x \<Turnstile>\<^sub>c f x \<and> (\<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(ptr_val (f x) \<mapsto> KOArch (KOPTE pte))\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (f x) pte'))) x) \<in> rf_sr
 2. cpte_relation pte pte' \<Longrightarrow> 1 < 2 ^ pteBits proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> ko' x y'. \<lbrakk>cpte_relation pte pte'; (\<sigma>, x) \<in> rf_sr; ko_at' ko' (ptr_val (f x)) \<sigma>; p = ptr_val (f x); map_to_ptes (ksPSpace \<sigma>) (ptr_val (f x)) = Some ko'; cpte_relation ko' y'; cslift x (pte_Ptr (ptr_val (f x))) = Some y'\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(ptr_val (f x) \<mapsto> KOArch (KOPTE pte))\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (f x) pte'))) x) \<in> rf_sr
 2. cpte_relation pte pte' \<Longrightarrow> 1 < 2 ^ pteBits proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> ko' x y'. \<lbrakk>cpte_relation pte pte'; ko_at' ko' (ptr_val (f x)) \<sigma>; p = ptr_val (f x); map_to_ptes (ksPSpace \<sigma>) (ptr_val (f x)) = Some ko'; cpte_relation ko' y'; cslift x (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>)(ptr_val (f x) \<mapsto> KOArch (KOPTE pte))) (underlying_memory (ksMachineState \<sigma>)) (hrs_mem_update (heap_update (f x) pte') (t_hrs_' (globals x))) \<and> cready_queues_relation (clift (hrs_mem_update (heap_update (f x) pte') (t_hrs_' (globals x)))) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>) \<and> zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (hrs_mem_update (heap_update (f x) pte') (t_hrs_' (globals x))) \<and> carch_state_relation (ksArchState \<sigma>) (t_hrs_'_update (hrs_mem_update (heap_update (f x) pte')) (globals x)) \<and> cmachine_state_relation (ksMachineState \<sigma>) (t_hrs_'_update (hrs_mem_update (heap_update (f x) pte')) (globals x)) \<and> cvariable_array_map_relation (map_to_tcbs ((ksPSpace \<sigma>)(ptr_val (f x) \<mapsto> KOArch (KOPTE pte)))) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals x)))
 2. cpte_relation pte pte' \<Longrightarrow> 1 < 2 ^ pteBits proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma> ko' x y'. \<lbrakk>cpte_relation pte pte'; ko_at' ko' (ptr_val (f x)) \<sigma>; p = ptr_val (f x); map_to_ptes (ksPSpace \<sigma>) (ptr_val (f x)) = Some ko'; cpte_relation ko' y'; cslift x (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>)(ptr_val (f x) \<mapsto> KOArch (KOPTE pte))) (underlying_memory (ksMachineState \<sigma>)) (hrs_mem_update (heap_update (f x) pte') (t_hrs_' (globals x)))
 2. \<And>\<sigma> ko' x y'. \<lbrakk>cpte_relation pte pte'; ko_at' ko' (ptr_val (f x)) \<sigma>; p = ptr_val (f x); map_to_ptes (ksPSpace \<sigma>) (ptr_val (f x)) = Some ko'; cpte_relation ko' y'; cslift x (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 (f x) pte') (t_hrs_' (globals x)))) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>) \<and> zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (hrs_mem_update (heap_update (f x) pte') (t_hrs_' (globals x))) \<and> carch_state_relation (ksArchState \<sigma>) (t_hrs_'_update (hrs_mem_update (heap_update (f x) pte')) (globals x)) \<and> cmachine_state_relation (ksMachineState \<sigma>) (t_hrs_'_update (hrs_mem_update (heap_update (f x) pte')) (globals x)) \<and> cvariable_array_map_relation (map_to_tcbs ((ksPSpace \<sigma>)(ptr_val (f x) \<mapsto> KOArch (KOPTE pte)))) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals x)))
 3. cpte_relation pte pte' \<Longrightarrow> 1 < 2 ^ pteBits proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma> ko' x y'. \<lbrakk>cpte_relation pte pte'; ko_at' ko' (ptr_val (f x)) \<sigma>; p = ptr_val (f x); map_to_ptes (ksPSpace \<sigma>) (ptr_val (f x)) = Some ko'; cpte_relation ko' y'; cslift x (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_ptes (ksPSpace \<sigma>))(ptr_val (f x) \<mapsto> pte)) ((cslift x)(f x \<mapsto> pte')) pte_Ptr cpte_relation
 2. \<And>\<sigma> ko' x y'. \<lbrakk>cpte_relation pte pte'; ko_at' ko' (ptr_val (f x)) \<sigma>; p = ptr_val (f x); map_to_ptes (ksPSpace \<sigma>) (ptr_val (f x)) = Some ko'; cpte_relation ko' y'; cslift x (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 (f x) pte') (t_hrs_' (globals x)))) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>) \<and> zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (hrs_mem_update (heap_update (f x) pte') (t_hrs_' (globals x))) \<and> carch_state_relation (ksArchState \<sigma>) (t_hrs_'_update (hrs_mem_update (heap_update (f x) pte')) (globals x)) \<and> cmachine_state_relation (ksMachineState \<sigma>) (t_hrs_'_update (hrs_mem_update (heap_update (f x) pte')) (globals x)) \<and> cvariable_array_map_relation (map_to_tcbs ((ksPSpace \<sigma>)(ptr_val (f x) \<mapsto> KOArch (KOPTE pte)))) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals x)))
 3. cpte_relation pte pte' \<Longrightarrow> 1 < 2 ^ pteBits proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma> ko' x y' xa. \<lbrakk>cpte_relation pte pte'; ko_at' ko' xa \<sigma>; p = xa; map_to_ptes (ksPSpace \<sigma>) xa = Some ko'; cpte_relation ko' y'; cslift x (pte_Ptr xa) = 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; f x = pte_Ptr xa\<rbrakk> \<Longrightarrow> cmap_relation ((map_to_ptes (ksPSpace \<sigma>))(xa \<mapsto> pte)) ((cslift x)(pte_Ptr xa \<mapsto> pte')) pte_Ptr cpte_relation
 2. \<And>\<sigma> ko' x y'. \<lbrakk>cpte_relation pte pte'; ko_at' ko' (ptr_val (f x)) \<sigma>; p = ptr_val (f x); map_to_ptes (ksPSpace \<sigma>) (ptr_val (f x)) = Some ko'; cpte_relation ko' y'; cslift x (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 (f x) pte') (t_hrs_' (globals x)))) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>) \<and> zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (hrs_mem_update (heap_update (f x) pte') (t_hrs_' (globals x))) \<and> carch_state_relation (ksArchState \<sigma>) (t_hrs_'_update (hrs_mem_update (heap_update (f x) pte')) (globals x)) \<and> cmachine_state_relation (ksMachineState \<sigma>) (t_hrs_'_update (hrs_mem_update (heap_update (f x) pte')) (globals x)) \<and> cvariable_array_map_relation (map_to_tcbs ((ksPSpace \<sigma>)(ptr_val (f x) \<mapsto> KOArch (KOPTE pte)))) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals x)))
 3. cpte_relation pte pte' \<Longrightarrow> 1 < 2 ^ pteBits proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> ko' x y'. \<lbrakk>cpte_relation pte pte'; ko_at' ko' (ptr_val (f x)) \<sigma>; p = ptr_val (f x); map_to_ptes (ksPSpace \<sigma>) (ptr_val (f x)) = Some ko'; cpte_relation ko' y'; cslift x (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 (f x) pte') (t_hrs_' (globals x)))) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>) \<and> zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (hrs_mem_update (heap_update (f x) pte') (t_hrs_' (globals x))) \<and> carch_state_relation (ksArchState \<sigma>) (t_hrs_'_update (hrs_mem_update (heap_update (f x) pte')) (globals x)) \<and> cmachine_state_relation (ksMachineState \<sigma>) (t_hrs_'_update (hrs_mem_update (heap_update (f x) pte')) (globals x)) \<and> cvariable_array_map_relation (map_to_tcbs ((ksPSpace \<sigma>)(ptr_val (f x) \<mapsto> KOArch (KOPTE pte)))) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals x)))
 2. cpte_relation pte pte' \<Longrightarrow> 1 < 2 ^ pteBits proof (prove)
goal (1 subgoal):
 1. cpte_relation pte pte' \<Longrightarrow> 1 < 2 ^ pteBits proof (prove)
goal:
No subgoals!