theory TcbAcc_R

lemma st_tcb_at_coerce_abstract:
  assumes t: "st_tcb_at' P t c"
  assumes sr: "(a, c) \<in> state_relation"
  shows "st_tcb_at (\<lambda>st. \<exists>st'. thread_state_relation st st' \<and> P st') t a" using assms apply (clarsimp simp: state_relation_def pred_tcb_at'_def obj_at'_def
                        projectKOs objBits_simps) apply (erule(1) pspace_dom_relatedE) apply (erule(1) obj_relation_cutsE, simp_all) apply (clarsimp simp: st_tcb_at_def obj_at_def other_obj_relation_def
                        tcb_relation_def
                 split: Structures_A.kernel_object.split_asm if_split_asm
                        ARM_A.arch_kernel_obj.split_asm)+ apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. st_tcb_at (\<lambda>st. \<exists>st'. thread_state_relation st st' \<and> P st') t a proof (prove)
using this:
st_tcb_at' P t c
(a, c) \<in> state_relation

goal (1 subgoal):
 1. st_tcb_at (\<lambda>st. \<exists>st'. thread_state_relation st st' \<and> P st') t a proof (prove)
goal (1 subgoal):
 1. \<And>obj. \<lbrakk>pspace_relation (kheap a) (ksPSpace c); ksPSpace c t = Some (KOTCB obj); ekheap_relation (ekheap a) (ksPSpace c); is_aligned t tcbBlockSizeBits; sched_act_relation (scheduler_action a) (ksSchedulerAction c); ready_queues_relation (ready_queues a) (ksReadyQueues c); P (tcbState obj); ps_clear t tcbBlockSizeBits c; ghost_relation (kheap a) (gsUserPages c) (gsCNodes c); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) a) (cdt a) (ctes_of c); cdt_list_relation (cdt_list a) (cdt a) (ctes_of c); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of c); (arch_state a, ksArchState c) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState c); cur_thread a = ksCurThread c; idle_thread a = ksIdleThread c; machine_state a = ksMachineState c; work_units_completed a = ksWorkUnitsCompleted c; domain_index a = ksDomScheduleIdx c; domain_list a = ksDomSchedule c; cur_domain a = ksCurDomain c; domain_time a = ksDomainTime c\<rbrakk> \<Longrightarrow> st_tcb_at (\<lambda>st. \<exists>st'. thread_state_relation st st' \<and> P st') t a proof (prove)
goal (1 subgoal):
 1. \<And>obj y ko Pa. \<lbrakk>pspace_relation (kheap a) (ksPSpace c); ekheap_relation (ekheap a) (ksPSpace c); is_aligned t tcbBlockSizeBits; sched_act_relation (scheduler_action a) (ksSchedulerAction c); ready_queues_relation (ready_queues a) (ksReadyQueues c); P (tcbState obj); ps_clear t tcbBlockSizeBits c; ghost_relation (kheap a) (gsUserPages c) (gsCNodes c); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) a) (cdt a) (ctes_of c); cdt_list_relation (cdt_list a) (cdt a) (ctes_of c); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of c); (arch_state a, ksArchState c) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState c); cur_thread a = ksCurThread c; idle_thread a = ksIdleThread c; machine_state a = ksMachineState c; work_units_completed a = ksWorkUnitsCompleted c; domain_index a = ksDomScheduleIdx c; domain_list a = ksDomSchedule c; cur_domain a = ksCurDomain c; domain_time a = ksDomainTime c; kheap a y = Some ko; (t, Pa) \<in> obj_relation_cuts ko y; Pa ko (KOTCB obj)\<rbrakk> \<Longrightarrow> st_tcb_at (\<lambda>st. \<exists>st'. thread_state_relation st st' \<and> P st') t a proof (prove)
goal (2 subgoals):
 1. \<And>obj y ko Pa sz dev n. \<lbrakk>pspace_relation (kheap a) (ksPSpace c); ekheap_relation (ekheap a) (ksPSpace c); is_aligned (y + n * 2 ^ pageBits) tcbBlockSizeBits; sched_act_relation (scheduler_action a) (ksSchedulerAction c); ready_queues_relation (ready_queues a) (ksReadyQueues c); P (tcbState obj); ps_clear (y + n * 2 ^ pageBits) tcbBlockSizeBits c; ghost_relation (kheap a) (gsUserPages c) (gsCNodes c); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) a) (cdt a) (ctes_of c); cdt_list_relation (cdt_list a) (cdt a) (ctes_of c); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of c); (arch_state a, ksArchState c) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState c); cur_thread a = ksCurThread c; idle_thread a = ksIdleThread c; machine_state a = ksMachineState c; work_units_completed a = ksWorkUnitsCompleted c; domain_index a = ksDomScheduleIdx c; domain_list a = ksDomSchedule c; cur_domain a = ksCurDomain c; domain_time a = ksDomainTime c; kheap a y = Some (ArchObj (DataPage dev sz)); Pa (ArchObj (DataPage dev sz)) (if dev then KOUserDataDevice else KOUserData); ko = ArchObj (DataPage dev sz); KOTCB obj = (if dev then KOUserDataDevice else KOUserData); t = y + n * 2 ^ pageBits; n < 2 ^ (pageBitsForSize sz - pageBits)\<rbrakk> \<Longrightarrow> st_tcb_at (\<lambda>st. \<exists>st'. thread_state_relation st st' \<and> P st') (y + n * 2 ^ pageBits) a
 2. \<And>obj y ko Pa. \<lbrakk>pspace_relation (kheap a) (ksPSpace c); ekheap_relation (ekheap a) (ksPSpace c); is_aligned y tcbBlockSizeBits; sched_act_relation (scheduler_action a) (ksSchedulerAction c); ready_queues_relation (ready_queues a) (ksReadyQueues c); P (tcbState obj); ps_clear y tcbBlockSizeBits c; ghost_relation (kheap a) (gsUserPages c) (gsCNodes c); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) a) (cdt a) (ctes_of c); cdt_list_relation (cdt_list a) (cdt a) (ctes_of c); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of c); (arch_state a, ksArchState c) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState c); cur_thread a = ksCurThread c; idle_thread a = ksIdleThread c; machine_state a = ksMachineState c; work_units_completed a = ksWorkUnitsCompleted c; domain_index a = ksDomScheduleIdx c; domain_list a = ksDomSchedule c; cur_domain a = ksCurDomain c; domain_time a = ksDomainTime c; kheap a y = Some ko; Pa ko (KOTCB obj); t = y; other_obj_relation ko (KOTCB obj); is_other_obj_relation_type (a_type ko)\<rbrakk> \<Longrightarrow> st_tcb_at (\<lambda>st. \<exists>st'. thread_state_relation st st' \<and> P st') y a proof (prove)
goal (1 subgoal):
 1. \<And>obj Pa x2. \<lbrakk>is_other_obj_relation_type ATCB; pspace_relation (kheap a) (ksPSpace c); ekheap_relation (ekheap a) (ksPSpace c); is_aligned t tcbBlockSizeBits; sched_act_relation (scheduler_action a) (ksSchedulerAction c); ready_queues_relation (ready_queues a) (ksReadyQueues c); P (tcbState obj); ps_clear t tcbBlockSizeBits c; ghost_relation (kheap a) (gsUserPages c) (gsCNodes c); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) a) (cdt a) (ctes_of c); cdt_list_relation (cdt_list a) (cdt a) (ctes_of c); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of c); (arch_state a, ksArchState c) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState c); cur_thread a = ksCurThread c; idle_thread a = ksIdleThread c; machine_state a = ksMachineState c; work_units_completed a = ksWorkUnitsCompleted c; domain_index a = ksDomScheduleIdx c; domain_list a = ksDomSchedule c; cur_domain a = ksCurDomain c; domain_time a = ksDomainTime c; kheap a t = Some (TCB x2); Pa (TCB x2) (KOTCB obj); tcb_fault_handler x2 = to_bl (tcbFaultHandler obj); tcb_ipc_buffer x2 = tcbIPCBuffer obj; arch_tcb_relation (tcb_arch x2) (tcbArch obj); thread_state_relation (tcb_state x2) (tcbState obj); fault_rel_optionation (tcb_fault x2) (tcbFault obj); cap_relation (tcb_ctable x2) (cteCap (tcbCTable obj)); cap_relation (tcb_vtable x2) (cteCap (tcbVTable obj)); cap_relation (tcb_reply x2) (cteCap (tcbReply obj)); cap_relation (tcb_caller x2) (cteCap (tcbCaller obj)); cap_relation (tcb_ipcframe x2) (cteCap (tcbIPCBufferFrame obj)); tcb_bound_notification x2 = tcbBoundNotification obj; tcb_mcpriority x2 = tcbMCP obj\<rbrakk> \<Longrightarrow> \<exists>st'. thread_state_relation (tcb_state x2) st' \<and> P st' proof (prove)
goal:
No subgoals!