theory SEL4GlobalsSwap

lemma ghost'state_update_globals_swap:
  "ghost'state_' (gswap gs) = ghost'state_' gs
    \<and> gswap (ghost'state_'_update f gs) = ghost'state_'_update f (gswap gs)" apply (rule globals_swap_ex_swap) apply (simp only: globals_list_def global_data_defs list.simps ball_simps
                     is_global_data_simps simp_thms) apply (simp add: global_data_def) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ghost'state_' (gswap gs) = ghost'state_' gs \<and> gswap (ghost'state_'_update f gs) = ghost'state_'_update f (gswap gs) proof (prove)
goal (2 subgoals):
 1. \<forall>x\<in>set kernel_all_global_addresses.global_data_list. is_global_data x \<longrightarrow> (case x of GlobalData nm sz tg g' s' \<Rightarrow> (\<forall>v v' gs. s' v (ghost'state_'_update f gs) = ghost'state_'_update f (s' v gs)) \<and> (\<forall>v gs. g' (ghost'state_'_update f gs) = g' gs) \<and> (\<forall>v gs. ghost'state_' (s' v gs) = ghost'state_' gs))
 2. (\<forall>v v' gs. t_hrs_'_update v (ghost'state_'_update f gs) = ghost'state_'_update f (t_hrs_'_update v gs)) \<and> (\<forall>v gs. ghost'state_' (t_hrs_'_update v gs) = ghost'state_' gs) \<and> (\<forall>v gs. t_hrs_' (ghost'state_'_update f gs) = t_hrs_' gs) proof (prove)
goal (2 subgoals):
 1. (case global_data ''active_irq'' active_irq_' active_irq_'_update of GlobalData nm sz tg g' s' \<Rightarrow> (\<forall>v gs. s' v (ghost'state_'_update f gs) = ghost'state_'_update f (s' v gs)) \<and> (\<forall>gs. g' (ghost'state_'_update f gs) = g' gs) \<and> (\<forall>v gs. ghost'state_' (s' v gs) = ghost'state_' gs)) \<and> (case global_data ''armKSASIDTable'' armKSASIDTable_' armKSASIDTable_'_update of GlobalData nm sz tg g' s' \<Rightarrow> (\<forall>v gs. s' v (ghost'state_'_update f gs) = ghost'state_'_update f (s' v gs)) \<and> (\<forall>gs. g' (ghost'state_'_update f gs) = g' gs) \<and> (\<forall>v gs. ghost'state_' (s' v gs) = ghost'state_' gs)) \<and> (case global_data ''armKSHWASIDTable'' armKSHWASIDTable_' armKSHWASIDTable_'_update of GlobalData nm sz tg g' s' \<Rightarrow> (\<forall>v gs. s' v (ghost'state_'_update f gs) = ghost'state_'_update f (s' v gs)) \<and> (\<forall>gs. g' (ghost'state_'_update f gs) = g' gs) \<and> (\<forall>v gs. ghost'state_' (s' v gs) = ghost'state_' gs)) \<and> (case global_data ''armKSNextASID'' armKSNextASID_' armKSNextASID_'_update of GlobalData nm sz tg g' s' \<Rightarrow> (\<forall>v gs. s' v (ghost'state_'_update f gs) = ghost'state_'_update f (s' v gs)) \<and> (\<forall>gs. g' (ghost'state_'_update f gs) = g' gs) \<and> (\<forall>v gs. ghost'state_' (s' v gs) = ghost'state_' gs)) \<and> (case global_data ''avail_reg'' avail_reg_' avail_reg_'_update of GlobalData nm sz tg g' s' \<Rightarrow> (\<forall>v gs. s' v (ghost'state_'_update f gs) = ghost'state_'_update f (s' v gs)) \<and> (\<forall>gs. g' (ghost'state_'_update f gs) = g' gs) \<and> (\<forall>v gs. ghost'state_' (s' v gs) = ghost'state_' gs)) \<and> (case global_data ''current_extra_caps'' current_extra_caps_' current_extra_caps_'_update of GlobalData nm sz tg g' s' \<Rightarrow> (\<forall>v gs. s' v (ghost'state_'_update f gs) = ghost'state_'_update f (s' v gs)) \<and> (\<forall>gs. g' (ghost'state_'_update f gs) = g' gs) \<and> (\<forall>v gs. ghost'state_' (s' v gs) = ghost'state_' gs)) \<and> (case global_data ''current_fault'' current_fault_' current_fault_'_update of GlobalData nm sz tg g' s' \<Rightarrow> (\<forall>v gs. s' v (ghost'state_'_update f gs) = ghost'state_'_update f (s' v gs)) \<and> (\<forall>gs. g' (ghost'state_'_update f gs) = g' gs) \<and> (\<forall>v gs. ghost'state_' (s' v gs) = ghost'state_' gs)) \<and> (case global_data ''current_lookup_fault'' current_lookup_fault_' current_lookup_fault_'_update of GlobalData nm sz tg g' s' \<Rightarrow> (\<forall>v gs. s' v (ghost'state_'_update f gs) = ghost'state_'_update f (s' v gs)) \<and> (\<forall>gs. g' (ghost'state_'_update f gs) = g' gs) \<and> (\<forall>v gs. ghost'state_' (s' v gs) = ghost'state_' gs)) \<and> (case global_data ''current_syscall_error'' current_syscall_error_' current_syscall_error_'_update of GlobalData nm sz tg g' s' \<Rightarrow> (\<forall>v gs. s' v (ghost'state_'_update f gs) = ghost'state_'_update f (s' v gs)) \<and> (\<forall>gs. g' (ghost'state_'_update f gs) = g' gs) \<and> (\<forall>v gs. ghost'state_' (s' v gs) = ghost'state_' gs)) \<and> (case global_data ''intStateIRQTable'' intStateIRQTable_' intStateIRQTable_'_update of GlobalData nm sz tg g' s' \<Rightarrow> (\<forall>v gs. s' v (ghost'state_'_update f gs) = ghost'state_'_update f (s' v gs)) \<and> (\<forall>gs. g' (ghost'state_'_update f gs) = g' gs) \<and> (\<forall>v gs. ghost'state_' (s' v gs) = ghost'state_' gs)) \<and> (case global_data ''isFPUEnabledCached'' isFPUEnabledCached_' isFPUEnabledCached_'_update of GlobalData nm sz tg g' s' \<Rightarrow> (\<forall>v gs. s' v (ghost'state_'_update f gs) = ghost'state_'_update f (s' v gs)) \<and> (\<forall>gs. g' (ghost'state_'_update f gs) = g' gs) \<and> (\<forall>v gs. ghost'state_' (s' v gs) = ghost'state_' gs)) \<and> (case global_data ''ksCurDomain'' ksCurDomain_' ksCurDomain_'_update of GlobalData nm sz tg g' s' \<Rightarrow> (\<forall>v gs. s' v (ghost'state_'_update f gs) = ghost'state_'_update f (s' v gs)) \<and> (\<forall>gs. g' (ghost'state_'_update f gs) = g' gs) \<and> (\<forall>v gs. ghost'state_' (s' v gs) = ghost'state_' gs)) \<and> (case global_data ''ksCurThread'' ksCurThread_' ksCurThread_'_update of GlobalData nm sz tg g' s' \<Rightarrow> (\<forall>v gs. s' v (ghost'state_'_update f gs) = ghost'state_'_update f (s' v gs)) \<and> (\<forall>gs. g' (ghost'state_'_update f gs) = g' gs) \<and> (\<forall>v gs. ghost'state_' (s' v gs) = ghost'state_' gs)) \<and> (case global_data ''ksDomScheduleIdx'' ksDomScheduleIdx_' ksDomScheduleIdx_'_update of GlobalData nm sz tg g' s' \<Rightarrow> (\<forall>v gs. s' v (ghost'state_'_update f gs) = ghost'state_'_update f (s' v gs)) \<and> (\<forall>gs. g' (ghost'state_'_update f gs) = g' gs) \<and> (\<forall>v gs. ghost'state_' (s' v gs) = ghost'state_' gs)) \<and> (case global_data ''ksDomainTime'' ksDomainTime_' ksDomainTime_'_update of GlobalData nm sz tg g' s' \<Rightarrow> (\<forall>v gs. s' v (ghost'state_'_update f gs) = ghost'state_'_update f (s' v gs)) \<and> (\<forall>gs. g' (ghost'state_'_update f gs) = g' gs) \<and> (\<forall>v gs. ghost'state_' (s' v gs) = ghost'state_' gs)) \<and> (case global_data ''ksIdleThread'' ksIdleThread_' ksIdleThread_'_update of GlobalData nm sz tg g' s' \<Rightarrow> (\<forall>v gs. s' v (ghost'state_'_update f gs) = ghost'state_'_update f (s' v gs)) \<and> (\<forall>gs. g' (ghost'state_'_update f gs) = g' gs) \<and> (\<forall>v gs. ghost'state_' (s' v gs) = ghost'state_' gs)) \<and> (case global_data ''ksNumCPUs'' ksNumCPUs_' ksNumCPUs_'_update of GlobalData nm sz tg g' s' \<Rightarrow> (\<forall>v gs. s' v (ghost'state_'_update f gs) = ghost'state_'_update f (s' v gs)) \<and> (\<forall>gs. g' (ghost'state_'_update f gs) = g' gs) \<and> (\<forall>v gs. ghost'state_' (s' v gs) = ghost'state_' gs)) \<and> (case global_data ''ksReadyQueues'' ksReadyQueues_' ksReadyQueues_'_update of GlobalData nm sz tg g' s' \<Rightarrow> (\<forall>v gs. s' v (ghost'state_'_update f gs) = ghost'state_'_update f (s' v gs)) \<and> (\<forall>gs. g' (ghost'state_'_update f gs) = g' gs) \<and> (\<forall>v gs. ghost'state_' (s' v gs) = ghost'state_' gs)) \<and> (case global_data ''ksReadyQueuesL1Bitmap'' ksReadyQueuesL1Bitmap_' ksReadyQueuesL1Bitmap_'_update of GlobalData nm sz tg g' s' \<Rightarrow> (\<forall>v gs. s' v (ghost'state_'_update f gs) = ghost'state_'_update f (s' v gs)) \<and> (\<forall>gs. g' (ghost'state_'_update f gs) = g' gs) \<and> (\<forall>v gs. ghost'state_' (s' v gs) = ghost'state_' gs)) \<and> (case global_data ''ksReadyQueuesL2Bitmap'' ksReadyQueuesL2Bitmap_' ksReadyQueuesL2Bitmap_'_update of GlobalData nm sz tg g' s' \<Rightarrow> (\<forall>v gs. s' v (ghost'state_'_update f gs) = ghost'state_'_update f (s' v gs)) \<and> (\<forall>gs. g' (ghost'state_'_update f gs) = g' gs) \<and> (\<forall>v gs. ghost'state_' (s' v gs) = ghost'state_' gs)) \<and> (case global_data ''ksSchedulerAction'' ksSchedulerAction_' ksSchedulerAction_'_update of GlobalData nm sz tg g' s' \<Rightarrow> (\<forall>v gs. s' v (ghost'state_'_update f gs) = ghost'state_'_update f (s' v gs)) \<and> (\<forall>gs. g' (ghost'state_'_update f gs) = g' gs) \<and> (\<forall>v gs. ghost'state_' (s' v gs) = ghost'state_' gs)) \<and> (case global_data ''ksWorkUnitsCompleted'' ksWorkUnitsCompleted_' ksWorkUnitsCompleted_'_update of GlobalData nm sz tg g' s' \<Rightarrow> (\<forall>v gs. s' v (ghost'state_'_update f gs) = ghost'state_'_update f (s' v gs)) \<and> (\<forall>gs. g' (ghost'state_'_update f gs) = g' gs) \<and> (\<forall>v gs. ghost'state_' (s' v gs) = ghost'state_' gs)) \<and> (case global_data ''ndks_boot'' ndks_boot_' ndks_boot_'_update of GlobalData nm sz tg g' s' \<Rightarrow> (\<forall>v gs. s' v (ghost'state_'_update f gs) = ghost'state_'_update f (s' v gs)) \<and> (\<forall>gs. g' (ghost'state_'_update f gs) = g' gs) \<and> (\<forall>v gs. ghost'state_' (s' v gs) = ghost'state_' gs)) \<and> (case global_data ''rootserver'' rootserver_' rootserver_'_update of GlobalData nm sz tg g' s' \<Rightarrow> (\<forall>v gs. s' v (ghost'state_'_update f gs) = ghost'state_'_update f (s' v gs)) \<and> (\<forall>gs. g' (ghost'state_'_update f gs) = g' gs) \<and> (\<forall>v gs. ghost'state_' (s' v gs) = ghost'state_' gs)) \<and> (case global_data ''rootserver_mem'' rootserver_mem_' rootserver_mem_'_update of GlobalData nm sz tg g' s' \<Rightarrow> (\<forall>v gs. s' v (ghost'state_'_update f gs) = ghost'state_'_update f (s' v gs)) \<and> (\<forall>gs. g' (ghost'state_'_update f gs) = g' gs) \<and> (\<forall>v gs. ghost'state_' (s' v gs) = ghost'state_' gs)) \<and> (case global_data ''tlbLockCount'' tlbLockCount_' tlbLockCount_'_update of GlobalData nm sz tg g' s' \<Rightarrow> (\<forall>v gs. s' v (ghost'state_'_update f gs) = ghost'state_'_update f (s' v gs)) \<and> (\<forall>gs. g' (ghost'state_'_update f gs) = g' gs) \<and> (\<forall>v gs. ghost'state_' (s' v gs) = ghost'state_' gs))
 2. (\<forall>v v' gs. t_hrs_'_update v (ghost'state_'_update f gs) = ghost'state_'_update f (t_hrs_'_update v gs)) \<and> (\<forall>v gs. ghost'state_' (t_hrs_'_update v gs) = ghost'state_' gs) \<and> (\<forall>v gs. t_hrs_' (ghost'state_'_update f gs) = t_hrs_' gs) proof (prove)
goal (1 subgoal):
 1. (\<forall>v v' gs. t_hrs_'_update v (ghost'state_'_update f gs) = ghost'state_'_update f (t_hrs_'_update v gs)) \<and> (\<forall>v gs. ghost'state_' (t_hrs_'_update v gs) = ghost'state_' gs) \<and> (\<forall>v gs. t_hrs_' (ghost'state_'_update f gs) = t_hrs_' gs) proof (prove)
goal:
No subgoals!