theory KHeap_R

lemma corres_get_tcb [corres]:
  "corres (tcb_relation \<circ> the) (tcb_at t) (tcb_at' t) (gets (get_tcb 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) 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 koa) apply (simp_all add: fail_def return_def) apply (case_tac bb) apply (simp_all add: fail_def return_def) apply (clarsimp simp add: state_relation_def pspace_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 (tcb_relation \<circ> the) (tcb_at t) (tcb_at' t) (gets (get_tcb 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 s \<and> tcb_at' t s' \<longrightarrow> (\<forall>(r', t')\<in>fst (getObject t s'). \<exists>(r, t)\<in>fst (gets (get_tcb t) s). (t, t') \<in> state_relation \<and> (tcb_relation \<circ> the) r r') proof (prove)
goal (1 subgoal):
 1. \<forall>(s, s')\<in>state_relation. tcb_at t s \<and> tcb_at' t s' \<longrightarrow> (\<forall>(r', t')\<in>fst (getObject t s'). \<exists>(r, t)\<in>fst (gets (get_tcb t) s). (t, t') \<in> state_relation \<and> (tcb_relation \<circ> the) 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); tcb_at t a; tcb_at' t b\<rbrakk> \<Longrightarrow> (a, ba) \<in> state_relation \<and> tcb_relation (the (case kheap a t of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | Some _ \<Rightarrow> None)) 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); tcb_at t a; tcb_at' t b; ba = b\<rbrakk> \<Longrightarrow> (a, ba) \<in> state_relation \<and> tcb_relation (the (case kheap a t of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | Some _ \<Rightarrow> None)) aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa bb koa s'' tcb obj. \<lbrakk>(a, b) \<in> state_relation; fst (lookupAround2 t (ksPSpace b)) = Some (t, bb); kheap a t = Some (TCB tcb); ksPSpace b t = Some koa; (aa, s'') \<in> fst ((case case bb of KOTCB x \<Rightarrow> Some x | _ \<Rightarrow> None of None \<Rightarrow> fail | Some x2 \<Rightarrow> return x2) b); is_aligned t (objBitsKO koa); is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) s''); ps_clear t (objBitsKO koa) b; fst ((case case koa of KOTCB x \<Rightarrow> Some x | _ \<Rightarrow> None of None \<Rightarrow> fail | Some x2 \<Rightarrow> return x2) b) = {(obj, b)}\<rbrakk> \<Longrightarrow> tcb_relation tcb aa proof (prove)
goal (8 subgoals):
 1. \<And>a b aa bb koa s'' tcb obj x1. \<lbrakk>(a, b) \<in> state_relation; fst (lookupAround2 t (ksPSpace b)) = Some (t, bb); kheap a t = Some (TCB tcb); ksPSpace b t = Some koa; (aa, s'') \<in> fst ((case case bb of KOTCB x \<Rightarrow> Some x | _ \<Rightarrow> None of None \<Rightarrow> fail | Some x2 \<Rightarrow> return x2) b); is_aligned t (objBitsKO koa); is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) s''); ps_clear t (objBitsKO koa) b; fst ((case case koa of KOTCB x \<Rightarrow> Some x | _ \<Rightarrow> None of None \<Rightarrow> fail | Some x2 \<Rightarrow> return x2) b) = {(obj, b)}; koa = KOEndpoint x1\<rbrakk> \<Longrightarrow> tcb_relation tcb aa
 2. \<And>a b aa bb koa s'' tcb obj x2. \<lbrakk>(a, b) \<in> state_relation; fst (lookupAround2 t (ksPSpace b)) = Some (t, bb); kheap a t = Some (TCB tcb); ksPSpace b t = Some koa; (aa, s'') \<in> fst ((case case bb of KOTCB x \<Rightarrow> Some x | _ \<Rightarrow> None of None \<Rightarrow> fail | Some x2 \<Rightarrow> return x2) b); is_aligned t (objBitsKO koa); is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) s''); ps_clear t (objBitsKO koa) b; fst ((case case koa of KOTCB x \<Rightarrow> Some x | _ \<Rightarrow> None of None \<Rightarrow> fail | Some x2 \<Rightarrow> return x2) b) = {(obj, b)}; koa = KONotification x2\<rbrakk> \<Longrightarrow> tcb_relation tcb aa
 3. \<And>a b aa bb koa s'' tcb obj. \<lbrakk>(a, b) \<in> state_relation; fst (lookupAround2 t (ksPSpace b)) = Some (t, bb); kheap a t = Some (TCB tcb); ksPSpace b t = Some koa; (aa, s'') \<in> fst ((case case bb of KOTCB x \<Rightarrow> Some x | _ \<Rightarrow> None of None \<Rightarrow> fail | Some x2 \<Rightarrow> return x2) b); is_aligned t (objBitsKO koa); is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) s''); ps_clear t (objBitsKO koa) b; fst ((case case koa of KOTCB x \<Rightarrow> Some x | _ \<Rightarrow> None of None \<Rightarrow> fail | Some x2 \<Rightarrow> return x2) b) = {(obj, b)}; koa = KOKernelData\<rbrakk> \<Longrightarrow> tcb_relation tcb aa
 4. \<And>a b aa bb koa s'' tcb obj. \<lbrakk>(a, b) \<in> state_relation; fst (lookupAround2 t (ksPSpace b)) = Some (t, bb); kheap a t = Some (TCB tcb); ksPSpace b t = Some koa; (aa, s'') \<in> fst ((case case bb of KOTCB x \<Rightarrow> Some x | _ \<Rightarrow> None of None \<Rightarrow> fail | Some x2 \<Rightarrow> return x2) b); is_aligned t (objBitsKO koa); is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) s''); ps_clear t (objBitsKO koa) b; fst ((case case koa of KOTCB x \<Rightarrow> Some x | _ \<Rightarrow> None of None \<Rightarrow> fail | Some x2 \<Rightarrow> return x2) b) = {(obj, b)}; koa = KOUserData\<rbrakk> \<Longrightarrow> tcb_relation tcb aa
 5. \<And>a b aa bb koa s'' tcb obj. \<lbrakk>(a, b) \<in> state_relation; fst (lookupAround2 t (ksPSpace b)) = Some (t, bb); kheap a t = Some (TCB tcb); ksPSpace b t = Some koa; (aa, s'') \<in> fst ((case case bb of KOTCB x \<Rightarrow> Some x | _ \<Rightarrow> None of None \<Rightarrow> fail | Some x2 \<Rightarrow> return x2) b); is_aligned t (objBitsKO koa); is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) s''); ps_clear t (objBitsKO koa) b; fst ((case case koa of KOTCB x \<Rightarrow> Some x | _ \<Rightarrow> None of None \<Rightarrow> fail | Some x2 \<Rightarrow> return x2) b) = {(obj, b)}; koa = KOUserDataDevice\<rbrakk> \<Longrightarrow> tcb_relation tcb aa
 6. \<And>a b aa bb koa s'' tcb obj x6. \<lbrakk>(a, b) \<in> state_relation; fst (lookupAround2 t (ksPSpace b)) = Some (t, bb); kheap a t = Some (TCB tcb); ksPSpace b t = Some koa; (aa, s'') \<in> fst ((case case bb of KOTCB x \<Rightarrow> Some x | _ \<Rightarrow> None of None \<Rightarrow> fail | Some x2 \<Rightarrow> return x2) b); is_aligned t (objBitsKO koa); is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) s''); ps_clear t (objBitsKO koa) b; fst ((case case koa of KOTCB x \<Rightarrow> Some x | _ \<Rightarrow> None of None \<Rightarrow> fail | Some x2 \<Rightarrow> return x2) b) = {(obj, b)}; koa = KOTCB x6\<rbrakk> \<Longrightarrow> tcb_relation tcb aa
 7. \<And>a b aa bb koa s'' tcb obj x7. \<lbrakk>(a, b) \<in> state_relation; fst (lookupAround2 t (ksPSpace b)) = Some (t, bb); kheap a t = Some (TCB tcb); ksPSpace b t = Some koa; (aa, s'') \<in> fst ((case case bb of KOTCB x \<Rightarrow> Some x | _ \<Rightarrow> None of None \<Rightarrow> fail | Some x2 \<Rightarrow> return x2) b); is_aligned t (objBitsKO koa); is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) s''); ps_clear t (objBitsKO koa) b; fst ((case case koa of KOTCB x \<Rightarrow> Some x | _ \<Rightarrow> None of None \<Rightarrow> fail | Some x2 \<Rightarrow> return x2) b) = {(obj, b)}; koa = KOCTE x7\<rbrakk> \<Longrightarrow> tcb_relation tcb aa
 8. \<And>a b aa bb koa s'' tcb obj x8. \<lbrakk>(a, b) \<in> state_relation; fst (lookupAround2 t (ksPSpace b)) = Some (t, bb); kheap a t = Some (TCB tcb); ksPSpace b t = Some koa; (aa, s'') \<in> fst ((case case bb of KOTCB x \<Rightarrow> Some x | _ \<Rightarrow> None of None \<Rightarrow> fail | Some x2 \<Rightarrow> return x2) b); is_aligned t (objBitsKO koa); is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) s''); ps_clear t (objBitsKO koa) b; fst ((case case koa of KOTCB x \<Rightarrow> Some x | _ \<Rightarrow> None of None \<Rightarrow> fail | Some x2 \<Rightarrow> return x2) b) = {(obj, b)}; koa = KOArch x8\<rbrakk> \<Longrightarrow> tcb_relation tcb aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa bb koa s'' tcb obj x6. \<lbrakk>(a, b) \<in> state_relation; fst (lookupAround2 t (ksPSpace b)) = Some (t, bb); kheap a t = Some (TCB tcb); ksPSpace b t = Some (KOTCB obj); (aa, s'') \<in> fst ((case case bb of KOTCB x \<Rightarrow> Some x | _ \<Rightarrow> None of None \<Rightarrow> \<lambda>s. ({}, True) | Some x2 \<Rightarrow> \<lambda>s. ({(x2, s)}, False)) b); is_aligned t (objBitsKO (KOTCB obj)); is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) s''); ps_clear t (objBitsKO (KOTCB obj)) b; x6 = obj; koa = KOTCB obj\<rbrakk> \<Longrightarrow> tcb_relation tcb aa proof (prove)
goal (8 subgoals):
 1. \<And>a b aa bb koa s'' tcb obj x6 x1. \<lbrakk>(a, b) \<in> state_relation; fst (lookupAround2 t (ksPSpace b)) = Some (t, bb); kheap a t = Some (TCB tcb); ksPSpace b t = Some (KOTCB obj); (aa, s'') \<in> fst ((case case bb of KOTCB x \<Rightarrow> Some x | _ \<Rightarrow> None of None \<Rightarrow> \<lambda>s. ({}, True) | Some x2 \<Rightarrow> \<lambda>s. ({(x2, s)}, False)) b); is_aligned t (objBitsKO (KOTCB obj)); is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) s''); ps_clear t (objBitsKO (KOTCB obj)) b; x6 = obj; koa = KOTCB obj; bb = KOEndpoint x1\<rbrakk> \<Longrightarrow> tcb_relation tcb aa
 2. \<And>a b aa bb koa s'' tcb obj x6 x2. \<lbrakk>(a, b) \<in> state_relation; fst (lookupAround2 t (ksPSpace b)) = Some (t, bb); kheap a t = Some (TCB tcb); ksPSpace b t = Some (KOTCB obj); (aa, s'') \<in> fst ((case case bb of KOTCB x \<Rightarrow> Some x | _ \<Rightarrow> None of None \<Rightarrow> \<lambda>s. ({}, True) | Some x2 \<Rightarrow> \<lambda>s. ({(x2, s)}, False)) b); is_aligned t (objBitsKO (KOTCB obj)); is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) s''); ps_clear t (objBitsKO (KOTCB obj)) b; x6 = obj; koa = KOTCB obj; bb = KONotification x2\<rbrakk> \<Longrightarrow> tcb_relation tcb aa
 3. \<And>a b aa bb koa s'' tcb obj x6. \<lbrakk>(a, b) \<in> state_relation; fst (lookupAround2 t (ksPSpace b)) = Some (t, bb); kheap a t = Some (TCB tcb); ksPSpace b t = Some (KOTCB obj); (aa, s'') \<in> fst ((case case bb of KOTCB x \<Rightarrow> Some x | _ \<Rightarrow> None of None \<Rightarrow> \<lambda>s. ({}, True) | Some x2 \<Rightarrow> \<lambda>s. ({(x2, s)}, False)) b); is_aligned t (objBitsKO (KOTCB obj)); is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) s''); ps_clear t (objBitsKO (KOTCB obj)) b; x6 = obj; koa = KOTCB obj; bb = KOKernelData\<rbrakk> \<Longrightarrow> tcb_relation tcb aa
 4. \<And>a b aa bb koa s'' tcb obj x6. \<lbrakk>(a, b) \<in> state_relation; fst (lookupAround2 t (ksPSpace b)) = Some (t, bb); kheap a t = Some (TCB tcb); ksPSpace b t = Some (KOTCB obj); (aa, s'') \<in> fst ((case case bb of KOTCB x \<Rightarrow> Some x | _ \<Rightarrow> None of None \<Rightarrow> \<lambda>s. ({}, True) | Some x2 \<Rightarrow> \<lambda>s. ({(x2, s)}, False)) b); is_aligned t (objBitsKO (KOTCB obj)); is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) s''); ps_clear t (objBitsKO (KOTCB obj)) b; x6 = obj; koa = KOTCB obj; bb = KOUserData\<rbrakk> \<Longrightarrow> tcb_relation tcb aa
 5. \<And>a b aa bb koa s'' tcb obj x6. \<lbrakk>(a, b) \<in> state_relation; fst (lookupAround2 t (ksPSpace b)) = Some (t, bb); kheap a t = Some (TCB tcb); ksPSpace b t = Some (KOTCB obj); (aa, s'') \<in> fst ((case case bb of KOTCB x \<Rightarrow> Some x | _ \<Rightarrow> None of None \<Rightarrow> \<lambda>s. ({}, True) | Some x2 \<Rightarrow> \<lambda>s. ({(x2, s)}, False)) b); is_aligned t (objBitsKO (KOTCB obj)); is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) s''); ps_clear t (objBitsKO (KOTCB obj)) b; x6 = obj; koa = KOTCB obj; bb = KOUserDataDevice\<rbrakk> \<Longrightarrow> tcb_relation tcb aa
 6. \<And>a b aa bb koa s'' tcb obj x6 x6a. \<lbrakk>(a, b) \<in> state_relation; fst (lookupAround2 t (ksPSpace b)) = Some (t, bb); kheap a t = Some (TCB tcb); ksPSpace b t = Some (KOTCB obj); (aa, s'') \<in> fst ((case case bb of KOTCB x \<Rightarrow> Some x | _ \<Rightarrow> None of None \<Rightarrow> \<lambda>s. ({}, True) | Some x2 \<Rightarrow> \<lambda>s. ({(x2, s)}, False)) b); is_aligned t (objBitsKO (KOTCB obj)); is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) s''); ps_clear t (objBitsKO (KOTCB obj)) b; x6 = obj; koa = KOTCB obj; bb = KOTCB x6a\<rbrakk> \<Longrightarrow> tcb_relation tcb aa
 7. \<And>a b aa bb koa s'' tcb obj x6 x7. \<lbrakk>(a, b) \<in> state_relation; fst (lookupAround2 t (ksPSpace b)) = Some (t, bb); kheap a t = Some (TCB tcb); ksPSpace b t = Some (KOTCB obj); (aa, s'') \<in> fst ((case case bb of KOTCB x \<Rightarrow> Some x | _ \<Rightarrow> None of None \<Rightarrow> \<lambda>s. ({}, True) | Some x2 \<Rightarrow> \<lambda>s. ({(x2, s)}, False)) b); is_aligned t (objBitsKO (KOTCB obj)); is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) s''); ps_clear t (objBitsKO (KOTCB obj)) b; x6 = obj; koa = KOTCB obj; bb = KOCTE x7\<rbrakk> \<Longrightarrow> tcb_relation tcb aa
 8. \<And>a b aa bb koa s'' tcb obj x6 x8. \<lbrakk>(a, b) \<in> state_relation; fst (lookupAround2 t (ksPSpace b)) = Some (t, bb); kheap a t = Some (TCB tcb); ksPSpace b t = Some (KOTCB obj); (aa, s'') \<in> fst ((case case bb of KOTCB x \<Rightarrow> Some x | _ \<Rightarrow> None of None \<Rightarrow> \<lambda>s. ({}, True) | Some x2 \<Rightarrow> \<lambda>s. ({(x2, s)}, False)) b); is_aligned t (objBitsKO (KOTCB obj)); is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) s''); ps_clear t (objBitsKO (KOTCB obj)) b; x6 = obj; koa = KOTCB obj; bb = KOArch x8\<rbrakk> \<Longrightarrow> tcb_relation tcb aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa bb koa s'' tcb obj x6. \<lbrakk>(a, b) \<in> state_relation; fst (lookupAround2 t (ksPSpace b)) = Some (t, KOTCB aa); kheap a t = Some (TCB tcb); ksPSpace b t = Some (KOTCB obj); s'' = b; is_aligned t (objBitsKO (KOTCB obj)); is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) b); ps_clear t (objBitsKO (KOTCB obj)) b; x6 = obj; koa = KOTCB obj; bb = KOTCB aa\<rbrakk> \<Longrightarrow> tcb_relation tcb aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa tcb obj. \<lbrakk>fst (lookupAround2 t (ksPSpace b)) = Some (t, KOTCB aa); kheap a t = Some (TCB tcb); ksPSpace b t = Some (KOTCB obj); is_aligned t (objBitsKO (KOTCB obj)); is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) b); ps_clear t (objBitsKO (KOTCB obj)) 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)); ekheap_relation (ekheap 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> tcb_relation tcb aa proof (prove)
goal (2 subgoals):
 1. \<And>a b aa tcb obj. \<lbrakk>fst (lookupAround2 t (ksPSpace b)) = Some (t, KOTCB aa); kheap a t = Some (TCB tcb); ksPSpace b t = Some (KOTCB obj); is_aligned t (objBitsKO (KOTCB obj)); is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) b); ps_clear t (objBitsKO (KOTCB obj)) b; pspace_dom (kheap a) = dom (ksPSpace b); ekheap_relation (ekheap 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> ?x103 a b aa tcb obj \<in> dom (kheap a)
 2. \<And>a b aa tcb obj. \<lbrakk>fst (lookupAround2 t (ksPSpace b)) = Some (t, KOTCB aa); kheap a t = Some (TCB tcb); ksPSpace b t = Some (KOTCB obj); is_aligned t (objBitsKO (KOTCB obj)); is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) b); ps_clear t (objBitsKO (KOTCB obj)) b; pspace_dom (kheap a) = dom (ksPSpace b); ekheap_relation (ekheap 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; \<forall>x\<in>obj_relation_cuts (the (kheap a (?x103 a b aa tcb obj))) (?x103 a b aa tcb obj). case x of (y, P) \<Rightarrow> P (the (kheap a (?x103 a b aa tcb obj))) (the (ksPSpace b y))\<rbrakk> \<Longrightarrow> tcb_relation tcb aa proof (prove)
goal (2 subgoals):
 1. \<And>a b aa tcb obj. \<lbrakk>fst (lookupAround2 t (ksPSpace b)) = Some (t, KOTCB aa); kheap a t = Some (TCB tcb); ksPSpace b t = Some (KOTCB obj); is_aligned t (objBitsKO (KOTCB obj)); is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) b); ps_clear t (objBitsKO (KOTCB obj)) b; pspace_dom (kheap a) = dom (ksPSpace b); ekheap_relation (ekheap 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>y. kheap a (?x103 a b aa tcb obj) = Some y
 2. \<And>a b aa tcb obj. \<lbrakk>fst (lookupAround2 t (ksPSpace b)) = Some (t, KOTCB aa); kheap a t = Some (TCB tcb); ksPSpace b t = Some (KOTCB obj); is_aligned t (objBitsKO (KOTCB obj)); is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) b); ps_clear t (objBitsKO (KOTCB obj)) b; pspace_dom (kheap a) = dom (ksPSpace b); ekheap_relation (ekheap 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; \<forall>x\<in>obj_relation_cuts (the (kheap a (?x103 a b aa tcb obj))) (?x103 a b aa tcb obj). case x of (y, P) \<Rightarrow> P (the (kheap a (?x103 a b aa tcb obj))) (the (ksPSpace b y))\<rbrakk> \<Longrightarrow> tcb_relation tcb aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa tcb obj. \<lbrakk>fst (lookupAround2 t (ksPSpace b)) = Some (t, KOTCB aa); kheap a t = Some (TCB tcb); ksPSpace b t = Some (KOTCB obj); is_aligned t (objBitsKO (KOTCB obj)); is_aligned t (objBits aa); ((), b) \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace b))) (objBits aa) b); ps_clear t (objBitsKO (KOTCB obj)) b; pspace_dom (kheap a) = dom (ksPSpace b); ekheap_relation (ekheap 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; \<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 proof (prove)
goal:
No subgoals!