theory SR_lemmas_C

lemma cstate_relation_only_t_hrs:
  "\<lbrakk> t_hrs_' s = t_hrs_' t;
  ksReadyQueues_' s = ksReadyQueues_' t;
  ksReadyQueuesL1Bitmap_' s = ksReadyQueuesL1Bitmap_' t;
  ksReadyQueuesL2Bitmap_' s = ksReadyQueuesL2Bitmap_' t;
  ksSchedulerAction_' s = ksSchedulerAction_' t;
  ksCurThread_' s = ksCurThread_' t;
  ksIdleThread_' s = ksIdleThread_' t;
  ksWorkUnitsCompleted_' s = ksWorkUnitsCompleted_' t;
  intStateIRQNode_' s = intStateIRQNode_' t;
  intStateIRQTable_' s = intStateIRQTable_' t;
  armKSHWASIDTable_' s = armKSHWASIDTable_' t;
  armKSASIDTable_' s = armKSASIDTable_' t;
  armKSNextASID_' s = armKSNextASID_' t;
  phantom_machine_state_' s = phantom_machine_state_' t;
  ghost'state_' s = ghost'state_' t;
  ksDomScheduleIdx_' s = ksDomScheduleIdx_' t;
  ksCurDomain_' s = ksCurDomain_' t;
  ksDomainTime_' s = ksDomainTime_' t
  \<rbrakk>
  \<Longrightarrow> cstate_relation a s = cstate_relation a t" unfolding cstate_relation_def by (clarsimp simp add: Let_def carch_state_relation_def cmachine_state_relation_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t_hrs_' s = t_hrs_' t; ksReadyQueues_' s = ksReadyQueues_' t; ksReadyQueuesL1Bitmap_' s = ksReadyQueuesL1Bitmap_' t; ksReadyQueuesL2Bitmap_' s = ksReadyQueuesL2Bitmap_' t; ksSchedulerAction_' s = ksSchedulerAction_' t; ksCurThread_' s = ksCurThread_' t; ksIdleThread_' s = ksIdleThread_' t; ksWorkUnitsCompleted_' s = ksWorkUnitsCompleted_' t; intStateIRQNode_' s = intStateIRQNode_' t; intStateIRQTable_' s = intStateIRQTable_' t; armKSHWASIDTable_' s = armKSHWASIDTable_' t; armKSASIDTable_' s = armKSASIDTable_' t; armKSNextASID_' s = armKSNextASID_' t; phantom_machine_state_' s = phantom_machine_state_' t; ghost'state_' s = ghost'state_' t; ksDomScheduleIdx_' s = ksDomScheduleIdx_' t; ksCurDomain_' s = ksCurDomain_' t; ksDomainTime_' s = ksDomainTime_' t\<rbrakk> \<Longrightarrow> cstate_relation a s = cstate_relation a t proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t_hrs_' s = t_hrs_' t; ksReadyQueues_' s = ksReadyQueues_' t; ksReadyQueuesL1Bitmap_' s = ksReadyQueuesL1Bitmap_' t; ksReadyQueuesL2Bitmap_' s = ksReadyQueuesL2Bitmap_' t; ksSchedulerAction_' s = ksSchedulerAction_' t; ksCurThread_' s = ksCurThread_' t; ksIdleThread_' s = ksIdleThread_' t; ksWorkUnitsCompleted_' s = ksWorkUnitsCompleted_' t; intStateIRQNode_' s = intStateIRQNode_' t; intStateIRQTable_' s = intStateIRQTable_' t; armKSHWASIDTable_' s = armKSHWASIDTable_' t; armKSASIDTable_' s = armKSASIDTable_' t; armKSNextASID_' s = armKSNextASID_' t; phantom_machine_state_' s = phantom_machine_state_' t; ghost'state_' s = ghost'state_' t; ksDomScheduleIdx_' s = ksDomScheduleIdx_' t; ksCurDomain_' s = ksCurDomain_' t; ksDomainTime_' s = ksDomainTime_' t\<rbrakk> \<Longrightarrow> (let cheap = t_hrs_' s in cpspace_relation (ksPSpace a) (underlying_memory (ksMachineState a)) cheap \<and> cready_queues_relation (clift cheap) (ksReadyQueues_' s) (ksReadyQueues a) \<and> zero_ranges_are_zero (gsUntypedZeroRanges a) cheap \<and> cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' s) (ksReadyQueuesL1Bitmap a) \<and> cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' s) (ksReadyQueuesL2Bitmap a) \<and> ksCurThread_' s = tcb_ptr_to_ctcb_ptr (ksCurThread a) \<and> ksIdleThread_' s = tcb_ptr_to_ctcb_ptr (ksIdleThread a) \<and> cinterrupt_relation (ksInterruptState a) intStateIRQNode_array_Ptr (intStateIRQTable_' s) \<and> cscheduler_action_relation (ksSchedulerAction a) (ksSchedulerAction_' s) \<and> carch_state_relation (ksArchState a) s \<and> cmachine_state_relation (ksMachineState a) s \<and> cte_array_relation a s \<and> tcb_cte_array_relation a s \<and> apsnd fst (ghost'state_' s) = (gsUserPages a, gsCNodes a) \<and> ghost_size_rel (ghost'state_' s) (gsMaxObjectSize a) \<and> ksWorkUnitsCompleted_' s = ksWorkUnitsCompleted a \<and> hrs_htd (t_hrs_' s) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr \<and> ptr_span intStateIRQNode_array_Ptr \<subseteq> kernel_data_refs \<and> hrs_htd (t_hrs_' s) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr \<and> ptr_span armKSGlobalPD_Ptr \<subseteq> kernel_data_refs \<and> htd_safe domain (hrs_htd (t_hrs_' s)) \<and> - domain \<subseteq> kernel_data_refs \<and> globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list \<and> cdom_schedule_relation (kernel_state.ksDomSchedule a) kernel_all_global_addresses.ksDomSchedule \<and> ksDomScheduleIdx_' s = word_of_nat (ksDomScheduleIdx a) \<and> ksCurDomain_' s = UCAST(8 \<rightarrow> 32) (ksCurDomain a) \<and> ksDomainTime_' s = ksDomainTime a) = (let cheap = t_hrs_' t in cpspace_relation (ksPSpace a) (underlying_memory (ksMachineState a)) cheap \<and> cready_queues_relation (clift cheap) (ksReadyQueues_' t) (ksReadyQueues a) \<and> zero_ranges_are_zero (gsUntypedZeroRanges a) cheap \<and> cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' t) (ksReadyQueuesL1Bitmap a) \<and> cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' t) (ksReadyQueuesL2Bitmap a) \<and> ksCurThread_' t = tcb_ptr_to_ctcb_ptr (ksCurThread a) \<and> ksIdleThread_' t = tcb_ptr_to_ctcb_ptr (ksIdleThread a) \<and> cinterrupt_relation (ksInterruptState a) intStateIRQNode_array_Ptr (intStateIRQTable_' t) \<and> cscheduler_action_relation (ksSchedulerAction a) (ksSchedulerAction_' t) \<and> carch_state_relation (ksArchState a) t \<and> cmachine_state_relation (ksMachineState a) t \<and> cte_array_relation a t \<and> tcb_cte_array_relation a t \<and> apsnd fst (ghost'state_' t) = (gsUserPages a, gsCNodes a) \<and> ghost_size_rel (ghost'state_' t) (gsMaxObjectSize a) \<and> ksWorkUnitsCompleted_' t = ksWorkUnitsCompleted a \<and> hrs_htd (t_hrs_' t) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr \<and> ptr_span intStateIRQNode_array_Ptr \<subseteq> kernel_data_refs \<and> hrs_htd (t_hrs_' t) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr \<and> ptr_span armKSGlobalPD_Ptr \<subseteq> kernel_data_refs \<and> htd_safe domain (hrs_htd (t_hrs_' t)) \<and> - domain \<subseteq> kernel_data_refs \<and> globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list \<and> cdom_schedule_relation (kernel_state.ksDomSchedule a) kernel_all_global_addresses.ksDomSchedule \<and> ksDomScheduleIdx_' t = word_of_nat (ksDomScheduleIdx a) \<and> ksCurDomain_' t = UCAST(8 \<rightarrow> 32) (ksCurDomain a) \<and> ksDomainTime_' t = ksDomainTime a)