theory ADT_C

lemma (in kernel)  mk_gsUntypedZeroRanges_correct:
  assumes valid: "valid_state' as"
  assumes cstate_rel: "cstate_relation as cs"
  shows "mk_gsUntypedZeroRanges cs = gsUntypedZeroRanges as" using assms apply (clarsimp simp: valid_state'_def untyped_ranges_zero_inv_def
                        mk_gsUntypedZeroRanges_def cteCaps_of_def) apply (subst cstate_to_pspace_H_correct[where c=cs], simp_all) apply (clarsimp simp: cstate_relation_def Let_def) apply (subst cstate_to_machine_H_correct, assumption, simp_all) apply (clarsimp simp: cpspace_relation_def)+ apply (clarsimp simp: observable_memory_def valid_pspace'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mk_gsUntypedZeroRanges cs = gsUntypedZeroRanges as proof (prove)
using this:
valid_state' as
cstate_relation as cs

goal (1 subgoal):
 1. mk_gsUntypedZeroRanges cs = gsUntypedZeroRanges as proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cstate_relation as cs; valid_pspace' as; sch_act_wf (ksSchedulerAction as) as; Invariants_H.valid_queues as; sym_refs (state_refs_of' as); if_live_then_nonz_cap' as; if_unsafe_then_cap' as; valid_idle' as; valid_global_refs' as; valid_arch_state' as; valid_irq_node' (irq_node' as) as; valid_irq_handlers' as; valid_irq_states' as; valid_machine_state' as; irqs_masked' as; valid_queues' as; ct_not_inQ as; ct_idle_or_in_cur_domain' as; valid_pde_mappings' as; pspace_domain_valid as; ksCurDomain as \<le> maxDomain; kernel_state.ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (kernel_state.ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; kernel_state.ksDomSchedule as = kernel_state.ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx as < length (kernel_state.ksDomSchedule (KernelInit_H.newKernelState undefined)); gsUntypedZeroRanges as = ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> ctes_of as))\<rbrakk> \<Longrightarrow> ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> map_to_ctes (cstate_to_pspace_H cs))) = ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> ctes_of as)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cstate_relation as cs; valid_pspace' as; sch_act_wf (ksSchedulerAction as) as; Invariants_H.valid_queues as; sym_refs (state_refs_of' as); if_live_then_nonz_cap' as; if_unsafe_then_cap' as; valid_idle' as; valid_global_refs' as; valid_arch_state' as; valid_irq_node' (irq_node' as) as; valid_irq_handlers' as; valid_irq_states' as; valid_machine_state' as; irqs_masked' as; valid_queues' as; ct_not_inQ as; ct_idle_or_in_cur_domain' as; valid_pde_mappings' as; pspace_domain_valid as; ksCurDomain as \<le> maxDomain; kernel_state.ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (kernel_state.ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; kernel_state.ksDomSchedule as = kernel_state.ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx as < length (kernel_state.ksDomSchedule (KernelInit_H.newKernelState undefined)); gsUntypedZeroRanges as = ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> ctes_of as))\<rbrakk> \<Longrightarrow> cpspace_relation (ksPSpace as) (underlying_memory (cstate_to_machine_H cs)) (t_hrs_' cs) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_pspace' as; sch_act_wf (ksSchedulerAction as) as; Invariants_H.valid_queues as; sym_refs (state_refs_of' as); if_live_then_nonz_cap' as; if_unsafe_then_cap' as; valid_idle' as; valid_global_refs' as; valid_arch_state' as; valid_irq_node' (irq_node' as) as; valid_irq_handlers' as; valid_irq_states' as; valid_machine_state' as; irqs_masked' as; valid_queues' as; ct_not_inQ as; ct_idle_or_in_cur_domain' as; valid_pde_mappings' as; pspace_domain_valid as; ksCurDomain as \<le> maxDomain; kernel_state.ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (kernel_state.ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; kernel_state.ksDomSchedule as = kernel_state.ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx as < length (kernel_state.ksDomSchedule (KernelInit_H.newKernelState undefined)); gsUntypedZeroRanges as = ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> ctes_of as)); cpspace_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs); cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as); zero_ranges_are_zero (ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> ctes_of as))) (t_hrs_' cs); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as); ksCurThread_' cs = tcb_ptr_to_ctcb_ptr (ksCurThread as); ksIdleThread_' cs = tcb_ptr_to_ctcb_ptr (ksIdleThread as); cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs); cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs); carch_state_relation (ksArchState as) cs; cmachine_state_relation (ksMachineState as) cs; cte_array_relation as cs; tcb_cte_array_relation as cs; apsnd fst (ghost'state_' cs) = (gsUserPages as, gsCNodes as); ghost_size_rel (ghost'state_' cs) (gsMaxObjectSize as); ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' cs)); - 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 (KernelInit_H.newKernelState undefined)) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' cs = word_of_nat (ksDomScheduleIdx as); ksCurDomain_' cs = UCAST(8 \<rightarrow> 32) (ksCurDomain as); ksDomainTime_' cs = ksDomainTime as\<rbrakk> \<Longrightarrow> cpspace_relation (ksPSpace as) (underlying_memory (cstate_to_machine_H cs)) (t_hrs_' cs) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_pspace' as; sch_act_wf (ksSchedulerAction as) as; Invariants_H.valid_queues as; sym_refs (state_refs_of' as); if_live_then_nonz_cap' as; if_unsafe_then_cap' as; valid_idle' as; valid_global_refs' as; valid_arch_state' as; valid_irq_node' (irq_node' as) as; valid_irq_handlers' as; valid_irq_states' as; valid_machine_state' as; irqs_masked' as; valid_queues' as; ct_not_inQ as; ct_idle_or_in_cur_domain' as; valid_pde_mappings' as; pspace_domain_valid as; ksCurDomain as \<le> maxDomain; kernel_state.ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (kernel_state.ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; kernel_state.ksDomSchedule as = kernel_state.ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx as < length (kernel_state.ksDomSchedule (KernelInit_H.newKernelState undefined)); gsUntypedZeroRanges as = ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> ctes_of as)); cpspace_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs); cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as); zero_ranges_are_zero (ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> ctes_of as))) (t_hrs_' cs); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as); ksCurThread_' cs = tcb_ptr_to_ctcb_ptr (ksCurThread as); ksIdleThread_' cs = tcb_ptr_to_ctcb_ptr (ksIdleThread as); cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs); cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs); carch_state_relation (ksArchState as) cs; cmachine_state_relation (ksMachineState as) cs; cte_array_relation as cs; tcb_cte_array_relation as cs; apsnd fst (ghost'state_' cs) = (gsUserPages as, gsCNodes as); ghost_size_rel (ghost'state_' cs) (gsMaxObjectSize as); ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' cs)); - 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 (KernelInit_H.newKernelState undefined)) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' cs = word_of_nat (ksDomScheduleIdx as); ksCurDomain_' cs = UCAST(8 \<rightarrow> 32) (ksCurDomain as); ksDomainTime_' cs = ksDomainTime as\<rbrakk> \<Longrightarrow> cpspace_user_data_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs)
 2. \<lbrakk>valid_pspace' as; sch_act_wf (ksSchedulerAction as) as; Invariants_H.valid_queues as; sym_refs (state_refs_of' as); if_live_then_nonz_cap' as; if_unsafe_then_cap' as; valid_idle' as; valid_global_refs' as; valid_arch_state' as; valid_irq_node' (irq_node' as) as; valid_irq_handlers' as; valid_irq_states' as; valid_machine_state' as; irqs_masked' as; valid_queues' as; ct_not_inQ as; ct_idle_or_in_cur_domain' as; valid_pde_mappings' as; pspace_domain_valid as; ksCurDomain as \<le> maxDomain; kernel_state.ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (kernel_state.ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; kernel_state.ksDomSchedule as = kernel_state.ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx as < length (kernel_state.ksDomSchedule (KernelInit_H.newKernelState undefined)); gsUntypedZeroRanges as = ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> ctes_of as)); cpspace_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs); cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as); zero_ranges_are_zero (ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> ctes_of as))) (t_hrs_' cs); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as); ksCurThread_' cs = tcb_ptr_to_ctcb_ptr (ksCurThread as); ksIdleThread_' cs = tcb_ptr_to_ctcb_ptr (ksIdleThread as); cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs); cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs); carch_state_relation (ksArchState as) cs; cmachine_state_relation (ksMachineState as) cs; cte_array_relation as cs; tcb_cte_array_relation as cs; apsnd fst (ghost'state_' cs) = (gsUserPages as, gsCNodes as); ghost_size_rel (ghost'state_' cs) (gsMaxObjectSize as); ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' cs)); - 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 (KernelInit_H.newKernelState undefined)) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' cs = word_of_nat (ksDomScheduleIdx as); ksCurDomain_' cs = UCAST(8 \<rightarrow> 32) (ksCurDomain as); ksDomainTime_' cs = ksDomainTime as\<rbrakk> \<Longrightarrow> pspace_distinct' as
 3. \<lbrakk>valid_pspace' as; sch_act_wf (ksSchedulerAction as) as; Invariants_H.valid_queues as; sym_refs (state_refs_of' as); if_live_then_nonz_cap' as; if_unsafe_then_cap' as; valid_idle' as; valid_global_refs' as; valid_arch_state' as; valid_irq_node' (irq_node' as) as; valid_irq_handlers' as; valid_irq_states' as; valid_machine_state' as; irqs_masked' as; valid_queues' as; ct_not_inQ as; ct_idle_or_in_cur_domain' as; valid_pde_mappings' as; pspace_domain_valid as; ksCurDomain as \<le> maxDomain; kernel_state.ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (kernel_state.ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; kernel_state.ksDomSchedule as = kernel_state.ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx as < length (kernel_state.ksDomSchedule (KernelInit_H.newKernelState undefined)); gsUntypedZeroRanges as = ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> ctes_of as)); cpspace_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs); cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as); zero_ranges_are_zero (ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> ctes_of as))) (t_hrs_' cs); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as); ksCurThread_' cs = tcb_ptr_to_ctcb_ptr (ksCurThread as); ksIdleThread_' cs = tcb_ptr_to_ctcb_ptr (ksIdleThread as); cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs); cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs); carch_state_relation (ksArchState as) cs; cmachine_state_relation (ksMachineState as) cs; cte_array_relation as cs; tcb_cte_array_relation as cs; apsnd fst (ghost'state_' cs) = (gsUserPages as, gsCNodes as); ghost_size_rel (ghost'state_' cs) (gsMaxObjectSize as); ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' cs)); - 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 (KernelInit_H.newKernelState undefined)) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' cs = word_of_nat (ksDomScheduleIdx as); ksCurDomain_' cs = UCAST(8 \<rightarrow> 32) (ksCurDomain as); ksDomainTime_' cs = ksDomainTime as\<rbrakk> \<Longrightarrow> cpspace_relation (ksPSpace as) (underlying_memory (observable_memory (ksMachineState as) (user_mem' as))) (t_hrs_' cs) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_pspace' as; sch_act_wf (ksSchedulerAction as) as; Invariants_H.valid_queues as; sym_refs (state_refs_of' as); if_live_then_nonz_cap' as; if_unsafe_then_cap' as; valid_idle' as; valid_global_refs' as; valid_arch_state' as; valid_irq_node' (irq_node' as) as; valid_irq_handlers' as; valid_irq_states' as; valid_machine_state' as; irqs_masked' as; valid_queues' as; ct_not_inQ as; ct_idle_or_in_cur_domain' as; valid_pde_mappings' as; pspace_domain_valid as; ksCurDomain as \<le> maxDomain; kernel_state.ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (kernel_state.ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; kernel_state.ksDomSchedule as = kernel_state.ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx as < length (kernel_state.ksDomSchedule (KernelInit_H.newKernelState undefined)); gsUntypedZeroRanges as = ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> ctes_of as)); cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as); zero_ranges_are_zero (ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> ctes_of as))) (t_hrs_' cs); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as); ksCurThread_' cs = tcb_ptr_to_ctcb_ptr (ksCurThread as); ksIdleThread_' cs = tcb_ptr_to_ctcb_ptr (ksIdleThread as); cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs); cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs); carch_state_relation (ksArchState as) cs; cmachine_state_relation (ksMachineState as) cs; cte_array_relation as cs; tcb_cte_array_relation as cs; apsnd fst (ghost'state_' cs) = (gsUserPages as, gsCNodes as); ghost_size_rel (ghost'state_' cs) (gsMaxObjectSize as); ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' cs)); - 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 (KernelInit_H.newKernelState undefined)) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' cs = word_of_nat (ksDomScheduleIdx as); ksCurDomain_' cs = UCAST(8 \<rightarrow> 32) (ksCurDomain as); ksDomainTime_' cs = ksDomainTime as; cmap_relation (ctes_of as) (clift (t_hrs_' cs)) cte_Ptr ccte_relation; cpspace_tcb_relation (ksPSpace as) (t_hrs_' cs); cmap_relation (map_to_eps (ksPSpace as)) (clift (t_hrs_' cs)) ep_Ptr (cendpoint_relation (clift (t_hrs_' cs))); cmap_relation (map_to_ntfns (ksPSpace as)) (clift (t_hrs_' cs)) ntfn_Ptr (cnotification_relation (clift (t_hrs_' cs))); cmap_relation (map_to_pdes (ksPSpace as)) (clift (t_hrs_' cs)) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace as)) (clift (t_hrs_' cs)) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace as)) (clift (t_hrs_' cs)) ap_Ptr casid_pool_relation; cpspace_user_data_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs); cpspace_device_data_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs); cpspace_pde_array_relation (ksPSpace as) (t_hrs_' cs); cpspace_pte_array_relation (ksPSpace as) (t_hrs_' cs)\<rbrakk> \<Longrightarrow> cpspace_user_data_relation (ksPSpace as) (underlying_memory (observable_memory (ksMachineState as) (user_mem' as))) (t_hrs_' cs) \<and> cpspace_device_data_relation (ksPSpace as) (underlying_memory (observable_memory (ksMachineState as) (user_mem' as))) (t_hrs_' cs) proof (prove)
goal:
No subgoals!