theory TcbAcc_R

lemma set_eobject_corres':
  assumes e: "etcb_relation etcb tcb'"
  assumes z: "\<And>s. obj_at' P ptr s
               \<Longrightarrow> map_to_ctes ((ksPSpace s) (ptr \<mapsto> KOTCB tcb')) = map_to_ctes (ksPSpace s)"
  shows "corres dc (tcb_at ptr and is_etcb_at ptr)
            (obj_at' (\<lambda>ko. non_exst_same ko tcb') ptr
            and obj_at' P ptr)
            (set_eobject ptr etcb) (setObject ptr tcb')" apply (rule corres_no_failI) apply (rule no_fail_pre) apply wp apply (clarsimp simp: obj_at'_def) apply (unfold set_eobject_def setObject_def) apply (clarsimp simp: in_monad split_def bind_def gets_def get_def Bex_def
                        put_def return_def modify_def get_object_def projectKOs
                        updateObject_default_def in_magnitude_check objBits_simps') apply (clarsimp simp add: state_relation_def z) apply (clarsimp simp add: obj_at_def is_etcb_at_def) apply (simp only: pspace_relation_def dom_fun_upd2 simp_thms) apply (elim conjE) apply (frule bspec, erule domI) apply (rule conjI) apply (rule ballI, drule(1) bspec) apply (drule domD) apply (clarsimp simp: is_other_obj_relation_type) apply (drule(1) bspec) apply (clarsimp simp: non_exst_same_def) apply (case_tac bb; simp) apply (clarsimp simp: obj_at'_def other_obj_relation_def cte_relation_def tcb_relation_def projectKOs split: if_split_asm)+ apply (clarsimp simp: aobj_relation_cuts_def split: ARM_A.arch_kernel_obj.splits) apply (rename_tac arch_kernel_obj obj d p ts) apply (case_tac arch_kernel_obj; simp) apply (clarsimp simp: pte_relation_def pde_relation_def is_tcb_def
                    split: if_split_asm)+ apply (simp only: ekheap_relation_def dom_fun_upd2 simp_thms) apply (frule bspec, erule domI) apply (rule ballI, drule(1) bspec) apply (drule domD) apply (clarsimp simp: obj_at'_def) apply (clarsimp simp: projectKOs) apply (insert e) apply (clarsimp simp: other_obj_relation_def etcb_relation_def is_other_obj_relation_type split: Structures_A.kernel_object.splits Structures_H.kernel_object.splits ARM_A.arch_kernel_obj.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (tcb_at ptr and is_etcb_at ptr) (obj_at' (\<lambda>ko. non_exst_same ko tcb') ptr and obj_at' P ptr) (set_eobject ptr etcb) (setObject ptr tcb') proof (prove)
goal (2 subgoals):
 1. True \<Longrightarrow> no_fail (obj_at' (\<lambda>ko. non_exst_same ko tcb') ptr and obj_at' P ptr) (setObject ptr tcb')
 2. \<forall>(s, s')\<in>state_relation. (tcb_at ptr and is_etcb_at ptr) s \<and> (obj_at' (\<lambda>ko. non_exst_same ko tcb') ptr and obj_at' P ptr) s' \<longrightarrow> (\<forall>(r', t')\<in>fst (setObject ptr tcb' s'). \<exists>(r, t)\<in>fst (set_eobject ptr etcb s). (t, t') \<in> state_relation \<and> dc r r') proof (prove)
goal (3 subgoals):
 1. True \<Longrightarrow> no_fail ?P3 (setObject ptr tcb')
 2. \<And>s. \<lbrakk>True; (obj_at' (\<lambda>ko. non_exst_same ko tcb') ptr and obj_at' P ptr) s\<rbrakk> \<Longrightarrow> ?P3 s
 3. \<forall>(s, s')\<in>state_relation. (tcb_at ptr and is_etcb_at ptr) s \<and> (obj_at' (\<lambda>ko. non_exst_same ko tcb') ptr and obj_at' P ptr) s' \<longrightarrow> (\<forall>(r', t')\<in>fst (setObject ptr tcb' s'). \<exists>(r, t)\<in>fst (set_eobject ptr etcb s). (t, t') \<in> state_relation \<and> dc r r') proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>True; (obj_at' (\<lambda>ko. non_exst_same ko tcb') ptr and obj_at' P ptr) s\<rbrakk> \<Longrightarrow> tcb_at' ptr s
 2. \<forall>(s, s')\<in>state_relation. (tcb_at ptr and is_etcb_at ptr) s \<and> (obj_at' (\<lambda>ko. non_exst_same ko tcb') ptr and obj_at' P ptr) s' \<longrightarrow> (\<forall>(r', t')\<in>fst (setObject ptr tcb' s'). \<exists>(r, t)\<in>fst (set_eobject ptr etcb s). (t, t') \<in> state_relation \<and> dc r r') proof (prove)
goal (1 subgoal):
 1. \<forall>(s, s')\<in>state_relation. (tcb_at ptr and is_etcb_at ptr) s \<and> (obj_at' (\<lambda>ko. non_exst_same ko tcb') ptr and obj_at' P ptr) s' \<longrightarrow> (\<forall>(r', t')\<in>fst (setObject ptr tcb' s'). \<exists>(r, t)\<in>fst (set_eobject ptr etcb s). (t, t') \<in> state_relation \<and> dc r r') proof (prove)
goal (1 subgoal):
 1. \<forall>(s, s')\<in>state_relation. (tcb_at ptr and is_etcb_at ptr) s \<and> (obj_at' (\<lambda>ko. non_exst_same ko tcb') ptr and obj_at' P ptr) s' \<longrightarrow> (\<forall>(r', t')\<in>fst ((do ps <- gets ksPSpace;
map <- return (psMap ps);
(before, after) <- return (lookupAround2 (fromPPtr ptr) map);
(ptr', obj) <- maybeToMonad before;
obj' <- updateObject tcb' obj (fromPPtr ptr) ptr' after;
map' <- return (data_map_insert ptr' obj' map);
ps' <- return (psMap_update (\<lambda>_. map') ps);
modify (ksPSpace_update (\<lambda>_. ps'))
od) s'). \<exists>(r, t)\<in>fst ((do es <- get;
ekh <- return $ (ekheap es)(ptr \<mapsto> etcb);
put (ekheap_update (\<lambda>_. ekh) es)
od) s). (t, t') \<in> state_relation \<and> dc r r') proof (prove)
goal (1 subgoal):
 1. \<And>a b ab. \<lbrakk>(a, b) \<in> state_relation; ksPSpace b ptr = Some (KOTCB ab); is_aligned ptr 9; ps_clear ptr 9 b; tcb_at ptr a; is_etcb_at ptr a; obj_at' (\<lambda>ko. non_exst_same ko tcb') ptr b; obj_at' P ptr b\<rbrakk> \<Longrightarrow> (ekheap_update (\<lambda>_. (ekheap a)(ptr \<mapsto> etcb)) a, b\<lparr>ksPSpace := (ksPSpace b)(ptr \<mapsto> KOTCB tcb')\<rparr>) \<in> state_relation proof (prove)
goal (1 subgoal):
 1. \<And>a b ab. \<lbrakk>ksPSpace b ptr = Some (KOTCB ab); is_aligned ptr 9; ps_clear ptr 9 b; tcb_at ptr a; is_etcb_at ptr a; obj_at' (\<lambda>ko. non_exst_same ko tcb') ptr b; obj_at' P ptr b; pspace_relation (kheap a) (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> pspace_relation (kheap a) ((ksPSpace b)(ptr \<mapsto> KOTCB tcb')) \<and> ekheap_relation ((ekheap a)(ptr \<mapsto> etcb)) ((ksPSpace b)(ptr \<mapsto> KOTCB tcb')) proof (prove)
goal (1 subgoal):
 1. \<And>a b ab ko y. \<lbrakk>ksPSpace b ptr = Some (KOTCB ab); is_aligned ptr 9; ps_clear ptr 9 b; obj_at' (\<lambda>ko. non_exst_same ko tcb') ptr b; obj_at' P ptr b; pspace_relation (kheap a) (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; ekheap a ptr = Some y; kheap a ptr = Some ko; is_tcb ko\<rbrakk> \<Longrightarrow> pspace_relation (kheap a) ((ksPSpace b)(ptr \<mapsto> KOTCB tcb')) \<and> ekheap_relation ((ekheap a)(ptr \<mapsto> etcb)) ((ksPSpace b)(ptr \<mapsto> KOTCB tcb')) proof (prove)
goal (1 subgoal):
 1. \<And>a b ab ko y. \<lbrakk>ksPSpace b ptr = Some (KOTCB ab); is_aligned ptr 9; ps_clear ptr 9 b; obj_at' (\<lambda>ko. non_exst_same ko tcb') ptr b; obj_at' P ptr b; pspace_dom (kheap a) = dom (ksPSpace b) \<and> (\<forall>x\<in>dom (kheap a). \<forall>(y, P)\<in>obj_relation_cuts (the (kheap a x)) x. 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; ekheap a ptr = Some y; kheap a ptr = Some ko; is_tcb ko\<rbrakk> \<Longrightarrow> (\<forall>x\<in>dom (kheap a). \<forall>(y, P)\<in>obj_relation_cuts (the (kheap a x)) x. P (the (kheap a x)) (the (((ksPSpace b)(ptr \<mapsto> KOTCB tcb')) y))) \<and> ekheap_relation ((ekheap a)(ptr \<mapsto> etcb)) ((ksPSpace b)(ptr \<mapsto> KOTCB tcb')) proof (prove)
goal (1 subgoal):
 1. \<And>a b ab ko y. \<lbrakk>ksPSpace b ptr = Some (KOTCB ab); is_aligned ptr 9; ps_clear ptr 9 b; obj_at' (\<lambda>ko. non_exst_same ko tcb') ptr b; obj_at' P ptr 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; ekheap a ptr = Some y; kheap a ptr = Some ko; is_tcb ko; pspace_dom (kheap a) = dom (ksPSpace b); \<forall>x\<in>dom (kheap a). \<forall>(y, P)\<in>obj_relation_cuts (the (kheap a x)) x. P (the (kheap a x)) (the (ksPSpace b y))\<rbrakk> \<Longrightarrow> (\<forall>x\<in>dom (kheap a). \<forall>(y, P)\<in>obj_relation_cuts (the (kheap a x)) x. P (the (kheap a x)) (the (((ksPSpace b)(ptr \<mapsto> KOTCB tcb')) y))) \<and> ekheap_relation ((ekheap a)(ptr \<mapsto> etcb)) ((ksPSpace b)(ptr \<mapsto> KOTCB tcb')) proof (prove)
goal (1 subgoal):
 1. \<And>a b ab ko y. \<lbrakk>ksPSpace b ptr = Some (KOTCB ab); is_aligned ptr 9; ps_clear ptr 9 b; obj_at' (\<lambda>ko. non_exst_same ko tcb') ptr b; obj_at' P ptr 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; ekheap a ptr = Some y; kheap a ptr = Some ko; is_tcb ko; pspace_dom (kheap a) = dom (ksPSpace b); \<forall>x\<in>dom (kheap a). \<forall>(y, P)\<in>obj_relation_cuts (the (kheap a x)) x. P (the (kheap a x)) (the (ksPSpace b y)); \<forall>(y, P)\<in>obj_relation_cuts (the (kheap a ptr)) ptr. P (the (kheap a ptr)) (the (ksPSpace b y))\<rbrakk> \<Longrightarrow> (\<forall>x\<in>dom (kheap a). \<forall>(y, P)\<in>obj_relation_cuts (the (kheap a x)) x. P (the (kheap a x)) (the (((ksPSpace b)(ptr \<mapsto> KOTCB tcb')) y))) \<and> ekheap_relation ((ekheap a)(ptr \<mapsto> etcb)) ((ksPSpace b)(ptr \<mapsto> KOTCB tcb')) proof (prove)
goal (2 subgoals):
 1. \<And>a b ab ko y. \<lbrakk>ksPSpace b ptr = Some (KOTCB ab); is_aligned ptr 9; ps_clear ptr 9 b; obj_at' (\<lambda>ko. non_exst_same ko tcb') ptr b; obj_at' P ptr 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; ekheap a ptr = Some y; kheap a ptr = Some ko; is_tcb ko; pspace_dom (kheap a) = dom (ksPSpace b); \<forall>x\<in>dom (kheap a). \<forall>(y, P)\<in>obj_relation_cuts (the (kheap a x)) x. P (the (kheap a x)) (the (ksPSpace b y)); \<forall>(y, P)\<in>obj_relation_cuts (the (kheap a ptr)) ptr. P (the (kheap a ptr)) (the (ksPSpace b y))\<rbrakk> \<Longrightarrow> \<forall>x\<in>dom (kheap a). \<forall>(y, P)\<in>obj_relation_cuts (the (kheap a x)) x. P (the (kheap a x)) (the (((ksPSpace b)(ptr \<mapsto> KOTCB tcb')) y))
 2. \<And>a b ab ko y. \<lbrakk>ksPSpace b ptr = Some (KOTCB ab); is_aligned ptr 9; ps_clear ptr 9 b; obj_at' (\<lambda>ko. non_exst_same ko tcb') ptr b; obj_at' P ptr 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; ekheap a ptr = Some y; kheap a ptr = Some ko; is_tcb ko; pspace_dom (kheap a) = dom (ksPSpace b); \<forall>x\<in>dom (kheap a). \<forall>(y, P)\<in>obj_relation_cuts (the (kheap a x)) x. P (the (kheap a x)) (the (ksPSpace b y)); \<forall>(y, P)\<in>obj_relation_cuts (the (kheap a ptr)) ptr. P (the (kheap a ptr)) (the (ksPSpace b y))\<rbrakk> \<Longrightarrow> ekheap_relation ((ekheap a)(ptr \<mapsto> etcb)) ((ksPSpace b)(ptr \<mapsto> KOTCB tcb')) proof (prove)
goal (2 subgoals):
 1. \<And>a b ab ko y x. \<lbrakk>ksPSpace b ptr = Some (KOTCB ab); is_aligned ptr 9; ps_clear ptr 9 b; obj_at' (\<lambda>ko. non_exst_same ko tcb') ptr b; obj_at' P ptr 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; ekheap a ptr = Some y; kheap a ptr = Some ko; is_tcb ko; pspace_dom (kheap a) = dom (ksPSpace b); \<forall>(y, P)\<in>obj_relation_cuts (the (kheap a ptr)) ptr. P (the (kheap a ptr)) (the (ksPSpace b y)); x \<in> dom (kheap a); \<forall>(y, P)\<in>obj_relation_cuts (the (kheap a x)) x. P (the (kheap a x)) (the (ksPSpace b y))\<rbrakk> \<Longrightarrow> \<forall>(y, P)\<in>obj_relation_cuts (the (kheap a x)) x. P (the (kheap a x)) (the (((ksPSpace b)(ptr \<mapsto> KOTCB tcb')) y))
 2. \<And>a b ab ko y. \<lbrakk>ksPSpace b ptr = Some (KOTCB ab); is_aligned ptr 9; ps_clear ptr 9 b; obj_at' (\<lambda>ko. non_exst_same ko tcb') ptr b; obj_at' P ptr 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; ekheap a ptr = Some y; kheap a ptr = Some ko; is_tcb ko; pspace_dom (kheap a) = dom (ksPSpace b); \<forall>x\<in>dom (kheap a). \<forall>(y, P)\<in>obj_relation_cuts (the (kheap a x)) x. P (the (kheap a x)) (the (ksPSpace b y)); \<forall>(y, P)\<in>obj_relation_cuts (the (kheap a ptr)) ptr. P (the (kheap a ptr)) (the (ksPSpace b y))\<rbrakk> \<Longrightarrow> ekheap_relation ((ekheap a)(ptr \<mapsto> etcb)) ((ksPSpace b)(ptr \<mapsto> KOTCB tcb')) proof (prove)
goal (2 subgoals):
 1. \<And>a b ab ko y x. \<lbrakk>ksPSpace b ptr = Some (KOTCB ab); is_aligned ptr 9; ps_clear ptr 9 b; obj_at' (\<lambda>ko. non_exst_same ko tcb') ptr b; obj_at' P ptr 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; ekheap a ptr = Some y; kheap a ptr = Some ko; is_tcb ko; pspace_dom (kheap a) = dom (ksPSpace b); \<forall>(y, P)\<in>obj_relation_cuts (the (kheap a ptr)) ptr. P (the (kheap a ptr)) (the (ksPSpace b y)); \<forall>(y, P)\<in>obj_relation_cuts (the (kheap a x)) x. P (the (kheap a x)) (the (ksPSpace b y)); \<exists>b. kheap a x = Some b\<rbrakk> \<Longrightarrow> \<forall>(y, P)\<in>obj_relation_cuts (the (kheap a x)) x. P (the (kheap a x)) (the (((ksPSpace b)(ptr \<mapsto> KOTCB tcb')) y))
 2. \<And>a b ab ko y. \<lbrakk>ksPSpace b ptr = Some (KOTCB ab); is_aligned ptr 9; ps_clear ptr 9 b; obj_at' (\<lambda>ko. non_exst_same ko tcb') ptr b; obj_at' P ptr 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; ekheap a ptr = Some y; kheap a ptr = Some ko; is_tcb ko; pspace_dom (kheap a) = dom (ksPSpace b); \<forall>x\<in>dom (kheap a). \<forall>(y, P)\<in>obj_relation_cuts (the (kheap a x)) x. P (the (kheap a x)) (the (ksPSpace b y)); \<forall>(y, P)\<in>obj_relation_cuts (the (kheap a ptr)) ptr. P (the (kheap a ptr)) (the (ksPSpace b y))\<rbrakk> \<Longrightarrow> ekheap_relation ((ekheap a)(ptr \<mapsto> etcb)) ((ksPSpace b)(ptr \<mapsto> KOTCB tcb')) proof (prove)
goal (2 subgoals):
 1. \<And>a b ab ko y x aa ba bb. \<lbrakk>ksPSpace b ptr = Some (KOTCB ab); is_aligned ptr 9; ps_clear ptr 9 b; obj_at' (\<lambda>ko. non_exst_same ko tcb') ptr b; obj_at' P ptr 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; ekheap a ptr = Some y; kheap a ptr = Some ko; is_tcb ko; pspace_dom (kheap a) = dom (ksPSpace b); \<forall>x\<in>obj_relation_cuts ko ptr. case x of (y, P) \<Rightarrow> P ko (the (ksPSpace b y)); \<forall>x\<in>obj_relation_cuts bb x. case x of (y, P) \<Rightarrow> P bb (the (ksPSpace b y)); (aa, ba) \<in> obj_relation_cuts bb x; kheap a x = Some bb\<rbrakk> \<Longrightarrow> (aa = ptr \<longrightarrow> ba bb (KOTCB tcb')) \<and> (aa \<noteq> ptr \<longrightarrow> ba bb (the (ksPSpace b aa)))
 2. \<And>a b ab ko y. \<lbrakk>ksPSpace b ptr = Some (KOTCB ab); is_aligned ptr 9; ps_clear ptr 9 b; obj_at' (\<lambda>ko. non_exst_same ko tcb') ptr b; obj_at' P ptr 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; ekheap a ptr = Some y; kheap a ptr = Some ko; is_tcb ko; pspace_dom (kheap a) = dom (ksPSpace b); \<forall>x\<in>dom (kheap a). \<forall>(y, P)\<in>obj_relation_cuts (the (kheap a x)) x. P (the (kheap a x)) (the (ksPSpace b y)); \<forall>(y, P)\<in>obj_relation_cuts (the (kheap a ptr)) ptr. P (the (kheap a ptr)) (the (ksPSpace b y))\<rbrakk> \<Longrightarrow> ekheap_relation ((ekheap a)(ptr \<mapsto> etcb)) ((ksPSpace b)(ptr \<mapsto> KOTCB tcb')) proof (prove)
goal (2 subgoals):
 1. \<And>a b ab ko y x aa ba bb. \<lbrakk>ksPSpace b ptr = Some (KOTCB ab); is_aligned ptr 9; ps_clear ptr 9 b; obj_at' (\<lambda>ko. non_exst_same ko tcb') ptr b; obj_at' P ptr 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; ekheap a ptr = Some y; kheap a ptr = Some ko; is_tcb ko; pspace_dom (kheap a) = dom (ksPSpace b); \<forall>x\<in>obj_relation_cuts ko ptr. case x of (y, P) \<Rightarrow> P ko (the (ksPSpace b y)); (aa, ba) \<in> obj_relation_cuts bb x; kheap a x = Some bb; case (aa, ba) of (y, P) \<Rightarrow> P bb (the (ksPSpace b y))\<rbrakk> \<Longrightarrow> (aa = ptr \<longrightarrow> ba bb (KOTCB tcb')) \<and> (aa \<noteq> ptr \<longrightarrow> ba bb (the (ksPSpace b aa)))
 2. \<And>a b ab ko y. \<lbrakk>ksPSpace b ptr = Some (KOTCB ab); is_aligned ptr 9; ps_clear ptr 9 b; obj_at' (\<lambda>ko. non_exst_same ko tcb') ptr b; obj_at' P ptr 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; ekheap a ptr = Some y; kheap a ptr = Some ko; is_tcb ko; pspace_dom (kheap a) = dom (ksPSpace b); \<forall>x\<in>dom (kheap a). \<forall>(y, P)\<in>obj_relation_cuts (the (kheap a x)) x. P (the (kheap a x)) (the (ksPSpace b y)); \<forall>(y, P)\<in>obj_relation_cuts (the (kheap a ptr)) ptr. P (the (kheap a ptr)) (the (ksPSpace b y))\<rbrakk> \<Longrightarrow> ekheap_relation ((ekheap a)(ptr \<mapsto> etcb)) ((ksPSpace b)(ptr \<mapsto> KOTCB tcb')) proof (prove)
goal (2 subgoals):
 1. \<And>a b ab ko y x ba bb. \<lbrakk>ksPSpace b ptr = Some (KOTCB ab); is_aligned ptr 9; ps_clear ptr 9 b; obj_at' (\<lambda>ko. \<exists>d p ts. tcb' = tcbTimeSlice_update (\<lambda>_. ts) (tcbPriority_update (\<lambda>_. p) (tcbDomain_update (\<lambda>_. d) ko))) ptr b; obj_at' P ptr 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; ekheap a ptr = Some y; kheap a ptr = Some ko; is_tcb ko; pspace_dom (kheap a) = dom (ksPSpace b); \<forall>x\<in>obj_relation_cuts ko ptr. case x of (y, P) \<Rightarrow> P ko (the (ksPSpace b y)); (ptr, ba) \<in> obj_relation_cuts bb x; kheap a x = Some bb; ba bb (KOTCB ab)\<rbrakk> \<Longrightarrow> ba bb (KOTCB tcb')
 2. \<And>a b ab ko y. \<lbrakk>ksPSpace b ptr = Some (KOTCB ab); is_aligned ptr 9; ps_clear ptr 9 b; obj_at' (\<lambda>ko. non_exst_same ko tcb') ptr b; obj_at' P ptr 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; ekheap a ptr = Some y; kheap a ptr = Some ko; is_tcb ko; pspace_dom (kheap a) = dom (ksPSpace b); \<forall>x\<in>dom (kheap a). \<forall>(y, P)\<in>obj_relation_cuts (the (kheap a x)) x. P (the (kheap a x)) (the (ksPSpace b y)); \<forall>(y, P)\<in>obj_relation_cuts (the (kheap a ptr)) ptr. P (the (kheap a ptr)) (the (ksPSpace b y))\<rbrakk> \<Longrightarrow> ekheap_relation ((ekheap a)(ptr \<mapsto> etcb)) ((ksPSpace b)(ptr \<mapsto> KOTCB tcb')) proof (prove)
goal (6 subgoals):
 1. \<And>a b ab ko y x ba bb x11 x12. \<lbrakk>ksPSpace b ptr = Some (KOTCB ab); is_aligned ptr 9; ps_clear ptr 9 b; obj_at' (\<lambda>ko. \<exists>d p ts. tcb' = tcbTimeSlice_update (\<lambda>_. ts) (tcbPriority_update (\<lambda>_. p) (tcbDomain_update (\<lambda>_. d) ko))) ptr b; obj_at' P ptr 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; ekheap a ptr = Some y; kheap a ptr = Some ko; is_tcb ko; pspace_dom (kheap a) = dom (ksPSpace b); \<forall>x\<in>obj_relation_cuts ko ptr. case x of (y, P) \<Rightarrow> P ko (the (ksPSpace b y)); (ptr, ba) \<in> (if well_formed_cnode_n x11 x12 then {(cte_map (x, y), cte_relation y) |y. y \<in> dom x12} else {(x, \<lambda>_ _. False)}); kheap a x = Some (CNode x11 x12); ba (CNode x11 x12) (KOTCB ab); bb = CNode x11 x12\<rbrakk> \<Longrightarrow> ba (CNode x11 x12) (KOTCB tcb')
 2. \<And>a b ab ko y x bb x2. \<lbrakk>ksPSpace b x = Some (KOTCB ab); is_aligned x 9; ps_clear x 9 b; obj_at' (\<lambda>ko. \<exists>d p ts. tcb' = tcbTimeSlice_update (\<lambda>_. ts) (tcbPriority_update (\<lambda>_. p) (tcbDomain_update (\<lambda>_. d) ko))) x b; obj_at' P x 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; ekheap a x = Some y; TCB x2 = ko; is_tcb ko; pspace_dom (kheap a) = dom (ksPSpace b); \<forall>x\<in>obj_relation_cuts ko x. case x of (y, P) \<Rightarrow> P ko (the (ksPSpace b y)); ptr = x; kheap a x = Some ko; other_obj_relation ko (KOTCB ab); bb = ko\<rbrakk> \<Longrightarrow> other_obj_relation ko (KOTCB tcb')
 3. \<And>a b ab ko y x bb x3. \<lbrakk>ksPSpace b x = Some (KOTCB ab); is_aligned x 9; ps_clear x 9 b; obj_at' (\<lambda>ko. \<exists>d p ts. tcb' = tcbTimeSlice_update (\<lambda>_. ts) (tcbPriority_update (\<lambda>_. p) (tcbDomain_update (\<lambda>_. d) ko))) x b; obj_at' P x 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; ekheap a x = Some y; Endpoint x3 = ko; is_tcb ko; pspace_dom (kheap a) = dom (ksPSpace b); \<forall>x\<in>obj_relation_cuts ko x. case x of (y, P) \<Rightarrow> P ko (the (ksPSpace b y)); ptr = x; kheap a x = Some ko; other_obj_relation ko (KOTCB ab); bb = ko\<rbrakk> \<Longrightarrow> other_obj_relation ko (KOTCB tcb')
 4. \<And>a b ab ko y x bb x4. \<lbrakk>ksPSpace b x = Some (KOTCB ab); is_aligned x 9; ps_clear x 9 b; obj_at' (\<lambda>ko. \<exists>d p ts. tcb' = tcbTimeSlice_update (\<lambda>_. ts) (tcbPriority_update (\<lambda>_. p) (tcbDomain_update (\<lambda>_. d) ko))) x b; obj_at' P x 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; ekheap a x = Some y; Notification x4 = ko; is_tcb ko; pspace_dom (kheap a) = dom (ksPSpace b); \<forall>x\<in>obj_relation_cuts ko x. case x of (y, P) \<Rightarrow> P ko (the (ksPSpace b y)); ptr = x; kheap a x = Some ko; other_obj_relation ko (KOTCB ab); bb = ko\<rbrakk> \<Longrightarrow> other_obj_relation ko (KOTCB tcb')
 5. \<And>a b ab ko y x ba bb x5. \<lbrakk>ksPSpace b ptr = Some (KOTCB ab); is_aligned ptr 9; ps_clear ptr 9 b; obj_at' (\<lambda>ko. \<exists>d p ts. tcb' = tcbTimeSlice_update (\<lambda>_. ts) (tcbPriority_update (\<lambda>_. p) (tcbDomain_update (\<lambda>_. d) ko))) ptr b; obj_at' P ptr 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; ekheap a ptr = Some y; kheap a ptr = Some ko; is_tcb ko; pspace_dom (kheap a) = dom (ksPSpace b); \<forall>x\<in>obj_relation_cuts ko ptr. case x of (y, P) \<Rightarrow> P ko (the (ksPSpace b y)); (ptr, ba) \<in> aobj_relation_cuts x5 x; kheap a x = Some (ArchObj x5); ba (ArchObj x5) (KOTCB ab); bb = ArchObj x5\<rbrakk> \<Longrightarrow> ba (ArchObj x5) (KOTCB tcb')
 6. \<And>a b ab ko y. \<lbrakk>ksPSpace b ptr = Some (KOTCB ab); is_aligned ptr 9; ps_clear ptr 9 b; obj_at' (\<lambda>ko. non_exst_same ko tcb') ptr b; obj_at' P ptr 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; ekheap a ptr = Some y; kheap a ptr = Some ko; is_tcb ko; pspace_dom (kheap a) = dom (ksPSpace b); \<forall>x\<in>dom (kheap a). \<forall>(y, P)\<in>obj_relation_cuts (the (kheap a x)) x. P (the (kheap a x)) (the (ksPSpace b y)); \<forall>(y, P)\<in>obj_relation_cuts (the (kheap a ptr)) ptr. P (the (kheap a ptr)) (the (ksPSpace b y))\<rbrakk> \<Longrightarrow> ekheap_relation ((ekheap a)(ptr \<mapsto> etcb)) ((ksPSpace b)(ptr \<mapsto> KOTCB tcb')) proof (prove)
goal (2 subgoals):
 1. \<And>a b ab ko y x ba x5 obj d p ts. \<lbrakk>ksPSpace b ptr = Some (KOTCB ab); is_aligned ptr 9; ps_clear ptr 9 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; ekheap a ptr = Some y; kheap a ptr = Some ko; is_tcb ko; pspace_dom (kheap a) = dom (ksPSpace b); \<forall>x\<in>obj_relation_cuts ko ptr. case x of (y, P) \<Rightarrow> P ko (the (ksPSpace b y)); (ptr, ba) \<in> aobj_relation_cuts x5 x; kheap a x = Some (ArchObj x5); ba (ArchObj x5) (KOTCB ab); is_aligned ptr (objBitsKO (KOTCB ab)); projectKO_opt (KOTCB ab) = Some obj; P obj; ps_clear ptr (objBitsKO (KOTCB ab)) b; tcb' = tcbTimeSlice_update (\<lambda>_. ts) (tcbPriority_update (\<lambda>_. p) (tcbDomain_update (\<lambda>_. d) ab))\<rbrakk> \<Longrightarrow> ba (ArchObj x5) (KOTCB (tcbTimeSlice_update (\<lambda>_. ts) (tcbPriority_update (\<lambda>_. p) (tcbDomain_update (\<lambda>_. d) ab))))
 2. \<And>a b ab ko y. \<lbrakk>ksPSpace b ptr = Some (KOTCB ab); is_aligned ptr 9; ps_clear ptr 9 b; obj_at' (\<lambda>ko. non_exst_same ko tcb') ptr b; obj_at' P ptr 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; ekheap a ptr = Some y; kheap a ptr = Some ko; is_tcb ko; pspace_dom (kheap a) = dom (ksPSpace b); \<forall>x\<in>dom (kheap a). \<forall>(y, P)\<in>obj_relation_cuts (the (kheap a x)) x. P (the (kheap a x)) (the (ksPSpace b y)); \<forall>(y, P)\<in>obj_relation_cuts (the (kheap a ptr)) ptr. P (the (kheap a ptr)) (the (ksPSpace b y))\<rbrakk> \<Longrightarrow> ekheap_relation ((ekheap a)(ptr \<mapsto> etcb)) ((ksPSpace b)(ptr \<mapsto> KOTCB tcb')) proof (prove)
goal (2 subgoals):
 1. \<And>a b ab ko y x ba x5 obj d p ts. \<lbrakk>ksPSpace b ptr = Some (KOTCB ab); is_aligned ptr 9; ps_clear ptr 9 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; ekheap a ptr = Some y; kheap a ptr = Some ko; is_tcb ko; pspace_dom (kheap a) = dom (ksPSpace b); \<forall>x\<in>obj_relation_cuts ko ptr. case x of (y, P) \<Rightarrow> P ko (the (ksPSpace b y)); (ptr, ba) \<in> rec_arch_kernel_obj (\<lambda>pool x. {(x, other_obj_relation)}) (\<lambda>pt x. range (\<lambda>y. (x + (UCAST(8 \<rightarrow> 32) y << 2), pte_relation y))) (\<lambda>pd x. range (\<lambda>y. (x + (UCAST(12 \<rightarrow> 32) y << 2), pde_relation y))) (\<lambda>dev sz x. {(x + n * 2 ^ pageBits, \<lambda>_ obj. obj = (if dev then KOUserDataDevice else KOUserData)) |n. n < 2 ^ (pageBitsForSize sz - pageBits)}) x5 x; kheap a x = Some (ArchObj x5); ba (ArchObj x5) (KOTCB ab); is_aligned ptr (objBitsKO (KOTCB ab)); projectKO_opt (KOTCB ab) = Some obj; P obj; ps_clear ptr (objBitsKO (KOTCB ab)) b; tcb' = tcbTimeSlice_update (\<lambda>_. ts) (tcbPriority_update (\<lambda>_. p) (tcbDomain_update (\<lambda>_. d) ab))\<rbrakk> \<Longrightarrow> ba (ArchObj x5) (KOTCB (tcbTimeSlice_update (\<lambda>_. ts) (tcbPriority_update (\<lambda>_. p) (tcbDomain_update (\<lambda>_. d) ab))))
 2. \<And>a b ab ko y. \<lbrakk>ksPSpace b ptr = Some (KOTCB ab); is_aligned ptr 9; ps_clear ptr 9 b; obj_at' (\<lambda>ko. non_exst_same ko tcb') ptr b; obj_at' P ptr 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; ekheap a ptr = Some y; kheap a ptr = Some ko; is_tcb ko; pspace_dom (kheap a) = dom (ksPSpace b); \<forall>x\<in>dom (kheap a). \<forall>(y, P)\<in>obj_relation_cuts (the (kheap a x)) x. P (the (kheap a x)) (the (ksPSpace b y)); \<forall>(y, P)\<in>obj_relation_cuts (the (kheap a ptr)) ptr. P (the (kheap a ptr)) (the (ksPSpace b y))\<rbrakk> \<Longrightarrow> ekheap_relation ((ekheap a)(ptr \<mapsto> etcb)) ((ksPSpace b)(ptr \<mapsto> KOTCB tcb')) proof (prove)
goal (2 subgoals):
 1. \<And>a b ab ko y x ba arch_kernel_obj obj d p ts. \<lbrakk>ksPSpace b ptr = Some (KOTCB ab); is_aligned ptr 9; ps_clear ptr 9 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; ekheap a ptr = Some y; kheap a ptr = Some ko; is_tcb ko; pspace_dom (kheap a) = dom (ksPSpace b); \<forall>x\<in>obj_relation_cuts ko ptr. case x of (y, P) \<Rightarrow> P ko (the (ksPSpace b y)); (ptr, ba) \<in> rec_arch_kernel_obj (\<lambda>pool x. {(x, other_obj_relation)}) (\<lambda>pt x. range (\<lambda>y. (x + (UCAST(8 \<rightarrow> 32) y << 2), pte_relation y))) (\<lambda>pd x. range (\<lambda>y. (x + (UCAST(12 \<rightarrow> 32) y << 2), pde_relation y))) (\<lambda>dev sz x. {(x + n * 2 ^ pageBits, \<lambda>_ obj. obj = (if dev then KOUserDataDevice else KOUserData)) |n. n < 2 ^ (pageBitsForSize sz - pageBits)}) arch_kernel_obj x; kheap a x = Some (ArchObj arch_kernel_obj); ba (ArchObj arch_kernel_obj) (KOTCB ab); is_aligned ptr (objBitsKO (KOTCB ab)); projectKO_opt (KOTCB ab) = Some obj; P obj; ps_clear ptr (objBitsKO (KOTCB ab)) b; tcb' = tcbTimeSlice_update (\<lambda>_. ts) (tcbPriority_update (\<lambda>_. p) (tcbDomain_update (\<lambda>_. d) ab))\<rbrakk> \<Longrightarrow> ba (ArchObj arch_kernel_obj) (KOTCB (tcbTimeSlice_update (\<lambda>_. ts) (tcbPriority_update (\<lambda>_. p) (tcbDomain_update (\<lambda>_. d) ab))))
 2. \<And>a b ab ko y. \<lbrakk>ksPSpace b ptr = Some (KOTCB ab); is_aligned ptr 9; ps_clear ptr 9 b; obj_at' (\<lambda>ko. non_exst_same ko tcb') ptr b; obj_at' P ptr 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; ekheap a ptr = Some y; kheap a ptr = Some ko; is_tcb ko; pspace_dom (kheap a) = dom (ksPSpace b); \<forall>x\<in>dom (kheap a). \<forall>(y, P)\<in>obj_relation_cuts (the (kheap a x)) x. P (the (kheap a x)) (the (ksPSpace b y)); \<forall>(y, P)\<in>obj_relation_cuts (the (kheap a ptr)) ptr. P (the (kheap a ptr)) (the (ksPSpace b y))\<rbrakk> \<Longrightarrow> ekheap_relation ((ekheap a)(ptr \<mapsto> etcb)) ((ksPSpace b)(ptr \<mapsto> KOTCB tcb')) proof (prove)
goal (5 subgoals):
 1. \<And>a b ab ko y x arch_kernel_obj obj d p ts x1. \<lbrakk>ksPSpace b x = Some (KOTCB ab); is_aligned x 9; ps_clear x 9 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; ekheap a x = Some y; ArchObj (arch_kernel_obj.ASIDPool x1) = ko; is_tcb ko; pspace_dom (kheap a) = dom (ksPSpace b); \<forall>x\<in>obj_relation_cuts ko x. case x of (y, P) \<Rightarrow> P ko (the (ksPSpace b y)); ptr = x; kheap a x = Some ko; other_obj_relation ko (KOTCB ab); is_aligned x (objBitsKO (KOTCB ab)); projectKO_opt (KOTCB ab) = Some obj; P obj; ps_clear x (objBitsKO (KOTCB ab)) b; tcb' = tcbTimeSlice_update (\<lambda>_. ts) (tcbPriority_update (\<lambda>_. p) (tcbDomain_update (\<lambda>_. d) ab)); arch_kernel_obj = arch_kernel_obj.ASIDPool x1\<rbrakk> \<Longrightarrow> other_obj_relation ko (KOTCB (tcbTimeSlice_update (\<lambda>_. ts) (tcbPriority_update (\<lambda>_. p) (tcbDomain_update (\<lambda>_. d) ab))))
 2. \<And>a b ab ko y x ba arch_kernel_obj obj d p ts x2. \<lbrakk>ksPSpace b ptr = Some (KOTCB ab); is_aligned ptr 9; ps_clear ptr 9 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; ekheap a ptr = Some y; kheap a ptr = Some ko; is_tcb ko; pspace_dom (kheap a) = dom (ksPSpace b); \<forall>x\<in>obj_relation_cuts ko ptr. case x of (y, P) \<Rightarrow> P ko (the (ksPSpace b y)); (ptr, ba) \<in> range (\<lambda>y. (x + (UCAST(8 \<rightarrow> 32) y << 2), pte_relation y)); kheap a x = Some (ArchObj (PageTable x2)); ba (ArchObj (PageTable x2)) (KOTCB ab); is_aligned ptr (objBitsKO (KOTCB ab)); projectKO_opt (KOTCB ab) = Some obj; P obj; ps_clear ptr (objBitsKO (KOTCB ab)) b; tcb' = tcbTimeSlice_update (\<lambda>_. ts) (tcbPriority_update (\<lambda>_. p) (tcbDomain_update (\<lambda>_. d) ab)); arch_kernel_obj = PageTable x2\<rbrakk> \<Longrightarrow> ba (ArchObj (PageTable x2)) (KOTCB (tcbTimeSlice_update (\<lambda>_. ts) (tcbPriority_update (\<lambda>_. p) (tcbDomain_update (\<lambda>_. d) ab))))
 3. \<And>a b ab ko y x ba arch_kernel_obj obj d p ts x3. \<lbrakk>ksPSpace b ptr = Some (KOTCB ab); is_aligned ptr 9; ps_clear ptr 9 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; ekheap a ptr = Some y; kheap a ptr = Some ko; is_tcb ko; pspace_dom (kheap a) = dom (ksPSpace b); \<forall>x\<in>obj_relation_cuts ko ptr. case x of (y, P) \<Rightarrow> P ko (the (ksPSpace b y)); (ptr, ba) \<in> range (\<lambda>y. (x + (UCAST(12 \<rightarrow> 32) y << 2), pde_relation y)); kheap a x = Some (ArchObj (PageDirectory x3)); ba (ArchObj (PageDirectory x3)) (KOTCB ab); is_aligned ptr (objBitsKO (KOTCB ab)); projectKO_opt (KOTCB ab) = Some obj; P obj; ps_clear ptr (objBitsKO (KOTCB ab)) b; tcb' = tcbTimeSlice_update (\<lambda>_. ts) (tcbPriority_update (\<lambda>_. p) (tcbDomain_update (\<lambda>_. d) ab)); arch_kernel_obj = PageDirectory x3\<rbrakk> \<Longrightarrow> ba (ArchObj (PageDirectory x3)) (KOTCB (tcbTimeSlice_update (\<lambda>_. ts) (tcbPriority_update (\<lambda>_. p) (tcbDomain_update (\<lambda>_. d) ab))))
 4. \<And>a b ab ko y x ba arch_kernel_obj obj d p ts x41 x42. \<lbrakk>ksPSpace b ptr = Some (KOTCB ab); is_aligned ptr 9; ps_clear ptr 9 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; ekheap a ptr = Some y; kheap a ptr = Some ko; is_tcb ko; pspace_dom (kheap a) = dom (ksPSpace b); \<forall>x\<in>obj_relation_cuts ko ptr. case x of (y, P) \<Rightarrow> P ko (the (ksPSpace b y)); \<exists>n. ptr = x + n * 2 ^ pageBits \<and> ba = (\<lambda>_ obj. obj = (if x41 then KOUserDataDevice else KOUserData)) \<and> n < 2 ^ (pageBitsForSize x42 - pageBits); kheap a x = Some (ArchObj (DataPage x41 x42)); ba (ArchObj (DataPage x41 x42)) (KOTCB ab); is_aligned ptr (objBitsKO (KOTCB ab)); projectKO_opt (KOTCB ab) = Some obj; P obj; ps_clear ptr (objBitsKO (KOTCB ab)) b; tcb' = tcbTimeSlice_update (\<lambda>_. ts) (tcbPriority_update (\<lambda>_. p) (tcbDomain_update (\<lambda>_. d) ab)); arch_kernel_obj = DataPage x41 x42\<rbrakk> \<Longrightarrow> ba (ArchObj (DataPage x41 x42)) (KOTCB (tcbTimeSlice_update (\<lambda>_. ts) (tcbPriority_update (\<lambda>_. p) (tcbDomain_update (\<lambda>_. d) ab))))
 5. \<And>a b ab ko y. \<lbrakk>ksPSpace b ptr = Some (KOTCB ab); is_aligned ptr 9; ps_clear ptr 9 b; obj_at' (\<lambda>ko. non_exst_same ko tcb') ptr b; obj_at' P ptr 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; ekheap a ptr = Some y; kheap a ptr = Some ko; is_tcb ko; pspace_dom (kheap a) = dom (ksPSpace b); \<forall>x\<in>dom (kheap a). \<forall>(y, P)\<in>obj_relation_cuts (the (kheap a x)) x. P (the (kheap a x)) (the (ksPSpace b y)); \<forall>(y, P)\<in>obj_relation_cuts (the (kheap a ptr)) ptr. P (the (kheap a ptr)) (the (ksPSpace b y))\<rbrakk> \<Longrightarrow> ekheap_relation ((ekheap a)(ptr \<mapsto> etcb)) ((ksPSpace b)(ptr \<mapsto> KOTCB tcb')) proof (prove)
goal (1 subgoal):
 1. \<And>a b ab ko y. \<lbrakk>ksPSpace b ptr = Some (KOTCB ab); is_aligned ptr 9; ps_clear ptr 9 b; obj_at' (\<lambda>ko. non_exst_same ko tcb') ptr b; obj_at' P ptr 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; ekheap a ptr = Some y; kheap a ptr = Some ko; case ko of TCB t \<Rightarrow> True | _ \<Rightarrow> False; 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>obj_relation_cuts ko ptr. case x of (y, P) \<Rightarrow> P ko (the (ksPSpace b y))\<rbrakk> \<Longrightarrow> ekheap_relation ((ekheap a)(ptr \<mapsto> etcb)) ((ksPSpace b)(ptr \<mapsto> KOTCB tcb')) proof (prove)
goal (1 subgoal):
 1. \<And>a b ab ko y. \<lbrakk>ksPSpace b ptr = Some (KOTCB ab); is_aligned ptr 9; ps_clear ptr 9 b; obj_at' (\<lambda>ko. non_exst_same ko tcb') ptr b; obj_at' P ptr 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; ekheap a ptr = Some y; kheap a ptr = Some ko; case ko of TCB t \<Rightarrow> True | _ \<Rightarrow> False; 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>obj_relation_cuts ko ptr. case x of (y, P) \<Rightarrow> P ko (the (ksPSpace b y))\<rbrakk> \<Longrightarrow> \<forall>x\<in>dom (ekheap a). \<exists>tcb'a. ((ksPSpace b)(ptr \<mapsto> KOTCB tcb')) x = Some (KOTCB tcb'a) \<and> etcb_relation (the (((ekheap a)(ptr \<mapsto> etcb)) x)) tcb'a proof (prove)
goal (1 subgoal):
 1. \<And>a b ab ko y. \<lbrakk>ksPSpace b ptr = Some (KOTCB ab); is_aligned ptr 9; ps_clear ptr 9 b; obj_at' (\<lambda>ko. non_exst_same ko tcb') ptr b; obj_at' P ptr 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; ekheap a ptr = Some y; kheap a ptr = Some ko; case ko of TCB t \<Rightarrow> True | _ \<Rightarrow> False; 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>obj_relation_cuts ko ptr. case x of (y, P) \<Rightarrow> P ko (the (ksPSpace b y)); \<exists>tcb'. ksPSpace b ptr = Some (KOTCB tcb') \<and> etcb_relation (the (ekheap a ptr)) tcb'\<rbrakk> \<Longrightarrow> \<forall>x\<in>dom (ekheap a). \<exists>tcb'a. ((ksPSpace b)(ptr \<mapsto> KOTCB tcb')) x = Some (KOTCB tcb'a) \<and> etcb_relation (the (((ekheap a)(ptr \<mapsto> etcb)) x)) tcb'a proof (prove)
goal (1 subgoal):
 1. \<And>a b ab ko y x. \<lbrakk>ksPSpace b ptr = Some (KOTCB ab); is_aligned ptr 9; ps_clear ptr 9 b; obj_at' (\<lambda>ko. non_exst_same ko tcb') ptr b; obj_at' P ptr 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; ekheap a ptr = Some y; kheap a ptr = Some ko; case ko of TCB t \<Rightarrow> True | _ \<Rightarrow> False; 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>obj_relation_cuts ko ptr. case x of (y, P) \<Rightarrow> P ko (the (ksPSpace b y)); \<exists>tcb'. ksPSpace b ptr = Some (KOTCB tcb') \<and> etcb_relation (the (ekheap a ptr)) tcb'; x \<in> dom (ekheap a); \<exists>tcb'. ksPSpace b x = Some (KOTCB tcb') \<and> etcb_relation (the (ekheap a x)) tcb'\<rbrakk> \<Longrightarrow> \<exists>tcb'a. ((ksPSpace b)(ptr \<mapsto> KOTCB tcb')) x = Some (KOTCB tcb'a) \<and> etcb_relation (the (((ekheap a)(ptr \<mapsto> etcb)) x)) tcb'a proof (prove)
goal (1 subgoal):
 1. \<And>a b ab ko y x. \<lbrakk>ksPSpace b ptr = Some (KOTCB ab); is_aligned ptr 9; ps_clear ptr 9 b; obj_at' (\<lambda>ko. non_exst_same ko tcb') ptr b; obj_at' P ptr 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; ekheap a ptr = Some y; kheap a ptr = Some ko; case ko of TCB t \<Rightarrow> True | _ \<Rightarrow> False; 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>obj_relation_cuts ko ptr. case x of (y, P) \<Rightarrow> P ko (the (ksPSpace b y)); \<exists>tcb'. ksPSpace b ptr = Some (KOTCB tcb') \<and> etcb_relation (the (ekheap a ptr)) tcb'; \<exists>tcb'. ksPSpace b x = Some (KOTCB tcb') \<and> etcb_relation (the (ekheap a x)) tcb'; \<exists>b. ekheap a x = Some b\<rbrakk> \<Longrightarrow> \<exists>tcb'a. ((ksPSpace b)(ptr \<mapsto> KOTCB tcb')) x = Some (KOTCB tcb'a) \<and> etcb_relation (the (((ekheap a)(ptr \<mapsto> etcb)) x)) tcb'a proof (prove)
goal (1 subgoal):
 1. \<And>a b ab ko y obj obja. \<lbrakk>is_aligned ptr 9; ps_clear ptr 9 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; kheap a ptr = Some ko; case ko of TCB t \<Rightarrow> True | _ \<Rightarrow> False; 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>obj_relation_cuts ko ptr. case x of (y, P) \<Rightarrow> P ko (the (ksPSpace b y)); etcb_relation y ab; ekheap a ptr = Some y; is_aligned ptr (objBitsKO (KOTCB ab)); fst (projectKO (KOTCB ab) b) = {(obj, b)}; ksPSpace b ptr = Some (KOTCB ab); fst (projectKO (KOTCB ab) b) = {(obja, b)}; P obj; non_exst_same obja tcb'; ps_clear ptr (objBitsKO (KOTCB ab)) b\<rbrakk> \<Longrightarrow> etcb_relation etcb tcb' proof (prove)
goal (1 subgoal):
 1. \<And>a b ko y obj obja. \<lbrakk>is_aligned ptr 9; ps_clear ptr 9 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; kheap a ptr = Some ko; case ko of TCB t \<Rightarrow> True | _ \<Rightarrow> False; 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>obj_relation_cuts ko ptr. case x of (y, P) \<Rightarrow> P ko (the (ksPSpace b y)); etcb_relation y obja; ekheap a ptr = Some y; is_aligned ptr (objBitsKO (KOTCB obja)); projectKO_opt (KOTCB obja) = Some obj; ksPSpace b ptr = Some (KOTCB obja); P obj; non_exst_same obja tcb'; ps_clear ptr (objBitsKO (KOTCB obja)) b\<rbrakk> \<Longrightarrow> etcb_relation etcb tcb' proof (prove)
goal (1 subgoal):
 1. \<And>a b ko y obj obja. \<lbrakk>is_aligned ptr 9; ps_clear ptr 9 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; kheap a ptr = Some ko; case ko of TCB t \<Rightarrow> True | _ \<Rightarrow> False; 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>obj_relation_cuts ko ptr. case x of (y, P) \<Rightarrow> P ko (the (ksPSpace b y)); etcb_relation y obja; ekheap a ptr = Some y; is_aligned ptr (objBitsKO (KOTCB obja)); projectKO_opt (KOTCB obja) = Some obj; ksPSpace b ptr = Some (KOTCB obja); P obj; non_exst_same obja tcb'; ps_clear ptr (objBitsKO (KOTCB obja)) b; etcb_relation etcb tcb'\<rbrakk> \<Longrightarrow> etcb_relation etcb tcb' proof (prove)
goal:
No subgoals!