theory TcbAcc_R

lemma corres_get_etcb:
  "corres (etcb_relation) (is_etcb_at t) (tcb_at' t)
                    (gets_the (get_etcb t)) (getObject t)" apply (rule corres_no_failI) apply wp apply (clarsimp simp add: get_etcb_def gets_the_def gets_def
                            get_def assert_opt_def bind_def
                            return_def fail_def
                            split: option.splits
                            ) apply (frule in_inv_by_hoareD [OF getObject_inv_tcb]) apply (clarsimp simp add: is_etcb_at_def obj_at'_def projectKO_def
                            projectKO_opt_tcb split_def
                            getObject_def loadObject_default_def in_monad) apply (case_tac bb) apply (simp_all add: fail_def return_def) apply (clarsimp simp add: state_relation_def ekheap_relation_def) apply (drule bspec) apply clarsimp apply blast apply (clarsimp simp add: other_obj_relation_def lookupAround2_known1) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres etcb_relation (is_etcb_at t) (tcb_at' t) (gets_the (get_etcb t)) (getObject t) proof (prove)
goal (2 subgoals):
 1. True \<Longrightarrow> no_fail (tcb_at' t) (getObject t)
 2. \<forall>(s, s')\<in>state_relation. is_etcb_at t s \<and> tcb_at' t s' \<longrightarrow> (\<forall>(r', t')\<in>fst (getObject t s'). \<exists>(r, t)\<in>fst (gets_the (get_etcb t) s). (t, t') \<in> state_relation \<and> etcb_relation r r') proof (prove)
goal (1 subgoal):
 1. \<forall>(s, s')\<in>state_relation. is_etcb_at t s \<and> tcb_at' t s' \<longrightarrow> (\<forall>(r', t')\<in>fst (getObject t s'). \<exists>(r, t)\<in>fst (gets_the (get_etcb t) s). (t, t') \<in> state_relation \<and> etcb_relation r r') proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>(a, b) \<in> state_relation; (aa, ba) \<in> fst (getObject t b); is_etcb_at t a; tcb_at' t b\<rbrakk> \<Longrightarrow> (\<exists>y. ekheap a t = Some y) \<and> (\<forall>x2. ekheap a t = Some x2 \<longrightarrow> (a, ba) \<in> state_relation \<and> etcb_relation x2 aa) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>(a, b) \<in> state_relation; (aa, ba) \<in> fst (getObject t b); is_etcb_at t a; tcb_at' t b; ba = b\<rbrakk> \<Longrightarrow> (\<exists>y. ekheap a t = Some y) \<and> (\<forall>x2. ekheap a t = Some x2 \<longrightarrow> (a, ba) \<in> state_relation \<and> etcb_relation x2 aa) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa bb y. \<lbrakk>(a, b) \<in> state_relation; ksPSpace b t = Some bb; is_aligned t (objBitsKO bb); is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) b); ps_clear t (objBitsKO bb) b; fst ((case case bb of KOTCB x \<Rightarrow> Some x | _ \<Rightarrow> None of None \<Rightarrow> fail | Some x2 \<Rightarrow> return x2) b) = {(aa, b)}; ekheap a t = Some y\<rbrakk> \<Longrightarrow> etcb_relation y aa proof (prove)
goal (8 subgoals):
 1. \<And>a b aa bb y x1. \<lbrakk>(a, b) \<in> state_relation; ksPSpace b t = Some bb; is_aligned t (objBitsKO bb); is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) b); ps_clear t (objBitsKO bb) b; fst ((case case bb of KOTCB x \<Rightarrow> Some x | _ \<Rightarrow> None of None \<Rightarrow> fail | Some x2 \<Rightarrow> return x2) b) = {(aa, b)}; ekheap a t = Some y; bb = KOEndpoint x1\<rbrakk> \<Longrightarrow> etcb_relation y aa
 2. \<And>a b aa bb y x2. \<lbrakk>(a, b) \<in> state_relation; ksPSpace b t = Some bb; is_aligned t (objBitsKO bb); is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) b); ps_clear t (objBitsKO bb) b; fst ((case case bb of KOTCB x \<Rightarrow> Some x | _ \<Rightarrow> None of None \<Rightarrow> fail | Some x2 \<Rightarrow> return x2) b) = {(aa, b)}; ekheap a t = Some y; bb = KONotification x2\<rbrakk> \<Longrightarrow> etcb_relation y aa
 3. \<And>a b aa bb y. \<lbrakk>(a, b) \<in> state_relation; ksPSpace b t = Some bb; is_aligned t (objBitsKO bb); is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) b); ps_clear t (objBitsKO bb) b; fst ((case case bb of KOTCB x \<Rightarrow> Some x | _ \<Rightarrow> None of None \<Rightarrow> fail | Some x2 \<Rightarrow> return x2) b) = {(aa, b)}; ekheap a t = Some y; bb = KOKernelData\<rbrakk> \<Longrightarrow> etcb_relation y aa
 4. \<And>a b aa bb y. \<lbrakk>(a, b) \<in> state_relation; ksPSpace b t = Some bb; is_aligned t (objBitsKO bb); is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) b); ps_clear t (objBitsKO bb) b; fst ((case case bb of KOTCB x \<Rightarrow> Some x | _ \<Rightarrow> None of None \<Rightarrow> fail | Some x2 \<Rightarrow> return x2) b) = {(aa, b)}; ekheap a t = Some y; bb = KOUserData\<rbrakk> \<Longrightarrow> etcb_relation y aa
 5. \<And>a b aa bb y. \<lbrakk>(a, b) \<in> state_relation; ksPSpace b t = Some bb; is_aligned t (objBitsKO bb); is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) b); ps_clear t (objBitsKO bb) b; fst ((case case bb of KOTCB x \<Rightarrow> Some x | _ \<Rightarrow> None of None \<Rightarrow> fail | Some x2 \<Rightarrow> return x2) b) = {(aa, b)}; ekheap a t = Some y; bb = KOUserDataDevice\<rbrakk> \<Longrightarrow> etcb_relation y aa
 6. \<And>a b aa bb y x6. \<lbrakk>(a, b) \<in> state_relation; ksPSpace b t = Some bb; is_aligned t (objBitsKO bb); is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) b); ps_clear t (objBitsKO bb) b; fst ((case case bb of KOTCB x \<Rightarrow> Some x | _ \<Rightarrow> None of None \<Rightarrow> fail | Some x2 \<Rightarrow> return x2) b) = {(aa, b)}; ekheap a t = Some y; bb = KOTCB x6\<rbrakk> \<Longrightarrow> etcb_relation y aa
 7. \<And>a b aa bb y x7. \<lbrakk>(a, b) \<in> state_relation; ksPSpace b t = Some bb; is_aligned t (objBitsKO bb); is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) b); ps_clear t (objBitsKO bb) b; fst ((case case bb of KOTCB x \<Rightarrow> Some x | _ \<Rightarrow> None of None \<Rightarrow> fail | Some x2 \<Rightarrow> return x2) b) = {(aa, b)}; ekheap a t = Some y; bb = KOCTE x7\<rbrakk> \<Longrightarrow> etcb_relation y aa
 8. \<And>a b aa bb y x8. \<lbrakk>(a, b) \<in> state_relation; ksPSpace b t = Some bb; is_aligned t (objBitsKO bb); is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) b); ps_clear t (objBitsKO bb) b; fst ((case case bb of KOTCB x \<Rightarrow> Some x | _ \<Rightarrow> None of None \<Rightarrow> fail | Some x2 \<Rightarrow> return x2) b) = {(aa, b)}; ekheap a t = Some y; bb = KOArch x8\<rbrakk> \<Longrightarrow> etcb_relation y aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa bb y x6. \<lbrakk>(a, b) \<in> state_relation; ksPSpace b t = Some (KOTCB aa); is_aligned t (objBitsKO (KOTCB aa)); is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) b); ps_clear t (objBitsKO (KOTCB aa)) b; x6 = aa; ekheap a t = Some y; bb = KOTCB aa\<rbrakk> \<Longrightarrow> etcb_relation y aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa y. \<lbrakk>ksPSpace b t = Some (KOTCB aa); is_aligned t (objBitsKO (KOTCB aa)); is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) b); ps_clear t (objBitsKO (KOTCB aa)) b; ekheap a t = Some y; pspace_relation (kheap a) (ksPSpace b); \<forall>x\<in>dom (ekheap a). \<exists>tcb'. ksPSpace b x = Some (KOTCB tcb') \<and> etcb_relation (the (ekheap a x)) tcb'; sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); ghost_relation (kheap a) (gsUserPages b) (gsCNodes b); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) a) (cdt a) (ctes_of b); cdt_list_relation (cdt_list a) (cdt a) (ctes_of b); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of b); (arch_state a, ksArchState b) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState b); cur_thread a = ksCurThread b; idle_thread a = ksIdleThread b; machine_state a = ksMachineState b; work_units_completed a = ksWorkUnitsCompleted b; domain_index a = ksDomScheduleIdx b; domain_list a = ksDomSchedule b; cur_domain a = ksCurDomain b; domain_time a = ksDomainTime b\<rbrakk> \<Longrightarrow> etcb_relation y aa proof (prove)
goal (2 subgoals):
 1. \<And>a b aa y. \<lbrakk>ksPSpace b t = Some (KOTCB aa); is_aligned t (objBitsKO (KOTCB aa)); is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) b); ps_clear t (objBitsKO (KOTCB aa)) b; ekheap a t = Some y; pspace_relation (kheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); ghost_relation (kheap a) (gsUserPages b) (gsCNodes b); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) a) (cdt a) (ctes_of b); cdt_list_relation (cdt_list a) (cdt a) (ctes_of b); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of b); (arch_state a, ksArchState b) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState b); cur_thread a = ksCurThread b; idle_thread a = ksIdleThread b; machine_state a = ksMachineState b; work_units_completed a = ksWorkUnitsCompleted b; domain_index a = ksDomScheduleIdx b; domain_list a = ksDomSchedule b; cur_domain a = ksCurDomain b; domain_time a = ksDomainTime b\<rbrakk> \<Longrightarrow> ?x101 a b aa y \<in> dom (ekheap a)
 2. \<And>a b aa y. \<lbrakk>ksPSpace b t = Some (KOTCB aa); is_aligned t (objBitsKO (KOTCB aa)); is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) b); ps_clear t (objBitsKO (KOTCB aa)) b; ekheap a t = Some y; pspace_relation (kheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); ghost_relation (kheap a) (gsUserPages b) (gsCNodes b); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) a) (cdt a) (ctes_of b); cdt_list_relation (cdt_list a) (cdt a) (ctes_of b); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of b); (arch_state a, ksArchState b) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState b); cur_thread a = ksCurThread b; idle_thread a = ksIdleThread b; machine_state a = ksMachineState b; work_units_completed a = ksWorkUnitsCompleted b; domain_index a = ksDomScheduleIdx b; domain_list a = ksDomSchedule b; cur_domain a = ksCurDomain b; domain_time a = ksDomainTime b; \<exists>tcb'. ksPSpace b (?x101 a b aa y) = Some (KOTCB tcb') \<and> etcb_relation (the (ekheap a (?x101 a b aa y))) tcb'\<rbrakk> \<Longrightarrow> etcb_relation y aa proof (prove)
goal (2 subgoals):
 1. \<And>a b aa y. \<lbrakk>ksPSpace b t = Some (KOTCB aa); is_aligned t (objBitsKO (KOTCB aa)); is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) b); ps_clear t (objBitsKO (KOTCB aa)) b; ekheap a t = Some y; pspace_relation (kheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); ghost_relation (kheap a) (gsUserPages b) (gsCNodes b); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) a) (cdt a) (ctes_of b); cdt_list_relation (cdt_list a) (cdt a) (ctes_of b); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of b); (arch_state a, ksArchState b) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState b); cur_thread a = ksCurThread b; idle_thread a = ksIdleThread b; machine_state a = ksMachineState b; work_units_completed a = ksWorkUnitsCompleted b; domain_index a = ksDomScheduleIdx b; domain_list a = ksDomSchedule b; cur_domain a = ksCurDomain b; domain_time a = ksDomainTime b\<rbrakk> \<Longrightarrow> \<exists>ya. ekheap a (?x101 a b aa y) = Some ya
 2. \<And>a b aa y. \<lbrakk>ksPSpace b t = Some (KOTCB aa); is_aligned t (objBitsKO (KOTCB aa)); is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) b); ps_clear t (objBitsKO (KOTCB aa)) b; ekheap a t = Some y; pspace_relation (kheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); ghost_relation (kheap a) (gsUserPages b) (gsCNodes b); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) a) (cdt a) (ctes_of b); cdt_list_relation (cdt_list a) (cdt a) (ctes_of b); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of b); (arch_state a, ksArchState b) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState b); cur_thread a = ksCurThread b; idle_thread a = ksIdleThread b; machine_state a = ksMachineState b; work_units_completed a = ksWorkUnitsCompleted b; domain_index a = ksDomScheduleIdx b; domain_list a = ksDomSchedule b; cur_domain a = ksCurDomain b; domain_time a = ksDomainTime b; \<exists>tcb'. ksPSpace b (?x101 a b aa y) = Some (KOTCB tcb') \<and> etcb_relation (the (ekheap a (?x101 a b aa y))) tcb'\<rbrakk> \<Longrightarrow> etcb_relation y aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa y. \<lbrakk>ksPSpace b t = Some (KOTCB aa); is_aligned t (objBitsKO (KOTCB aa)); is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) b); ps_clear t (objBitsKO (KOTCB aa)) b; ekheap a t = Some y; pspace_relation (kheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); ghost_relation (kheap a) (gsUserPages b) (gsCNodes b); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) a) (cdt a) (ctes_of b); cdt_list_relation (cdt_list a) (cdt a) (ctes_of b); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of b); (arch_state a, ksArchState b) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState b); cur_thread a = ksCurThread b; idle_thread a = ksIdleThread b; machine_state a = ksMachineState b; work_units_completed a = ksWorkUnitsCompleted b; domain_index a = ksDomScheduleIdx b; domain_list a = ksDomSchedule b; cur_domain a = ksCurDomain b; domain_time a = ksDomainTime b; \<exists>tcb'. ksPSpace b t = Some (KOTCB tcb') \<and> etcb_relation (the (ekheap a t)) tcb'\<rbrakk> \<Longrightarrow> etcb_relation y aa proof (prove)
goal:
No subgoals!