theory KHeap_R

lemma setObject_other_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 t: "is_other_obj_relation_type (a_type ob)"
  assumes b: "\<And>ko. P ko \<Longrightarrow> objBits ko = objBits ob'"
  assumes e: "\<And>ko. P ko \<Longrightarrow> exst_same' (injectKO ko) (injectKO ob')"
  assumes P: "\<And>(v::'a::pspace_storable). (1 :: word32) < 2 ^ (objBits v)"
  shows      "other_obj_relation ob (injectKO (ob' :: 'a :: pspace_storable)) \<Longrightarrow>
  corres dc (obj_at (\<lambda>ko. a_type ko = a_type ob) ptr and obj_at (same_caps ob) ptr)
            (obj_at' (P :: 'a \<Rightarrow> bool) ptr)
            (set_object ptr ob) (setObject ptr ob')" supply image_cong_simp [cong del] 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_object_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 obj_at_def
                        updateObject_default_def in_magnitude_check [OF _ P]) apply (rename_tac ko) apply (clarsimp simp add: state_relation_def z) apply (clarsimp simp add: caps_of_state_after_update cte_wp_at_after_update
                            swp_def fun_upd_def obj_at_def) 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 a_type_def
                   split: Structures_A.kernel_object.splits if_split_asm) apply (simp split: arch_kernel_obj.splits if_splits) apply (fold fun_upd_def) apply (simp only: pspace_relation_def pspace_dom_update 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 t) apply (drule(1) bspec) apply clarsimp apply (frule_tac ko'=ko and x'=ptr in obj_relation_cut_same_type,
           (fastforce simp add: is_other_obj_relation_type t)+) apply (erule disjE) apply (simp add: is_other_obj_relation_type t) apply (erule disjE) apply (insert t,
      clarsimp simp: is_other_obj_relation_type_CapTable a_type_def) apply (erule disjE) apply (insert t,
       clarsimp simp: is_other_obj_relation_type_UserData a_type_def) apply (insert t,
      clarsimp simp: is_other_obj_relation_type_DeviceData a_type_def) apply (simp only: ekheap_relation_def) apply (rule ballI, drule(1) bspec) apply (drule domD) apply (insert e) apply atomize apply (clarsimp simp: obj_at'_def) apply (erule_tac x=obj in allE) apply (clarsimp simp: projectKO_eq project_inject) apply (case_tac ob;
         simp_all add: a_type_def other_obj_relation_def etcb_relation_def
                       is_other_obj_relation_type t exst_same_def) by (clarsimp simp: is_other_obj_relation_type t exst_same_def
              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 ob (injectKO ob') \<Longrightarrow> corres dc (typ_at (a_type ob) ptr and obj_at (same_caps ob) ptr) (obj_at' P ptr) (set_object ptr ob) (setObject ptr ob') proof (prove)
goal (1 subgoal):
 1. other_obj_relation ob (injectKO ob') \<Longrightarrow> corres dc (typ_at (a_type ob) ptr and obj_at (same_caps ob) ptr) (obj_at' P ptr) (set_object ptr ob) (setObject ptr ob') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>other_obj_relation ob (injectKO ob'); True\<rbrakk> \<Longrightarrow> no_fail (obj_at' P ptr) (setObject ptr ob')
 2. other_obj_relation ob (injectKO ob') \<Longrightarrow> \<forall>(s, s')\<in>state_relation. (typ_at (a_type ob) ptr and obj_at (same_caps ob) ptr) s \<and> obj_at' P ptr s' \<longrightarrow> (\<forall>(r', t')\<in>fst (setObject ptr ob' s'). \<exists>(r, t)\<in>fst (set_object ptr ob s). (t, t') \<in> state_relation \<and> dc r r') proof (prove)
goal (3 subgoals):
 1. \<lbrakk>other_obj_relation ob (injectKO ob'); True\<rbrakk> \<Longrightarrow> no_fail ?P3 (setObject ptr ob')
 2. \<And>s. \<lbrakk>other_obj_relation ob (injectKO ob'); True; obj_at' P ptr s\<rbrakk> \<Longrightarrow> ?P3 s
 3. other_obj_relation ob (injectKO ob') \<Longrightarrow> \<forall>(s, s')\<in>state_relation. (typ_at (a_type ob) ptr and obj_at (same_caps ob) ptr) s \<and> obj_at' P ptr s' \<longrightarrow> (\<forall>(r', t')\<in>fst (setObject ptr ob' s'). \<exists>(r, t)\<in>fst (set_object ptr ob s). (t, t') \<in> state_relation \<and> dc r r') proof (prove)
goal (3 subgoals):
 1. \<lbrakk>other_obj_relation ob (injectKO ob'); True\<rbrakk> \<Longrightarrow> updateObject ob' = updateObject_default ob'
 2. \<And>s. \<lbrakk>other_obj_relation ob (injectKO ob'); True; obj_at' P ptr s\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>k. objBits k = objBits ob') ptr s
 3. other_obj_relation ob (injectKO ob') \<Longrightarrow> \<forall>(s, s')\<in>state_relation. (typ_at (a_type ob) ptr and obj_at (same_caps ob) ptr) s \<and> obj_at' P ptr s' \<longrightarrow> (\<forall>(r', t')\<in>fst (setObject ptr ob' s'). \<exists>(r, t)\<in>fst (set_object ptr ob s). (t, t') \<in> state_relation \<and> dc r r') proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>other_obj_relation ob (injectKO ob'); True; obj_at' P ptr s\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>k. objBits k = objBits ob') ptr s
 2. other_obj_relation ob (injectKO ob') \<Longrightarrow> \<forall>(s, s')\<in>state_relation. (typ_at (a_type ob) ptr and obj_at (same_caps ob) ptr) s \<and> obj_at' P ptr s' \<longrightarrow> (\<forall>(r', t')\<in>fst (setObject ptr ob' s'). \<exists>(r, t)\<in>fst (set_object ptr ob s). (t, t') \<in> state_relation \<and> dc r r') proof (prove)
goal (1 subgoal):
 1. other_obj_relation ob (injectKO ob') \<Longrightarrow> \<forall>(s, s')\<in>state_relation. (typ_at (a_type ob) ptr and obj_at (same_caps ob) ptr) s \<and> obj_at' P ptr s' \<longrightarrow> (\<forall>(r', t')\<in>fst (setObject ptr ob' s'). \<exists>(r, t)\<in>fst (set_object ptr ob s). (t, t') \<in> state_relation \<and> dc r r') proof (prove)
goal (1 subgoal):
 1. other_obj_relation ob (injectKO ob') \<Longrightarrow> \<forall>(s, s')\<in>state_relation. (typ_at (a_type ob) ptr and obj_at (same_caps ob) 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 kobj <- get_object ptr;
assert (a_type kobj = a_type ob);
s <- get;
put (s\<lparr>kheap := (kheap s)(ptr \<mapsto> ob)\<rparr>)
od) s). (t, t') \<in> state_relation \<and> dc r r') proof (prove)
goal (1 subgoal):
 1. \<And>a b ba ab koa. \<lbrakk>other_obj_relation ob (injectKO 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' P ptr b; kheap a ptr = Some koa; a_type koa = a_type ob; same_caps ob koa\<rbrakk> \<Longrightarrow> (a\<lparr>kheap := (kheap a)(ptr \<mapsto> ob)\<rparr>, b\<lparr>ksPSpace := (ksPSpace b)(ptr \<mapsto> injectKO ob')\<rparr>) \<in> state_relation proof (prove)
goal (1 subgoal):
 1. \<And>a b ba ab ko. \<lbrakk>other_obj_relation ob (injectKO 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' P ptr b; kheap a ptr = Some ko; a_type ko = a_type ob; same_caps ob ko\<rbrakk> \<Longrightarrow> (a\<lparr>kheap := (kheap a)(ptr \<mapsto> ob)\<rparr>, b\<lparr>ksPSpace := (ksPSpace b)(ptr \<mapsto> injectKO ob')\<rparr>) \<in> state_relation proof (prove)
goal (1 subgoal):
 1. \<And>a b ba ab ko. \<lbrakk>other_obj_relation ob (injectKO 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; kheap a ptr = Some ko; a_type ko = a_type ob; same_caps ob ko; 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> ob)) ((ksPSpace b)(ptr \<mapsto> injectKO ob')) \<and> ekheap_relation (ekheap a) ((ksPSpace b)(ptr \<mapsto> injectKO ob')) \<and> ghost_relation ((kheap a)(ptr \<mapsto> ob)) (gsUserPages b) (gsCNodes b) \<and> cdt_relation (swp (cte_wp_at (\<lambda>_. True)) (a\<lparr>kheap := (kheap a)(ptr \<mapsto> ob)\<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> ob)\<rparr>))) (ctes_of b) proof (prove)
goal (1 subgoal):
 1. \<And>a b ba ab ko. \<lbrakk>other_obj_relation ob (injectKO 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; kheap a ptr = Some ko; a_type ko = a_type ob; same_caps ob ko; 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\<rbrakk> \<Longrightarrow> pspace_relation (\<lambda>x. if x = ptr then Some ob else kheap a x) (\<lambda>x. if x = ptr then Some (injectKO ob') else ksPSpace b x) \<and> ekheap_relation (ekheap a) (\<lambda>x. if x = ptr then Some (injectKO ob') else ksPSpace b x) \<and> ghost_relation (\<lambda>x. if x = ptr then Some ob else kheap a x) (gsUserPages b) (gsCNodes b) proof (prove)
goal (1 subgoal):
 1. \<And>a b ba ab ko. \<lbrakk>other_obj_relation ob (injectKO 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; kheap a ptr = Some ko; a_type ko = a_type ob; same_caps ob ko; 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\<rbrakk> \<Longrightarrow> (pspace_relation (\<lambda>x. if x = ptr then Some ob else kheap a x) (\<lambda>x. if x = ptr then Some (injectKO ob') else ksPSpace b x) \<and> ekheap_relation (ekheap a) (\<lambda>x. if x = ptr then Some (injectKO ob') else ksPSpace b x)) \<and> ghost_relation (\<lambda>x. if x = ptr then Some ob else kheap a x) (gsUserPages b) (gsCNodes b) proof (prove)
goal (2 subgoals):
 1. \<And>a b ba ab ko. \<lbrakk>other_obj_relation ob (injectKO 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; kheap a ptr = Some ko; a_type ko = a_type ob; same_caps ob ko; 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\<rbrakk> \<Longrightarrow> ghost_relation (\<lambda>x. if x = ptr then Some ob else kheap a x) (gsUserPages b) (gsCNodes b)
 2. \<And>a b ba ab ko. \<lbrakk>other_obj_relation ob (injectKO 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; kheap a ptr = Some ko; a_type ko = a_type ob; same_caps ob ko; 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\<rbrakk> \<Longrightarrow> pspace_relation (\<lambda>x. if x = ptr then Some ob else kheap a x) (\<lambda>x. if x = ptr then Some (injectKO ob') else ksPSpace b x) \<and> ekheap_relation (ekheap a) (\<lambda>x. if x = ptr then Some (injectKO ob') else ksPSpace b x) proof (prove)
goal (2 subgoals):
 1. \<And>a b ba ab ko. \<lbrakk>other_obj_relation ob (injectKO 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; kheap a ptr = Some ko; a_type ko = a_type ob; same_caps ob ko; 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; \<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> (\<forall>sz. (\<exists>dev. ob = ArchObj (DataPage dev sz)) = (gsUserPages b ptr = Some sz)) \<and> (\<forall>n. (\<exists>cs. ob = CNode n cs \<and> well_formed_cnode_n n cs) = (gsCNodes b ptr = Some n))
 2. \<And>a b ba ab ko. \<lbrakk>other_obj_relation ob (injectKO 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; kheap a ptr = Some ko; a_type ko = a_type ob; same_caps ob ko; 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\<rbrakk> \<Longrightarrow> pspace_relation (\<lambda>x. if x = ptr then Some ob else kheap a x) (\<lambda>x. if x = ptr then Some (injectKO ob') else ksPSpace b x) \<and> ekheap_relation (ekheap a) (\<lambda>x. if x = ptr then Some (injectKO ob') else ksPSpace b x) proof (prove)
goal (2 subgoals):
 1. \<And>a b ba ab ko. \<lbrakk>other_obj_relation ob (injectKO 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; kheap a ptr = Some ko; a_type ko = a_type ob; same_caps ob ko; 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; \<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> (\<forall>sz. (\<exists>dev. ob = ArchObj (DataPage dev sz)) = (gsUserPages b ptr = Some sz)) \<and> (\<forall>n. (\<exists>cs. ob = CNode n cs \<and> well_formed_cnode_n n cs) = (gsCNodes b ptr = Some n))
 2. \<And>a b ba ab ko. \<lbrakk>other_obj_relation ob (injectKO 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; kheap a ptr = Some ko; a_type ko = a_type ob; same_caps ob ko; 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\<rbrakk> \<Longrightarrow> pspace_relation (\<lambda>x. if x = ptr then Some ob else kheap a x) (\<lambda>x. if x = ptr then Some (injectKO ob') else ksPSpace b x) \<and> ekheap_relation (ekheap a) (\<lambda>x. if x = ptr then Some (injectKO ob') else ksPSpace b x) proof (prove)
goal (2 subgoals):
 1. \<And>a b ba ab x5 x5a sz. \<lbrakk>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; \<forall>sz. (\<exists>dev. x5a = DataPage dev sz) = (gsUserPages b ptr = Some sz); gsCNodes b ptr = None; other_obj_relation (ArchObj x5) (injectKO 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; kheap a ptr = Some (ArchObj x5a); ob = ArchObj x5; (case x5a of arch_kernel_obj.ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz) = (case x5 of arch_kernel_obj.ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)\<rbrakk> \<Longrightarrow> (\<exists>dev. x5 = DataPage dev sz) = (gsUserPages b ptr = Some sz)
 2. \<And>a b ba ab ko. \<lbrakk>other_obj_relation ob (injectKO 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; kheap a ptr = Some ko; a_type ko = a_type ob; same_caps ob ko; 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\<rbrakk> \<Longrightarrow> pspace_relation (\<lambda>x. if x = ptr then Some ob else kheap a x) (\<lambda>x. if x = ptr then Some (injectKO ob') else ksPSpace b x) \<and> ekheap_relation (ekheap a) (\<lambda>x. if x = ptr then Some (injectKO ob') else ksPSpace b x) proof (prove)
goal (1 subgoal):
 1. \<And>a b ba ab ko. \<lbrakk>other_obj_relation ob (injectKO 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; kheap a ptr = Some ko; a_type ko = a_type ob; same_caps ob ko; 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\<rbrakk> \<Longrightarrow> pspace_relation (\<lambda>x. if x = ptr then Some ob else kheap a x) (\<lambda>x. if x = ptr then Some (injectKO ob') else ksPSpace b x) \<and> ekheap_relation (ekheap a) (\<lambda>x. if x = ptr then Some (injectKO ob') else ksPSpace b x) proof (prove)
goal (1 subgoal):
 1. \<And>a b ba ab ko. \<lbrakk>other_obj_relation ob (injectKO 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; kheap a ptr = Some ko; a_type ko = a_type ob; same_caps ob ko; 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\<rbrakk> \<Longrightarrow> pspace_relation ((kheap a)(ptr \<mapsto> ob)) ((ksPSpace b)(ptr \<mapsto> injectKO ob')) \<and> ekheap_relation (ekheap a) ((ksPSpace b)(ptr \<mapsto> injectKO ob')) proof (prove)
goal (1 subgoal):
 1. \<And>a b ba ab ko. \<lbrakk>other_obj_relation ob (injectKO 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; kheap a ptr = Some ko; a_type ko = a_type ob; same_caps ob ko; 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\<rbrakk> \<Longrightarrow> (\<forall>x\<in>dom (kheap a). \<forall>(y, P)\<in>obj_relation_cuts (the (((kheap a)(ptr \<mapsto> ob)) x)) x. P (the (((kheap a)(ptr \<mapsto> ob)) x)) (the (((ksPSpace b)(ptr \<mapsto> injectKO ob')) y))) \<and> ekheap_relation (ekheap a) ((ksPSpace b)(ptr \<mapsto> injectKO ob')) proof (prove)
goal (1 subgoal):
 1. \<And>a b ba ab ko. \<lbrakk>other_obj_relation ob (injectKO 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; kheap a ptr = Some ko; a_type ko = a_type ob; same_caps ob ko; 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; 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> ob)) x)) x. P (the (((kheap a)(ptr \<mapsto> ob)) x)) (the (((ksPSpace b)(ptr \<mapsto> injectKO ob')) y))) \<and> ekheap_relation (ekheap a) ((ksPSpace b)(ptr \<mapsto> injectKO ob')) proof (prove)
goal (1 subgoal):
 1. \<And>a b ba ab ko. \<lbrakk>other_obj_relation ob (injectKO 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; kheap a ptr = Some ko; a_type ko = a_type ob; same_caps ob ko; 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; 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> ob)) x)) x. P (the (((kheap a)(ptr \<mapsto> ob)) x)) (the (((ksPSpace b)(ptr \<mapsto> injectKO ob')) y))) \<and> ekheap_relation (ekheap a) ((ksPSpace b)(ptr \<mapsto> injectKO ob')) proof (prove)
goal (2 subgoals):
 1. \<And>a b ba ab ko. \<lbrakk>other_obj_relation ob (injectKO 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; kheap a ptr = Some ko; a_type ko = a_type ob; same_caps ob ko; 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; 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> ob)) x)) x. P (the (((kheap a)(ptr \<mapsto> ob)) x)) (the (((ksPSpace b)(ptr \<mapsto> injectKO ob')) y))
 2. \<And>a b ba ab ko. \<lbrakk>other_obj_relation ob (injectKO 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; kheap a ptr = Some ko; a_type ko = a_type ob; same_caps ob ko; 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; 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) ((ksPSpace b)(ptr \<mapsto> injectKO ob')) proof (prove)
goal (2 subgoals):
 1. \<And>a b ba ab ko x. \<lbrakk>other_obj_relation ob (injectKO 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; kheap a ptr = Some ko; a_type ko = a_type ob; same_caps ob ko; 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; 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> ob)) x)) x. P (the (((kheap a)(ptr \<mapsto> ob)) x)) (the (((ksPSpace b)(ptr \<mapsto> injectKO ob')) y))
 2. \<And>a b ba ab ko. \<lbrakk>other_obj_relation ob (injectKO 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; kheap a ptr = Some ko; a_type ko = a_type ob; same_caps ob ko; 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; 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) ((ksPSpace b)(ptr \<mapsto> injectKO ob')) proof (prove)
goal (2 subgoals):
 1. \<And>a b ba ab ko x. \<lbrakk>other_obj_relation ob (injectKO 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; kheap a ptr = Some ko; a_type ko = a_type ob; same_caps ob ko; 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; 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> ob)) x)) x. P (the (((kheap a)(ptr \<mapsto> ob)) x)) (the (((ksPSpace b)(ptr \<mapsto> injectKO ob')) y))
 2. \<And>a b ba ab ko. \<lbrakk>other_obj_relation ob (injectKO 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; kheap a ptr = Some ko; a_type ko = a_type ob; same_caps ob ko; 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; 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) ((ksPSpace b)(ptr \<mapsto> injectKO ob')) proof (prove)
goal (2 subgoals):
 1. \<And>a b ba ab ko x bb aa bc. \<lbrakk>other_obj_relation ob (injectKO 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; kheap a ptr = Some ko; a_type ko = a_type ob; same_caps ob ko; 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; pspace_dom (kheap a) = dom (ksPSpace b); other_obj_relation ko 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 (injectKO ob')) \<and> (aa \<noteq> ptr \<longrightarrow> bc bb (the (ksPSpace b aa)))
 2. \<And>a b ba ab ko. \<lbrakk>other_obj_relation ob (injectKO 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; kheap a ptr = Some ko; a_type ko = a_type ob; same_caps ob ko; 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; 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) ((ksPSpace b)(ptr \<mapsto> injectKO ob')) proof (prove)
goal (2 subgoals):
 1. \<And>a b ba ab ko x bb aa bc. \<lbrakk>other_obj_relation ob (injectKO 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; kheap a ptr = Some ko; a_type ko = a_type ob; same_caps ob ko; 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; pspace_dom (kheap a) = dom (ksPSpace b); other_obj_relation ko 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 (injectKO ob')) \<and> (aa \<noteq> ptr \<longrightarrow> bc bb (the (ksPSpace b aa)))
 2. \<And>a b ba ab ko. \<lbrakk>other_obj_relation ob (injectKO 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; kheap a ptr = Some ko; a_type ko = a_type ob; same_caps ob ko; 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; 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) ((ksPSpace b)(ptr \<mapsto> injectKO ob')) proof (prove)
goal (2 subgoals):
 1. \<And>a b ba ab ko x bb bc. \<lbrakk>other_obj_relation ob (injectKO 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; kheap a ptr = Some ko; a_type ko = a_type ob; same_caps ob ko; 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; pspace_dom (kheap a) = dom (ksPSpace b); other_obj_relation ko ba; kheap a x = Some bb; x \<noteq> ptr; (ptr, bc) \<in> obj_relation_cuts bb x; bc bb ba\<rbrakk> \<Longrightarrow> bc bb (injectKO ob')
 2. \<And>a b ba ab ko. \<lbrakk>other_obj_relation ob (injectKO 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; kheap a ptr = Some ko; a_type ko = a_type ob; same_caps ob ko; 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; 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) ((ksPSpace b)(ptr \<mapsto> injectKO ob')) proof (prove)
goal (2 subgoals):
 1. \<And>a b ba ab ko x bb bc. \<lbrakk>other_obj_relation ob (injectKO 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; kheap a ptr = Some ko; a_type ko = a_type ob; same_caps ob ko; 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; pspace_dom (kheap a) = dom (ksPSpace b); other_obj_relation ko ba; kheap a x = Some bb; x \<noteq> ptr; (ptr, bc) \<in> obj_relation_cuts bb x; bc bb ba; a_type bb = a_type ko \<or> (\<exists>n n'. a_type bb = ACapTable n \<and> a_type ko = ACapTable n') \<or> (\<exists>sz sz'. a_type bb = AArch (AUserData sz) \<and> a_type ko = AArch (AUserData sz')) \<or> (\<exists>sz sz'. a_type bb = AArch (ADeviceData sz) \<and> a_type ko = AArch (ADeviceData sz'))\<rbrakk> \<Longrightarrow> bc bb (injectKO ob')
 2. \<And>a b ba ab ko. \<lbrakk>other_obj_relation ob (injectKO 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; kheap a ptr = Some ko; a_type ko = a_type ob; same_caps ob ko; 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; 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) ((ksPSpace b)(ptr \<mapsto> injectKO ob')) proof (prove)
goal (3 subgoals):
 1. \<And>a b ba ab ko x bb bc. \<lbrakk>other_obj_relation ob (injectKO 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; kheap a ptr = Some ko; a_type ko = a_type ob; same_caps ob ko; 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; pspace_dom (kheap a) = dom (ksPSpace b); other_obj_relation ko ba; kheap a x = Some bb; x \<noteq> ptr; (ptr, bc) \<in> obj_relation_cuts bb x; bc bb ba; a_type bb = a_type ko\<rbrakk> \<Longrightarrow> bc bb (injectKO ob')
 2. \<And>a b ba ab ko x bb bc. \<lbrakk>other_obj_relation ob (injectKO 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; kheap a ptr = Some ko; a_type ko = a_type ob; same_caps ob ko; 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; pspace_dom (kheap a) = dom (ksPSpace b); other_obj_relation ko ba; kheap a x = Some bb; x \<noteq> ptr; (ptr, bc) \<in> obj_relation_cuts bb x; bc bb ba; (\<exists>n n'. a_type bb = ACapTable n \<and> a_type ko = ACapTable n') \<or> (\<exists>sz sz'. a_type bb = AArch (AUserData sz) \<and> a_type ko = AArch (AUserData sz')) \<or> (\<exists>sz sz'. a_type bb = AArch (ADeviceData sz) \<and> a_type ko = AArch (ADeviceData sz'))\<rbrakk> \<Longrightarrow> bc bb (injectKO ob')
 3. \<And>a b ba ab ko. \<lbrakk>other_obj_relation ob (injectKO 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; kheap a ptr = Some ko; a_type ko = a_type ob; same_caps ob ko; 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; 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) ((ksPSpace b)(ptr \<mapsto> injectKO ob')) proof (prove)
goal (2 subgoals):
 1. \<And>a b ba ab ko x bb bc. \<lbrakk>other_obj_relation ob (injectKO 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; kheap a ptr = Some ko; a_type ko = a_type ob; same_caps ob ko; 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; pspace_dom (kheap a) = dom (ksPSpace b); other_obj_relation ko ba; kheap a x = Some bb; x \<noteq> ptr; (ptr, bc) \<in> obj_relation_cuts bb x; bc bb ba; (\<exists>n n'. a_type bb = ACapTable n \<and> a_type ko = ACapTable n') \<or> (\<exists>sz sz'. a_type bb = AArch (AUserData sz) \<and> a_type ko = AArch (AUserData sz')) \<or> (\<exists>sz sz'. a_type bb = AArch (ADeviceData sz) \<and> a_type ko = AArch (ADeviceData sz'))\<rbrakk> \<Longrightarrow> bc bb (injectKO ob')
 2. \<And>a b ba ab ko. \<lbrakk>other_obj_relation ob (injectKO 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; kheap a ptr = Some ko; a_type ko = a_type ob; same_caps ob ko; 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; 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) ((ksPSpace b)(ptr \<mapsto> injectKO ob')) proof (prove)
goal (3 subgoals):
 1. \<And>a b ba ab ko x bb bc. \<lbrakk>other_obj_relation ob (injectKO 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; kheap a ptr = Some ko; a_type ko = a_type ob; same_caps ob ko; 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; pspace_dom (kheap a) = dom (ksPSpace b); other_obj_relation ko ba; kheap a x = Some bb; x \<noteq> ptr; (ptr, bc) \<in> obj_relation_cuts bb x; bc bb ba; \<exists>n n'. a_type bb = ACapTable n \<and> a_type ko = ACapTable n'\<rbrakk> \<Longrightarrow> bc bb (injectKO ob')
 2. \<And>a b ba ab ko x bb bc. \<lbrakk>other_obj_relation ob (injectKO 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; kheap a ptr = Some ko; a_type ko = a_type ob; same_caps ob ko; 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; pspace_dom (kheap a) = dom (ksPSpace b); other_obj_relation ko ba; kheap a x = Some bb; x \<noteq> ptr; (ptr, bc) \<in> obj_relation_cuts bb x; bc bb ba; (\<exists>sz sz'. a_type bb = AArch (AUserData sz) \<and> a_type ko = AArch (AUserData sz')) \<or> (\<exists>sz sz'. a_type bb = AArch (ADeviceData sz) \<and> a_type ko = AArch (ADeviceData sz'))\<rbrakk> \<Longrightarrow> bc bb (injectKO ob')
 3. \<And>a b ba ab ko. \<lbrakk>other_obj_relation ob (injectKO 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; kheap a ptr = Some ko; a_type ko = a_type ob; same_caps ob ko; 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; 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) ((ksPSpace b)(ptr \<mapsto> injectKO ob')) proof (prove)
goal (2 subgoals):
 1. \<And>a b ba ab ko x bb bc. \<lbrakk>other_obj_relation ob (injectKO 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; kheap a ptr = Some ko; a_type ko = a_type ob; same_caps ob ko; 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; pspace_dom (kheap a) = dom (ksPSpace b); other_obj_relation ko ba; kheap a x = Some bb; x \<noteq> ptr; (ptr, bc) \<in> obj_relation_cuts bb x; bc bb ba; (\<exists>sz sz'. a_type bb = AArch (AUserData sz) \<and> a_type ko = AArch (AUserData sz')) \<or> (\<exists>sz sz'. a_type bb = AArch (ADeviceData sz) \<and> a_type ko = AArch (ADeviceData sz')); is_other_obj_relation_type (a_type ob)\<rbrakk> \<Longrightarrow> bc bb (injectKO ob')
 2. \<And>a b ba ab ko. \<lbrakk>other_obj_relation ob (injectKO 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; kheap a ptr = Some ko; a_type ko = a_type ob; same_caps ob ko; 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; 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)); is_other_obj_relation_type (a_type ob)\<rbrakk> \<Longrightarrow> ekheap_relation (ekheap a) ((ksPSpace b)(ptr \<mapsto> injectKO ob')) proof (prove)
goal (3 subgoals):
 1. \<And>a b ba ab ko x bb bc. \<lbrakk>other_obj_relation ob (injectKO 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; kheap a ptr = Some ko; a_type ko = a_type ob; same_caps ob ko; 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; pspace_dom (kheap a) = dom (ksPSpace b); other_obj_relation ko ba; kheap a x = Some bb; x \<noteq> ptr; (ptr, bc) \<in> obj_relation_cuts bb x; bc bb ba; is_other_obj_relation_type (a_type ob); \<exists>sz sz'. a_type bb = AArch (AUserData sz) \<and> a_type ko = AArch (AUserData sz')\<rbrakk> \<Longrightarrow> bc bb (injectKO ob')
 2. \<And>a b ba ab ko x bb bc. \<lbrakk>other_obj_relation ob (injectKO 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; kheap a ptr = Some ko; a_type ko = a_type ob; same_caps ob ko; 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; pspace_dom (kheap a) = dom (ksPSpace b); other_obj_relation ko ba; kheap a x = Some bb; x \<noteq> ptr; (ptr, bc) \<in> obj_relation_cuts bb x; bc bb ba; is_other_obj_relation_type (a_type ob); \<exists>sz sz'. a_type bb = AArch (ADeviceData sz) \<and> a_type ko = AArch (ADeviceData sz')\<rbrakk> \<Longrightarrow> bc bb (injectKO ob')
 3. \<And>a b ba ab ko. \<lbrakk>other_obj_relation ob (injectKO 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; kheap a ptr = Some ko; a_type ko = a_type ob; same_caps ob ko; 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; 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)); is_other_obj_relation_type (a_type ob)\<rbrakk> \<Longrightarrow> ekheap_relation (ekheap a) ((ksPSpace b)(ptr \<mapsto> injectKO ob')) proof (prove)
goal (2 subgoals):
 1. \<And>a b ba ab ko x bb bc. \<lbrakk>other_obj_relation ob (injectKO 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; kheap a ptr = Some ko; a_type ko = a_type ob; same_caps ob ko; 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; pspace_dom (kheap a) = dom (ksPSpace b); other_obj_relation ko ba; kheap a x = Some bb; x \<noteq> ptr; (ptr, bc) \<in> obj_relation_cuts bb x; bc bb ba; is_other_obj_relation_type (a_type ob); \<exists>sz sz'. a_type bb = AArch (ADeviceData sz) \<and> a_type ko = AArch (ADeviceData sz'); is_other_obj_relation_type (a_type ob)\<rbrakk> \<Longrightarrow> bc bb (injectKO ob')
 2. \<And>a b ba ab ko. \<lbrakk>other_obj_relation ob (injectKO 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; kheap a ptr = Some ko; a_type ko = a_type ob; same_caps ob ko; 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; 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)); is_other_obj_relation_type (a_type ob); is_other_obj_relation_type (a_type ob)\<rbrakk> \<Longrightarrow> ekheap_relation (ekheap a) ((ksPSpace b)(ptr \<mapsto> injectKO ob')) proof (prove)
goal (1 subgoal):
 1. \<And>a b ba ab ko. \<lbrakk>other_obj_relation ob (injectKO 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; kheap a ptr = Some ko; a_type ko = a_type ob; same_caps ob ko; 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; 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)); is_other_obj_relation_type (a_type ob); is_other_obj_relation_type (a_type ob); is_other_obj_relation_type (a_type ob)\<rbrakk> \<Longrightarrow> ekheap_relation (ekheap a) ((ksPSpace b)(ptr \<mapsto> injectKO ob')) proof (prove)
goal (1 subgoal):
 1. \<And>a b ba ab ko. \<lbrakk>other_obj_relation ob (injectKO 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; kheap a ptr = Some ko; a_type ko = a_type ob; same_caps ob ko; \<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; 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 ko)) ptr. P (the (Some ko)) (the (ksPSpace b y)); True; True; is_other_obj_relation_type (a_type ob)\<rbrakk> \<Longrightarrow> \<forall>x\<in>dom (ekheap a). \<exists>tcb'. ((ksPSpace b)(ptr \<mapsto> injectKO ob')) x = Some (KOTCB tcb') \<and> etcb_relation (the (ekheap a x)) tcb' proof (prove)
goal (1 subgoal):
 1. \<And>a b ba ab ko x. \<lbrakk>other_obj_relation ob (injectKO 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; kheap a ptr = Some ko; a_type ko = a_type ob; same_caps ob ko; 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; 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 ko)) ptr. P (the (Some ko)) (the (ksPSpace b y)); True; True; is_other_obj_relation_type (a_type ob); 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> injectKO ob')) x = Some (KOTCB tcb') \<and> etcb_relation (the (ekheap a x)) tcb' proof (prove)
goal (1 subgoal):
 1. \<And>a b ba ab ko x. \<lbrakk>other_obj_relation ob (injectKO 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; kheap a ptr = Some ko; a_type ko = a_type ob; same_caps ob ko; 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; 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 ko)) ptr. P (the (Some ko)) (the (ksPSpace b y)); True; True; is_other_obj_relation_type (a_type ob); \<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> injectKO ob')) x = Some (KOTCB tcb') \<and> etcb_relation (the (ekheap a x)) tcb' proof (prove)
goal (1 subgoal):
 1. \<And>a b ba ab ko x. \<lbrakk>other_obj_relation ob (injectKO 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; kheap a ptr = Some ko; a_type ko = a_type ob; same_caps ob ko; 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; 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 ko)) ptr. P (the (Some ko)) (the (ksPSpace b y)); True; True; is_other_obj_relation_type (a_type ob); \<exists>tcb'. ksPSpace b x = Some (KOTCB tcb') \<and> etcb_relation (the (ekheap a x)) tcb'; \<exists>b. ekheap a x = Some b; \<And>ko. P ko \<Longrightarrow> exst_same' (injectKO ko) (injectKO ob')\<rbrakk> \<Longrightarrow> \<exists>tcb'. ((ksPSpace b)(ptr \<mapsto> injectKO ob')) x = Some (KOTCB tcb') \<and> etcb_relation (the (ekheap a x)) tcb' proof (prove)
goal (1 subgoal):
 1. \<And>a b ba ab ko x. \<lbrakk>other_obj_relation ob (injectKO 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; kheap a ptr = Some ko; a_type ko = a_type ob; same_caps ob ko; 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; 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 ko)) ptr. P (the (Some ko)) (the (ksPSpace b y)); True; True; is_other_obj_relation_type (a_type ob); \<exists>tcb'. ksPSpace b x = Some (KOTCB tcb') \<and> etcb_relation (the (ekheap a x)) tcb'; \<exists>b. ekheap a x = Some b; \<forall>ko. P ko \<longrightarrow> exst_same' (injectKO ko) (injectKO ob')\<rbrakk> \<Longrightarrow> \<exists>tcb'. ((ksPSpace b)(ptr \<mapsto> injectKO ob')) x = Some (KOTCB tcb') \<and> etcb_relation (the (ekheap a x)) tcb' proof (prove)
goal (1 subgoal):
 1. \<And>a b ab ko tcb' bb obj. \<lbrakk>other_obj_relation ob (injectKO ob'); projectKO_opt (KOTCB tcb') = Some ab; is_aligned ptr (objBits ob'); ps_clear ptr (objBits ob') b; kheap a ptr = Some ko; a_type ko = a_type ob; same_caps ob ko; 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; 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)); is_other_obj_relation_type (a_type ob); \<forall>ko. P ko \<longrightarrow> exst_same' (injectKO ko) (injectKO ob'); ekheap a ptr = Some bb; is_aligned ptr (objBitsKO (KOTCB tcb')); ksPSpace b ptr = Some (KOTCB tcb'); etcb_relation bb tcb'; fst (projectKO (KOTCB tcb') b) = {(obj, b)}; P obj; ps_clear ptr (objBitsKO (KOTCB tcb')) b\<rbrakk> \<Longrightarrow> \<exists>tcb'. injectKO ob' = KOTCB tcb' \<and> etcb_relation bb tcb' proof (prove)
goal (1 subgoal):
 1. \<And>a b ab ko tcb' bb obj. \<lbrakk>other_obj_relation ob (injectKO ob'); projectKO_opt (KOTCB tcb') = Some ab; is_aligned ptr (objBits ob'); ps_clear ptr (objBits ob') b; kheap a ptr = Some ko; a_type ko = a_type ob; same_caps ob ko; 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; 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)); is_other_obj_relation_type (a_type ob); ekheap a ptr = Some bb; is_aligned ptr (objBitsKO (KOTCB tcb')); ksPSpace b ptr = Some (KOTCB tcb'); etcb_relation bb tcb'; fst (projectKO (KOTCB tcb') b) = {(obj, b)}; P obj; ps_clear ptr (objBitsKO (KOTCB tcb')) b; P obj \<longrightarrow> exst_same' (injectKO obj) (injectKO ob')\<rbrakk> \<Longrightarrow> \<exists>tcb'. injectKO ob' = KOTCB tcb' \<and> etcb_relation bb tcb' proof (prove)
goal (1 subgoal):
 1. \<And>a b ab ko tcb' bb obj. \<lbrakk>other_obj_relation ob (injectKO ob'); injectKO ab = KOTCB tcb'; is_aligned ptr (objBits ob'); ps_clear ptr (objBits ob') b; kheap a ptr = Some ko; a_type ko = a_type ob; same_caps ob ko; 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; 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)); is_other_obj_relation_type (a_type ob); ekheap a ptr = Some bb; is_aligned ptr (objBitsKO (KOTCB tcb')); ksPSpace b ptr = Some (KOTCB tcb'); etcb_relation bb tcb'; injectKO obj = KOTCB tcb'; P obj; ps_clear ptr (objBitsKO (KOTCB tcb')) b; exst_same' (KOTCB tcb') (injectKO ob')\<rbrakk> \<Longrightarrow> \<exists>tcb'. injectKO ob' = KOTCB tcb' \<and> etcb_relation bb tcb' proof (prove)
goal (4 subgoals):
 1. \<And>a b ab ko tcb' bb obj x2. \<lbrakk>case injectKO ob' of KOTCB x \<Rightarrow> tcb_relation x2 x | _ \<Rightarrow> False; injectKO ab = KOTCB tcb'; is_aligned ptr (objBits ob'); ps_clear ptr (objBits ob') b; kheap a ptr = Some ko; (case ko of CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | Endpoint endpoint \<Rightarrow> AEndpoint | Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of arch_kernel_obj.ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB; \<exists>tcb'. ko = TCB tcb' \<and> (\<forall>x\<in>ran tcb_cap_cases. case x of (getF, t) \<Rightarrow> getF tcb' = getF x2); 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; 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)); case ko of CNode nat fun \<Rightarrow> False | TCB tcb \<Rightarrow> case KOTCB tcb' of KOTCB x \<Rightarrow> tcb_relation tcb x | _ \<Rightarrow> False | Endpoint ep \<Rightarrow> case KOTCB tcb' of KOEndpoint x \<Rightarrow> ep_relation ep x | _ \<Rightarrow> False | Notification ntfn \<Rightarrow> case KOTCB tcb' of KONotification x \<Rightarrow> ntfn_relation ntfn x | _ \<Rightarrow> False | ArchObj (arch_kernel_obj.ASIDPool pool) \<Rightarrow> case KOTCB tcb' of KOArch (KOASIDPool xa) \<Rightarrow> asid_pool_relation pool xa | KOArch _ \<Rightarrow> False | _ \<Rightarrow> False | ArchObj _ \<Rightarrow> False; is_other_obj_relation_type ATCB; ekheap a ptr = Some bb; is_aligned ptr (objBitsKO (KOTCB tcb')); ksPSpace b ptr = Some (KOTCB tcb'); tcb_priority bb = tcbPriority tcb' \<and> tcb_time_slice bb = tcbTimeSlice tcb' \<and> tcb_domain bb = tcbDomain tcb'; injectKO obj = KOTCB tcb'; P obj; ps_clear ptr (objBitsKO (KOTCB tcb')) b; exst_same' (KOTCB tcb') (injectKO ob'); ob = TCB x2\<rbrakk> \<Longrightarrow> \<exists>tcb'a. injectKO ob' = KOTCB tcb'a \<and> tcbPriority tcb' = tcbPriority tcb'a \<and> tcbTimeSlice tcb' = tcbTimeSlice tcb'a \<and> tcbDomain tcb' = tcbDomain tcb'a
 2. \<And>a b ab ko tcb' bb obj x3. \<lbrakk>case injectKO ob' of KOEndpoint x \<Rightarrow> ep_relation x3 x | _ \<Rightarrow> False; injectKO ab = KOTCB tcb'; is_aligned ptr (objBits ob'); ps_clear ptr (objBits ob') b; kheap a ptr = Some ko; (case ko of CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | Endpoint endpoint \<Rightarrow> AEndpoint | Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of arch_kernel_obj.ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = AEndpoint; is_ep ko; 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; 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)); case ko of CNode nat fun \<Rightarrow> False | TCB tcb \<Rightarrow> case KOTCB tcb' of KOTCB x \<Rightarrow> tcb_relation tcb x | _ \<Rightarrow> False | Endpoint ep \<Rightarrow> case KOTCB tcb' of KOEndpoint x \<Rightarrow> ep_relation ep x | _ \<Rightarrow> False | Notification ntfn \<Rightarrow> case KOTCB tcb' of KONotification x \<Rightarrow> ntfn_relation ntfn x | _ \<Rightarrow> False | ArchObj (arch_kernel_obj.ASIDPool pool) \<Rightarrow> case KOTCB tcb' of KOArch (KOASIDPool xa) \<Rightarrow> asid_pool_relation pool xa | KOArch _ \<Rightarrow> False | _ \<Rightarrow> False | ArchObj _ \<Rightarrow> False; is_other_obj_relation_type AEndpoint; ekheap a ptr = Some bb; is_aligned ptr (objBitsKO (KOTCB tcb')); ksPSpace b ptr = Some (KOTCB tcb'); tcb_priority bb = tcbPriority tcb' \<and> tcb_time_slice bb = tcbTimeSlice tcb' \<and> tcb_domain bb = tcbDomain tcb'; injectKO obj = KOTCB tcb'; P obj; ps_clear ptr (objBitsKO (KOTCB tcb')) b; exst_same' (KOTCB tcb') (injectKO ob'); ob = Endpoint x3\<rbrakk> \<Longrightarrow> \<exists>tcb'a. injectKO ob' = KOTCB tcb'a \<and> tcbPriority tcb' = tcbPriority tcb'a \<and> tcbTimeSlice tcb' = tcbTimeSlice tcb'a \<and> tcbDomain tcb' = tcbDomain tcb'a
 3. \<And>a b ab ko tcb' bb obj x4. \<lbrakk>case injectKO ob' of KONotification x \<Rightarrow> ntfn_relation x4 x | _ \<Rightarrow> False; injectKO ab = KOTCB tcb'; is_aligned ptr (objBits ob'); ps_clear ptr (objBits ob') b; kheap a ptr = Some ko; (case ko of CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | Endpoint endpoint \<Rightarrow> AEndpoint | Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of arch_kernel_obj.ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ANTFN; is_ntfn ko; 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; 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)); case ko of CNode nat fun \<Rightarrow> False | TCB tcb \<Rightarrow> case KOTCB tcb' of KOTCB x \<Rightarrow> tcb_relation tcb x | _ \<Rightarrow> False | Endpoint ep \<Rightarrow> case KOTCB tcb' of KOEndpoint x \<Rightarrow> ep_relation ep x | _ \<Rightarrow> False | Notification ntfn \<Rightarrow> case KOTCB tcb' of KONotification x \<Rightarrow> ntfn_relation ntfn x | _ \<Rightarrow> False | ArchObj (arch_kernel_obj.ASIDPool pool) \<Rightarrow> case KOTCB tcb' of KOArch (KOASIDPool xa) \<Rightarrow> asid_pool_relation pool xa | KOArch _ \<Rightarrow> False | _ \<Rightarrow> False | ArchObj _ \<Rightarrow> False; is_other_obj_relation_type ANTFN; ekheap a ptr = Some bb; is_aligned ptr (objBitsKO (KOTCB tcb')); ksPSpace b ptr = Some (KOTCB tcb'); tcb_priority bb = tcbPriority tcb' \<and> tcb_time_slice bb = tcbTimeSlice tcb' \<and> tcb_domain bb = tcbDomain tcb'; injectKO obj = KOTCB tcb'; P obj; ps_clear ptr (objBitsKO (KOTCB tcb')) b; exst_same' (KOTCB tcb') (injectKO ob'); ob = Notification x4\<rbrakk> \<Longrightarrow> \<exists>tcb'a. injectKO ob' = KOTCB tcb'a \<and> tcbPriority tcb' = tcbPriority tcb'a \<and> tcbTimeSlice tcb' = tcbTimeSlice tcb'a \<and> tcbDomain tcb' = tcbDomain tcb'a
 4. \<And>a b ab ko tcb' bb obj x5. \<lbrakk>case x5 of arch_kernel_obj.ASIDPool pool \<Rightarrow> case injectKO ob' of KOArch (KOASIDPool xa) \<Rightarrow> asid_pool_relation pool xa | KOArch _ \<Rightarrow> False | _ \<Rightarrow> False | _ \<Rightarrow> False; injectKO ab = KOTCB tcb'; is_aligned ptr (objBits ob'); ps_clear ptr (objBits ob') b; kheap a ptr = Some ko; (case ko of CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | Endpoint endpoint \<Rightarrow> AEndpoint | Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of arch_kernel_obj.ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = AArch (case x5 of arch_kernel_obj.ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz); \<exists>ao'. ko = ArchObj ao'; 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; 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)); case ko of CNode nat fun \<Rightarrow> False | TCB tcb \<Rightarrow> case KOTCB tcb' of KOTCB x \<Rightarrow> tcb_relation tcb x | _ \<Rightarrow> False | Endpoint ep \<Rightarrow> case KOTCB tcb' of KOEndpoint x \<Rightarrow> ep_relation ep x | _ \<Rightarrow> False | Notification ntfn \<Rightarrow> case KOTCB tcb' of KONotification x \<Rightarrow> ntfn_relation ntfn x | _ \<Rightarrow> False | ArchObj (arch_kernel_obj.ASIDPool pool) \<Rightarrow> case KOTCB tcb' of KOArch (KOASIDPool xa) \<Rightarrow> asid_pool_relation pool xa | KOArch _ \<Rightarrow> False | _ \<Rightarrow> False | ArchObj _ \<Rightarrow> False; is_other_obj_relation_type (AArch (case x5 of arch_kernel_obj.ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)); ekheap a ptr = Some bb; is_aligned ptr (objBitsKO (KOTCB tcb')); ksPSpace b ptr = Some (KOTCB tcb'); tcb_priority bb = tcbPriority tcb' \<and> tcb_time_slice bb = tcbTimeSlice tcb' \<and> tcb_domain bb = tcbDomain tcb'; injectKO obj = KOTCB tcb'; P obj; ps_clear ptr (objBitsKO (KOTCB tcb')) b; exst_same' (KOTCB tcb') (injectKO ob'); ob = ArchObj x5\<rbrakk> \<Longrightarrow> \<exists>tcb'a. injectKO ob' = KOTCB tcb'a \<and> tcbPriority tcb' = tcbPriority tcb'a \<and> tcbTimeSlice tcb' = tcbTimeSlice tcb'a \<and> tcbDomain tcb' = tcbDomain tcb'a