theory ADT_C

lemma setTCBContext_C_corres:
  "\<lbrakk> ccontext_relation tc tc'; t' = tcb_ptr_to_ctcb_ptr t \<rbrakk> \<Longrightarrow>
  corres_underlying rf_sr nf nf' dc (pspace_domain_valid and tcb_at' t) \<top>
    (threadSet (\<lambda>tcb. tcb \<lparr> tcbArch := atcbContextSet tc (tcbArch tcb)\<rparr>) t) (setTCBContext_C tc' t')" apply (simp add: setTCBContext_C_def exec_C_def Basic_sem_eq corres_underlying_def) apply clarsimp apply (simp add: threadSet_def bind_assoc split_def exec_gets) apply (frule (1) obj_at_cslift_tcb) apply clarsimp apply (frule getObject_eq [rotated -1], simp) apply (simp add: objBits_simps') apply (simp add: Nondet_Monad.bind_def split_def) apply (rule bexI) prefer 2 apply assumption apply simp apply (frule setObject_eq [rotated -1], simp) apply (simp add: objBits_simps') apply (simp add: objBits_simps) apply clarsimp apply (rule bexI) prefer 2 apply assumption apply clarsimp apply (clarsimp simp: typ_heap_simps') apply (thin_tac "(a,b) \<in> fst t" for a b t)+ apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def cpspace_relation_def
                        carch_state_relation_def cmachine_state_relation_def
                        typ_heap_simps' update_tcb_map_tos) apply (simp add: map_to_ctes_upd_tcb_no_ctes map_to_tcbs_upd tcb_cte_cases_def
                   cvariable_relation_upd_const ko_at_projectKO_opt cteSizeBits_def) apply (simp add: cep_relations_drop_fun_upd) apply (apply_conjunct \<open>match conclusion in \<open>cready_queues_relation _ _ _\<close> \<Rightarrow>
         \<open>erule cready_queues_relation_not_queue_ptrs; rule ext; simp split: if_split\<close>\<close>) apply (drule ko_at_projectKO_opt) apply (erule (2) cmap_relation_upd_relI) apply (simp add: ctcb_relation_def carch_tcb_relation_def) apply assumption apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccontext_relation tc tc'; t' = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> corres_underlying rf_sr nf nf' dc (pspace_domain_valid and tcb_at' t) (\<lambda>_. True) (threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb)) tcb) t) (setTCBContext_C tc' t') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccontext_relation tc tc'; t' = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> \<forall>x\<in>rf_sr. case x of (s, s') \<Rightarrow> pspace_domain_valid s \<and> tcb_at' t s \<longrightarrow> (nf \<longrightarrow> \<not> snd (threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb)) tcb) t s)) \<longrightarrow> (\<exists>(r, ta)\<in>fst (threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb)) tcb) t s). (ta, globals_update (t_hrs_'_update (\<lambda>_. hrs_mem_update (heap_update (PTR(user_context_C) &(PTR(arch_tcb_C) &(tcb_ptr_to_ctcb_ptr t\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])) tc') (t_hrs_' (globals s')))) s') \<in> rf_sr) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>ccontext_relation tc tc'; t' = tcb_ptr_to_ctcb_ptr t; (a, b) \<in> rf_sr; pspace_domain_valid a; tcb_at' t a; nf \<longrightarrow> \<not> snd (threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb)) tcb) t a)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb)) tcb) t a). case x of (r, ta) \<Rightarrow> (ta, globals_update (t_hrs_'_update (\<lambda>_. hrs_mem_update (heap_update (PTR(user_context_C) &(PTR(arch_tcb_C) &(tcb_ptr_to_ctcb_ptr t\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])) tc') (t_hrs_' (globals b)))) b) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>ccontext_relation tc tc'; t' = tcb_ptr_to_ctcb_ptr t; (a, b) \<in> rf_sr; pspace_domain_valid a; tcb_at' t a; nf \<longrightarrow> \<not> snd ((do tcb <- getObject t;
setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb)) tcb)
od) a)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((do tcb <- getObject t;
setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb)) tcb)
od) a). (snd x, globals_update (t_hrs_'_update (\<lambda>_. hrs_mem_update (heap_update (PTR(user_context_C) &(PTR(arch_tcb_C) &(tcb_ptr_to_ctcb_ptr t\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])) tc') (t_hrs_' (globals b)))) b) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>ccontext_relation tc tc'; t' = tcb_ptr_to_ctcb_ptr t; (a, b) \<in> rf_sr; pspace_domain_valid a; tcb_at' t a; nf \<longrightarrow> \<not> snd ((do tcb <- getObject t;
setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb)) tcb)
od) a); \<exists>ko ko'. ko_at' ko t a \<and> True \<and> cslift b (tcb_ptr_to_ctcb_ptr t) = Some ko' \<and> ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((do tcb <- getObject t;
setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb)) tcb)
od) a). (snd x, globals_update (t_hrs_'_update (\<lambda>_. hrs_mem_update (heap_update (PTR(user_context_C) &(PTR(arch_tcb_C) &(tcb_ptr_to_ctcb_ptr t\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])) tc') (t_hrs_' (globals b)))) b) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>a b ko ko'. \<lbrakk>ccontext_relation tc tc'; t' = tcb_ptr_to_ctcb_ptr t; (a, b) \<in> rf_sr; pspace_domain_valid a; tcb_at' t a; nf \<longrightarrow> \<not> snd ((do tcb <- getObject t;
setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb)) tcb)
od) a); ko_at' ko t a; cslift b (tcb_ptr_to_ctcb_ptr t) = Some ko'; ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((do tcb <- getObject t;
setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb)) tcb)
od) a). (snd x, globals_update (t_hrs_'_update (\<lambda>_. hrs_mem_update (heap_update (PTR(user_context_C) &(PTR(arch_tcb_C) &(tcb_ptr_to_ctcb_ptr t\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])) tc') (t_hrs_' (globals b)))) b) \<in> rf_sr proof (prove)
goal (2 subgoals):
 1. \<And>a b ko ko' v. \<lbrakk>ccontext_relation tc tc'; t' = tcb_ptr_to_ctcb_ptr t; (a, b) \<in> rf_sr; pspace_domain_valid a; tcb_at' t a; nf \<longrightarrow> \<not> snd ((do tcb <- getObject t;
setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb)) tcb)
od) a); ko_at' ko t a; cslift b (tcb_ptr_to_ctcb_ptr t) = Some ko'; ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> 1 < 2 ^ objBits v
 2. \<And>a b ko ko'. \<lbrakk>ccontext_relation tc tc'; t' = tcb_ptr_to_ctcb_ptr t; (a, b) \<in> rf_sr; pspace_domain_valid a; tcb_at' t a; nf \<longrightarrow> \<not> snd ((do tcb <- getObject t;
setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb)) tcb)
od) a); ko_at' ko t a; cslift b (tcb_ptr_to_ctcb_ptr t) = Some ko'; ctcb_relation ko ko'; (ko, a) \<in> fst (getObject t a)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((do tcb <- getObject t;
setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb)) tcb)
od) a). (snd x, globals_update (t_hrs_'_update (\<lambda>_. hrs_mem_update (heap_update (PTR(user_context_C) &(PTR(arch_tcb_C) &(tcb_ptr_to_ctcb_ptr t\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])) tc') (t_hrs_' (globals b)))) b) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>a b ko ko'. \<lbrakk>ccontext_relation tc tc'; t' = tcb_ptr_to_ctcb_ptr t; (a, b) \<in> rf_sr; pspace_domain_valid a; tcb_at' t a; nf \<longrightarrow> \<not> snd ((do tcb <- getObject t;
setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb)) tcb)
od) a); ko_at' ko t a; cslift b (tcb_ptr_to_ctcb_ptr t) = Some ko'; ctcb_relation ko ko'; (ko, a) \<in> fst (getObject t a)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((do tcb <- getObject t;
setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb)) tcb)
od) a). (snd x, globals_update (t_hrs_'_update (\<lambda>_. hrs_mem_update (heap_update (PTR(user_context_C) &(PTR(arch_tcb_C) &(tcb_ptr_to_ctcb_ptr t\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])) tc') (t_hrs_' (globals b)))) b) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>a b ko ko'. \<lbrakk>ccontext_relation tc tc'; t' = tcb_ptr_to_ctcb_ptr t; (a, b) \<in> rf_sr; pspace_domain_valid a; tcb_at' t a; nf \<longrightarrow> (\<forall>x\<in>fst (getObject t a). \<not> snd (setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch (fst x))) (fst x)) (snd x))) \<and> \<not> snd (getObject t a); ko_at' ko t a; cslift b (tcb_ptr_to_ctcb_ptr t) = Some ko'; ctcb_relation ko ko'; (ko, a) \<in> fst (getObject t a)\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst (getObject t a). \<exists>x\<in>fst (setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch (fst y))) (fst y)) (snd y)). (snd x, globals_update (t_hrs_'_update (\<lambda>_. hrs_mem_update (heap_update (PTR(user_context_C) &(PTR(arch_tcb_C) &(tcb_ptr_to_ctcb_ptr t\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])) tc') (t_hrs_' (globals b)))) b) \<in> rf_sr proof (prove)
goal (2 subgoals):
 1. \<And>a b ko ko'. \<lbrakk>ccontext_relation tc tc'; t' = tcb_ptr_to_ctcb_ptr t; (a, b) \<in> rf_sr; pspace_domain_valid a; tcb_at' t a; nf \<longrightarrow> (\<forall>x\<in>fst (getObject t a). \<not> snd (setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch (fst x))) (fst x)) (snd x))) \<and> \<not> snd (getObject t a); ko_at' ko t a; cslift b (tcb_ptr_to_ctcb_ptr t) = Some ko'; ctcb_relation ko ko'; (ko, a) \<in> fst (getObject t a)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch (fst (?y42 a b ko ko')))) (fst (?y42 a b ko ko'))) (snd (?y42 a b ko ko'))). (snd x, globals_update (t_hrs_'_update (\<lambda>_. hrs_mem_update (heap_update (PTR(user_context_C) &(PTR(arch_tcb_C) &(tcb_ptr_to_ctcb_ptr t\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])) tc') (t_hrs_' (globals b)))) b) \<in> rf_sr
 2. \<And>a b ko ko'. \<lbrakk>ccontext_relation tc tc'; t' = tcb_ptr_to_ctcb_ptr t; (a, b) \<in> rf_sr; pspace_domain_valid a; tcb_at' t a; nf \<longrightarrow> (\<forall>x\<in>fst (getObject t a). \<not> snd (setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch (fst x))) (fst x)) (snd x))) \<and> \<not> snd (getObject t a); ko_at' ko t a; cslift b (tcb_ptr_to_ctcb_ptr t) = Some ko'; ctcb_relation ko ko'; (ko, a) \<in> fst (getObject t a)\<rbrakk> \<Longrightarrow> ?y42 a b ko ko' \<in> fst (getObject t a) proof (prove)
goal (2 subgoals):
 1. \<And>a b ko ko'. \<lbrakk>ccontext_relation tc tc'; t' = tcb_ptr_to_ctcb_ptr t; (a, b) \<in> rf_sr; pspace_domain_valid a; tcb_at' t a; nf \<longrightarrow> (\<forall>x\<in>fst (getObject t a). \<not> snd (setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch (fst x))) (fst x)) (snd x))) \<and> \<not> snd (getObject t a); ko_at' ko t a; cslift b (tcb_ptr_to_ctcb_ptr t) = Some ko'; ctcb_relation ko ko'; (ko, a) \<in> fst (getObject t a)\<rbrakk> \<Longrightarrow> ?y42 a b ko ko' \<in> fst (getObject t a)
 2. \<And>a b ko ko'. \<lbrakk>ccontext_relation tc tc'; t' = tcb_ptr_to_ctcb_ptr t; (a, b) \<in> rf_sr; pspace_domain_valid a; tcb_at' t a; nf \<longrightarrow> (\<forall>x\<in>fst (getObject t a). \<not> snd (setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch (fst x))) (fst x)) (snd x))) \<and> \<not> snd (getObject t a); ko_at' ko t a; cslift b (tcb_ptr_to_ctcb_ptr t) = Some ko'; ctcb_relation ko ko'; (ko, a) \<in> fst (getObject t a)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch (fst (?y42 a b ko ko')))) (fst (?y42 a b ko ko'))) (snd (?y42 a b ko ko'))). (snd x, globals_update (t_hrs_'_update (\<lambda>_. hrs_mem_update (heap_update (PTR(user_context_C) &(PTR(arch_tcb_C) &(tcb_ptr_to_ctcb_ptr t\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])) tc') (t_hrs_' (globals b)))) b) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>a b ko ko'. \<lbrakk>ccontext_relation tc tc'; t' = tcb_ptr_to_ctcb_ptr t; (a, b) \<in> rf_sr; pspace_domain_valid a; tcb_at' t a; nf \<longrightarrow> (\<forall>x\<in>fst (getObject t a). \<not> snd (setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch (fst x))) (fst x)) (snd x))) \<and> \<not> snd (getObject t a); ko_at' ko t a; cslift b (tcb_ptr_to_ctcb_ptr t) = Some ko'; ctcb_relation ko ko'; (ko, a) \<in> fst (getObject t a)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch (fst (ko, a)))) (fst (ko, a))) (snd (ko, a))). (snd x, globals_update (t_hrs_'_update (\<lambda>_. hrs_mem_update (heap_update (PTR(user_context_C) &(PTR(arch_tcb_C) &(tcb_ptr_to_ctcb_ptr t\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])) tc') (t_hrs_' (globals b)))) b) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>a b ko ko'. \<lbrakk>ccontext_relation tc tc'; t' = tcb_ptr_to_ctcb_ptr t; (a, b) \<in> rf_sr; pspace_domain_valid a; tcb_at' t a; nf \<longrightarrow> (\<forall>x\<in>fst (getObject t a). \<not> snd (setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch (fst x))) (fst x)) (snd x))) \<and> \<not> snd (getObject t a); ko_at' ko t a; cslift b (tcb_ptr_to_ctcb_ptr t) = Some ko'; ctcb_relation ko ko'; (ko, a) \<in> fst (getObject t a)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch ko)) ko) a). (snd x, globals_update (t_hrs_'_update (\<lambda>_. hrs_mem_update (heap_update (PTR(user_context_C) &(PTR(arch_tcb_C) &(tcb_ptr_to_ctcb_ptr t\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])) tc') (t_hrs_' (globals b)))) b) \<in> rf_sr proof (prove)
goal (3 subgoals):
 1. \<And>a b ko ko' v. \<lbrakk>ccontext_relation tc tc'; t' = tcb_ptr_to_ctcb_ptr t; (a, b) \<in> rf_sr; pspace_domain_valid a; tcb_at' t a; nf \<longrightarrow> (\<forall>x\<in>fst (getObject t a). \<not> snd (setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch (fst x))) (fst x)) (snd x))) \<and> \<not> snd (getObject t a); ko_at' ko t a; cslift b (tcb_ptr_to_ctcb_ptr t) = Some ko'; ctcb_relation ko ko'; (ko, a) \<in> fst (getObject t a)\<rbrakk> \<Longrightarrow> 1 < 2 ^ objBits v
 2. \<And>a b ko ko' v v'. \<lbrakk>ccontext_relation tc tc'; t' = tcb_ptr_to_ctcb_ptr t; (a, b) \<in> rf_sr; pspace_domain_valid a; tcb_at' t a; nf \<longrightarrow> (\<forall>x\<in>fst (getObject t a). \<not> snd (setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch (fst x))) (fst x)) (snd x))) \<and> \<not> snd (getObject t a); ko_at' ko t a; cslift b (tcb_ptr_to_ctcb_ptr t) = Some ko'; ctcb_relation ko ko'; (ko, a) \<in> fst (getObject t a)\<rbrakk> \<Longrightarrow> objBits v = objBits v'
 3. \<And>a b ko ko'. \<lbrakk>ccontext_relation tc tc'; t' = tcb_ptr_to_ctcb_ptr t; (a, b) \<in> rf_sr; pspace_domain_valid a; tcb_at' t a; nf \<longrightarrow> (\<forall>x\<in>fst (getObject t a). \<not> snd (setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch (fst x))) (fst x)) (snd x))) \<and> \<not> snd (getObject t a); ko_at' ko t a; cslift b (tcb_ptr_to_ctcb_ptr t) = Some ko'; ctcb_relation ko ko'; (ko, a) \<in> fst (getObject t a); ((), a\<lparr>ksPSpace := (ksPSpace a)(t \<mapsto> injectKOS (?ko45 a b ko ko'))\<rparr>) \<in> fst (setObject t (?ko45 a b ko ko') a)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch ko)) ko) a). (snd x, globals_update (t_hrs_'_update (\<lambda>_. hrs_mem_update (heap_update (PTR(user_context_C) &(PTR(arch_tcb_C) &(tcb_ptr_to_ctcb_ptr t\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])) tc') (t_hrs_' (globals b)))) b) \<in> rf_sr proof (prove)
goal (2 subgoals):
 1. \<And>a b ko ko' v v'. \<lbrakk>ccontext_relation tc tc'; t' = tcb_ptr_to_ctcb_ptr t; (a, b) \<in> rf_sr; pspace_domain_valid a; tcb_at' t a; nf \<longrightarrow> (\<forall>x\<in>fst (getObject t a). \<not> snd (setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch (fst x))) (fst x)) (snd x))) \<and> \<not> snd (getObject t a); ko_at' ko t a; cslift b (tcb_ptr_to_ctcb_ptr t) = Some ko'; ctcb_relation ko ko'; (ko, a) \<in> fst (getObject t a)\<rbrakk> \<Longrightarrow> objBits v = objBits v'
 2. \<And>a b ko ko'. \<lbrakk>ccontext_relation tc tc'; t' = tcb_ptr_to_ctcb_ptr t; (a, b) \<in> rf_sr; pspace_domain_valid a; tcb_at' t a; nf \<longrightarrow> (\<forall>x\<in>fst (getObject t a). \<not> snd (setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch (fst x))) (fst x)) (snd x))) \<and> \<not> snd (getObject t a); ko_at' ko t a; cslift b (tcb_ptr_to_ctcb_ptr t) = Some ko'; ctcb_relation ko ko'; (ko, a) \<in> fst (getObject t a); ((), a\<lparr>ksPSpace := (ksPSpace a)(t \<mapsto> injectKOS (?ko45 a b ko ko'))\<rparr>) \<in> fst (setObject t (?ko45 a b ko ko') a)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch ko)) ko) a). (snd x, globals_update (t_hrs_'_update (\<lambda>_. hrs_mem_update (heap_update (PTR(user_context_C) &(PTR(arch_tcb_C) &(tcb_ptr_to_ctcb_ptr t\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])) tc') (t_hrs_' (globals b)))) b) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>a b ko ko'. \<lbrakk>ccontext_relation tc tc'; t' = tcb_ptr_to_ctcb_ptr t; (a, b) \<in> rf_sr; pspace_domain_valid a; tcb_at' t a; nf \<longrightarrow> (\<forall>x\<in>fst (getObject t a). \<not> snd (setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch (fst x))) (fst x)) (snd x))) \<and> \<not> snd (getObject t a); ko_at' ko t a; cslift b (tcb_ptr_to_ctcb_ptr t) = Some ko'; ctcb_relation ko ko'; (ko, a) \<in> fst (getObject t a); ((), a\<lparr>ksPSpace := (ksPSpace a)(t \<mapsto> injectKOS (?ko45 a b ko ko'))\<rparr>) \<in> fst (setObject t (?ko45 a b ko ko') a)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch ko)) ko) a). (snd x, globals_update (t_hrs_'_update (\<lambda>_. hrs_mem_update (heap_update (PTR(user_context_C) &(PTR(arch_tcb_C) &(tcb_ptr_to_ctcb_ptr t\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])) tc') (t_hrs_' (globals b)))) b) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>a b ko ko'. \<lbrakk>ccontext_relation tc tc'; t' = tcb_ptr_to_ctcb_ptr t; (a, b) \<in> rf_sr; pspace_domain_valid a; tcb_at' t a; nf \<longrightarrow> (\<forall>x\<in>fst (getObject t a). \<not> snd (setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch (fst x))) (fst x)) (snd x))) \<and> \<not> snd (getObject t a); ko_at' ko t a; cslift b (tcb_ptr_to_ctcb_ptr t) = Some ko'; ctcb_relation ko ko'; (ko, a) \<in> fst (getObject t a); ((), a\<lparr>ksPSpace := (ksPSpace a)(t \<mapsto> KOTCB (?ko45 a b ko ko'))\<rparr>) \<in> fst (setObject t (?ko45 a b ko ko') a)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch ko)) ko) a). (snd x, globals_update (t_hrs_'_update (\<lambda>_. hrs_mem_update (heap_update (PTR(user_context_C) &(PTR(arch_tcb_C) &(tcb_ptr_to_ctcb_ptr t\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])) tc') (t_hrs_' (globals b)))) b) \<in> rf_sr proof (prove)
goal (2 subgoals):
 1. \<And>a b ko ko'. \<lbrakk>ccontext_relation tc tc'; t' = tcb_ptr_to_ctcb_ptr t; (a, b) \<in> rf_sr; pspace_domain_valid a; tcb_at' t a; nf \<longrightarrow> (\<forall>x\<in>fst (getObject t a). \<not> snd (setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch (fst x))) (fst x)) (snd x))) \<and> \<not> snd (getObject t a); ko_at' ko t a; cslift b (tcb_ptr_to_ctcb_ptr t) = Some ko'; ctcb_relation ko ko'; (ko, a) \<in> fst (getObject t a); ((), a\<lparr>ksPSpace := (ksPSpace a)(t \<mapsto> KOTCB (?ko45 a b ko ko'))\<rparr>) \<in> fst (setObject t (?ko45 a b ko ko') a)\<rbrakk> \<Longrightarrow> (snd (?x50 a b ko ko'), globals_update (t_hrs_'_update (\<lambda>_. hrs_mem_update (heap_update (PTR(user_context_C) &(PTR(arch_tcb_C) &(tcb_ptr_to_ctcb_ptr t\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])) tc') (t_hrs_' (globals b)))) b) \<in> rf_sr
 2. \<And>a b ko ko'. \<lbrakk>ccontext_relation tc tc'; t' = tcb_ptr_to_ctcb_ptr t; (a, b) \<in> rf_sr; pspace_domain_valid a; tcb_at' t a; nf \<longrightarrow> (\<forall>x\<in>fst (getObject t a). \<not> snd (setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch (fst x))) (fst x)) (snd x))) \<and> \<not> snd (getObject t a); ko_at' ko t a; cslift b (tcb_ptr_to_ctcb_ptr t) = Some ko'; ctcb_relation ko ko'; (ko, a) \<in> fst (getObject t a); ((), a\<lparr>ksPSpace := (ksPSpace a)(t \<mapsto> KOTCB (?ko45 a b ko ko'))\<rparr>) \<in> fst (setObject t (?ko45 a b ko ko') a)\<rbrakk> \<Longrightarrow> ?x50 a b ko ko' \<in> fst (setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch ko)) ko) a) proof (prove)
goal (2 subgoals):
 1. \<And>a b ko ko'. \<lbrakk>ccontext_relation tc tc'; t' = tcb_ptr_to_ctcb_ptr t; (a, b) \<in> rf_sr; pspace_domain_valid a; tcb_at' t a; nf \<longrightarrow> (\<forall>x\<in>fst (getObject t a). \<not> snd (setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch (fst x))) (fst x)) (snd x))) \<and> \<not> snd (getObject t a); ko_at' ko t a; cslift b (tcb_ptr_to_ctcb_ptr t) = Some ko'; ctcb_relation ko ko'; (ko, a) \<in> fst (getObject t a); ((), a\<lparr>ksPSpace := (ksPSpace a)(t \<mapsto> KOTCB (?ko45 a b ko ko'))\<rparr>) \<in> fst (setObject t (?ko45 a b ko ko') a)\<rbrakk> \<Longrightarrow> ?x50 a b ko ko' \<in> fst (setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch ko)) ko) a)
 2. \<And>a b ko ko'. \<lbrakk>ccontext_relation tc tc'; t' = tcb_ptr_to_ctcb_ptr t; (a, b) \<in> rf_sr; pspace_domain_valid a; tcb_at' t a; nf \<longrightarrow> (\<forall>x\<in>fst (getObject t a). \<not> snd (setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch (fst x))) (fst x)) (snd x))) \<and> \<not> snd (getObject t a); ko_at' ko t a; cslift b (tcb_ptr_to_ctcb_ptr t) = Some ko'; ctcb_relation ko ko'; (ko, a) \<in> fst (getObject t a); ((), a\<lparr>ksPSpace := (ksPSpace a)(t \<mapsto> KOTCB (?ko45 a b ko ko'))\<rparr>) \<in> fst (setObject t (?ko45 a b ko ko') a)\<rbrakk> \<Longrightarrow> (snd (?x50 a b ko ko'), globals_update (t_hrs_'_update (\<lambda>_. hrs_mem_update (heap_update (PTR(user_context_C) &(PTR(arch_tcb_C) &(tcb_ptr_to_ctcb_ptr t\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])) tc') (t_hrs_' (globals b)))) b) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>a b ko ko'. \<lbrakk>ccontext_relation tc tc'; t' = tcb_ptr_to_ctcb_ptr t; (a, b) \<in> rf_sr; pspace_domain_valid a; tcb_at' t a; nf \<longrightarrow> (\<forall>x\<in>fst (getObject t a). \<not> snd (setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch (fst x))) (fst x)) (snd x))) \<and> \<not> snd (getObject t a); ko_at' ko t a; cslift b (tcb_ptr_to_ctcb_ptr t) = Some ko'; ctcb_relation ko ko'; (ko, a) \<in> fst (getObject t a); ((), a\<lparr>ksPSpace := (ksPSpace a)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch ko)) ko))\<rparr>) \<in> fst (setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch ko)) ko) a)\<rbrakk> \<Longrightarrow> (snd ((), a\<lparr>ksPSpace := (ksPSpace a)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch ko)) ko))\<rparr>), globals_update (t_hrs_'_update (\<lambda>_. hrs_mem_update (heap_update (PTR(user_context_C) &(PTR(arch_tcb_C) &(tcb_ptr_to_ctcb_ptr t\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])) tc') (t_hrs_' (globals b)))) b) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>a b ko ko'. \<lbrakk>ccontext_relation tc tc'; t' = tcb_ptr_to_ctcb_ptr t; (a, b) \<in> rf_sr; pspace_domain_valid a; tcb_at' t a; nf \<longrightarrow> (\<forall>x\<in>fst (getObject t a). \<not> snd (setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch (fst x))) (fst x)) (snd x))) \<and> \<not> snd (getObject t a); ko_at' ko t a; cslift b (tcb_ptr_to_ctcb_ptr t) = Some ko'; ctcb_relation ko ko'; (ko, a) \<in> fst (getObject t a); ((), a\<lparr>ksPSpace := (ksPSpace a)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch ko)) ko))\<rparr>) \<in> fst (setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch ko)) ko) a)\<rbrakk> \<Longrightarrow> (a\<lparr>ksPSpace := (ksPSpace a)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch ko)) ko))\<rparr>, globals_update (t_hrs_'_update (\<lambda>_. hrs_mem_update (heap_update (PTR(user_context_C) &(PTR(arch_tcb_C) &(tcb_ptr_to_ctcb_ptr t\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])) tc') (t_hrs_' (globals b)))) b) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>a b ko ko'. \<lbrakk>ccontext_relation tc tc'; t' = tcb_ptr_to_ctcb_ptr t; (a, b) \<in> rf_sr; pspace_domain_valid a; tcb_at' t a; nf \<longrightarrow> (\<forall>x\<in>fst (getObject t a). \<not> snd (setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch (fst x))) (fst x)) (snd x))) \<and> \<not> snd (getObject t a); ko_at' ko t a; cslift b (tcb_ptr_to_ctcb_ptr t) = Some ko'; ctcb_relation ko ko'; (ko, a) \<in> fst (getObject t a); ((), a\<lparr>ksPSpace := (ksPSpace a)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch ko)) ko))\<rparr>) \<in> fst (setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch ko)) ko) a)\<rbrakk> \<Longrightarrow> (a\<lparr>ksPSpace := (ksPSpace a)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch ko)) ko))\<rparr>, globals_update (t_hrs_'_update (\<lambda>_. hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr t) (tcbArch_C_update (\<lambda>_. tcbContext_C_update (\<lambda>_. tc') (tcbArch_C ko')) ko')) (t_hrs_' (globals b)))) b) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>a b ko ko'. \<lbrakk>ccontext_relation tc tc'; t' = tcb_ptr_to_ctcb_ptr t; (a, b) \<in> rf_sr; pspace_domain_valid a; tcb_at' t a; nf \<longrightarrow> (\<forall>x\<in>fst (getObject t a). \<not> snd (setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch (fst x))) (fst x)) (snd x))) \<and> \<not> snd (getObject t a); ko_at' ko t a; cslift b (tcb_ptr_to_ctcb_ptr t) = Some ko'; ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> (a\<lparr>ksPSpace := (ksPSpace a)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch ko)) ko))\<rparr>, globals_update (t_hrs_'_update (\<lambda>_. hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr t) (tcbArch_C_update (\<lambda>_. tcbContext_C_update (\<lambda>_. tc') (tcbArch_C ko')) ko')) (t_hrs_' (globals b)))) b) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>a b ko ko'. \<lbrakk>ccontext_relation tc tc'; t' = tcb_ptr_to_ctcb_ptr t; pspace_domain_valid a; tcb_at' t a; nf \<longrightarrow> (\<forall>x\<in>fst (getObject t a). \<not> snd (setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch (fst x))) (fst x)) (snd x))) \<and> \<not> snd (getObject t a); ko_at' ko t a; cslift b (tcb_ptr_to_ctcb_ptr t) = Some ko'; ctcb_relation ko ko'; cmap_relation (ctes_of a) (cslift b) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace a)) (cslift b) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace a)) (cslift b) ep_Ptr (cendpoint_relation (cslift b)); cmap_relation (map_to_ntfns (ksPSpace a)) (cslift b) ntfn_Ptr (cnotification_relation (cslift b)); cmap_relation (map_to_pdes (ksPSpace a)) (cslift b) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace a)) (cslift b) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace a)) (cslift b) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace a) (underlying_memory (ksMachineState a))) (cslift b) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace a) (underlying_memory (ksMachineState a))) (cslift b) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace a)) (c_h_t_valid b) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace a)) (c_h_t_valid b) pt_Ptr; cready_queues_relation (cslift b) (ksReadyQueues_' (globals b)) (ksReadyQueues a); zero_ranges_are_zero (gsUntypedZeroRanges a) (t_hrs_' (globals b)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals b)) (ksReadyQueuesL1Bitmap a); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals b)) (ksReadyQueuesL2Bitmap a); ksCurThread_' (globals b) = tcb_ptr_to_ctcb_ptr (ksCurThread a); ksIdleThread_' (globals b) = tcb_ptr_to_ctcb_ptr (ksIdleThread a); cinterrupt_relation (ksInterruptState a) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals b)); cscheduler_action_relation (ksSchedulerAction a) (ksSchedulerAction_' (globals b)); armKSNextASID_' (globals b) = armKSNextASID (ksArchState a); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState a); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState a)) (armKSHWASIDTable_' (globals b)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState a)) (armKSASIDTable_' (globals b)); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState a)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift b \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState a); irq_masks (ksMachineState a) = irq_masks (phantom_machine_state_' (globals b)); irq_state (ksMachineState a) = irq_state (phantom_machine_state_' (globals b)); device_state (ksMachineState a) = device_state (phantom_machine_state_' (globals b)); exclusive_state (ksMachineState a) = exclusive_state (phantom_machine_state_' (globals b)); machine_state_rest (ksMachineState a) = machine_state_rest (phantom_machine_state_' (globals b)); cte_array_relation a (globals b); tcb_cte_array_relation a (globals b); apsnd fst (ghost'state_' (globals b)) = (gsUserPages a, gsCNodes a); ghost_size_rel (ghost'state_' (globals b)) (gsMaxObjectSize a); ksWorkUnitsCompleted_' (globals b) = ksWorkUnitsCompleted a; b \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; b \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals b))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule a) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals b) = word_of_nat (ksDomScheduleIdx a); ksCurDomain_' (globals b) = UCAST(8 \<rightarrow> 32) (ksCurDomain a); ksDomainTime_' (globals b) = ksDomainTime a\<rbrakk> \<Longrightarrow> cmap_relation (map_to_ctes ((ksPSpace a)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch ko)) ko)))) (cslift b) cte_Ptr ccte_relation \<and> cmap_relation (map_to_tcbs ((ksPSpace a)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch ko)) ko)))) ((cslift b)(tcb_ptr_to_ctcb_ptr t \<mapsto> tcbArch_C_update (\<lambda>_. tcbContext_C_update (\<lambda>_. tc') (tcbArch_C ko')) ko')) tcb_ptr_to_ctcb_ptr ctcb_relation \<and> cmap_relation (map_to_eps (ksPSpace a)) (cslift b) ep_Ptr (cendpoint_relation ((cslift b)(tcb_ptr_to_ctcb_ptr t \<mapsto> tcbArch_C_update (\<lambda>_. tcbContext_C_update (\<lambda>_. tc') (tcbArch_C ko')) ko'))) \<and> cmap_relation (map_to_ntfns (ksPSpace a)) (cslift b) ntfn_Ptr (cnotification_relation ((cslift b)(tcb_ptr_to_ctcb_ptr t \<mapsto> tcbArch_C_update (\<lambda>_. tcbContext_C_update (\<lambda>_. tc') (tcbArch_C ko')) ko'))) \<and> cready_queues_relation ((cslift b)(tcb_ptr_to_ctcb_ptr t \<mapsto> tcbArch_C_update (\<lambda>_. tcbContext_C_update (\<lambda>_. tc') (tcbArch_C ko')) ko')) (ksReadyQueues_' (globals b)) (ksReadyQueues a) \<and> cvariable_array_map_relation (map_to_tcbs ((ksPSpace a)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch ko)) ko)))) (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' (globals b))) proof (prove)
goal (1 subgoal):
 1. \<And>a b ko ko'. \<lbrakk>ccontext_relation tc tc'; t' = tcb_ptr_to_ctcb_ptr t; pspace_domain_valid a; tcb_at' t a; nf \<longrightarrow> (\<forall>x\<in>fst (getObject t a). \<not> snd (setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch (fst x))) (fst x)) (snd x))) \<and> \<not> snd (getObject t a); ko_at' ko t a; cslift b (tcb_ptr_to_ctcb_ptr t) = Some ko'; ctcb_relation ko ko'; cmap_relation (ctes_of a) (cslift b) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace a)) (cslift b) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace a)) (cslift b) ep_Ptr (cendpoint_relation (cslift b)); cmap_relation (map_to_ntfns (ksPSpace a)) (cslift b) ntfn_Ptr (cnotification_relation (cslift b)); cmap_relation (map_to_pdes (ksPSpace a)) (cslift b) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace a)) (cslift b) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace a)) (cslift b) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace a) (underlying_memory (ksMachineState a))) (cslift b) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace a) (underlying_memory (ksMachineState a))) (cslift b) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace a)) (c_h_t_valid b) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace a)) (c_h_t_valid b) pt_Ptr; cready_queues_relation (cslift b) (ksReadyQueues_' (globals b)) (ksReadyQueues a); zero_ranges_are_zero (gsUntypedZeroRanges a) (t_hrs_' (globals b)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals b)) (ksReadyQueuesL1Bitmap a); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals b)) (ksReadyQueuesL2Bitmap a); ksCurThread_' (globals b) = tcb_ptr_to_ctcb_ptr (ksCurThread a); ksIdleThread_' (globals b) = tcb_ptr_to_ctcb_ptr (ksIdleThread a); cinterrupt_relation (ksInterruptState a) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals b)); cscheduler_action_relation (ksSchedulerAction a) (ksSchedulerAction_' (globals b)); armKSNextASID_' (globals b) = armKSNextASID (ksArchState a); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState a); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState a)) (armKSHWASIDTable_' (globals b)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState a)) (armKSASIDTable_' (globals b)); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState a)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift b \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState a); irq_masks (ksMachineState a) = irq_masks (phantom_machine_state_' (globals b)); irq_state (ksMachineState a) = irq_state (phantom_machine_state_' (globals b)); device_state (ksMachineState a) = device_state (phantom_machine_state_' (globals b)); exclusive_state (ksMachineState a) = exclusive_state (phantom_machine_state_' (globals b)); machine_state_rest (ksMachineState a) = machine_state_rest (phantom_machine_state_' (globals b)); cte_array_relation a (globals b); tcb_cte_array_relation a (globals b); apsnd fst (ghost'state_' (globals b)) = (gsUserPages a, gsCNodes a); ghost_size_rel (ghost'state_' (globals b)) (gsMaxObjectSize a); ksWorkUnitsCompleted_' (globals b) = ksWorkUnitsCompleted a; b \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; b \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals b))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule a) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals b) = word_of_nat (ksDomScheduleIdx a); ksCurDomain_' (globals b) = UCAST(8 \<rightarrow> 32) (ksCurDomain a); ksDomainTime_' (globals b) = ksDomainTime a\<rbrakk> \<Longrightarrow> cmap_relation ((map_to_tcbs (ksPSpace a))(t \<mapsto> tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch ko)) ko)) ((cslift b)(tcb_ptr_to_ctcb_ptr t \<mapsto> tcbArch_C_update (\<lambda>_. tcbContext_C_update (\<lambda>_. tc') (tcbArch_C ko')) ko')) tcb_ptr_to_ctcb_ptr ctcb_relation \<and> cmap_relation (map_to_eps (ksPSpace a)) (cslift b) ep_Ptr (cendpoint_relation ((cslift b)(tcb_ptr_to_ctcb_ptr t \<mapsto> tcbArch_C_update (\<lambda>_. tcbContext_C_update (\<lambda>_. tc') (tcbArch_C ko')) ko'))) \<and> cmap_relation (map_to_ntfns (ksPSpace a)) (cslift b) ntfn_Ptr (cnotification_relation ((cslift b)(tcb_ptr_to_ctcb_ptr t \<mapsto> tcbArch_C_update (\<lambda>_. tcbContext_C_update (\<lambda>_. tc') (tcbArch_C ko')) ko'))) \<and> cready_queues_relation ((cslift b)(tcb_ptr_to_ctcb_ptr t \<mapsto> tcbArch_C_update (\<lambda>_. tcbContext_C_update (\<lambda>_. tc') (tcbArch_C ko')) ko')) (ksReadyQueues_' (globals b)) (ksReadyQueues a) proof (prove)
goal (1 subgoal):
 1. \<And>a b ko ko'. \<lbrakk>ccontext_relation tc tc'; t' = tcb_ptr_to_ctcb_ptr t; pspace_domain_valid a; tcb_at' t a; nf \<longrightarrow> (\<forall>x\<in>fst (getObject t a). \<not> snd (setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch (fst x))) (fst x)) (snd x))) \<and> \<not> snd (getObject t a); ko_at' ko t a; cslift b (tcb_ptr_to_ctcb_ptr t) = Some ko'; ctcb_relation ko ko'; cmap_relation (ctes_of a) (cslift b) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace a)) (cslift b) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace a)) (cslift b) ep_Ptr (cendpoint_relation (cslift b)); cmap_relation (map_to_ntfns (ksPSpace a)) (cslift b) ntfn_Ptr (cnotification_relation (cslift b)); cmap_relation (map_to_pdes (ksPSpace a)) (cslift b) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace a)) (cslift b) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace a)) (cslift b) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace a) (underlying_memory (ksMachineState a))) (cslift b) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace a) (underlying_memory (ksMachineState a))) (cslift b) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace a)) (c_h_t_valid b) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace a)) (c_h_t_valid b) pt_Ptr; cready_queues_relation (cslift b) (ksReadyQueues_' (globals b)) (ksReadyQueues a); zero_ranges_are_zero (gsUntypedZeroRanges a) (t_hrs_' (globals b)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals b)) (ksReadyQueuesL1Bitmap a); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals b)) (ksReadyQueuesL2Bitmap a); ksCurThread_' (globals b) = tcb_ptr_to_ctcb_ptr (ksCurThread a); ksIdleThread_' (globals b) = tcb_ptr_to_ctcb_ptr (ksIdleThread a); cinterrupt_relation (ksInterruptState a) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals b)); cscheduler_action_relation (ksSchedulerAction a) (ksSchedulerAction_' (globals b)); armKSNextASID_' (globals b) = armKSNextASID (ksArchState a); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState a); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState a)) (armKSHWASIDTable_' (globals b)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState a)) (armKSASIDTable_' (globals b)); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState a)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift b \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState a); irq_masks (ksMachineState a) = irq_masks (phantom_machine_state_' (globals b)); irq_state (ksMachineState a) = irq_state (phantom_machine_state_' (globals b)); device_state (ksMachineState a) = device_state (phantom_machine_state_' (globals b)); exclusive_state (ksMachineState a) = exclusive_state (phantom_machine_state_' (globals b)); machine_state_rest (ksMachineState a) = machine_state_rest (phantom_machine_state_' (globals b)); cte_array_relation a (globals b); tcb_cte_array_relation a (globals b); apsnd fst (ghost'state_' (globals b)) = (gsUserPages a, gsCNodes a); ghost_size_rel (ghost'state_' (globals b)) (gsMaxObjectSize a); ksWorkUnitsCompleted_' (globals b) = ksWorkUnitsCompleted a; b \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; b \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals b))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule a) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals b) = word_of_nat (ksDomScheduleIdx a); ksCurDomain_' (globals b) = UCAST(8 \<rightarrow> 32) (ksCurDomain a); ksDomainTime_' (globals b) = ksDomainTime a\<rbrakk> \<Longrightarrow> cmap_relation ((map_to_tcbs (ksPSpace a))(t \<mapsto> tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch ko)) ko)) ((cslift b)(tcb_ptr_to_ctcb_ptr t \<mapsto> tcbArch_C_update (\<lambda>_. tcbContext_C_update (\<lambda>_. tc') (tcbArch_C ko')) ko')) tcb_ptr_to_ctcb_ptr ctcb_relation \<and> cready_queues_relation ((cslift b)(tcb_ptr_to_ctcb_ptr t \<mapsto> tcbArch_C_update (\<lambda>_. tcbContext_C_update (\<lambda>_. tc') (tcbArch_C ko')) ko')) (ksReadyQueues_' (globals b)) (ksReadyQueues a) proof (prove)
goal (1 subgoal):
 1. \<And>a b ko ko'. \<lbrakk>ccontext_relation tc tc'; t' = tcb_ptr_to_ctcb_ptr t; pspace_domain_valid a; tcb_at' t a; nf \<longrightarrow> (\<forall>x\<in>fst (getObject t a). \<not> snd (setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch (fst x))) (fst x)) (snd x))) \<and> \<not> snd (getObject t a); ko_at' ko t a; cslift b (tcb_ptr_to_ctcb_ptr t) = Some ko'; ctcb_relation ko ko'; cmap_relation (ctes_of a) (cslift b) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace a)) (cslift b) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace a)) (cslift b) ep_Ptr (cendpoint_relation (cslift b)); cmap_relation (map_to_ntfns (ksPSpace a)) (cslift b) ntfn_Ptr (cnotification_relation (cslift b)); cmap_relation (map_to_pdes (ksPSpace a)) (cslift b) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace a)) (cslift b) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace a)) (cslift b) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace a) (underlying_memory (ksMachineState a))) (cslift b) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace a) (underlying_memory (ksMachineState a))) (cslift b) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace a)) (c_h_t_valid b) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace a)) (c_h_t_valid b) pt_Ptr; cready_queues_relation (cslift b) (ksReadyQueues_' (globals b)) (ksReadyQueues a); zero_ranges_are_zero (gsUntypedZeroRanges a) (t_hrs_' (globals b)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals b)) (ksReadyQueuesL1Bitmap a); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals b)) (ksReadyQueuesL2Bitmap a); ksCurThread_' (globals b) = tcb_ptr_to_ctcb_ptr (ksCurThread a); ksIdleThread_' (globals b) = tcb_ptr_to_ctcb_ptr (ksIdleThread a); cinterrupt_relation (ksInterruptState a) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals b)); cscheduler_action_relation (ksSchedulerAction a) (ksSchedulerAction_' (globals b)); armKSNextASID_' (globals b) = armKSNextASID (ksArchState a); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState a); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState a)) (armKSHWASIDTable_' (globals b)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState a)) (armKSASIDTable_' (globals b)); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState a)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift b \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState a); irq_masks (ksMachineState a) = irq_masks (phantom_machine_state_' (globals b)); irq_state (ksMachineState a) = irq_state (phantom_machine_state_' (globals b)); device_state (ksMachineState a) = device_state (phantom_machine_state_' (globals b)); exclusive_state (ksMachineState a) = exclusive_state (phantom_machine_state_' (globals b)); machine_state_rest (ksMachineState a) = machine_state_rest (phantom_machine_state_' (globals b)); cte_array_relation a (globals b); tcb_cte_array_relation a (globals b); apsnd fst (ghost'state_' (globals b)) = (gsUserPages a, gsCNodes a); ghost_size_rel (ghost'state_' (globals b)) (gsMaxObjectSize a); ksWorkUnitsCompleted_' (globals b) = ksWorkUnitsCompleted a; b \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; b \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals b))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule a) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals b) = word_of_nat (ksDomScheduleIdx a); ksCurDomain_' (globals b) = UCAST(8 \<rightarrow> 32) (ksCurDomain a); ksDomainTime_' (globals b) = ksDomainTime a\<rbrakk> \<Longrightarrow> cmap_relation ((map_to_tcbs (ksPSpace a))(t \<mapsto> tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch ko)) ko)) ((cslift b)(tcb_ptr_to_ctcb_ptr t \<mapsto> tcbArch_C_update (\<lambda>_. tcbContext_C_update (\<lambda>_. tc') (tcbArch_C ko')) ko')) tcb_ptr_to_ctcb_ptr ctcb_relation proof (prove)
goal (1 subgoal):
 1. \<And>a b ko ko'. \<lbrakk>ccontext_relation tc tc'; t' = tcb_ptr_to_ctcb_ptr t; pspace_domain_valid a; tcb_at' t a; nf \<longrightarrow> (\<forall>x\<in>fst (getObject t a). \<not> snd (setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch (fst x))) (fst x)) (snd x))) \<and> \<not> snd (getObject t a); cslift b (tcb_ptr_to_ctcb_ptr t) = Some ko'; ctcb_relation ko ko'; cmap_relation (ctes_of a) (cslift b) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace a)) (cslift b) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace a)) (cslift b) ep_Ptr (cendpoint_relation (cslift b)); cmap_relation (map_to_ntfns (ksPSpace a)) (cslift b) ntfn_Ptr (cnotification_relation (cslift b)); cmap_relation (map_to_pdes (ksPSpace a)) (cslift b) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace a)) (cslift b) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace a)) (cslift b) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace a) (underlying_memory (ksMachineState a))) (cslift b) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace a) (underlying_memory (ksMachineState a))) (cslift b) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace a)) (c_h_t_valid b) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace a)) (c_h_t_valid b) pt_Ptr; cready_queues_relation (cslift b) (ksReadyQueues_' (globals b)) (ksReadyQueues a); zero_ranges_are_zero (gsUntypedZeroRanges a) (t_hrs_' (globals b)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals b)) (ksReadyQueuesL1Bitmap a); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals b)) (ksReadyQueuesL2Bitmap a); ksCurThread_' (globals b) = tcb_ptr_to_ctcb_ptr (ksCurThread a); ksIdleThread_' (globals b) = tcb_ptr_to_ctcb_ptr (ksIdleThread a); cinterrupt_relation (ksInterruptState a) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals b)); cscheduler_action_relation (ksSchedulerAction a) (ksSchedulerAction_' (globals b)); armKSNextASID_' (globals b) = armKSNextASID (ksArchState a); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState a); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState a)) (armKSHWASIDTable_' (globals b)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState a)) (armKSASIDTable_' (globals b)); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState a)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift b \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState a); irq_masks (ksMachineState a) = irq_masks (phantom_machine_state_' (globals b)); irq_state (ksMachineState a) = irq_state (phantom_machine_state_' (globals b)); device_state (ksMachineState a) = device_state (phantom_machine_state_' (globals b)); exclusive_state (ksMachineState a) = exclusive_state (phantom_machine_state_' (globals b)); machine_state_rest (ksMachineState a) = machine_state_rest (phantom_machine_state_' (globals b)); cte_array_relation a (globals b); tcb_cte_array_relation a (globals b); apsnd fst (ghost'state_' (globals b)) = (gsUserPages a, gsCNodes a); ghost_size_rel (ghost'state_' (globals b)) (gsMaxObjectSize a); ksWorkUnitsCompleted_' (globals b) = ksWorkUnitsCompleted a; b \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; b \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals b))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule a) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals b) = word_of_nat (ksDomScheduleIdx a); ksCurDomain_' (globals b) = UCAST(8 \<rightarrow> 32) (ksCurDomain a); ksDomainTime_' (globals b) = ksDomainTime a; map_to_tcbs (ksPSpace a) t = Some ko\<rbrakk> \<Longrightarrow> cmap_relation ((map_to_tcbs (ksPSpace a))(t \<mapsto> tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch ko)) ko)) ((cslift b)(tcb_ptr_to_ctcb_ptr t \<mapsto> tcbArch_C_update (\<lambda>_. tcbContext_C_update (\<lambda>_. tc') (tcbArch_C ko')) ko')) tcb_ptr_to_ctcb_ptr ctcb_relation proof (prove)
goal (3 subgoals):
 1. \<And>a b ko ko'. \<lbrakk>ccontext_relation tc tc'; t' = tcb_ptr_to_ctcb_ptr t; pspace_domain_valid a; tcb_at' t a; nf \<longrightarrow> (\<forall>x\<in>fst (getObject t a). \<not> snd (setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch (fst x))) (fst x)) (snd x))) \<and> \<not> snd (getObject t a); cslift b (tcb_ptr_to_ctcb_ptr t) = Some ko'; ctcb_relation ko ko'; cmap_relation (ctes_of a) (cslift b) cte_Ptr ccte_relation; cmap_relation (map_to_eps (ksPSpace a)) (cslift b) ep_Ptr (cendpoint_relation (cslift b)); cmap_relation (map_to_ntfns (ksPSpace a)) (cslift b) ntfn_Ptr (cnotification_relation (cslift b)); cmap_relation (map_to_pdes (ksPSpace a)) (cslift b) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace a)) (cslift b) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace a)) (cslift b) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace a) (underlying_memory (ksMachineState a))) (cslift b) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace a) (underlying_memory (ksMachineState a))) (cslift b) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace a)) (c_h_t_valid b) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace a)) (c_h_t_valid b) pt_Ptr; cready_queues_relation (cslift b) (ksReadyQueues_' (globals b)) (ksReadyQueues a); zero_ranges_are_zero (gsUntypedZeroRanges a) (t_hrs_' (globals b)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals b)) (ksReadyQueuesL1Bitmap a); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals b)) (ksReadyQueuesL2Bitmap a); ksCurThread_' (globals b) = tcb_ptr_to_ctcb_ptr (ksCurThread a); ksIdleThread_' (globals b) = tcb_ptr_to_ctcb_ptr (ksIdleThread a); cinterrupt_relation (ksInterruptState a) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals b)); cscheduler_action_relation (ksSchedulerAction a) (ksSchedulerAction_' (globals b)); armKSNextASID_' (globals b) = armKSNextASID (ksArchState a); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState a); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState a)) (armKSHWASIDTable_' (globals b)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState a)) (armKSASIDTable_' (globals b)); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState a)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift b \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState a); irq_masks (ksMachineState a) = irq_masks (phantom_machine_state_' (globals b)); irq_state (ksMachineState a) = irq_state (phantom_machine_state_' (globals b)); device_state (ksMachineState a) = device_state (phantom_machine_state_' (globals b)); exclusive_state (ksMachineState a) = exclusive_state (phantom_machine_state_' (globals b)); machine_state_rest (ksMachineState a) = machine_state_rest (phantom_machine_state_' (globals b)); cte_array_relation a (globals b); tcb_cte_array_relation a (globals b); apsnd fst (ghost'state_' (globals b)) = (gsUserPages a, gsCNodes a); ghost_size_rel (ghost'state_' (globals b)) (gsMaxObjectSize a); ksWorkUnitsCompleted_' (globals b) = ksWorkUnitsCompleted a; b \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; b \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals b))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule a) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals b) = word_of_nat (ksDomScheduleIdx a); ksCurDomain_' (globals b) = UCAST(8 \<rightarrow> 32) (ksCurDomain a); ksDomainTime_' (globals b) = ksDomainTime a; map_to_tcbs (ksPSpace a) t = Some ko\<rbrakk> \<Longrightarrow> ctcb_relation (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch ko)) ko) (tcbArch_C_update (\<lambda>_. tcbContext_C_update (\<lambda>_. tc') (tcbArch_C ko')) ko')
 2. \<And>a b ko ko' x ov ov'. \<lbrakk>ccontext_relation tc tc'; t' = tcb_ptr_to_ctcb_ptr t; pspace_domain_valid a; tcb_at' t a; nf \<longrightarrow> (\<forall>x\<in>fst (getObject t a). \<not> snd (setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch (fst x))) (fst x)) (snd x))) \<and> \<not> snd (getObject t a); cslift b (tcb_ptr_to_ctcb_ptr t) = Some ko'; ctcb_relation ko ko'; cmap_relation (ctes_of a) (cslift b) cte_Ptr ccte_relation; cmap_relation (map_to_eps (ksPSpace a)) (cslift b) ep_Ptr (cendpoint_relation (cslift b)); cmap_relation (map_to_ntfns (ksPSpace a)) (cslift b) ntfn_Ptr (cnotification_relation (cslift b)); cmap_relation (map_to_pdes (ksPSpace a)) (cslift b) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace a)) (cslift b) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace a)) (cslift b) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace a) (underlying_memory (ksMachineState a))) (cslift b) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace a) (underlying_memory (ksMachineState a))) (cslift b) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace a)) (c_h_t_valid b) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace a)) (c_h_t_valid b) pt_Ptr; cready_queues_relation (cslift b) (ksReadyQueues_' (globals b)) (ksReadyQueues a); zero_ranges_are_zero (gsUntypedZeroRanges a) (t_hrs_' (globals b)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals b)) (ksReadyQueuesL1Bitmap a); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals b)) (ksReadyQueuesL2Bitmap a); ksCurThread_' (globals b) = tcb_ptr_to_ctcb_ptr (ksCurThread a); ksIdleThread_' (globals b) = tcb_ptr_to_ctcb_ptr (ksIdleThread a); cinterrupt_relation (ksInterruptState a) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals b)); cscheduler_action_relation (ksSchedulerAction a) (ksSchedulerAction_' (globals b)); armKSNextASID_' (globals b) = armKSNextASID (ksArchState a); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState a); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState a)) (armKSHWASIDTable_' (globals b)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState a)) (armKSASIDTable_' (globals b)); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState a)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift b \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState a); irq_masks (ksMachineState a) = irq_masks (phantom_machine_state_' (globals b)); irq_state (ksMachineState a) = irq_state (phantom_machine_state_' (globals b)); device_state (ksMachineState a) = device_state (phantom_machine_state_' (globals b)); exclusive_state (ksMachineState a) = exclusive_state (phantom_machine_state_' (globals b)); machine_state_rest (ksMachineState a) = machine_state_rest (phantom_machine_state_' (globals b)); cte_array_relation a (globals b); tcb_cte_array_relation a (globals b); apsnd fst (ghost'state_' (globals b)) = (gsUserPages a, gsCNodes a); ghost_size_rel (ghost'state_' (globals b)) (gsMaxObjectSize a); ksWorkUnitsCompleted_' (globals b) = ksWorkUnitsCompleted a; b \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; b \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals b))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule a) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals b) = word_of_nat (ksDomScheduleIdx a); ksCurDomain_' (globals b) = UCAST(8 \<rightarrow> 32) (ksCurDomain a); ksDomainTime_' (globals b) = ksDomainTime a; map_to_tcbs (ksPSpace a) t = Some ko; x \<noteq> t; map_to_tcbs (ksPSpace a) x = Some ov; cslift b (tcb_ptr_to_ctcb_ptr x) = Some ov'; ctcb_relation ov ov'\<rbrakk> \<Longrightarrow> ctcb_relation ov ov'
 3. \<And>a b ko ko'. \<lbrakk>ccontext_relation tc tc'; t' = tcb_ptr_to_ctcb_ptr t; pspace_domain_valid a; tcb_at' t a; nf \<longrightarrow> (\<forall>x\<in>fst (getObject t a). \<not> snd (setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch (fst x))) (fst x)) (snd x))) \<and> \<not> snd (getObject t a); cslift b (tcb_ptr_to_ctcb_ptr t) = Some ko'; ctcb_relation ko ko'; cmap_relation (ctes_of a) (cslift b) cte_Ptr ccte_relation; cmap_relation (map_to_eps (ksPSpace a)) (cslift b) ep_Ptr (cendpoint_relation (cslift b)); cmap_relation (map_to_ntfns (ksPSpace a)) (cslift b) ntfn_Ptr (cnotification_relation (cslift b)); cmap_relation (map_to_pdes (ksPSpace a)) (cslift b) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace a)) (cslift b) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace a)) (cslift b) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace a) (underlying_memory (ksMachineState a))) (cslift b) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace a) (underlying_memory (ksMachineState a))) (cslift b) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace a)) (c_h_t_valid b) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace a)) (c_h_t_valid b) pt_Ptr; cready_queues_relation (cslift b) (ksReadyQueues_' (globals b)) (ksReadyQueues a); zero_ranges_are_zero (gsUntypedZeroRanges a) (t_hrs_' (globals b)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals b)) (ksReadyQueuesL1Bitmap a); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals b)) (ksReadyQueuesL2Bitmap a); ksCurThread_' (globals b) = tcb_ptr_to_ctcb_ptr (ksCurThread a); ksIdleThread_' (globals b) = tcb_ptr_to_ctcb_ptr (ksIdleThread a); cinterrupt_relation (ksInterruptState a) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals b)); cscheduler_action_relation (ksSchedulerAction a) (ksSchedulerAction_' (globals b)); armKSNextASID_' (globals b) = armKSNextASID (ksArchState a); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState a); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState a)) (armKSHWASIDTable_' (globals b)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState a)) (armKSASIDTable_' (globals b)); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState a)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift b \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState a); irq_masks (ksMachineState a) = irq_masks (phantom_machine_state_' (globals b)); irq_state (ksMachineState a) = irq_state (phantom_machine_state_' (globals b)); device_state (ksMachineState a) = device_state (phantom_machine_state_' (globals b)); exclusive_state (ksMachineState a) = exclusive_state (phantom_machine_state_' (globals b)); machine_state_rest (ksMachineState a) = machine_state_rest (phantom_machine_state_' (globals b)); cte_array_relation a (globals b); tcb_cte_array_relation a (globals b); apsnd fst (ghost'state_' (globals b)) = (gsUserPages a, gsCNodes a); ghost_size_rel (ghost'state_' (globals b)) (gsMaxObjectSize a); ksWorkUnitsCompleted_' (globals b) = ksWorkUnitsCompleted a; b \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; b \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals b))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule a) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals b) = word_of_nat (ksDomScheduleIdx a); ksCurDomain_' (globals b) = UCAST(8 \<rightarrow> 32) (ksCurDomain a); ksDomainTime_' (globals b) = ksDomainTime a; map_to_tcbs (ksPSpace a) t = Some ko\<rbrakk> \<Longrightarrow> inj tcb_ptr_to_ctcb_ptr proof (prove)
goal (2 subgoals):
 1. \<And>a b ko ko' x ov ov'. \<lbrakk>ccontext_relation tc tc'; t' = tcb_ptr_to_ctcb_ptr t; pspace_domain_valid a; tcb_at' t a; nf \<longrightarrow> (\<forall>x\<in>fst (getObject t a). \<not> snd (setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch (fst x))) (fst x)) (snd x))) \<and> \<not> snd (getObject t a); cslift b (tcb_ptr_to_ctcb_ptr t) = Some ko'; ctcb_relation ko ko'; cmap_relation (ctes_of a) (cslift b) cte_Ptr ccte_relation; cmap_relation (map_to_eps (ksPSpace a)) (cslift b) ep_Ptr (cendpoint_relation (cslift b)); cmap_relation (map_to_ntfns (ksPSpace a)) (cslift b) ntfn_Ptr (cnotification_relation (cslift b)); cmap_relation (map_to_pdes (ksPSpace a)) (cslift b) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace a)) (cslift b) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace a)) (cslift b) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace a) (underlying_memory (ksMachineState a))) (cslift b) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace a) (underlying_memory (ksMachineState a))) (cslift b) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace a)) (c_h_t_valid b) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace a)) (c_h_t_valid b) pt_Ptr; cready_queues_relation (cslift b) (ksReadyQueues_' (globals b)) (ksReadyQueues a); zero_ranges_are_zero (gsUntypedZeroRanges a) (t_hrs_' (globals b)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals b)) (ksReadyQueuesL1Bitmap a); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals b)) (ksReadyQueuesL2Bitmap a); ksCurThread_' (globals b) = tcb_ptr_to_ctcb_ptr (ksCurThread a); ksIdleThread_' (globals b) = tcb_ptr_to_ctcb_ptr (ksIdleThread a); cinterrupt_relation (ksInterruptState a) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals b)); cscheduler_action_relation (ksSchedulerAction a) (ksSchedulerAction_' (globals b)); armKSNextASID_' (globals b) = armKSNextASID (ksArchState a); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState a); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState a)) (armKSHWASIDTable_' (globals b)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState a)) (armKSASIDTable_' (globals b)); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState a)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift b \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState a); irq_masks (ksMachineState a) = irq_masks (phantom_machine_state_' (globals b)); irq_state (ksMachineState a) = irq_state (phantom_machine_state_' (globals b)); device_state (ksMachineState a) = device_state (phantom_machine_state_' (globals b)); exclusive_state (ksMachineState a) = exclusive_state (phantom_machine_state_' (globals b)); machine_state_rest (ksMachineState a) = machine_state_rest (phantom_machine_state_' (globals b)); cte_array_relation a (globals b); tcb_cte_array_relation a (globals b); apsnd fst (ghost'state_' (globals b)) = (gsUserPages a, gsCNodes a); ghost_size_rel (ghost'state_' (globals b)) (gsMaxObjectSize a); ksWorkUnitsCompleted_' (globals b) = ksWorkUnitsCompleted a; b \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; b \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals b))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule a) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals b) = word_of_nat (ksDomScheduleIdx a); ksCurDomain_' (globals b) = UCAST(8 \<rightarrow> 32) (ksCurDomain a); ksDomainTime_' (globals b) = ksDomainTime a; map_to_tcbs (ksPSpace a) t = Some ko; x \<noteq> t; map_to_tcbs (ksPSpace a) x = Some ov; cslift b (tcb_ptr_to_ctcb_ptr x) = Some ov'; ctcb_relation ov ov'\<rbrakk> \<Longrightarrow> ctcb_relation ov ov'
 2. \<And>a b ko ko'. \<lbrakk>ccontext_relation tc tc'; t' = tcb_ptr_to_ctcb_ptr t; pspace_domain_valid a; tcb_at' t a; nf \<longrightarrow> (\<forall>x\<in>fst (getObject t a). \<not> snd (setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch (fst x))) (fst x)) (snd x))) \<and> \<not> snd (getObject t a); cslift b (tcb_ptr_to_ctcb_ptr t) = Some ko'; ctcb_relation ko ko'; cmap_relation (ctes_of a) (cslift b) cte_Ptr ccte_relation; cmap_relation (map_to_eps (ksPSpace a)) (cslift b) ep_Ptr (cendpoint_relation (cslift b)); cmap_relation (map_to_ntfns (ksPSpace a)) (cslift b) ntfn_Ptr (cnotification_relation (cslift b)); cmap_relation (map_to_pdes (ksPSpace a)) (cslift b) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace a)) (cslift b) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace a)) (cslift b) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace a) (underlying_memory (ksMachineState a))) (cslift b) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace a) (underlying_memory (ksMachineState a))) (cslift b) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace a)) (c_h_t_valid b) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace a)) (c_h_t_valid b) pt_Ptr; cready_queues_relation (cslift b) (ksReadyQueues_' (globals b)) (ksReadyQueues a); zero_ranges_are_zero (gsUntypedZeroRanges a) (t_hrs_' (globals b)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals b)) (ksReadyQueuesL1Bitmap a); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals b)) (ksReadyQueuesL2Bitmap a); ksCurThread_' (globals b) = tcb_ptr_to_ctcb_ptr (ksCurThread a); ksIdleThread_' (globals b) = tcb_ptr_to_ctcb_ptr (ksIdleThread a); cinterrupt_relation (ksInterruptState a) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals b)); cscheduler_action_relation (ksSchedulerAction a) (ksSchedulerAction_' (globals b)); armKSNextASID_' (globals b) = armKSNextASID (ksArchState a); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState a); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState a)) (armKSHWASIDTable_' (globals b)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState a)) (armKSASIDTable_' (globals b)); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState a)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift b \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState a); irq_masks (ksMachineState a) = irq_masks (phantom_machine_state_' (globals b)); irq_state (ksMachineState a) = irq_state (phantom_machine_state_' (globals b)); device_state (ksMachineState a) = device_state (phantom_machine_state_' (globals b)); exclusive_state (ksMachineState a) = exclusive_state (phantom_machine_state_' (globals b)); machine_state_rest (ksMachineState a) = machine_state_rest (phantom_machine_state_' (globals b)); cte_array_relation a (globals b); tcb_cte_array_relation a (globals b); apsnd fst (ghost'state_' (globals b)) = (gsUserPages a, gsCNodes a); ghost_size_rel (ghost'state_' (globals b)) (gsMaxObjectSize a); ksWorkUnitsCompleted_' (globals b) = ksWorkUnitsCompleted a; b \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; b \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals b))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule a) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals b) = word_of_nat (ksDomScheduleIdx a); ksCurDomain_' (globals b) = UCAST(8 \<rightarrow> 32) (ksCurDomain a); ksDomainTime_' (globals b) = ksDomainTime a; map_to_tcbs (ksPSpace a) t = Some ko\<rbrakk> \<Longrightarrow> inj tcb_ptr_to_ctcb_ptr proof (prove)
goal (1 subgoal):
 1. \<And>a b ko ko'. \<lbrakk>ccontext_relation tc tc'; t' = tcb_ptr_to_ctcb_ptr t; pspace_domain_valid a; tcb_at' t a; nf \<longrightarrow> (\<forall>x\<in>fst (getObject t a). \<not> snd (setObject t (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch (fst x))) (fst x)) (snd x))) \<and> \<not> snd (getObject t a); cslift b (tcb_ptr_to_ctcb_ptr t) = Some ko'; ctcb_relation ko ko'; cmap_relation (ctes_of a) (cslift b) cte_Ptr ccte_relation; cmap_relation (map_to_eps (ksPSpace a)) (cslift b) ep_Ptr (cendpoint_relation (cslift b)); cmap_relation (map_to_ntfns (ksPSpace a)) (cslift b) ntfn_Ptr (cnotification_relation (cslift b)); cmap_relation (map_to_pdes (ksPSpace a)) (cslift b) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace a)) (cslift b) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace a)) (cslift b) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace a) (underlying_memory (ksMachineState a))) (cslift b) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace a) (underlying_memory (ksMachineState a))) (cslift b) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace a)) (c_h_t_valid b) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace a)) (c_h_t_valid b) pt_Ptr; cready_queues_relation (cslift b) (ksReadyQueues_' (globals b)) (ksReadyQueues a); zero_ranges_are_zero (gsUntypedZeroRanges a) (t_hrs_' (globals b)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals b)) (ksReadyQueuesL1Bitmap a); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals b)) (ksReadyQueuesL2Bitmap a); ksCurThread_' (globals b) = tcb_ptr_to_ctcb_ptr (ksCurThread a); ksIdleThread_' (globals b) = tcb_ptr_to_ctcb_ptr (ksIdleThread a); cinterrupt_relation (ksInterruptState a) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals b)); cscheduler_action_relation (ksSchedulerAction a) (ksSchedulerAction_' (globals b)); armKSNextASID_' (globals b) = armKSNextASID (ksArchState a); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState a); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState a)) (armKSHWASIDTable_' (globals b)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState a)) (armKSASIDTable_' (globals b)); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState a)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift b \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState a); irq_masks (ksMachineState a) = irq_masks (phantom_machine_state_' (globals b)); irq_state (ksMachineState a) = irq_state (phantom_machine_state_' (globals b)); device_state (ksMachineState a) = device_state (phantom_machine_state_' (globals b)); exclusive_state (ksMachineState a) = exclusive_state (phantom_machine_state_' (globals b)); machine_state_rest (ksMachineState a) = machine_state_rest (phantom_machine_state_' (globals b)); cte_array_relation a (globals b); tcb_cte_array_relation a (globals b); apsnd fst (ghost'state_' (globals b)) = (gsUserPages a, gsCNodes a); ghost_size_rel (ghost'state_' (globals b)) (gsMaxObjectSize a); ksWorkUnitsCompleted_' (globals b) = ksWorkUnitsCompleted a; b \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; b \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals b))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule a) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals b) = word_of_nat (ksDomScheduleIdx a); ksCurDomain_' (globals b) = UCAST(8 \<rightarrow> 32) (ksCurDomain a); ksDomainTime_' (globals b) = ksDomainTime a; map_to_tcbs (ksPSpace a) t = Some ko\<rbrakk> \<Longrightarrow> inj tcb_ptr_to_ctcb_ptr proof (prove)
goal:
No subgoals!