theory Finalise_R

lemma thread_gets_the_all_corres:
  shows      "corres (\<lambda>(tcb, etcb) tcb'. tcb_relation tcb tcb' \<and> etcb_relation etcb tcb')
                (tcb_at t and is_etcb_at t) (tcb_at' t)
                (thread_gets_the_all t) (getObject t)" apply (rule corres_no_failI) apply wp apply (clarsimp simp add: gets_def get_def return_def bind_def get_tcb_def thread_gets_the_all_def threadGet_def ethread_get_def gets_the_def assert_opt_def get_etcb_def is_etcb_at_def tcb_at_def liftM_def split: option.splits Structures_A.kernel_object.splits) apply (frule in_inv_by_hoareD [OF getObject_inv_tcb]) apply (clarsimp simp add: obj_at_def is_tcb obj_at'_def projectKO_def
                            projectKO_opt_tcb split_def
                            getObject_def loadObject_default_def in_monad) apply (case_tac ko) apply (simp_all add: fail_def return_def) apply (clarsimp simp add: state_relation_def pspace_relation_def ekheap_relation_def) apply (drule bspec) apply clarsimp apply blast apply (drule bspec, erule domI) apply (clarsimp simp add: other_obj_relation_def
                            lookupAround2_known1) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (\<lambda>(tcb, etcb) tcb'. tcb_relation tcb tcb' \<and> etcb_relation etcb tcb') (tcb_at t and is_etcb_at t) (tcb_at' t) (thread_gets_the_all 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. (tcb_at t and is_etcb_at t) s \<and> tcb_at' t s' \<longrightarrow> (\<forall>(r', t')\<in>fst (getObject t s'). \<exists>(r, t)\<in>fst (thread_gets_the_all t s). (t, t') \<in> state_relation \<and> (case r of (tcb, etcb) \<Rightarrow> \<lambda>tcb'. tcb_relation tcb tcb' \<and> etcb_relation etcb tcb') r') proof (prove)
goal (1 subgoal):
 1. \<forall>(s, s')\<in>state_relation. (tcb_at t and is_etcb_at t) s \<and> tcb_at' t s' \<longrightarrow> (\<forall>(r', t')\<in>fst (getObject t s'). \<exists>(r, t)\<in>fst (thread_gets_the_all t s). (t, t') \<in> state_relation \<and> (case r of (tcb, etcb) \<Rightarrow> \<lambda>tcb'. tcb_relation tcb tcb' \<and> etcb_relation etcb tcb') r') proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba tcb y. \<lbrakk>tcb_at' t b; ekheap a t = Some y; (a, b) \<in> state_relation; (aa, ba) \<in> fst (getObject t b); kheap a t = Some (TCB tcb)\<rbrakk> \<Longrightarrow> (a, ba) \<in> state_relation \<and> tcb_relation tcb aa \<and> etcb_relation y aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba tcb y. \<lbrakk>tcb_at' t b; ekheap a t = Some y; (a, b) \<in> state_relation; (aa, ba) \<in> fst (getObject t b); kheap a t = Some (TCB tcb); ba = b\<rbrakk> \<Longrightarrow> (a, ba) \<in> state_relation \<and> tcb_relation tcb aa \<and> etcb_relation y aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa tcb y ko. \<lbrakk>ekheap a t = Some y; (a, b) \<in> state_relation; kheap a t = Some (TCB tcb); ksPSpace b t = Some ko; is_aligned t (objBitsKO ko); ps_clear t (objBitsKO ko) b; fst ((case case ko of KOTCB x \<Rightarrow> Some x | _ \<Rightarrow> None of None \<Rightarrow> fail | Some x2 \<Rightarrow> return x2) b) = {(aa, b)}; is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) b)\<rbrakk> \<Longrightarrow> tcb_relation tcb aa \<and> etcb_relation y aa proof (prove)
goal (8 subgoals):
 1. \<And>a b aa tcb y ko x1. \<lbrakk>ekheap a t = Some y; (a, b) \<in> state_relation; kheap a t = Some (TCB tcb); ksPSpace b t = Some ko; is_aligned t (objBitsKO ko); ps_clear t (objBitsKO ko) b; fst ((case case ko of KOTCB x \<Rightarrow> Some x | _ \<Rightarrow> None of None \<Rightarrow> fail | Some x2 \<Rightarrow> return x2) b) = {(aa, b)}; is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) b); ko = KOEndpoint x1\<rbrakk> \<Longrightarrow> tcb_relation tcb aa \<and> etcb_relation y aa
 2. \<And>a b aa tcb y ko x2. \<lbrakk>ekheap a t = Some y; (a, b) \<in> state_relation; kheap a t = Some (TCB tcb); ksPSpace b t = Some ko; is_aligned t (objBitsKO ko); ps_clear t (objBitsKO ko) b; fst ((case case ko of KOTCB x \<Rightarrow> Some x | _ \<Rightarrow> None of None \<Rightarrow> fail | Some x2 \<Rightarrow> return x2) b) = {(aa, b)}; is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) b); ko = KONotification x2\<rbrakk> \<Longrightarrow> tcb_relation tcb aa \<and> etcb_relation y aa
 3. \<And>a b aa tcb y ko. \<lbrakk>ekheap a t = Some y; (a, b) \<in> state_relation; kheap a t = Some (TCB tcb); ksPSpace b t = Some ko; is_aligned t (objBitsKO ko); ps_clear t (objBitsKO ko) b; fst ((case case ko of KOTCB x \<Rightarrow> Some x | _ \<Rightarrow> None of None \<Rightarrow> fail | Some x2 \<Rightarrow> return x2) b) = {(aa, b)}; is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) b); ko = KOKernelData\<rbrakk> \<Longrightarrow> tcb_relation tcb aa \<and> etcb_relation y aa
 4. \<And>a b aa tcb y ko. \<lbrakk>ekheap a t = Some y; (a, b) \<in> state_relation; kheap a t = Some (TCB tcb); ksPSpace b t = Some ko; is_aligned t (objBitsKO ko); ps_clear t (objBitsKO ko) b; fst ((case case ko of KOTCB x \<Rightarrow> Some x | _ \<Rightarrow> None of None \<Rightarrow> fail | Some x2 \<Rightarrow> return x2) b) = {(aa, b)}; is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) b); ko = KOUserData\<rbrakk> \<Longrightarrow> tcb_relation tcb aa \<and> etcb_relation y aa
 5. \<And>a b aa tcb y ko. \<lbrakk>ekheap a t = Some y; (a, b) \<in> state_relation; kheap a t = Some (TCB tcb); ksPSpace b t = Some ko; is_aligned t (objBitsKO ko); ps_clear t (objBitsKO ko) b; fst ((case case ko of KOTCB x \<Rightarrow> Some x | _ \<Rightarrow> None of None \<Rightarrow> fail | Some x2 \<Rightarrow> return x2) b) = {(aa, b)}; is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) b); ko = KOUserDataDevice\<rbrakk> \<Longrightarrow> tcb_relation tcb aa \<and> etcb_relation y aa
 6. \<And>a b aa tcb y ko x6. \<lbrakk>ekheap a t = Some y; (a, b) \<in> state_relation; kheap a t = Some (TCB tcb); ksPSpace b t = Some ko; is_aligned t (objBitsKO ko); ps_clear t (objBitsKO ko) b; fst ((case case ko of KOTCB x \<Rightarrow> Some x | _ \<Rightarrow> None of None \<Rightarrow> fail | Some x2 \<Rightarrow> return x2) b) = {(aa, b)}; is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) b); ko = KOTCB x6\<rbrakk> \<Longrightarrow> tcb_relation tcb aa \<and> etcb_relation y aa
 7. \<And>a b aa tcb y ko x7. \<lbrakk>ekheap a t = Some y; (a, b) \<in> state_relation; kheap a t = Some (TCB tcb); ksPSpace b t = Some ko; is_aligned t (objBitsKO ko); ps_clear t (objBitsKO ko) b; fst ((case case ko of KOTCB x \<Rightarrow> Some x | _ \<Rightarrow> None of None \<Rightarrow> fail | Some x2 \<Rightarrow> return x2) b) = {(aa, b)}; is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) b); ko = KOCTE x7\<rbrakk> \<Longrightarrow> tcb_relation tcb aa \<and> etcb_relation y aa
 8. \<And>a b aa tcb y ko x8. \<lbrakk>ekheap a t = Some y; (a, b) \<in> state_relation; kheap a t = Some (TCB tcb); ksPSpace b t = Some ko; is_aligned t (objBitsKO ko); ps_clear t (objBitsKO ko) b; fst ((case case ko of KOTCB x \<Rightarrow> Some x | _ \<Rightarrow> None of None \<Rightarrow> fail | Some x2 \<Rightarrow> return x2) b) = {(aa, b)}; is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) b); ko = KOArch x8\<rbrakk> \<Longrightarrow> tcb_relation tcb aa \<and> etcb_relation y aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa tcb y ko x6. \<lbrakk>ekheap a t = Some y; (a, b) \<in> state_relation; kheap a t = Some (TCB tcb); ksPSpace b t = Some (KOTCB aa); is_aligned t (objBitsKO (KOTCB aa)); ps_clear t (objBitsKO (KOTCB aa)) b; x6 = aa; is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) b); ko = KOTCB aa\<rbrakk> \<Longrightarrow> tcb_relation tcb aa \<and> etcb_relation y aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa tcb y. \<lbrakk>ekheap a t = Some y; kheap a t = Some (TCB tcb); ksPSpace b t = Some (KOTCB aa); is_aligned t (objBitsKO (KOTCB aa)); ps_clear t (objBitsKO (KOTCB aa)) b; is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) b); pspace_dom (kheap a) = dom (ksPSpace b); \<forall>x\<in>dom (kheap a). \<forall>xa\<in>obj_relation_cuts (the (kheap a x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap a x)) (the (ksPSpace b y)); \<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> tcb_relation tcb aa \<and> etcb_relation y aa proof (prove)
goal (2 subgoals):
 1. \<And>a b aa tcb y. \<lbrakk>ekheap a t = Some y; kheap a t = Some (TCB tcb); ksPSpace b t = Some (KOTCB aa); is_aligned t (objBitsKO (KOTCB aa)); ps_clear t (objBitsKO (KOTCB aa)) b; is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) b); pspace_dom (kheap a) = dom (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> ?x148 a b aa tcb y \<in> dom (kheap a)
 2. \<And>a b aa tcb y. \<lbrakk>ekheap a t = Some y; kheap a t = Some (TCB tcb); ksPSpace b t = Some (KOTCB aa); is_aligned t (objBitsKO (KOTCB aa)); ps_clear t (objBitsKO (KOTCB aa)) b; is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) b); pspace_dom (kheap a) = dom (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; \<forall>x\<in>obj_relation_cuts (the (kheap a (?x148 a b aa tcb y))) (?x148 a b aa tcb y). case x of (ya, P) \<Rightarrow> P (the (kheap a (?x148 a b aa tcb y))) (the (ksPSpace b ya))\<rbrakk> \<Longrightarrow> tcb_relation tcb aa \<and> etcb_relation y aa proof (prove)
goal (2 subgoals):
 1. \<And>a b aa tcb y. \<lbrakk>ekheap a t = Some y; kheap a t = Some (TCB tcb); ksPSpace b t = Some (KOTCB aa); is_aligned t (objBitsKO (KOTCB aa)); ps_clear t (objBitsKO (KOTCB aa)) b; is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) b); pspace_dom (kheap a) = dom (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> \<exists>ya. kheap a (?x148 a b aa tcb y) = Some ya
 2. \<And>a b aa tcb y. \<lbrakk>ekheap a t = Some y; kheap a t = Some (TCB tcb); ksPSpace b t = Some (KOTCB aa); is_aligned t (objBitsKO (KOTCB aa)); ps_clear t (objBitsKO (KOTCB aa)) b; is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) b); pspace_dom (kheap a) = dom (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; \<forall>x\<in>obj_relation_cuts (the (kheap a (?x148 a b aa tcb y))) (?x148 a b aa tcb y). case x of (ya, P) \<Rightarrow> P (the (kheap a (?x148 a b aa tcb y))) (the (ksPSpace b ya))\<rbrakk> \<Longrightarrow> tcb_relation tcb aa \<and> etcb_relation y aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa tcb y. \<lbrakk>ekheap a t = Some y; kheap a t = Some (TCB tcb); ksPSpace b t = Some (KOTCB aa); is_aligned t (objBitsKO (KOTCB aa)); ps_clear t (objBitsKO (KOTCB aa)) b; is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) b); pspace_dom (kheap a) = dom (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; \<forall>x\<in>obj_relation_cuts (the (kheap a t)) t. case x of (y, P) \<Rightarrow> P (the (kheap a t)) (the (ksPSpace b y))\<rbrakk> \<Longrightarrow> tcb_relation tcb aa \<and> etcb_relation y aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa tcb y. \<lbrakk>ekheap a t = Some y; kheap a t = Some (TCB tcb); ksPSpace b t = Some (KOTCB aa); is_aligned t (objBitsKO (KOTCB aa)); ps_clear t (objBitsKO (KOTCB aa)) b; is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) b); pspace_dom (kheap a) = dom (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; \<forall>x\<in>obj_relation_cuts (the (kheap a t)) t. case x of (y, P) \<Rightarrow> P (the (kheap a t)) (the (ksPSpace b y)); \<exists>tcb'. ksPSpace b t = Some (KOTCB tcb') \<and> etcb_relation (the (ekheap a t)) tcb'\<rbrakk> \<Longrightarrow> tcb_relation tcb aa \<and> etcb_relation y aa proof (prove)
goal:
No subgoals!