theory SEL4GlobalsSwap

lemma globals_list_valid:
  "globals_list_valid symbol_table t_hrs_' t_hrs_'_update globals_list" apply (rule globals_list_valid_optimisation[OF _ _ globals_list_ok]) apply (simp_all add: globals_list_def globals_list_valid_def
                       global_data_defs
                  del: distinct_prop.simps split del: if_split) apply (simp add: global_data_swappable_def global_data_def) apply (simp_all add: global_data_valid) apply (simp_all add: global_data_valid_def addressed_global_data_def
                   const_global_data_def global_data_ok_def global_data_def
                   to_bytes_p_from_bytes) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. globals_list_valid symbol_table t_hrs_' t_hrs_'_update kernel_all_global_addresses.global_data_list proof (prove)
goal (2 subgoals):
 1. distinct_prop global_data_swappable (filter is_global_data kernel_all_global_addresses.global_data_list)
 2. \<forall>g\<in>set kernel_all_global_addresses.global_data_list. global_data_valid t_hrs_' t_hrs_'_update g proof (prove)
goal (2 subgoals):
 1. distinct_prop global_data_swappable [global_data ''active_irq'' active_irq_' active_irq_'_update, global_data ''armKSASIDTable'' armKSASIDTable_' armKSASIDTable_'_update, global_data ''armKSHWASIDTable'' armKSHWASIDTable_' armKSHWASIDTable_'_update, global_data ''armKSNextASID'' armKSNextASID_' armKSNextASID_'_update, global_data ''avail_reg'' avail_reg_' avail_reg_'_update, global_data ''current_extra_caps'' current_extra_caps_' current_extra_caps_'_update, global_data ''current_fault'' current_fault_' current_fault_'_update, global_data ''current_lookup_fault'' current_lookup_fault_' current_lookup_fault_'_update, global_data ''current_syscall_error'' current_syscall_error_' current_syscall_error_'_update, global_data ''intStateIRQTable'' intStateIRQTable_' intStateIRQTable_'_update, global_data ''isFPUEnabledCached'' isFPUEnabledCached_' isFPUEnabledCached_'_update, global_data ''ksCurDomain'' ksCurDomain_' ksCurDomain_'_update, global_data ''ksCurThread'' ksCurThread_' ksCurThread_'_update, global_data ''ksDomScheduleIdx'' ksDomScheduleIdx_' ksDomScheduleIdx_'_update, global_data ''ksDomainTime'' ksDomainTime_' ksDomainTime_'_update, global_data ''ksIdleThread'' ksIdleThread_' ksIdleThread_'_update, global_data ''ksNumCPUs'' ksNumCPUs_' ksNumCPUs_'_update, global_data ''ksReadyQueues'' ksReadyQueues_' ksReadyQueues_'_update, global_data ''ksReadyQueuesL1Bitmap'' ksReadyQueuesL1Bitmap_' ksReadyQueuesL1Bitmap_'_update, global_data ''ksReadyQueuesL2Bitmap'' ksReadyQueuesL2Bitmap_' ksReadyQueuesL2Bitmap_'_update, global_data ''ksSchedulerAction'' ksSchedulerAction_' ksSchedulerAction_'_update, global_data ''ksWorkUnitsCompleted'' ksWorkUnitsCompleted_' ksWorkUnitsCompleted_'_update, global_data ''ndks_boot'' ndks_boot_' ndks_boot_'_update, global_data ''rootserver'' rootserver_' rootserver_'_update, global_data ''rootserver_mem'' rootserver_mem_' rootserver_mem_'_update, global_data ''tlbLockCount'' tlbLockCount_' tlbLockCount_'_update]
 2. global_data_valid t_hrs_' t_hrs_'_update (global_data ''active_irq'' active_irq_' active_irq_'_update) \<and> global_data_valid t_hrs_' t_hrs_'_update (global_data ''armKSASIDTable'' armKSASIDTable_' armKSASIDTable_'_update) \<and> global_data_valid t_hrs_' t_hrs_'_update (addressed_global_data ''armKSGlobalPD'' TYPE(pde_C[4096])) \<and> global_data_valid t_hrs_' t_hrs_'_update (addressed_global_data ''armKSGlobalPT'' TYPE(pte_C[256])) \<and> global_data_valid t_hrs_' t_hrs_'_update (global_data ''armKSHWASIDTable'' armKSHWASIDTable_' armKSHWASIDTable_'_update) \<and> global_data_valid t_hrs_' t_hrs_'_update (global_data ''armKSNextASID'' armKSNextASID_' armKSNextASID_'_update) \<and> global_data_valid t_hrs_' t_hrs_'_update (addressed_global_data ''arm_vector_table'' TYPE(8 word[1])) \<and> global_data_valid t_hrs_' t_hrs_'_update (addressed_global_data ''avail_p_regs'' TYPE(p_region_C[1])) \<and> global_data_valid t_hrs_' t_hrs_'_update (global_data ''avail_reg'' avail_reg_' avail_reg_'_update) \<and> global_data_valid t_hrs_' t_hrs_'_update (global_data ''current_extra_caps'' current_extra_caps_' current_extra_caps_'_update) \<and> global_data_valid t_hrs_' t_hrs_'_update (global_data ''current_fault'' current_fault_' current_fault_'_update) \<and> global_data_valid t_hrs_' t_hrs_'_update (global_data ''current_lookup_fault'' current_lookup_fault_' current_lookup_fault_'_update) \<and> global_data_valid t_hrs_' t_hrs_'_update (global_data ''current_syscall_error'' current_syscall_error_' current_syscall_error_'_update) \<and> global_data_valid t_hrs_' t_hrs_'_update (const_global_data ''default_resolve_ret_t'' kernel_all_global_addresses.default_resolve_ret_t) \<and> global_data_valid t_hrs_' t_hrs_'_update (const_global_data ''fault_messages'' kernel_all_global_addresses.fault_messages) \<and> global_data_valid t_hrs_' t_hrs_'_update (const_global_data ''frameRegisters'' kernel_all_global_addresses.frameRegisters) \<and> global_data_valid t_hrs_' t_hrs_'_update (const_global_data ''gic_cpuiface'' kernel_all_global_addresses.gic_cpuiface) \<and> global_data_valid t_hrs_' t_hrs_'_update (const_global_data ''gic_dist'' kernel_all_global_addresses.gic_dist) \<and> global_data_valid t_hrs_' t_hrs_'_update (const_global_data ''gpRegisters'' kernel_all_global_addresses.gpRegisters) \<and> global_data_valid t_hrs_' t_hrs_'_update (addressed_global_data ''intStateIRQNode'' TYPE(cte_C[256])) \<and> global_data_valid t_hrs_' t_hrs_'_update (global_data ''intStateIRQTable'' intStateIRQTable_' intStateIRQTable_'_update) \<and> global_data_valid t_hrs_' t_hrs_'_update (const_global_data ''ipiReschedulePending'' kernel_all_global_addresses.ipiReschedulePending) \<and> global_data_valid t_hrs_' t_hrs_'_update (const_global_data ''irqInvalid'' kernel_all_global_addresses.irqInvalid) \<and> global_data_valid t_hrs_' t_hrs_'_update (global_data ''isFPUEnabledCached'' isFPUEnabledCached_' isFPUEnabledCached_'_update) \<and> global_data_valid t_hrs_' t_hrs_'_update (addressed_global_data ''kernel_device_frames'' TYPE(kernel_frame_C[3])) \<and> global_data_valid t_hrs_' t_hrs_'_update (addressed_global_data ''kernel_stack_alloc'' TYPE(8 word[4096][1])) \<and> global_data_valid t_hrs_' t_hrs_'_update (addressed_global_data ''ki_boot_end'' TYPE(8 word[1])) \<and> global_data_valid t_hrs_' t_hrs_'_update (addressed_global_data ''ki_end'' TYPE(8 word[1])) \<and> global_data_valid t_hrs_' t_hrs_'_update (global_data ''ksCurDomain'' ksCurDomain_' ksCurDomain_'_update) \<and> global_data_valid t_hrs_' t_hrs_'_update (global_data ''ksCurThread'' ksCurThread_' ksCurThread_'_update) \<and> global_data_valid t_hrs_' t_hrs_'_update (const_global_data ''ksDomSchedule'' kernel_all_global_addresses.ksDomSchedule) \<and> global_data_valid t_hrs_' t_hrs_'_update (global_data ''ksDomScheduleIdx'' ksDomScheduleIdx_' ksDomScheduleIdx_'_update) \<and> global_data_valid t_hrs_' t_hrs_'_update (const_global_data ''ksDomScheduleLength'' kernel_all_global_addresses.ksDomScheduleLength) \<and> global_data_valid t_hrs_' t_hrs_'_update (global_data ''ksDomainTime'' ksDomainTime_' ksDomainTime_'_update) \<and> global_data_valid t_hrs_' t_hrs_'_update (global_data ''ksIdleThread'' ksIdleThread_' ksIdleThread_'_update) \<and> global_data_valid t_hrs_' t_hrs_'_update (addressed_global_data ''ksIdleThreadTCB'' TYPE(8 word[512][1])) \<and> global_data_valid t_hrs_' t_hrs_'_update (global_data ''ksNumCPUs'' ksNumCPUs_' ksNumCPUs_'_update) \<and> global_data_valid t_hrs_' t_hrs_'_update (global_data ''ksReadyQueues'' ksReadyQueues_' ksReadyQueues_'_update) \<and> global_data_valid t_hrs_' t_hrs_'_update (global_data ''ksReadyQueuesL1Bitmap'' ksReadyQueuesL1Bitmap_' ksReadyQueuesL1Bitmap_'_update) \<and> global_data_valid t_hrs_' t_hrs_'_update (global_data ''ksReadyQueuesL2Bitmap'' ksReadyQueuesL2Bitmap_' ksReadyQueuesL2Bitmap_'_update) \<and> global_data_valid t_hrs_' t_hrs_'_update (global_data ''ksSchedulerAction'' ksSchedulerAction_' ksSchedulerAction_'_update) \<and> global_data_valid t_hrs_' t_hrs_'_update (global_data ''ksWorkUnitsCompleted'' ksWorkUnitsCompleted_' ksWorkUnitsCompleted_'_update) \<and> global_data_valid t_hrs_' t_hrs_'_update (const_global_data ''l2cc'' kernel_all_global_addresses.l2cc) \<and> global_data_valid t_hrs_' t_hrs_'_update (const_global_data ''mode_reserved_region'' kernel_all_global_addresses.mode_reserved_region) \<and> global_data_valid t_hrs_' t_hrs_'_update (const_global_data ''msgRegisters'' kernel_all_global_addresses.msgRegisters) \<and> global_data_valid t_hrs_' t_hrs_'_update (global_data ''ndks_boot'' ndks_boot_' ndks_boot_'_update) \<and> global_data_valid t_hrs_' t_hrs_'_update (const_global_data ''platform_interrupt_t'' kernel_all_global_addresses.platform_interrupt_t) \<and> global_data_valid t_hrs_' t_hrs_'_update (const_global_data ''priv_timer'' kernel_all_global_addresses.priv_timer) \<and> global_data_valid t_hrs_' t_hrs_'_update (addressed_global_data ''reserved'' TYPE(region_C[4])) \<and> global_data_valid t_hrs_' t_hrs_'_update (global_data ''rootserver'' rootserver_' rootserver_'_update) \<and> global_data_valid t_hrs_' t_hrs_'_update (global_data ''rootserver_mem'' rootserver_mem_' rootserver_mem_'_update) \<and> global_data_valid t_hrs_' t_hrs_'_update (const_global_data ''seL4_AsyncEndpointObject'' kernel_all_global_addresses.seL4_AsyncEndpointObject) \<and> global_data_valid t_hrs_' t_hrs_'_update (global_data ''tlbLockCount'' tlbLockCount_' tlbLockCount_'_update) proof (prove)
goal (1 subgoal):
 1. global_data_valid t_hrs_' t_hrs_'_update (global_data ''active_irq'' active_irq_' active_irq_'_update) \<and> global_data_valid t_hrs_' t_hrs_'_update (global_data ''armKSASIDTable'' armKSASIDTable_' armKSASIDTable_'_update) \<and> global_data_valid t_hrs_' t_hrs_'_update (addressed_global_data ''armKSGlobalPD'' TYPE(pde_C[4096])) \<and> global_data_valid t_hrs_' t_hrs_'_update (addressed_global_data ''armKSGlobalPT'' TYPE(pte_C[256])) \<and> global_data_valid t_hrs_' t_hrs_'_update (global_data ''armKSHWASIDTable'' armKSHWASIDTable_' armKSHWASIDTable_'_update) \<and> global_data_valid t_hrs_' t_hrs_'_update (global_data ''armKSNextASID'' armKSNextASID_' armKSNextASID_'_update) \<and> global_data_valid t_hrs_' t_hrs_'_update (addressed_global_data ''arm_vector_table'' TYPE(8 word[1])) \<and> global_data_valid t_hrs_' t_hrs_'_update (addressed_global_data ''avail_p_regs'' TYPE(p_region_C[1])) \<and> global_data_valid t_hrs_' t_hrs_'_update (global_data ''avail_reg'' avail_reg_' avail_reg_'_update) \<and> global_data_valid t_hrs_' t_hrs_'_update (global_data ''current_extra_caps'' current_extra_caps_' current_extra_caps_'_update) \<and> global_data_valid t_hrs_' t_hrs_'_update (global_data ''current_fault'' current_fault_' current_fault_'_update) \<and> global_data_valid t_hrs_' t_hrs_'_update (global_data ''current_lookup_fault'' current_lookup_fault_' current_lookup_fault_'_update) \<and> global_data_valid t_hrs_' t_hrs_'_update (global_data ''current_syscall_error'' current_syscall_error_' current_syscall_error_'_update) \<and> global_data_valid t_hrs_' t_hrs_'_update (const_global_data ''default_resolve_ret_t'' kernel_all_global_addresses.default_resolve_ret_t) \<and> global_data_valid t_hrs_' t_hrs_'_update (const_global_data ''fault_messages'' kernel_all_global_addresses.fault_messages) \<and> global_data_valid t_hrs_' t_hrs_'_update (const_global_data ''frameRegisters'' kernel_all_global_addresses.frameRegisters) \<and> global_data_valid t_hrs_' t_hrs_'_update (const_global_data ''gic_cpuiface'' kernel_all_global_addresses.gic_cpuiface) \<and> global_data_valid t_hrs_' t_hrs_'_update (const_global_data ''gic_dist'' kernel_all_global_addresses.gic_dist) \<and> global_data_valid t_hrs_' t_hrs_'_update (const_global_data ''gpRegisters'' kernel_all_global_addresses.gpRegisters) \<and> global_data_valid t_hrs_' t_hrs_'_update (addressed_global_data ''intStateIRQNode'' TYPE(cte_C[256])) \<and> global_data_valid t_hrs_' t_hrs_'_update (global_data ''intStateIRQTable'' intStateIRQTable_' intStateIRQTable_'_update) \<and> global_data_valid t_hrs_' t_hrs_'_update (const_global_data ''ipiReschedulePending'' kernel_all_global_addresses.ipiReschedulePending) \<and> global_data_valid t_hrs_' t_hrs_'_update (const_global_data ''irqInvalid'' kernel_all_global_addresses.irqInvalid) \<and> global_data_valid t_hrs_' t_hrs_'_update (global_data ''isFPUEnabledCached'' isFPUEnabledCached_' isFPUEnabledCached_'_update) \<and> global_data_valid t_hrs_' t_hrs_'_update (addressed_global_data ''kernel_device_frames'' TYPE(kernel_frame_C[3])) \<and> global_data_valid t_hrs_' t_hrs_'_update (addressed_global_data ''kernel_stack_alloc'' TYPE(8 word[4096][1])) \<and> global_data_valid t_hrs_' t_hrs_'_update (addressed_global_data ''ki_boot_end'' TYPE(8 word[1])) \<and> global_data_valid t_hrs_' t_hrs_'_update (addressed_global_data ''ki_end'' TYPE(8 word[1])) \<and> global_data_valid t_hrs_' t_hrs_'_update (global_data ''ksCurDomain'' ksCurDomain_' ksCurDomain_'_update) \<and> global_data_valid t_hrs_' t_hrs_'_update (global_data ''ksCurThread'' ksCurThread_' ksCurThread_'_update) \<and> global_data_valid t_hrs_' t_hrs_'_update (const_global_data ''ksDomSchedule'' kernel_all_global_addresses.ksDomSchedule) \<and> global_data_valid t_hrs_' t_hrs_'_update (global_data ''ksDomScheduleIdx'' ksDomScheduleIdx_' ksDomScheduleIdx_'_update) \<and> global_data_valid t_hrs_' t_hrs_'_update (const_global_data ''ksDomScheduleLength'' kernel_all_global_addresses.ksDomScheduleLength) \<and> global_data_valid t_hrs_' t_hrs_'_update (global_data ''ksDomainTime'' ksDomainTime_' ksDomainTime_'_update) \<and> global_data_valid t_hrs_' t_hrs_'_update (global_data ''ksIdleThread'' ksIdleThread_' ksIdleThread_'_update) \<and> global_data_valid t_hrs_' t_hrs_'_update (addressed_global_data ''ksIdleThreadTCB'' TYPE(8 word[512][1])) \<and> global_data_valid t_hrs_' t_hrs_'_update (global_data ''ksNumCPUs'' ksNumCPUs_' ksNumCPUs_'_update) \<and> global_data_valid t_hrs_' t_hrs_'_update (global_data ''ksReadyQueues'' ksReadyQueues_' ksReadyQueues_'_update) \<and> global_data_valid t_hrs_' t_hrs_'_update (global_data ''ksReadyQueuesL1Bitmap'' ksReadyQueuesL1Bitmap_' ksReadyQueuesL1Bitmap_'_update) \<and> global_data_valid t_hrs_' t_hrs_'_update (global_data ''ksReadyQueuesL2Bitmap'' ksReadyQueuesL2Bitmap_' ksReadyQueuesL2Bitmap_'_update) \<and> global_data_valid t_hrs_' t_hrs_'_update (global_data ''ksSchedulerAction'' ksSchedulerAction_' ksSchedulerAction_'_update) \<and> global_data_valid t_hrs_' t_hrs_'_update (global_data ''ksWorkUnitsCompleted'' ksWorkUnitsCompleted_' ksWorkUnitsCompleted_'_update) \<and> global_data_valid t_hrs_' t_hrs_'_update (const_global_data ''l2cc'' kernel_all_global_addresses.l2cc) \<and> global_data_valid t_hrs_' t_hrs_'_update (const_global_data ''mode_reserved_region'' kernel_all_global_addresses.mode_reserved_region) \<and> global_data_valid t_hrs_' t_hrs_'_update (const_global_data ''msgRegisters'' kernel_all_global_addresses.msgRegisters) \<and> global_data_valid t_hrs_' t_hrs_'_update (global_data ''ndks_boot'' ndks_boot_' ndks_boot_'_update) \<and> global_data_valid t_hrs_' t_hrs_'_update (const_global_data ''platform_interrupt_t'' kernel_all_global_addresses.platform_interrupt_t) \<and> global_data_valid t_hrs_' t_hrs_'_update (const_global_data ''priv_timer'' kernel_all_global_addresses.priv_timer) \<and> global_data_valid t_hrs_' t_hrs_'_update (addressed_global_data ''reserved'' TYPE(region_C[4])) \<and> global_data_valid t_hrs_' t_hrs_'_update (global_data ''rootserver'' rootserver_' rootserver_'_update) \<and> global_data_valid t_hrs_' t_hrs_'_update (global_data ''rootserver_mem'' rootserver_mem_' rootserver_mem_'_update) \<and> global_data_valid t_hrs_' t_hrs_'_update (const_global_data ''seL4_AsyncEndpointObject'' kernel_all_global_addresses.seL4_AsyncEndpointObject) \<and> global_data_valid t_hrs_' t_hrs_'_update (global_data ''tlbLockCount'' tlbLockCount_' tlbLockCount_'_update) proof (prove)
goal (1 subgoal):
 1. global_data_valid t_hrs_' t_hrs_'_update (addressed_global_data ''armKSGlobalPD'' TYPE(pde_C[4096])) \<and> global_data_valid t_hrs_' t_hrs_'_update (addressed_global_data ''armKSGlobalPT'' TYPE(pte_C[256])) \<and> global_data_valid t_hrs_' t_hrs_'_update (addressed_global_data ''arm_vector_table'' TYPE(8 word[1])) \<and> global_data_valid t_hrs_' t_hrs_'_update (addressed_global_data ''avail_p_regs'' TYPE(p_region_C[1])) \<and> global_data_valid t_hrs_' t_hrs_'_update (const_global_data ''default_resolve_ret_t'' kernel_all_global_addresses.default_resolve_ret_t) \<and> global_data_valid t_hrs_' t_hrs_'_update (const_global_data ''fault_messages'' kernel_all_global_addresses.fault_messages) \<and> global_data_valid t_hrs_' t_hrs_'_update (const_global_data ''frameRegisters'' kernel_all_global_addresses.frameRegisters) \<and> global_data_valid t_hrs_' t_hrs_'_update (const_global_data ''gic_cpuiface'' kernel_all_global_addresses.gic_cpuiface) \<and> global_data_valid t_hrs_' t_hrs_'_update (const_global_data ''gic_dist'' kernel_all_global_addresses.gic_dist) \<and> global_data_valid t_hrs_' t_hrs_'_update (const_global_data ''gpRegisters'' kernel_all_global_addresses.gpRegisters) \<and> global_data_valid t_hrs_' t_hrs_'_update (addressed_global_data ''intStateIRQNode'' TYPE(cte_C[256])) \<and> global_data_valid t_hrs_' t_hrs_'_update (const_global_data ''ipiReschedulePending'' kernel_all_global_addresses.ipiReschedulePending) \<and> global_data_valid t_hrs_' t_hrs_'_update (const_global_data ''irqInvalid'' kernel_all_global_addresses.irqInvalid) \<and> global_data_valid t_hrs_' t_hrs_'_update (addressed_global_data ''kernel_device_frames'' TYPE(kernel_frame_C[3])) \<and> global_data_valid t_hrs_' t_hrs_'_update (addressed_global_data ''kernel_stack_alloc'' TYPE(8 word[4096][1])) \<and> global_data_valid t_hrs_' t_hrs_'_update (addressed_global_data ''ki_boot_end'' TYPE(8 word[1])) \<and> global_data_valid t_hrs_' t_hrs_'_update (addressed_global_data ''ki_end'' TYPE(8 word[1])) \<and> global_data_valid t_hrs_' t_hrs_'_update (const_global_data ''ksDomSchedule'' kernel_all_global_addresses.ksDomSchedule) \<and> global_data_valid t_hrs_' t_hrs_'_update (const_global_data ''ksDomScheduleLength'' kernel_all_global_addresses.ksDomScheduleLength) \<and> global_data_valid t_hrs_' t_hrs_'_update (addressed_global_data ''ksIdleThreadTCB'' TYPE(8 word[512][1])) \<and> global_data_valid t_hrs_' t_hrs_'_update (const_global_data ''l2cc'' kernel_all_global_addresses.l2cc) \<and> global_data_valid t_hrs_' t_hrs_'_update (const_global_data ''mode_reserved_region'' kernel_all_global_addresses.mode_reserved_region) \<and> global_data_valid t_hrs_' t_hrs_'_update (const_global_data ''msgRegisters'' kernel_all_global_addresses.msgRegisters) \<and> global_data_valid t_hrs_' t_hrs_'_update (const_global_data ''platform_interrupt_t'' kernel_all_global_addresses.platform_interrupt_t) \<and> global_data_valid t_hrs_' t_hrs_'_update (const_global_data ''priv_timer'' kernel_all_global_addresses.priv_timer) \<and> global_data_valid t_hrs_' t_hrs_'_update (addressed_global_data ''reserved'' TYPE(region_C[4])) \<and> global_data_valid t_hrs_' t_hrs_'_update (const_global_data ''seL4_AsyncEndpointObject'' kernel_all_global_addresses.seL4_AsyncEndpointObject) proof (prove)
goal:
No subgoals!