theory Finalise_R

lemma set_thread_all_corres:
  fixes ob' :: "'a :: pspace_storable"
  assumes x: "updateObject ob' = updateObject_default ob'"
  assumes z: "\<And>s. obj_at' P ptr s
               \<Longrightarrow> map_to_ctes ((ksPSpace s) (ptr \<mapsto> injectKO ob')) = map_to_ctes (ksPSpace s)"
  assumes b: "\<And>ko. P ko \<Longrightarrow> objBits ko = objBits ob'"
  assumes P: "\<And>(v::'a::pspace_storable). (1 :: word32) < 2 ^ (objBits v)"
  assumes e: "etcb_relation etcb tcb'"
  assumes is_t: "injectKO (ob' :: 'a :: pspace_storable) = KOTCB tcb'"
  shows      "other_obj_relation (TCB tcb) (injectKO (ob' :: 'a :: pspace_storable)) \<Longrightarrow>
  corres dc (obj_at (same_caps (TCB tcb)) ptr and is_etcb_at ptr)
            (obj_at' (P :: 'a \<Rightarrow> bool) ptr)
            (set_thread_all ptr tcb etcb) (setObject ptr ob')" apply (rule corres_no_failI) apply (rule no_fail_pre) apply wp apply (rule x) apply (clarsimp simp: b elim!: obj_at'_weakenE) apply (unfold set_thread_all_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 x
                        projectKOs
                        updateObject_default_def in_magnitude_check [OF _ P]) apply (clarsimp simp add: state_relation_def z) apply (simp add: trans_state_update'[symmetric] trans_state_update[symmetric]
         del: trans_state_update) apply (clarsimp simp add: swp_def fun_upd_def obj_at_def is_etcb_at_def) apply (subst cte_wp_at_after_update,fastforce simp add: obj_at_def) apply (subst caps_of_state_after_update,fastforce simp add: obj_at_def) apply clarsimp apply (subst conj_assoc[symmetric]) apply (rule conjI[rotated]) apply (clarsimp simp add: ghost_relation_def) apply (erule_tac x=ptr in allE)+ apply (clarsimp simp: obj_at_def
                   split: Structures_A.kernel_object.splits if_split_asm) apply (fold fun_upd_def) apply (simp only: pspace_relation_def dom_fun_upd2 simp_thms) apply (subst pspace_dom_update) apply assumption apply simp apply (simp only: 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 apply (frule_tac ko'="TCB tcb'" and x'=ptr in obj_relation_cut_same_type,
           (fastforce simp add: is_other_obj_relation_type)+)[1] 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 is_t) by (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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. other_obj_relation (TCB tcb) (injectKOS ob') \<Longrightarrow> corres dc (obj_at (same_caps (TCB tcb)) ptr and is_etcb_at ptr) (obj_at' P ptr) (set_thread_all ptr tcb etcb) (setObject ptr ob') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>other_obj_relation (TCB tcb) (injectKOS ob'); True\<rbrakk> \<Longrightarrow> no_fail (obj_at' P ptr) (setObject ptr ob')
 2. other_obj_relation (TCB tcb) (injectKOS ob') \<Longrightarrow> \<forall>(s, s')\<in>state_relation. (obj_at (same_caps (TCB tcb)) ptr and is_etcb_at ptr) s \<and> obj_at' P ptr s' \<longrightarrow> (\<forall>(r', t')\<in>fst (setObject ptr ob' s'). \<exists>(r, t)\<in>fst (set_thread_all ptr tcb etcb s). (t, t') \<in> state_relation \<and> dc r r') proof (prove)
goal (3 subgoals):
 1. \<lbrakk>other_obj_relation (TCB tcb) (injectKOS ob'); True\<rbrakk> \<Longrightarrow> no_fail ?P3 (setObject ptr ob')
 2. \<And>s. \<lbrakk>other_obj_relation (TCB tcb) (injectKOS ob'); True; obj_at' P ptr s\<rbrakk> \<Longrightarrow> ?P3 s
 3. other_obj_relation (TCB tcb) (injectKOS ob') \<Longrightarrow> \<forall>(s, s')\<in>state_relation. (obj_at (same_caps (TCB tcb)) ptr and is_etcb_at ptr) s \<and> obj_at' P ptr s' \<longrightarrow> (\<forall>(r', t')\<in>fst (setObject ptr ob' s'). \<exists>(r, t)\<in>fst (set_thread_all ptr tcb etcb s). (t, t') \<in> state_relation \<and> dc r r') proof (prove)
goal (3 subgoals):
 1. \<lbrakk>other_obj_relation (TCB tcb) (injectKOS ob'); True\<rbrakk> \<Longrightarrow> updateObject ob' = updateObject_default ob'
 2. \<And>s. \<lbrakk>other_obj_relation (TCB tcb) (injectKOS ob'); True; obj_at' P ptr s\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>k. objBits k = objBits ob') ptr s
 3. other_obj_relation (TCB tcb) (injectKOS ob') \<Longrightarrow> \<forall>(s, s')\<in>state_relation. (obj_at (same_caps (TCB tcb)) ptr and is_etcb_at ptr) s \<and> obj_at' P ptr s' \<longrightarrow> (\<forall>(r', t')\<in>fst (setObject ptr ob' s'). \<exists>(r, t)\<in>fst (set_thread_all ptr tcb etcb s). (t, t') \<in> state_relation \<and> dc r r') proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>other_obj_relation (TCB tcb) (injectKOS ob'); True; obj_at' P ptr s\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>k. objBits k = objBits ob') ptr s
 2. other_obj_relation (TCB tcb) (injectKOS ob') \<Longrightarrow> \<forall>(s, s')\<in>state_relation. (obj_at (same_caps (TCB tcb)) ptr and is_etcb_at ptr) s \<and> obj_at' P ptr s' \<longrightarrow> (\<forall>(r', t')\<in>fst (setObject ptr ob' s'). \<exists>(r, t)\<in>fst (set_thread_all ptr tcb etcb s). (t, t') \<in> state_relation \<and> dc r r') proof (prove)
goal (1 subgoal):
 1. other_obj_relation (TCB tcb) (injectKOS ob') \<Longrightarrow> \<forall>(s, s')\<in>state_relation. (obj_at (same_caps (TCB tcb)) ptr and is_etcb_at ptr) s \<and> obj_at' P ptr s' \<longrightarrow> (\<forall>(r', t')\<in>fst (setObject ptr ob' s'). \<exists>(r, t)\<in>fst (set_thread_all ptr tcb etcb s). (t, t') \<in> state_relation \<and> dc r r') proof (prove)
goal (1 subgoal):
 1. other_obj_relation (TCB tcb) (injectKOS ob') \<Longrightarrow> \<forall>(s, s')\<in>state_relation. (obj_at (same_caps (TCB tcb)) ptr and is_etcb_at ptr) s \<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 ob' 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 s <- get;
kh <- return $ (kheap s)(ptr \<mapsto> TCB tcb);
ekh <- return $ (ekheap s)(ptr \<mapsto> etcb);
put (ekheap_update (\<lambda>_. ekh) (s\<lparr>kheap := kh\<rparr>))
od) s). (t, t') \<in> state_relation \<and> dc r r') proof (prove)
goal (1 subgoal):
 1. \<And>a b ba ab. \<lbrakk>other_obj_relation (TCB tcb) (injectKOS ob'); (a, b) \<in> state_relation; ksPSpace b ptr = Some ba; projectKO_opt ba = Some ab; is_aligned ptr (objBits ob'); ps_clear ptr (objBits ob') b; obj_at (\<lambda>val. \<exists>tcb'. val = TCB tcb' \<and> (\<forall>x\<in>ran tcb_cap_cases. fst x tcb' = fst x tcb)) ptr a; is_etcb_at ptr a; obj_at' P ptr b\<rbrakk> \<Longrightarrow> (a\<lparr>ekheap := (ekheap a)(ptr \<mapsto> etcb), kheap := (kheap a)(ptr \<mapsto> TCB tcb)\<rparr>, b\<lparr>ksPSpace := (ksPSpace b)(ptr \<mapsto> injectKOS ob')\<rparr>) \<in> state_relation proof (prove)
goal (1 subgoal):
 1. \<And>a b ba ab. \<lbrakk>other_obj_relation (TCB tcb) (injectKOS ob'); ksPSpace b ptr = Some ba; projectKO_opt ba = Some ab; is_aligned ptr (objBits ob'); ps_clear ptr (objBits ob') b; obj_at (\<lambda>val. \<exists>tcb'. val = TCB tcb' \<and> (\<forall>x\<in>ran tcb_cap_cases. fst x tcb' = fst x tcb)) ptr a; is_etcb_at ptr a; 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)(ptr \<mapsto> TCB tcb)) ((ksPSpace b)(ptr \<mapsto> injectKOS ob')) \<and> ekheap_relation ((ekheap a)(ptr \<mapsto> etcb)) ((ksPSpace b)(ptr \<mapsto> injectKOS ob')) \<and> ghost_relation ((kheap a)(ptr \<mapsto> TCB tcb)) (gsUserPages b) (gsCNodes b) \<and> cdt_relation (swp (cte_wp_at (\<lambda>_. True)) (a\<lparr>ekheap := (ekheap a)(ptr \<mapsto> etcb), kheap := (kheap a)(ptr \<mapsto> TCB tcb)\<rparr>)) (cdt a) (ctes_of b) \<and> revokable_relation (is_original_cap a) (null_filter (caps_of_state (a\<lparr>kheap := (kheap a)(ptr \<mapsto> TCB tcb)\<rparr>))) (ctes_of b) proof (prove)
goal (1 subgoal):
 1. \<And>a b ba ab. \<lbrakk>other_obj_relation (TCB tcb) (injectKOS ob'); ksPSpace b ptr = Some ba; projectKO_opt ba = Some ab; is_aligned ptr (objBits ob'); ps_clear ptr (objBits ob') b; obj_at (\<lambda>val. \<exists>tcb'. val = TCB tcb' \<and> (\<forall>x\<in>ran tcb_cap_cases. fst x tcb' = fst x tcb)) ptr a; is_etcb_at ptr a; 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)(ptr \<mapsto> TCB tcb)) ((ksPSpace b)(ptr \<mapsto> injectKOS ob')) \<and> ekheap_relation ((ekheap a)(ptr \<mapsto> etcb)) ((ksPSpace b)(ptr \<mapsto> injectKOS ob')) \<and> ghost_relation ((kheap a)(ptr \<mapsto> TCB tcb)) (gsUserPages b) (gsCNodes b) \<and> cdt_relation (swp (cte_wp_at (\<lambda>_. True)) (a\<lparr>kheap := (kheap a)(ptr \<mapsto> TCB tcb)\<rparr>)) (cdt a) (ctes_of b) \<and> revokable_relation (is_original_cap a) (null_filter (caps_of_state (a\<lparr>kheap := (kheap a)(ptr \<mapsto> TCB tcb)\<rparr>))) (ctes_of b) proof (prove)
goal (1 subgoal):
 1. \<And>a b ba ab y tcb'. \<lbrakk>other_obj_relation (TCB tcb) (injectKOS ob'); ksPSpace b ptr = Some ba; projectKO_opt ba = Some ab; is_aligned ptr (objBits ob'); ps_clear ptr (objBits ob') 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 (\<lambda>y. cte_wp_at (\<lambda>_. True) y 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 (TCB tcb'); \<forall>x\<in>ran tcb_cap_cases. fst x tcb' = fst x tcb\<rbrakk> \<Longrightarrow> pspace_relation (\<lambda>x. if x = ptr then Some (TCB tcb) else kheap a x) (\<lambda>x. if x = ptr then Some (injectKOS ob') else ksPSpace b x) \<and> ekheap_relation (\<lambda>x. if x = ptr then Some etcb else ekheap a x) (\<lambda>x. if x = ptr then Some (injectKOS ob') else ksPSpace b x) \<and> ghost_relation (\<lambda>x. if x = ptr then Some (TCB tcb) else kheap a x) (gsUserPages b) (gsCNodes b) \<and> cdt_relation (\<lambda>y. cte_wp_at (\<lambda>_. True) y (a\<lparr>kheap := \<lambda>x. if x = ptr then Some (TCB tcb) else kheap a x\<rparr>)) (cdt a) (ctes_of b) \<and> revokable_relation (is_original_cap a) (null_filter (caps_of_state (a\<lparr>kheap := \<lambda>x. if x = ptr then Some (TCB tcb) else kheap a x\<rparr>))) (ctes_of b) proof (prove)
goal (1 subgoal):
 1. \<And>a b ba ab y tcb'. \<lbrakk>other_obj_relation (TCB tcb) (injectKOS ob'); ksPSpace b ptr = Some ba; projectKO_opt ba = Some ab; is_aligned ptr (objBits ob'); ps_clear ptr (objBits ob') 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 (\<lambda>y. cte_wp_at (\<lambda>_. True) y 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 (TCB tcb'); \<forall>x\<in>ran tcb_cap_cases. fst x tcb' = fst x tcb\<rbrakk> \<Longrightarrow> pspace_relation (\<lambda>x. if x = ptr then Some (TCB tcb) else kheap a x) (\<lambda>x. if x = ptr then Some (injectKOS ob') else ksPSpace b x) \<and> ekheap_relation (\<lambda>x. if x = ptr then Some etcb else ekheap a x) (\<lambda>x. if x = ptr then Some (injectKOS ob') else ksPSpace b x) \<and> ghost_relation (\<lambda>x. if x = ptr then Some (TCB tcb) else kheap a x) (gsUserPages b) (gsCNodes b) \<and> cdt_relation (\<lambda>y. cte_wp_at (\<lambda>_. True) y a) (cdt a) (ctes_of b) \<and> revokable_relation (is_original_cap a) (null_filter (caps_of_state (a\<lparr>kheap := \<lambda>x. if x = ptr then Some (TCB tcb) else kheap a x\<rparr>))) (ctes_of b) proof (prove)
goal (1 subgoal):
 1. \<And>a b ba ab y tcb'. \<lbrakk>other_obj_relation (TCB tcb) (injectKOS ob'); ksPSpace b ptr = Some ba; projectKO_opt ba = Some ab; is_aligned ptr (objBits ob'); ps_clear ptr (objBits ob') 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 (\<lambda>y. cte_wp_at (\<lambda>_. True) y 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 (TCB tcb'); \<forall>x\<in>ran tcb_cap_cases. fst x tcb' = fst x tcb\<rbrakk> \<Longrightarrow> pspace_relation (\<lambda>x. if x = ptr then Some (TCB tcb) else kheap a x) (\<lambda>x. if x = ptr then Some (injectKOS ob') else ksPSpace b x) \<and> ekheap_relation (\<lambda>x. if x = ptr then Some etcb else ekheap a x) (\<lambda>x. if x = ptr then Some (injectKOS ob') else ksPSpace b x) \<and> ghost_relation (\<lambda>x. if x = ptr then Some (TCB tcb) else kheap a x) (gsUserPages b) (gsCNodes b) \<and> cdt_relation (\<lambda>y. cte_wp_at (\<lambda>_. True) y a) (cdt a) (ctes_of b) \<and> revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of b) proof (prove)
goal (1 subgoal):
 1. \<And>a b ba ab y tcb'. \<lbrakk>other_obj_relation (TCB tcb) (injectKOS ob'); ksPSpace b ptr = Some ba; projectKO_opt ba = Some ab; is_aligned ptr (objBits ob'); ps_clear ptr (objBits ob') 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 (\<lambda>y. cte_wp_at (\<lambda>_. True) y 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 (TCB tcb'); \<forall>x\<in>ran tcb_cap_cases. fst x tcb' = fst x tcb\<rbrakk> \<Longrightarrow> pspace_relation (\<lambda>x. if x = ptr then Some (TCB tcb) else kheap a x) (\<lambda>x. if x = ptr then Some (injectKOS ob') else ksPSpace b x) \<and> ekheap_relation (\<lambda>x. if x = ptr then Some etcb else ekheap a x) (\<lambda>x. if x = ptr then Some (injectKOS ob') else ksPSpace b x) \<and> ghost_relation (\<lambda>x. if x = ptr then Some (TCB tcb) else kheap a x) (gsUserPages b) (gsCNodes b) proof (prove)
goal (1 subgoal):
 1. \<And>a b ba ab y tcb'. \<lbrakk>other_obj_relation (TCB tcb) (injectKOS ob'); ksPSpace b ptr = Some ba; projectKO_opt ba = Some ab; is_aligned ptr (objBits ob'); ps_clear ptr (objBits ob') 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 (\<lambda>y. cte_wp_at (\<lambda>_. True) y 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 (TCB tcb'); \<forall>x\<in>ran tcb_cap_cases. fst x tcb' = fst x tcb\<rbrakk> \<Longrightarrow> (pspace_relation (\<lambda>x. if x = ptr then Some (TCB tcb) else kheap a x) (\<lambda>x. if x = ptr then Some (injectKOS ob') else ksPSpace b x) \<and> ekheap_relation (\<lambda>x. if x = ptr then Some etcb else ekheap a x) (\<lambda>x. if x = ptr then Some (injectKOS ob') else ksPSpace b x)) \<and> ghost_relation (\<lambda>x. if x = ptr then Some (TCB tcb) else kheap a x) (gsUserPages b) (gsCNodes b) proof (prove)
goal (2 subgoals):
 1. \<And>a b ba ab y tcb'. \<lbrakk>other_obj_relation (TCB tcb) (injectKOS ob'); ksPSpace b ptr = Some ba; projectKO_opt ba = Some ab; is_aligned ptr (objBits ob'); ps_clear ptr (objBits ob') 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 (\<lambda>y. cte_wp_at (\<lambda>_. True) y 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 (TCB tcb'); \<forall>x\<in>ran tcb_cap_cases. fst x tcb' = fst x tcb\<rbrakk> \<Longrightarrow> ghost_relation (\<lambda>x. if x = ptr then Some (TCB tcb) else kheap a x) (gsUserPages b) (gsCNodes b)
 2. \<And>a b ba ab y tcb'. \<lbrakk>other_obj_relation (TCB tcb) (injectKOS ob'); ksPSpace b ptr = Some ba; projectKO_opt ba = Some ab; is_aligned ptr (objBits ob'); ps_clear ptr (objBits ob') 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 (\<lambda>y. cte_wp_at (\<lambda>_. True) y 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 (TCB tcb'); \<forall>x\<in>ran tcb_cap_cases. fst x tcb' = fst x tcb\<rbrakk> \<Longrightarrow> pspace_relation (\<lambda>x. if x = ptr then Some (TCB tcb) else kheap a x) (\<lambda>x. if x = ptr then Some (injectKOS ob') else ksPSpace b x) \<and> ekheap_relation (\<lambda>x. if x = ptr then Some etcb else ekheap a x) (\<lambda>x. if x = ptr then Some (injectKOS ob') else ksPSpace b x) proof (prove)
goal (2 subgoals):
 1. \<And>a b ba ab y tcb'. \<lbrakk>other_obj_relation (TCB tcb) (injectKOS ob'); ksPSpace b ptr = Some ba; projectKO_opt ba = Some ab; is_aligned ptr (objBits ob'); ps_clear ptr (objBits ob') 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); cdt_relation (\<lambda>y. cte_wp_at (\<lambda>_. True) y 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 (TCB tcb'); \<forall>x\<in>ran tcb_cap_cases. fst x tcb' = fst x tcb; \<forall>aa sz. (\<exists>dev. kheap a aa = Some (ArchObj (DataPage dev sz))) = (gsUserPages b aa = Some sz); \<forall>aa n. (\<exists>cs. kheap a aa = Some (CNode n cs) \<and> well_formed_cnode_n n cs) = (gsCNodes b aa = Some n)\<rbrakk> \<Longrightarrow> gsUserPages b ptr = None \<and> gsCNodes b ptr = None
 2. \<And>a b ba ab y tcb'. \<lbrakk>other_obj_relation (TCB tcb) (injectKOS ob'); ksPSpace b ptr = Some ba; projectKO_opt ba = Some ab; is_aligned ptr (objBits ob'); ps_clear ptr (objBits ob') 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 (\<lambda>y. cte_wp_at (\<lambda>_. True) y 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 (TCB tcb'); \<forall>x\<in>ran tcb_cap_cases. fst x tcb' = fst x tcb\<rbrakk> \<Longrightarrow> pspace_relation (\<lambda>x. if x = ptr then Some (TCB tcb) else kheap a x) (\<lambda>x. if x = ptr then Some (injectKOS ob') else ksPSpace b x) \<and> ekheap_relation (\<lambda>x. if x = ptr then Some etcb else ekheap a x) (\<lambda>x. if x = ptr then Some (injectKOS ob') else ksPSpace b x) proof (prove)
goal (2 subgoals):
 1. \<And>a b ba ab y tcb'. \<lbrakk>other_obj_relation (TCB tcb) (injectKOS ob'); ksPSpace b ptr = Some ba; projectKO_opt ba = Some ab; is_aligned ptr (objBits ob'); ps_clear ptr (objBits ob') 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); cdt_relation (\<lambda>y. cte_wp_at (\<lambda>_. True) y 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 (TCB tcb'); \<forall>x\<in>ran tcb_cap_cases. fst x tcb' = fst x tcb; \<forall>sz. (\<exists>dev. kheap a ptr = Some (ArchObj (DataPage dev sz))) = (gsUserPages b ptr = Some sz); \<forall>n. (\<exists>cs. kheap a ptr = Some (CNode n cs) \<and> well_formed_cnode_n n cs) = (gsCNodes b ptr = Some n)\<rbrakk> \<Longrightarrow> gsUserPages b ptr = None \<and> gsCNodes b ptr = None
 2. \<And>a b ba ab y tcb'. \<lbrakk>other_obj_relation (TCB tcb) (injectKOS ob'); ksPSpace b ptr = Some ba; projectKO_opt ba = Some ab; is_aligned ptr (objBits ob'); ps_clear ptr (objBits ob') 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 (\<lambda>y. cte_wp_at (\<lambda>_. True) y 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 (TCB tcb'); \<forall>x\<in>ran tcb_cap_cases. fst x tcb' = fst x tcb\<rbrakk> \<Longrightarrow> pspace_relation (\<lambda>x. if x = ptr then Some (TCB tcb) else kheap a x) (\<lambda>x. if x = ptr then Some (injectKOS ob') else ksPSpace b x) \<and> ekheap_relation (\<lambda>x. if x = ptr then Some etcb else ekheap a x) (\<lambda>x. if x = ptr then Some (injectKOS ob') else ksPSpace b x) proof (prove)
goal (1 subgoal):
 1. \<And>a b ba ab y tcb'. \<lbrakk>other_obj_relation (TCB tcb) (injectKOS ob'); ksPSpace b ptr = Some ba; projectKO_opt ba = Some ab; is_aligned ptr (objBits ob'); ps_clear ptr (objBits ob') 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 (\<lambda>y. cte_wp_at (\<lambda>_. True) y 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 (TCB tcb'); \<forall>x\<in>ran tcb_cap_cases. fst x tcb' = fst x tcb\<rbrakk> \<Longrightarrow> pspace_relation (\<lambda>x. if x = ptr then Some (TCB tcb) else kheap a x) (\<lambda>x. if x = ptr then Some (injectKOS ob') else ksPSpace b x) \<and> ekheap_relation (\<lambda>x. if x = ptr then Some etcb else ekheap a x) (\<lambda>x. if x = ptr then Some (injectKOS ob') else ksPSpace b x) proof (prove)
goal (1 subgoal):
 1. \<And>a b ba ab y tcb'. \<lbrakk>other_obj_relation (TCB tcb) (injectKOS ob'); ksPSpace b ptr = Some ba; projectKO_opt ba = Some ab; is_aligned ptr (objBits ob'); ps_clear ptr (objBits ob') 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 (\<lambda>y. cte_wp_at (\<lambda>_. True) y 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 (TCB tcb'); \<forall>x\<in>ran tcb_cap_cases. fst x tcb' = fst x tcb\<rbrakk> \<Longrightarrow> pspace_relation ((kheap a)(ptr \<mapsto> TCB tcb)) ((ksPSpace b)(ptr \<mapsto> injectKOS ob')) \<and> ekheap_relation ((ekheap a)(ptr \<mapsto> etcb)) ((ksPSpace b)(ptr \<mapsto> injectKOS ob')) proof (prove)
goal (1 subgoal):
 1. \<And>a b ba ab y tcb'. \<lbrakk>other_obj_relation (TCB tcb) (injectKOS ob'); ksPSpace b ptr = Some ba; projectKO_opt ba = Some ab; is_aligned ptr (objBits ob'); ps_clear ptr (objBits ob') 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 (\<lambda>y. cte_wp_at (\<lambda>_. True) y 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 (TCB tcb'); \<forall>x\<in>ran tcb_cap_cases. fst x tcb' = fst x tcb\<rbrakk> \<Longrightarrow> (pspace_dom ((kheap a)(ptr \<mapsto> TCB tcb)) = dom (ksPSpace b) \<and> (\<forall>x\<in>dom (kheap a). \<forall>(y, P)\<in>obj_relation_cuts (the (((kheap a)(ptr \<mapsto> TCB tcb)) x)) x. P (the (((kheap a)(ptr \<mapsto> TCB tcb)) x)) (the (((ksPSpace b)(ptr \<mapsto> injectKOS ob')) y)))) \<and> ekheap_relation ((ekheap a)(ptr \<mapsto> etcb)) ((ksPSpace b)(ptr \<mapsto> injectKOS ob')) proof (prove)
goal (3 subgoals):
 1. \<And>a b ba ab y tcb'. \<lbrakk>other_obj_relation (TCB tcb) (injectKOS ob'); ksPSpace b ptr = Some ba; projectKO_opt ba = Some ab; is_aligned ptr (objBits ob'); ps_clear ptr (objBits ob') 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 (\<lambda>y. cte_wp_at (\<lambda>_. True) y 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 (TCB tcb'); \<forall>x\<in>ran tcb_cap_cases. fst x tcb' = fst x tcb\<rbrakk> \<Longrightarrow> kheap a ptr = Some (?x162 a b ba ab y tcb')
 2. \<And>a b ba ab y tcb'. \<lbrakk>other_obj_relation (TCB tcb) (injectKOS ob'); ksPSpace b ptr = Some ba; projectKO_opt ba = Some ab; is_aligned ptr (objBits ob'); ps_clear ptr (objBits ob') 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 (\<lambda>y. cte_wp_at (\<lambda>_. True) y 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 (TCB tcb'); \<forall>x\<in>ran tcb_cap_cases. fst x tcb' = fst x tcb\<rbrakk> \<Longrightarrow> a_type (?x162 a b ba ab y tcb') = a_type (TCB tcb)
 3. \<And>a b ba ab y tcb'. \<lbrakk>other_obj_relation (TCB tcb) (injectKOS ob'); ksPSpace b ptr = Some ba; projectKO_opt ba = Some ab; is_aligned ptr (objBits ob'); ps_clear ptr (objBits ob') 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 (\<lambda>y. cte_wp_at (\<lambda>_. True) y 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 (TCB tcb'); \<forall>x\<in>ran tcb_cap_cases. fst x tcb' = fst x tcb\<rbrakk> \<Longrightarrow> (pspace_dom (kheap a) = dom (ksPSpace b) \<and> (\<forall>x\<in>dom (kheap a). \<forall>(y, P)\<in>obj_relation_cuts (the (((kheap a)(ptr \<mapsto> TCB tcb)) x)) x. P (the (((kheap a)(ptr \<mapsto> TCB tcb)) x)) (the (((ksPSpace b)(ptr \<mapsto> injectKOS ob')) y)))) \<and> ekheap_relation ((ekheap a)(ptr \<mapsto> etcb)) ((ksPSpace b)(ptr \<mapsto> injectKOS ob')) proof (prove)
goal (2 subgoals):
 1. \<And>a b ba ab y tcb'. \<lbrakk>other_obj_relation (TCB tcb) (injectKOS ob'); ksPSpace b ptr = Some ba; projectKO_opt ba = Some ab; is_aligned ptr (objBits ob'); ps_clear ptr (objBits ob') 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 (\<lambda>y. cte_wp_at (\<lambda>_. True) y 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 (TCB tcb'); \<forall>x\<in>ran tcb_cap_cases. fst x tcb' = fst x tcb\<rbrakk> \<Longrightarrow> a_type (TCB tcb') = a_type (TCB tcb)
 2. \<And>a b ba ab y tcb'. \<lbrakk>other_obj_relation (TCB tcb) (injectKOS ob'); ksPSpace b ptr = Some ba; projectKO_opt ba = Some ab; is_aligned ptr (objBits ob'); ps_clear ptr (objBits ob') 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 (\<lambda>y. cte_wp_at (\<lambda>_. True) y 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 (TCB tcb'); \<forall>x\<in>ran tcb_cap_cases. fst x tcb' = fst x tcb\<rbrakk> \<Longrightarrow> (pspace_dom (kheap a) = dom (ksPSpace b) \<and> (\<forall>x\<in>dom (kheap a). \<forall>(y, P)\<in>obj_relation_cuts (the (((kheap a)(ptr \<mapsto> TCB tcb)) x)) x. P (the (((kheap a)(ptr \<mapsto> TCB tcb)) x)) (the (((ksPSpace b)(ptr \<mapsto> injectKOS ob')) y)))) \<and> ekheap_relation ((ekheap a)(ptr \<mapsto> etcb)) ((ksPSpace b)(ptr \<mapsto> injectKOS ob')) proof (prove)
goal (1 subgoal):
 1. \<And>a b ba ab y tcb'. \<lbrakk>other_obj_relation (TCB tcb) (injectKOS ob'); ksPSpace b ptr = Some ba; projectKO_opt ba = Some ab; is_aligned ptr (objBits ob'); ps_clear ptr (objBits ob') 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 (\<lambda>y. cte_wp_at (\<lambda>_. True) y 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 (TCB tcb'); \<forall>x\<in>ran tcb_cap_cases. fst x tcb' = fst x tcb\<rbrakk> \<Longrightarrow> (pspace_dom (kheap a) = dom (ksPSpace b) \<and> (\<forall>x\<in>dom (kheap a). \<forall>(y, P)\<in>obj_relation_cuts (the (((kheap a)(ptr \<mapsto> TCB tcb)) x)) x. P (the (((kheap a)(ptr \<mapsto> TCB tcb)) x)) (the (((ksPSpace b)(ptr \<mapsto> injectKOS ob')) y)))) \<and> ekheap_relation ((ekheap a)(ptr \<mapsto> etcb)) ((ksPSpace b)(ptr \<mapsto> injectKOS ob')) proof (prove)
goal (1 subgoal):
 1. \<And>a b ba ab y tcb'. \<lbrakk>other_obj_relation (TCB tcb) (injectKOS ob'); ksPSpace b ptr = Some ba; projectKO_opt ba = Some ab; is_aligned ptr (objBits ob'); ps_clear ptr (objBits ob') 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 (\<lambda>y. cte_wp_at (\<lambda>_. True) y 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 (TCB tcb'); \<forall>x\<in>ran tcb_cap_cases. fst x tcb' = fst x tcb\<rbrakk> \<Longrightarrow> (\<forall>x\<in>dom (kheap a). \<forall>(y, P)\<in>obj_relation_cuts (the (((kheap a)(ptr \<mapsto> TCB tcb)) x)) x. P (the (((kheap a)(ptr \<mapsto> TCB tcb)) x)) (the (((ksPSpace b)(ptr \<mapsto> injectKOS ob')) y))) \<and> ekheap_relation ((ekheap a)(ptr \<mapsto> etcb)) ((ksPSpace b)(ptr \<mapsto> injectKOS ob')) proof (prove)
goal (1 subgoal):
 1. \<And>a b ba ab y tcb'. \<lbrakk>other_obj_relation (TCB tcb) (injectKOS ob'); ksPSpace b ptr = Some ba; projectKO_opt ba = Some ab; is_aligned ptr (objBits ob'); ps_clear ptr (objBits ob') 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 (\<lambda>y. cte_wp_at (\<lambda>_. True) y 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 (TCB tcb'); \<forall>x\<in>ran tcb_cap_cases. fst x tcb' = fst x tcb; 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)(ptr \<mapsto> TCB tcb)) x)) x. P (the (((kheap a)(ptr \<mapsto> TCB tcb)) x)) (the (((ksPSpace b)(ptr \<mapsto> injectKOS ob')) y))) \<and> ekheap_relation ((ekheap a)(ptr \<mapsto> etcb)) ((ksPSpace b)(ptr \<mapsto> injectKOS ob')) proof (prove)
goal (1 subgoal):
 1. \<And>a b ba ab y tcb'. \<lbrakk>other_obj_relation (TCB tcb) (injectKOS ob'); ksPSpace b ptr = Some ba; projectKO_opt ba = Some ab; is_aligned ptr (objBits ob'); ps_clear ptr (objBits ob') 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 (\<lambda>y. cte_wp_at (\<lambda>_. True) y 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 (TCB tcb'); \<forall>x\<in>ran tcb_cap_cases. fst x tcb' = fst x tcb; 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)(ptr \<mapsto> TCB tcb)) x)) x. P (the (((kheap a)(ptr \<mapsto> TCB tcb)) x)) (the (((ksPSpace b)(ptr \<mapsto> injectKOS ob')) y))) \<and> ekheap_relation ((ekheap a)(ptr \<mapsto> etcb)) ((ksPSpace b)(ptr \<mapsto> injectKOS ob')) proof (prove)
goal (2 subgoals):
 1. \<And>a b ba ab y tcb'. \<lbrakk>other_obj_relation (TCB tcb) (injectKOS ob'); ksPSpace b ptr = Some ba; projectKO_opt ba = Some ab; is_aligned ptr (objBits ob'); ps_clear ptr (objBits ob') 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 (\<lambda>y. cte_wp_at (\<lambda>_. True) y 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 (TCB tcb'); \<forall>x\<in>ran tcb_cap_cases. fst x tcb' = fst x tcb; 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)(ptr \<mapsto> TCB tcb)) x)) x. P (the (((kheap a)(ptr \<mapsto> TCB tcb)) x)) (the (((ksPSpace b)(ptr \<mapsto> injectKOS ob')) y))
 2. \<And>a b ba ab y tcb'. \<lbrakk>other_obj_relation (TCB tcb) (injectKOS ob'); ksPSpace b ptr = Some ba; projectKO_opt ba = Some ab; is_aligned ptr (objBits ob'); ps_clear ptr (objBits ob') 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 (\<lambda>y. cte_wp_at (\<lambda>_. True) y 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 (TCB tcb'); \<forall>x\<in>ran tcb_cap_cases. fst x tcb' = fst x tcb; 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> injectKOS ob')) proof (prove)
goal (2 subgoals):
 1. \<And>a b ba ab y tcb' x. \<lbrakk>other_obj_relation (TCB tcb) (injectKOS ob'); ksPSpace b ptr = Some ba; projectKO_opt ba = Some ab; is_aligned ptr (objBits ob'); ps_clear ptr (objBits ob') 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 (\<lambda>y. cte_wp_at (\<lambda>_. True) y 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 (TCB tcb'); \<forall>x\<in>ran tcb_cap_cases. fst x tcb' = fst x tcb; 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)(ptr \<mapsto> TCB tcb)) x)) x. P (the (((kheap a)(ptr \<mapsto> TCB tcb)) x)) (the (((ksPSpace b)(ptr \<mapsto> injectKOS ob')) y))
 2. \<And>a b ba ab y tcb'. \<lbrakk>other_obj_relation (TCB tcb) (injectKOS ob'); ksPSpace b ptr = Some ba; projectKO_opt ba = Some ab; is_aligned ptr (objBits ob'); ps_clear ptr (objBits ob') 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 (\<lambda>y. cte_wp_at (\<lambda>_. True) y 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 (TCB tcb'); \<forall>x\<in>ran tcb_cap_cases. fst x tcb' = fst x tcb; 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> injectKOS ob')) proof (prove)
goal (2 subgoals):
 1. \<And>a b ba ab y tcb' x. \<lbrakk>other_obj_relation (TCB tcb) (injectKOS ob'); ksPSpace b ptr = Some ba; projectKO_opt ba = Some ab; is_aligned ptr (objBits ob'); ps_clear ptr (objBits ob') 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 (\<lambda>y. cte_wp_at (\<lambda>_. True) y 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 (TCB tcb'); \<forall>x\<in>ran tcb_cap_cases. fst x tcb' = fst x tcb; 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)(ptr \<mapsto> TCB tcb)) x)) x. P (the (((kheap a)(ptr \<mapsto> TCB tcb)) x)) (the (((ksPSpace b)(ptr \<mapsto> injectKOS ob')) y))
 2. \<And>a b ba ab y tcb'. \<lbrakk>other_obj_relation (TCB tcb) (injectKOS ob'); ksPSpace b ptr = Some ba; projectKO_opt ba = Some ab; is_aligned ptr (objBits ob'); ps_clear ptr (objBits ob') 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 (\<lambda>y. cte_wp_at (\<lambda>_. True) y 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 (TCB tcb'); \<forall>x\<in>ran tcb_cap_cases. fst x tcb' = fst x tcb; 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> injectKOS ob')) proof (prove)
goal (2 subgoals):
 1. \<And>a b ba ab y tcb' x bb aa bc. \<lbrakk>other_obj_relation (TCB tcb) (injectKOS ob'); ksPSpace b ptr = Some ba; projectKO_opt ba = Some ab; is_aligned ptr (objBits ob'); ps_clear ptr (objBits ob') 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 (\<lambda>y. cte_wp_at (\<lambda>_. True) y 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 (TCB tcb'); \<forall>x\<in>ran tcb_cap_cases. fst x tcb' = fst x tcb; pspace_dom (kheap a) = dom (ksPSpace b); other_obj_relation (TCB tcb') ba; \<forall>x\<in>obj_relation_cuts bb x. case x of (y, P) \<Rightarrow> P bb (the (ksPSpace b y)); kheap a x = Some bb; x \<noteq> ptr; (aa, bc) \<in> obj_relation_cuts bb x\<rbrakk> \<Longrightarrow> (aa = ptr \<longrightarrow> bc bb (injectKOS ob')) \<and> (aa \<noteq> ptr \<longrightarrow> bc bb (the (ksPSpace b aa)))
 2. \<And>a b ba ab y tcb'. \<lbrakk>other_obj_relation (TCB tcb) (injectKOS ob'); ksPSpace b ptr = Some ba; projectKO_opt ba = Some ab; is_aligned ptr (objBits ob'); ps_clear ptr (objBits ob') 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 (\<lambda>y. cte_wp_at (\<lambda>_. True) y 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 (TCB tcb'); \<forall>x\<in>ran tcb_cap_cases. fst x tcb' = fst x tcb; 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> injectKOS ob')) proof (prove)
goal (2 subgoals):
 1. \<And>a b ba ab y tcb' x bb aa bc. \<lbrakk>other_obj_relation (TCB tcb) (injectKOS ob'); ksPSpace b ptr = Some ba; projectKO_opt ba = Some ab; is_aligned ptr (objBits ob'); ps_clear ptr (objBits ob') 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 (\<lambda>y. cte_wp_at (\<lambda>_. True) y 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 (TCB tcb'); \<forall>x\<in>ran tcb_cap_cases. fst x tcb' = fst x tcb; pspace_dom (kheap a) = dom (ksPSpace b); other_obj_relation (TCB tcb') ba; kheap a x = Some bb; x \<noteq> ptr; (aa, bc) \<in> obj_relation_cuts bb x; case (aa, bc) of (y, P) \<Rightarrow> P bb (the (ksPSpace b y))\<rbrakk> \<Longrightarrow> (aa = ptr \<longrightarrow> bc bb (injectKOS ob')) \<and> (aa \<noteq> ptr \<longrightarrow> bc bb (the (ksPSpace b aa)))
 2. \<And>a b ba ab y tcb'. \<lbrakk>other_obj_relation (TCB tcb) (injectKOS ob'); ksPSpace b ptr = Some ba; projectKO_opt ba = Some ab; is_aligned ptr (objBits ob'); ps_clear ptr (objBits ob') 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 (\<lambda>y. cte_wp_at (\<lambda>_. True) y 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 (TCB tcb'); \<forall>x\<in>ran tcb_cap_cases. fst x tcb' = fst x tcb; 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> injectKOS ob')) proof (prove)
goal (2 subgoals):
 1. \<And>a b ba ab y tcb' x bb bc. \<lbrakk>other_obj_relation (TCB tcb) (injectKOS ob'); ksPSpace b ptr = Some ba; projectKO_opt ba = Some ab; is_aligned ptr (objBits ob'); ps_clear ptr (objBits ob') 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 (\<lambda>y. cte_wp_at (\<lambda>_. True) y 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 (TCB tcb'); \<forall>x\<in>ran tcb_cap_cases. fst x tcb' = fst x tcb; pspace_dom (kheap a) = dom (ksPSpace b); other_obj_relation (TCB tcb') ba; kheap a x = Some bb; x \<noteq> ptr; (ptr, bc) \<in> obj_relation_cuts bb x; bc bb ba\<rbrakk> \<Longrightarrow> bc bb (injectKOS ob')
 2. \<And>a b ba ab y tcb'. \<lbrakk>other_obj_relation (TCB tcb) (injectKOS ob'); ksPSpace b ptr = Some ba; projectKO_opt ba = Some ab; is_aligned ptr (objBits ob'); ps_clear ptr (objBits ob') 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 (\<lambda>y. cte_wp_at (\<lambda>_. True) y 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 (TCB tcb'); \<forall>x\<in>ran tcb_cap_cases. fst x tcb' = fst x tcb; 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> injectKOS ob')) proof (prove)
goal (1 subgoal):
 1. \<And>a b ba ab y tcb'. \<lbrakk>other_obj_relation (TCB tcb) (injectKOS ob'); ksPSpace b ptr = Some ba; projectKO_opt ba = Some ab; is_aligned ptr (objBits ob'); ps_clear ptr (objBits ob') 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 (\<lambda>y. cte_wp_at (\<lambda>_. True) y 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 (TCB tcb'); \<forall>x\<in>ran tcb_cap_cases. fst x tcb' = fst x tcb; 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> injectKOS ob')) proof (prove)
goal (1 subgoal):
 1. \<And>a b ba ab y tcb'. \<lbrakk>other_obj_relation (TCB tcb) (injectKOS ob'); ksPSpace b ptr = Some ba; projectKO_opt ba = Some ab; is_aligned ptr (objBits ob'); ps_clear ptr (objBits ob') 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 (\<lambda>y. cte_wp_at (\<lambda>_. True) y 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 (TCB tcb'); \<forall>x\<in>ran tcb_cap_cases. fst x tcb' = fst x tcb; 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 (Some (TCB tcb'))) ptr. P (the (Some (TCB tcb'))) (the (ksPSpace b y))\<rbrakk> \<Longrightarrow> \<forall>x\<in>dom (ekheap a). \<exists>tcb'. ((ksPSpace b)(ptr \<mapsto> injectKOS ob')) x = Some (KOTCB tcb') \<and> etcb_relation (the (((ekheap a)(ptr \<mapsto> etcb)) x)) tcb' proof (prove)
goal (1 subgoal):
 1. \<And>a b ba ab y tcb'. \<lbrakk>other_obj_relation (TCB tcb) (injectKOS ob'); ksPSpace b ptr = Some ba; projectKO_opt ba = Some ab; is_aligned ptr (objBits ob'); ps_clear ptr (objBits ob') 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 (\<lambda>y. cte_wp_at (\<lambda>_. True) y 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 (TCB tcb'); \<forall>x\<in>ran tcb_cap_cases. fst x tcb' = fst x tcb; 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 (Some (TCB tcb'))) ptr. P (the (Some (TCB tcb'))) (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'. ((ksPSpace b)(ptr \<mapsto> injectKOS ob')) x = Some (KOTCB tcb') \<and> etcb_relation (the (((ekheap a)(ptr \<mapsto> etcb)) x)) tcb' proof (prove)
goal (1 subgoal):
 1. \<And>a b ba ab y tcb' x. \<lbrakk>other_obj_relation (TCB tcb) (injectKOS ob'); ksPSpace b ptr = Some ba; projectKO_opt ba = Some ab; is_aligned ptr (objBits ob'); ps_clear ptr (objBits ob') 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 (\<lambda>y. cte_wp_at (\<lambda>_. True) y 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 (TCB tcb'); \<forall>x\<in>ran tcb_cap_cases. fst x tcb' = fst x tcb; 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 (Some (TCB tcb'))) ptr. P (the (Some (TCB tcb'))) (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'. ((ksPSpace b)(ptr \<mapsto> injectKOS ob')) x = Some (KOTCB tcb') \<and> etcb_relation (the (((ekheap a)(ptr \<mapsto> etcb)) x)) tcb' proof (prove)
goal (1 subgoal):
 1. \<And>a b ba ab y tcb' x. \<lbrakk>other_obj_relation (TCB tcb) (injectKOS ob'); ksPSpace b ptr = Some ba; projectKO_opt ba = Some ab; is_aligned ptr (objBits ob'); ps_clear ptr (objBits ob') 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 (\<lambda>y. cte_wp_at (\<lambda>_. True) y 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 (TCB tcb'); \<forall>x\<in>ran tcb_cap_cases. fst x tcb' = fst x tcb; 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 (Some (TCB tcb'))) ptr. P (the (Some (TCB tcb'))) (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'. ((ksPSpace b)(ptr \<mapsto> injectKOS ob')) x = Some (KOTCB tcb') \<and> etcb_relation (the (((ekheap a)(ptr \<mapsto> etcb)) x)) tcb' proof (prove)
goal (1 subgoal):
 1. \<And>a b ab y tcb' tcb'a obj. \<lbrakk>other_obj_relation (TCB tcb) (injectKOS ob'); projectKO_opt (KOTCB tcb'a) = Some ab; is_aligned ptr (objBits ob'); ps_clear ptr (objBits ob') 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 (\<lambda>y. cte_wp_at (\<lambda>_. True) y 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 (TCB tcb'); \<forall>x\<in>ran tcb_cap_cases. fst x tcb' = fst x tcb; 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)); other_obj_relation (TCB tcb') (KOTCB tcb'a); ekheap a ptr = Some y; is_aligned ptr (objBitsKO (KOTCB tcb'a)); etcb_relation y tcb'a; ksPSpace b ptr = Some (KOTCB tcb'a); fst (projectKO (KOTCB tcb'a) b) = {(obj, b)}; P obj; ps_clear ptr (objBitsKO (KOTCB tcb'a)) b\<rbrakk> \<Longrightarrow> \<exists>tcb'. injectKOS ob' = KOTCB tcb' \<and> etcb_relation etcb tcb' proof (prove)
goal (1 subgoal):
 1. \<And>a b y tcb' tcb'a obj. \<lbrakk>other_obj_relation (TCB tcb) (injectKOS ob'); projectKO_opt (KOTCB tcb'a) = Some obj; is_aligned ptr (objBits ob'); ps_clear ptr (objBits ob') 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 (\<lambda>y. cte_wp_at (\<lambda>_. True) y 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 (TCB tcb'); \<forall>x\<in>ran tcb_cap_cases. fst x tcb' = fst x tcb; 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)); other_obj_relation (TCB tcb') (KOTCB tcb'a); ekheap a ptr = Some y; is_aligned ptr (objBitsKO (KOTCB tcb'a)); etcb_relation y tcb'a; ksPSpace b ptr = Some (KOTCB tcb'a); P obj; ps_clear ptr (objBitsKO (KOTCB tcb'a)) b\<rbrakk> \<Longrightarrow> \<exists>tcb'. injectKOS ob' = KOTCB tcb' \<and> etcb_relation etcb tcb' proof (prove)
goal (1 subgoal):
 1. \<And>a b y tcb'a tcb'aa obj. \<lbrakk>other_obj_relation (TCB tcb) (injectKOS ob'); projectKO_opt (KOTCB tcb'aa) = Some obj; is_aligned ptr (objBits ob'); ps_clear ptr (objBits ob') 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 (\<lambda>y. cte_wp_at (\<lambda>_. True) y 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 (TCB tcb'a); \<forall>x\<in>ran tcb_cap_cases. fst x tcb'a = fst x tcb; 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)); other_obj_relation (TCB tcb'a) (KOTCB tcb'aa); ekheap a ptr = Some y; is_aligned ptr (objBitsKO (KOTCB tcb'aa)); etcb_relation y tcb'aa; ksPSpace b ptr = Some (KOTCB tcb'aa); P obj; ps_clear ptr (objBitsKO (KOTCB tcb'aa)) b; etcb_relation etcb tcb'; injectKOS ob' = KOTCB tcb'\<rbrakk> \<Longrightarrow> \<exists>tcb'. injectKOS ob' = KOTCB tcb' \<and> etcb_relation etcb tcb'