theory PSpace_C

lemma storePDE_Basic_ccorres':
  "\<lbrakk> cpde_relation pde pde' \<rbrakk> \<Longrightarrow>
   ccorres dc xfdc
     (\<lambda>_. valid_pde_mapping_offset' (p && mask pdBits))
     {s. ptr_val (f s) = p} hs
     (storePDE p pde)
     (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) pde'))) s)))" apply (simp add: storePDE_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_cpde_relation,
         erule ko_at_projectKO_opt) apply (rule conjI, fastforce intro: typ_heap_simps) apply (case_tac "f x", clarsimp) apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def) apply (rule conjI) apply (clarsimp simp: cpspace_relation_def typ_heap_simps
                         update_pde_map_to_pdes
                         update_pde_map_tos
                         carray_map_relation_upd_triv) 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
                   pde_stored_asid_update_valid_offset
                   cteCaps_of_def update_pde_map_tos) apply (simp add: pdeBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cpde_relation pde pde' \<Longrightarrow> ccorres dc xfdc (\<lambda>_. valid_pde_mapping_offset' (p && mask pdBits)) {s. ptr_val (f s) = p} hs (storePDE p pde) (Guard C_Guard {s. s \<Turnstile>\<^sub>c f s} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update \<acute>f pde')))) proof (prove)
goal (1 subgoal):
 1. cpde_relation pde pde' \<Longrightarrow> ccorres dc xfdc (\<lambda>_. valid_pde_mapping_offset' (p && mask pdBits)) {s. ptr_val (f s) = p} hs (setObject p pde) (Guard C_Guard {s. s \<Turnstile>\<^sub>c f s} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update \<acute>f pde')))) proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma> ko'. cpde_relation pde pde' \<Longrightarrow> \<Gamma>\<turnstile> {s. (\<sigma>, s) \<in> rf_sr \<and> valid_pde_mapping_offset' (p && mask pdBits) \<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 pde'))) {s. (\<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(p \<mapsto> injectKOS pde)\<rparr>, s) \<in> rf_sr}
 2. \<And>ko. cpde_relation pde pde' \<Longrightarrow> updateObject ko = updateObject_default ko
 3. \<And>ko. cpde_relation pde pde' \<Longrightarrow> 1 < 2 ^ objBits ko proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> ko'. cpde_relation pde pde' \<Longrightarrow> \<Gamma>\<turnstile> {s. (\<sigma>, s) \<in> rf_sr \<and> valid_pde_mapping_offset' (p && mask pdBits) \<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 pde'))) {s. (\<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(p \<mapsto> KOArch (KOPDE pde))\<rparr>, s) \<in> rf_sr}
 2. cpde_relation pde pde' \<Longrightarrow> 1 < 2 ^ pdeBits proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> ko'. cpde_relation pde pde' \<Longrightarrow> {s. (\<sigma>, s) \<in> rf_sr \<and> valid_pde_mapping_offset' (p && mask pdBits) \<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 (KOPDE pde))\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (f s) pde'))) s) \<in> rf_sr}
 2. cpde_relation pde pde' \<Longrightarrow> 1 < 2 ^ pdeBits proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> ko' x. \<lbrakk>cpde_relation pde pde'; (\<sigma>, x) \<in> rf_sr; valid_pde_mapping_offset' (ptr_val (f x) && mask pdBits); 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 (KOPDE pde))\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (f x) pde'))) x) \<in> rf_sr
 2. cpde_relation pde pde' \<Longrightarrow> 1 < 2 ^ pdeBits proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> ko' x y'. \<lbrakk>cpde_relation pde pde'; (\<sigma>, x) \<in> rf_sr; valid_pde_mapping_offset' (ptr_val (f x) && mask pdBits); ko_at' ko' (ptr_val (f x)) \<sigma>; p = ptr_val (f x); map_to_pdes (ksPSpace \<sigma>) (ptr_val (f x)) = Some ko'; cpde_relation ko' y'; cslift x (pde_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 (KOPDE pde))\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (f x) pde'))) x) \<in> rf_sr
 2. cpde_relation pde pde' \<Longrightarrow> 1 < 2 ^ pdeBits proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> ko' x y'. \<lbrakk>cpde_relation pde pde'; (\<sigma>, x) \<in> rf_sr; valid_pde_mapping_offset' (ptr_val (f x) && mask pdBits); ko_at' ko' (ptr_val (f x)) \<sigma>; p = ptr_val (f x); map_to_pdes (ksPSpace \<sigma>) (ptr_val (f x)) = Some ko'; cpde_relation ko' y'; cslift x (pde_Ptr (ptr_val (f x))) = Some y'\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(ptr_val (f x) \<mapsto> KOArch (KOPDE pde))\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (f x) pde'))) x) \<in> rf_sr
 2. cpde_relation pde pde' \<Longrightarrow> 1 < 2 ^ pdeBits proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> ko' x y'. \<lbrakk>cpde_relation pde pde'; (\<sigma>, x) \<in> rf_sr; valid_pde_mapping_offset' (p && mask pdBits); ko_at' ko' p \<sigma>; map_to_pdes (ksPSpace \<sigma>) p = Some ko'; cpde_relation ko' y'; cslift x (pde_Ptr p) = Some y'; f x = pde_Ptr p\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(p \<mapsto> KOArch (KOPDE pde))\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (pde_Ptr p) pde'))) x) \<in> rf_sr
 2. cpde_relation pde pde' \<Longrightarrow> 1 < 2 ^ pdeBits proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> ko' x y'. \<lbrakk>cpde_relation pde pde'; valid_pde_mapping_offset' (p && mask pdBits); ko_at' ko' p \<sigma>; map_to_pdes (ksPSpace \<sigma>) p = Some ko'; cpde_relation ko' y'; cslift x (pde_Ptr p) = Some y'; f x = pde_Ptr p; 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>)(p \<mapsto> KOArch (KOPDE pde))) (underlying_memory (ksMachineState \<sigma>)) (hrs_mem_update (heap_update (pde_Ptr p) pde') (t_hrs_' (globals x))) \<and> cready_queues_relation (clift (hrs_mem_update (heap_update (pde_Ptr p) pde') (t_hrs_' (globals x)))) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>) \<and> zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (hrs_mem_update (heap_update (pde_Ptr p) pde') (t_hrs_' (globals x))) \<and> carch_state_relation (ksArchState \<sigma>) (t_hrs_'_update (hrs_mem_update (heap_update (pde_Ptr p) pde')) (globals x)) \<and> cmachine_state_relation (ksMachineState \<sigma>) (t_hrs_'_update (hrs_mem_update (heap_update (pde_Ptr p) pde')) (globals x)) \<and> cvariable_array_map_relation (map_to_tcbs ((ksPSpace \<sigma>)(p \<mapsto> KOArch (KOPDE pde)))) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals x)))
 2. cpde_relation pde pde' \<Longrightarrow> 1 < 2 ^ pdeBits proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma> ko' x y'. \<lbrakk>cpde_relation pde pde'; valid_pde_mapping_offset' (p && mask pdBits); ko_at' ko' p \<sigma>; map_to_pdes (ksPSpace \<sigma>) p = Some ko'; cpde_relation ko' y'; cslift x (pde_Ptr p) = Some y'; f x = pde_Ptr p; 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>)(p \<mapsto> KOArch (KOPDE pde))) (underlying_memory (ksMachineState \<sigma>)) (hrs_mem_update (heap_update (pde_Ptr p) pde') (t_hrs_' (globals x)))
 2. \<And>\<sigma> ko' x y'. \<lbrakk>cpde_relation pde pde'; valid_pde_mapping_offset' (p && mask pdBits); ko_at' ko' p \<sigma>; map_to_pdes (ksPSpace \<sigma>) p = Some ko'; cpde_relation ko' y'; cslift x (pde_Ptr p) = Some y'; f x = pde_Ptr p; 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 (pde_Ptr p) pde') (t_hrs_' (globals x)))) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>) \<and> zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (hrs_mem_update (heap_update (pde_Ptr p) pde') (t_hrs_' (globals x))) \<and> carch_state_relation (ksArchState \<sigma>) (t_hrs_'_update (hrs_mem_update (heap_update (pde_Ptr p) pde')) (globals x)) \<and> cmachine_state_relation (ksMachineState \<sigma>) (t_hrs_'_update (hrs_mem_update (heap_update (pde_Ptr p) pde')) (globals x)) \<and> cvariable_array_map_relation (map_to_tcbs ((ksPSpace \<sigma>)(p \<mapsto> KOArch (KOPDE pde)))) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals x)))
 3. cpde_relation pde pde' \<Longrightarrow> 1 < 2 ^ pdeBits proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma> ko' x y'. \<lbrakk>cpde_relation pde pde'; valid_pde_mapping_offset' (p && mask pdBits); ko_at' ko' p \<sigma>; map_to_pdes (ksPSpace \<sigma>) p = Some ko'; cpde_relation ko' y'; cslift x (pde_Ptr p) = Some y'; f x = pde_Ptr p; 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_pdes (ksPSpace \<sigma>))(p \<mapsto> pde)) ((cslift x)(pde_Ptr p \<mapsto> pde')) pde_Ptr cpde_relation
 2. \<And>\<sigma> ko' x y'. \<lbrakk>cpde_relation pde pde'; valid_pde_mapping_offset' (p && mask pdBits); ko_at' ko' p \<sigma>; map_to_pdes (ksPSpace \<sigma>) p = Some ko'; cpde_relation ko' y'; cslift x (pde_Ptr p) = Some y'; f x = pde_Ptr p; 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 (pde_Ptr p) pde') (t_hrs_' (globals x)))) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>) \<and> zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (hrs_mem_update (heap_update (pde_Ptr p) pde') (t_hrs_' (globals x))) \<and> carch_state_relation (ksArchState \<sigma>) (t_hrs_'_update (hrs_mem_update (heap_update (pde_Ptr p) pde')) (globals x)) \<and> cmachine_state_relation (ksMachineState \<sigma>) (t_hrs_'_update (hrs_mem_update (heap_update (pde_Ptr p) pde')) (globals x)) \<and> cvariable_array_map_relation (map_to_tcbs ((ksPSpace \<sigma>)(p \<mapsto> KOArch (KOPDE pde)))) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals x)))
 3. cpde_relation pde pde' \<Longrightarrow> 1 < 2 ^ pdeBits proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> ko' x y'. \<lbrakk>cpde_relation pde pde'; valid_pde_mapping_offset' (p && mask pdBits); ko_at' ko' p \<sigma>; map_to_pdes (ksPSpace \<sigma>) p = Some ko'; cpde_relation ko' y'; cslift x (pde_Ptr p) = Some y'; f x = pde_Ptr p; 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 (pde_Ptr p) pde') (t_hrs_' (globals x)))) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>) \<and> zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (hrs_mem_update (heap_update (pde_Ptr p) pde') (t_hrs_' (globals x))) \<and> carch_state_relation (ksArchState \<sigma>) (t_hrs_'_update (hrs_mem_update (heap_update (pde_Ptr p) pde')) (globals x)) \<and> cmachine_state_relation (ksMachineState \<sigma>) (t_hrs_'_update (hrs_mem_update (heap_update (pde_Ptr p) pde')) (globals x)) \<and> cvariable_array_map_relation (map_to_tcbs ((ksPSpace \<sigma>)(p \<mapsto> KOArch (KOPDE pde)))) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals x)))
 2. cpde_relation pde pde' \<Longrightarrow> 1 < 2 ^ pdeBits proof (prove)
goal (1 subgoal):
 1. cpde_relation pde pde' \<Longrightarrow> 1 < 2 ^ pdeBits proof (prove)
goal:
No subgoals!