theory VSpace_C

lemma asid_pool_at_rf_sr:
  "\<lbrakk>ko_at' (ASIDPool pool) p s; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow>
  \<exists>pool'. cslift s' (ap_Ptr p) = Some pool' \<and>
          casid_pool_relation (ASIDPool pool) pool'" apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def cpspace_relation_def) apply (erule (1) cmap_relation_ko_atE) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at' (asidpool.ASIDPool pool) p s; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> \<exists>pool'. cslift s' (ap_Ptr p) = Some pool' \<and> casid_pool_relation (asidpool.ASIDPool pool) pool' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at' (asidpool.ASIDPool pool) p s; cmap_relation (ctes_of s) (cslift s') cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace s)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace s)) (cslift s') ep_Ptr (cendpoint_relation (cslift s')); cmap_relation (map_to_ntfns (ksPSpace s)) (cslift s') ntfn_Ptr (cnotification_relation (cslift s')); cmap_relation (map_to_pdes (ksPSpace s)) (cslift s') pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s)) (cslift s') pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (cslift s') ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s)) (c_h_t_valid s') pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s)) (c_h_t_valid s') pt_Ptr; cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')); carch_state_relation (ksArchState s) (globals s'); cmachine_state_relation (ksMachineState s) (globals s'); cte_array_relation s (globals s'); tcb_cte_array_relation s (globals s'); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s\<rbrakk> \<Longrightarrow> \<exists>pool'. cslift s' (ap_Ptr p) = Some pool' \<and> casid_pool_relation (asidpool.ASIDPool pool) pool' proof (prove)
goal (1 subgoal):
 1. \<And>ko'. \<lbrakk>ko_at' (asidpool.ASIDPool pool) p s; cmap_relation (ctes_of s) (cslift s') cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace s)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace s)) (cslift s') ep_Ptr (cendpoint_relation (cslift s')); cmap_relation (map_to_ntfns (ksPSpace s)) (cslift s') ntfn_Ptr (cnotification_relation (cslift s')); cmap_relation (map_to_pdes (ksPSpace s)) (cslift s') pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s)) (cslift s') pte_Ptr cpte_relation; cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s)) (c_h_t_valid s') pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s)) (c_h_t_valid s') pt_Ptr; cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')); carch_state_relation (ksArchState s) (globals s'); cmachine_state_relation (ksMachineState s) (globals s'); cte_array_relation s (globals s'); tcb_cte_array_relation s (globals s'); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s; cslift s' (ap_Ptr p) = Some ko'; casid_pool_relation (asidpool.ASIDPool pool) ko'\<rbrakk> \<Longrightarrow> \<exists>pool'. cslift s' (ap_Ptr p) = Some pool' \<and> casid_pool_relation (asidpool.ASIDPool pool) pool' proof (prove)
goal:
No subgoals!