theory TcbAcc_C

lemma getRegister_ccorres [corres]:
  "ccorres (=) ret__unsigned_long_' \<top>
             ({s. thread_' s = tcb_ptr_to_ctcb_ptr thread} \<inter> {s. reg_' s = register_from_H reg}) []
             (asUser thread (getRegister reg)) (Call getRegister_'proc)" apply (unfold asUser_def) apply (rule ccorres_guard_imp) apply (rule ccorres_symb_exec_l [where Q="\<lambda>u. obj_at' (\<lambda>t. (atcbContextGet o tcbArch) t = u) thread" and
      Q'="\<lambda>rv. {s. thread_' s = tcb_ptr_to_ctcb_ptr thread} \<inter> {s. reg_' s = register_from_H reg}"]) apply (rule ccorres_from_vcg) apply (rule allI, rule conseqPre) apply vcg apply clarsimp apply (drule (1) obj_at_cslift_tcb) apply (clarsimp simp: typ_heap_simps register_from_H_less) apply (clarsimp simp: getRegister_def typ_heap_simps) apply (rule_tac x = "((atcbContextGet o tcbArch) ko reg, \<sigma>)" in bexI [rotated]) apply (simp add: in_monad' asUser_def select_f_def split_def) apply (subst arg_cong2 [where f = "(\<in>)"]) defer apply (rule refl) apply (erule threadSet_eq) apply (clarsimp simp: ctcb_relation_def ccontext_relation_def carch_tcb_relation_def) apply (wp threadGet_obj_at2)+ apply simp apply simp apply (erule obj_atE') apply (clarsimp simp: projectKOs ) apply (subst fun_upd_idem) apply (case_tac ko) apply clarsimp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (=) ret__unsigned_long_' (\<lambda>_. True) (\<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H reg\<rbrace>) [] (asUser thread (getRegister reg)) (Call getRegister_'proc) proof (prove)
goal (1 subgoal):
 1. ccorres (=) ret__unsigned_long_' (\<lambda>_. True) (\<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H reg\<rbrace>) [] (do uc <- threadGet (atcbContextGet \<circ> tcbArch) thread;
(a, uc') <- select_f (getRegister reg uc);
threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet uc' (tcbArch tcb)) tcb) thread;
return a
od) (Call getRegister_'proc) proof (prove)
goal (3 subgoals):
 1. ccorres (=) ret__unsigned_long_' ?Q ?Q' [] (do uc <- threadGet (atcbContextGet \<circ> tcbArch) thread;
(a, uc') <- select_f (getRegister reg uc);
threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet uc' (tcbArch tcb)) tcb) thread;
return a
od) (Call getRegister_'proc)
 2. \<And>s. True \<Longrightarrow> ?Q s
 3. \<And>s. s \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H reg\<rbrace> \<Longrightarrow> s \<in> ?Q' proof (prove)
goal (6 subgoals):
 1. \<And>uc. ccorres (=) ret__unsigned_long_' (obj_at' (\<lambda>t. (atcbContextGet \<circ> tcbArch) t = uc) thread) (\<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H reg\<rbrace>) [] (do (a, uc') <- select_f (getRegister reg uc);
threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet uc' (tcbArch tcb)) tcb) thread;
return a
od) (Call getRegister_'proc)
 2. \<And>s. \<lbrace>(=) s\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<lbrace>?Q\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) thread \<lbrace>\<lambda>u. obj_at' (\<lambda>t. (atcbContextGet \<circ> tcbArch) t = u) thread\<rbrace>
 4. empty_fail (threadGet (atcbContextGet \<circ> tcbArch) thread)
 5. \<And>s. True \<Longrightarrow> ?Q s
 6. \<And>s. s \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H reg\<rbrace> \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> obj_at' (\<lambda>t. (atcbContextGet \<circ> tcbArch) t = rv) thread s \<longrightarrow> s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H reg\<rbrace>} proof (prove)
goal (6 subgoals):
 1. \<And>uc. \<forall>\<sigma>. \<Gamma>\<turnstile> {s. obj_at' (\<lambda>t. (atcbContextGet \<circ> tcbArch) t = uc) thread \<sigma> \<and> s \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H reg\<rbrace> \<and> (\<sigma>, s) \<in> rf_sr} Call getRegister_'proc {s. \<exists>(rv, \<sigma>')\<in>fst ((do (a, uc') <- select_f (getRegister reg uc);
threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet uc' (tcbArch tcb)) tcb) thread;
return a
od) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> rv = ret__unsigned_long_' s}
 2. \<And>s. \<lbrace>(=) s\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<lbrace>?Q\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) thread \<lbrace>\<lambda>u. obj_at' (\<lambda>t. (atcbContextGet \<circ> tcbArch) t = u) thread\<rbrace>
 4. empty_fail (threadGet (atcbContextGet \<circ> tcbArch) thread)
 5. \<And>s. True \<Longrightarrow> ?Q s
 6. \<And>s. s \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H reg\<rbrace> \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> obj_at' (\<lambda>t. (atcbContextGet \<circ> tcbArch) t = rv) thread s \<longrightarrow> s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H reg\<rbrace>} proof (prove)
goal (7 subgoals):
 1. \<And>uc \<sigma>. \<Gamma>\<turnstile> (?P'14 uc \<sigma>) Call getRegister_'proc {s. \<exists>(rv, \<sigma>')\<in>fst ((do (a, uc') <- select_f (getRegister reg uc);
threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet uc' (tcbArch tcb)) tcb) thread;
return a
od) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> rv = ret__unsigned_long_' s}
 2. \<And>uc \<sigma>. {s. obj_at' (\<lambda>t. (atcbContextGet \<circ> tcbArch) t = uc) thread \<sigma> \<and> s \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H reg\<rbrace> \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> ?P'14 uc \<sigma>
 3. \<And>s. \<lbrace>(=) s\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<lbrace>?Q\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) thread \<lbrace>\<lambda>u. obj_at' (\<lambda>t. (atcbContextGet \<circ> tcbArch) t = u) thread\<rbrace>
 5. empty_fail (threadGet (atcbContextGet \<circ> tcbArch) thread)
 6. \<And>s. True \<Longrightarrow> ?Q s
 7. \<And>s. s \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H reg\<rbrace> \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> obj_at' (\<lambda>t. (atcbContextGet \<circ> tcbArch) t = rv) thread s \<longrightarrow> s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H reg\<rbrace>} proof (prove)
goal (6 subgoals):
 1. \<And>uc \<sigma>. {s. obj_at' (\<lambda>t. (atcbContextGet \<circ> tcbArch) t = uc) thread \<sigma> \<and> s \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H reg\<rbrace> \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. reg_' s < SCAST(32 signed \<rightarrow> 32) 0x14 \<and> s \<Turnstile>\<^sub>c thread_' s \<and> (\<exists>(rv, \<sigma>')\<in>fst ((do (a, uc') <- select_f (getRegister reg uc);
threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet uc' (tcbArch tcb)) tcb) thread;
return a
od) \<sigma>). (\<sigma>', s\<lparr>ret__unsigned_long_' := h_val (hrs_mem (t_hrs_' (globals s))) (PTR(32 word[20]) &(PTR(user_context_C) &(PTR(arch_tcb_C) &(thread_' s\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])\<rightarrow>[''registers_C''])).[unat (reg_' s)], global_exn_var_' := Return\<rparr>) \<in> rf_sr \<and> rv = h_val (hrs_mem (t_hrs_' (globals s))) (PTR(32 word[20]) &(PTR(user_context_C) &(PTR(arch_tcb_C) &(thread_' s\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])\<rightarrow>[''registers_C''])).[unat (reg_' s)])}
 2. \<And>s. \<lbrace>(=) s\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<lbrace>?Q\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) thread \<lbrace>\<lambda>u. obj_at' (\<lambda>t. (atcbContextGet \<circ> tcbArch) t = u) thread\<rbrace>
 4. empty_fail (threadGet (atcbContextGet \<circ> tcbArch) thread)
 5. \<And>s. True \<Longrightarrow> ?Q s
 6. \<And>s. s \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H reg\<rbrace> \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> obj_at' (\<lambda>t. (atcbContextGet \<circ> tcbArch) t = rv) thread s \<longrightarrow> s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H reg\<rbrace>} proof (prove)
goal (6 subgoals):
 1. \<And>uc \<sigma> x. \<lbrakk>obj_at' (\<lambda>t. atcbContextGet (tcbArch t) = uc) thread \<sigma>; thread_' x = tcb_ptr_to_ctcb_ptr thread; reg_' x = register_from_H reg; (\<sigma>, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> register_from_H reg < 0x14 \<and> x \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<and> (\<exists>xa\<in>fst ((do (a, uc') <- select_f (getRegister reg uc);
y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet uc' (tcbArch tcb)) tcb) thread;
return a
od) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x) \<in> rf_sr \<and> rv = h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[20]) &(PTR(user_context_C) &(PTR(arch_tcb_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])\<rightarrow>[''registers_C''])).[unat (register_from_H reg)])
 2. \<And>s. \<lbrace>(=) s\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<lbrace>?Q\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) thread \<lbrace>\<lambda>u. obj_at' (\<lambda>t. (atcbContextGet \<circ> tcbArch) t = u) thread\<rbrace>
 4. empty_fail (threadGet (atcbContextGet \<circ> tcbArch) thread)
 5. \<And>s. True \<Longrightarrow> ?Q s
 6. \<And>s. s \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H reg\<rbrace> \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> obj_at' (\<lambda>t. (atcbContextGet \<circ> tcbArch) t = rv) thread s \<longrightarrow> s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H reg\<rbrace>} proof (prove)
goal (6 subgoals):
 1. \<And>uc \<sigma> x. \<lbrakk>thread_' x = tcb_ptr_to_ctcb_ptr thread; reg_' x = register_from_H reg; (\<sigma>, x) \<in> rf_sr; \<exists>ko ko'. ko_at' ko thread \<sigma> \<and> atcbContextGet (tcbArch ko) = uc \<and> cslift x (tcb_ptr_to_ctcb_ptr thread) = Some ko' \<and> ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> register_from_H reg < 0x14 \<and> x \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<and> (\<exists>xa\<in>fst ((do (a, uc') <- select_f (getRegister reg uc);
y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet uc' (tcbArch tcb)) tcb) thread;
return a
od) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x) \<in> rf_sr \<and> rv = h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[20]) &(PTR(user_context_C) &(PTR(arch_tcb_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])\<rightarrow>[''registers_C''])).[unat (register_from_H reg)])
 2. \<And>s. \<lbrace>(=) s\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<lbrace>?Q\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) thread \<lbrace>\<lambda>u. obj_at' (\<lambda>t. (atcbContextGet \<circ> tcbArch) t = u) thread\<rbrace>
 4. empty_fail (threadGet (atcbContextGet \<circ> tcbArch) thread)
 5. \<And>s. True \<Longrightarrow> ?Q s
 6. \<And>s. s \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H reg\<rbrace> \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> obj_at' (\<lambda>t. (atcbContextGet \<circ> tcbArch) t = rv) thread s \<longrightarrow> s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H reg\<rbrace>} proof (prove)
goal (6 subgoals):
 1. \<And>\<sigma> x ko ko'. \<lbrakk>thread_' x = tcb_ptr_to_ctcb_ptr thread; reg_' x = register_from_H reg; (\<sigma>, x) \<in> rf_sr; ko_at' ko thread \<sigma>; cslift x (tcb_ptr_to_ctcb_ptr thread) = Some ko'; ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst ((do (a, uc') <- select_f (getRegister reg (atcbContextGet (tcbArch ko)));
y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet uc' (tcbArch tcb)) tcb) thread;
return a
od) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x) \<in> rf_sr \<and> rv = registers_C (tcbContext_C (tcbArch_C ko')).[unat (register_from_H reg)]
 2. \<And>s. \<lbrace>(=) s\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<lbrace>?Q\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) thread \<lbrace>\<lambda>u. obj_at' (\<lambda>t. (atcbContextGet \<circ> tcbArch) t = u) thread\<rbrace>
 4. empty_fail (threadGet (atcbContextGet \<circ> tcbArch) thread)
 5. \<And>s. True \<Longrightarrow> ?Q s
 6. \<And>s. s \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H reg\<rbrace> \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> obj_at' (\<lambda>t. (atcbContextGet \<circ> tcbArch) t = rv) thread s \<longrightarrow> s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H reg\<rbrace>} proof (prove)
goal (6 subgoals):
 1. \<And>\<sigma> x ko ko'. \<lbrakk>thread_' x = tcb_ptr_to_ctcb_ptr thread; reg_' x = register_from_H reg; (\<sigma>, x) \<in> rf_sr; ko_at' ko thread \<sigma>; cslift x (tcb_ptr_to_ctcb_ptr thread) = Some ko'; ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst ((do (a, uc') <- select_f (gets (\<lambda>uc. uc reg) (atcbContextGet (tcbArch ko)));
y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet uc' (tcbArch tcb)) tcb) thread;
return a
od) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x) \<in> rf_sr \<and> rv = registers_C (tcbContext_C (tcbArch_C ko')).[unat (register_from_H reg)]
 2. \<And>s. \<lbrace>(=) s\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<lbrace>?Q\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) thread \<lbrace>\<lambda>u. obj_at' (\<lambda>t. (atcbContextGet \<circ> tcbArch) t = u) thread\<rbrace>
 4. empty_fail (threadGet (atcbContextGet \<circ> tcbArch) thread)
 5. \<And>s. True \<Longrightarrow> ?Q s
 6. \<And>s. s \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H reg\<rbrace> \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> obj_at' (\<lambda>t. (atcbContextGet \<circ> tcbArch) t = rv) thread s \<longrightarrow> s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H reg\<rbrace>} proof (prove)
goal (7 subgoals):
 1. \<And>\<sigma> x ko ko'. \<lbrakk>thread_' x = tcb_ptr_to_ctcb_ptr thread; reg_' x = register_from_H reg; (\<sigma>, x) \<in> rf_sr; ko_at' ko thread \<sigma>; cslift x (tcb_ptr_to_ctcb_ptr thread) = Some ko'; ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> ((atcbContextGet \<circ> tcbArch) ko reg, \<sigma>) \<in> fst ((do (a, uc') <- select_f (gets (\<lambda>uc. uc reg) (atcbContextGet (tcbArch ko)));
y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet uc' (tcbArch tcb)) tcb) thread;
return a
od) \<sigma>)
 2. \<And>\<sigma> x ko ko'. \<lbrakk>thread_' x = tcb_ptr_to_ctcb_ptr thread; reg_' x = register_from_H reg; (\<sigma>, x) \<in> rf_sr; ko_at' ko thread \<sigma>; cslift x (tcb_ptr_to_ctcb_ptr thread) = Some ko'; ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> case ((atcbContextGet \<circ> tcbArch) ko reg, \<sigma>) of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x) \<in> rf_sr \<and> rv = registers_C (tcbContext_C (tcbArch_C ko')).[unat (register_from_H reg)]
 3. \<And>s. \<lbrace>(=) s\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<lbrace>?Q\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) thread \<lbrace>\<lambda>u. obj_at' (\<lambda>t. (atcbContextGet \<circ> tcbArch) t = u) thread\<rbrace>
 5. empty_fail (threadGet (atcbContextGet \<circ> tcbArch) thread)
 6. \<And>s. True \<Longrightarrow> ?Q s
 7. \<And>s. s \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H reg\<rbrace> \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> obj_at' (\<lambda>t. (atcbContextGet \<circ> tcbArch) t = rv) thread s \<longrightarrow> s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H reg\<rbrace>} proof (prove)
goal (7 subgoals):
 1. \<And>\<sigma> x ko ko'. \<lbrakk>thread_' x = tcb_ptr_to_ctcb_ptr thread; reg_' x = register_from_H reg; (\<sigma>, x) \<in> rf_sr; ko_at' ko thread \<sigma>; cslift x (tcb_ptr_to_ctcb_ptr thread) = Some ko'; ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> ((), \<sigma>) \<in> fst (threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet (atcbContextGet (tcbArch ko)) (tcbArch tcb)) tcb) thread \<sigma>)
 2. \<And>\<sigma> x ko ko'. \<lbrakk>thread_' x = tcb_ptr_to_ctcb_ptr thread; reg_' x = register_from_H reg; (\<sigma>, x) \<in> rf_sr; ko_at' ko thread \<sigma>; cslift x (tcb_ptr_to_ctcb_ptr thread) = Some ko'; ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> case ((atcbContextGet \<circ> tcbArch) ko reg, \<sigma>) of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x) \<in> rf_sr \<and> rv = registers_C (tcbContext_C (tcbArch_C ko')).[unat (register_from_H reg)]
 3. \<And>s. \<lbrace>(=) s\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<lbrace>?Q\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) thread \<lbrace>\<lambda>u. obj_at' (\<lambda>t. (atcbContextGet \<circ> tcbArch) t = u) thread\<rbrace>
 5. empty_fail (threadGet (atcbContextGet \<circ> tcbArch) thread)
 6. \<And>s. True \<Longrightarrow> ?Q s
 7. \<And>s. s \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H reg\<rbrace> \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> obj_at' (\<lambda>t. (atcbContextGet \<circ> tcbArch) t = rv) thread s \<longrightarrow> s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H reg\<rbrace>} proof (prove)
goal (9 subgoals):
 1. \<And>\<sigma> x ko ko'. \<lbrakk>thread_' x = tcb_ptr_to_ctcb_ptr thread; reg_' x = register_from_H reg; (\<sigma>, x) \<in> rf_sr; ko_at' ko thread \<sigma>; cslift x (tcb_ptr_to_ctcb_ptr thread) = Some ko'; ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> ((), \<sigma>) = ?b58 \<sigma> x ko ko'
 2. \<And>\<sigma> x ko ko'. \<lbrakk>thread_' x = tcb_ptr_to_ctcb_ptr thread; reg_' x = register_from_H reg; (\<sigma>, x) \<in> rf_sr; ko_at' ko thread \<sigma>; cslift x (tcb_ptr_to_ctcb_ptr thread) = Some ko'; ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> fst (threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet (atcbContextGet (tcbArch ko)) (tcbArch tcb)) tcb) thread \<sigma>) = ?d58 \<sigma> x ko ko'
 3. \<And>\<sigma> x ko ko'. \<lbrakk>thread_' x = tcb_ptr_to_ctcb_ptr thread; reg_' x = register_from_H reg; (\<sigma>, x) \<in> rf_sr; ko_at' ko thread \<sigma>; cslift x (tcb_ptr_to_ctcb_ptr thread) = Some ko'; ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> ?b58 \<sigma> x ko ko' \<in> ?d58 \<sigma> x ko ko'
 4. \<And>\<sigma> x ko ko'. \<lbrakk>thread_' x = tcb_ptr_to_ctcb_ptr thread; reg_' x = register_from_H reg; (\<sigma>, x) \<in> rf_sr; ko_at' ko thread \<sigma>; cslift x (tcb_ptr_to_ctcb_ptr thread) = Some ko'; ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> case ((atcbContextGet \<circ> tcbArch) ko reg, \<sigma>) of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x) \<in> rf_sr \<and> rv = registers_C (tcbContext_C (tcbArch_C ko')).[unat (register_from_H reg)]
 5. \<And>s. \<lbrace>(=) s\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<lbrace>?Q\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) thread \<lbrace>\<lambda>u. obj_at' (\<lambda>t. (atcbContextGet \<circ> tcbArch) t = u) thread\<rbrace>
 7. empty_fail (threadGet (atcbContextGet \<circ> tcbArch) thread)
 8. \<And>s. True \<Longrightarrow> ?Q s
 9. \<And>s. s \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H reg\<rbrace> \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> obj_at' (\<lambda>t. (atcbContextGet \<circ> tcbArch) t = rv) thread s \<longrightarrow> s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H reg\<rbrace>} proof (prove)
goal (9 subgoals):
 1. \<And>\<sigma> x ko ko'. \<lbrakk>thread_' x = tcb_ptr_to_ctcb_ptr thread; reg_' x = register_from_H reg; (\<sigma>, x) \<in> rf_sr; ko_at' ko thread \<sigma>; cslift x (tcb_ptr_to_ctcb_ptr thread) = Some ko'; ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> fst (threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet (atcbContextGet (tcbArch ko)) (tcbArch tcb)) tcb) thread \<sigma>) = ?d58 \<sigma> x ko ko'
 2. \<And>\<sigma> x ko ko'. \<lbrakk>thread_' x = tcb_ptr_to_ctcb_ptr thread; reg_' x = register_from_H reg; (\<sigma>, x) \<in> rf_sr; ko_at' ko thread \<sigma>; cslift x (tcb_ptr_to_ctcb_ptr thread) = Some ko'; ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> ?b58 \<sigma> x ko ko' \<in> ?d58 \<sigma> x ko ko'
 3. \<And>\<sigma> x ko ko'. \<lbrakk>thread_' x = tcb_ptr_to_ctcb_ptr thread; reg_' x = register_from_H reg; (\<sigma>, x) \<in> rf_sr; ko_at' ko thread \<sigma>; cslift x (tcb_ptr_to_ctcb_ptr thread) = Some ko'; ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> case ((atcbContextGet \<circ> tcbArch) ko reg, \<sigma>) of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x) \<in> rf_sr \<and> rv = registers_C (tcbContext_C (tcbArch_C ko')).[unat (register_from_H reg)]
 4. \<And>s. \<lbrace>(=) s\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<lbrace>?Q\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) thread \<lbrace>\<lambda>u. obj_at' (\<lambda>t. (atcbContextGet \<circ> tcbArch) t = u) thread\<rbrace>
 6. empty_fail (threadGet (atcbContextGet \<circ> tcbArch) thread)
 7. \<And>s. True \<Longrightarrow> ?Q s
 8. \<And>s. s \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H reg\<rbrace> \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> obj_at' (\<lambda>t. (atcbContextGet \<circ> tcbArch) t = rv) thread s \<longrightarrow> s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H reg\<rbrace>}
 9. \<And>\<sigma> x ko ko'. \<lbrakk>thread_' x = tcb_ptr_to_ctcb_ptr thread; reg_' x = register_from_H reg; (\<sigma>, x) \<in> rf_sr; ko_at' ko thread \<sigma>; cslift x (tcb_ptr_to_ctcb_ptr thread) = Some ko'; ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> ((), \<sigma>) = ?b58 \<sigma> x ko ko' proof (prove)
goal (8 subgoals):
 1. \<And>\<sigma> x ko ko'. \<lbrakk>thread_' x = tcb_ptr_to_ctcb_ptr thread; reg_' x = register_from_H reg; (\<sigma>, x) \<in> rf_sr; ko_at' ko thread \<sigma>; cslift x (tcb_ptr_to_ctcb_ptr thread) = Some ko'; ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> ?b58 \<sigma> x ko ko' \<in> fst (threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet (atcbContextGet (tcbArch ko)) (tcbArch tcb)) tcb) thread \<sigma>)
 2. \<And>\<sigma> x ko ko'. \<lbrakk>thread_' x = tcb_ptr_to_ctcb_ptr thread; reg_' x = register_from_H reg; (\<sigma>, x) \<in> rf_sr; ko_at' ko thread \<sigma>; cslift x (tcb_ptr_to_ctcb_ptr thread) = Some ko'; ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> case ((atcbContextGet \<circ> tcbArch) ko reg, \<sigma>) of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x) \<in> rf_sr \<and> rv = registers_C (tcbContext_C (tcbArch_C ko')).[unat (register_from_H reg)]
 3. \<And>s. \<lbrace>(=) s\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<lbrace>?Q\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) thread \<lbrace>\<lambda>u. obj_at' (\<lambda>t. (atcbContextGet \<circ> tcbArch) t = u) thread\<rbrace>
 5. empty_fail (threadGet (atcbContextGet \<circ> tcbArch) thread)
 6. \<And>s. True \<Longrightarrow> ?Q s
 7. \<And>s. s \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H reg\<rbrace> \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> obj_at' (\<lambda>t. (atcbContextGet \<circ> tcbArch) t = rv) thread s \<longrightarrow> s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H reg\<rbrace>}
 8. \<And>\<sigma> x ko ko'. \<lbrakk>thread_' x = tcb_ptr_to_ctcb_ptr thread; reg_' x = register_from_H reg; (\<sigma>, x) \<in> rf_sr; ko_at' ko thread \<sigma>; cslift x (tcb_ptr_to_ctcb_ptr thread) = Some ko'; ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> ((), \<sigma>) = ?b58 \<sigma> x ko ko' proof (prove)
goal (7 subgoals):
 1. \<And>\<sigma> x ko ko'. \<lbrakk>thread_' x = tcb_ptr_to_ctcb_ptr thread; reg_' x = register_from_H reg; (\<sigma>, x) \<in> rf_sr; ko_at' ko thread \<sigma>; cslift x (tcb_ptr_to_ctcb_ptr thread) = Some ko'; ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> case ((atcbContextGet \<circ> tcbArch) ko reg, \<sigma>) of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x) \<in> rf_sr \<and> rv = registers_C (tcbContext_C (tcbArch_C ko')).[unat (register_from_H reg)]
 2. \<And>s. \<lbrace>(=) s\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<lbrace>?Q\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) thread \<lbrace>\<lambda>u. obj_at' (\<lambda>t. (atcbContextGet \<circ> tcbArch) t = u) thread\<rbrace>
 4. empty_fail (threadGet (atcbContextGet \<circ> tcbArch) thread)
 5. \<And>s. True \<Longrightarrow> ?Q s
 6. \<And>s. s \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H reg\<rbrace> \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> obj_at' (\<lambda>t. (atcbContextGet \<circ> tcbArch) t = rv) thread s \<longrightarrow> s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H reg\<rbrace>}
 7. \<And>\<sigma> x ko ko'. \<lbrakk>thread_' x = tcb_ptr_to_ctcb_ptr thread; reg_' x = register_from_H reg; (\<sigma>, x) \<in> rf_sr; ko_at' ko thread \<sigma>; cslift x (tcb_ptr_to_ctcb_ptr thread) = Some ko'; ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> ((), \<sigma>) = ((), \<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(thread \<mapsto> injectKOS (tcbArch_update (\<lambda>_. atcbContextSet (atcbContextGet (tcbArch ko)) (tcbArch ko)) ko))\<rparr>) proof (prove)
goal (6 subgoals):
 1. \<And>s. \<lbrace>(=) s\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<lbrace>?Q\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) thread \<lbrace>\<lambda>u. obj_at' (\<lambda>t. (atcbContextGet \<circ> tcbArch) t = u) thread\<rbrace>
 3. empty_fail (threadGet (atcbContextGet \<circ> tcbArch) thread)
 4. \<And>s. True \<Longrightarrow> ?Q s
 5. \<And>s. s \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H reg\<rbrace> \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> obj_at' (\<lambda>t. (atcbContextGet \<circ> tcbArch) t = rv) thread s \<longrightarrow> s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H reg\<rbrace>}
 6. \<And>\<sigma> x ko ko'. \<lbrakk>thread_' x = tcb_ptr_to_ctcb_ptr thread; reg_' x = register_from_H reg; (\<sigma>, x) \<in> rf_sr; ko_at' ko thread \<sigma>; cslift x (tcb_ptr_to_ctcb_ptr thread) = Some ko'; ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> ((), \<sigma>) = ((), \<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(thread \<mapsto> injectKOS (tcbArch_update (\<lambda>_. atcbContextSet (atcbContextGet (tcbArch ko)) (tcbArch ko)) ko))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s. s \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H reg\<rbrace> \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> obj_at' (\<lambda>t. (atcbContextGet \<circ> tcbArch) t = rv) thread s \<longrightarrow> s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H reg\<rbrace>}
 2. \<And>\<sigma> x ko ko'. \<lbrakk>thread_' x = tcb_ptr_to_ctcb_ptr thread; reg_' x = register_from_H reg; (\<sigma>, x) \<in> rf_sr; ko_at' ko thread \<sigma>; cslift x (tcb_ptr_to_ctcb_ptr thread) = Some ko'; ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> ((), \<sigma>) = ((), \<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(thread \<mapsto> injectKOS (tcbArch_update (\<lambda>_. atcbContextSet (atcbContextGet (tcbArch ko)) (tcbArch ko)) ko))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x ko ko'. \<lbrakk>thread_' x = tcb_ptr_to_ctcb_ptr thread; reg_' x = register_from_H reg; (\<sigma>, x) \<in> rf_sr; ko_at' ko thread \<sigma>; cslift x (tcb_ptr_to_ctcb_ptr thread) = Some ko'; ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> ((), \<sigma>) = ((), \<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(thread \<mapsto> injectKOS (tcbArch_update (\<lambda>_. atcbContextSet (atcbContextGet (tcbArch ko)) (tcbArch ko)) ko))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x ko ko'. \<lbrakk>thread_' x = tcb_ptr_to_ctcb_ptr thread; reg_' x = register_from_H reg; (\<sigma>, x) \<in> rf_sr; ko_at' ko thread \<sigma>; cslift x (tcb_ptr_to_ctcb_ptr thread) = Some ko'; ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> \<sigma> = \<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(thread \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) ko))\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x ko ko' koa obj. \<lbrakk>thread_' x = tcb_ptr_to_ctcb_ptr thread; reg_' x = register_from_H reg; (\<sigma>, x) \<in> rf_sr; cslift x (tcb_ptr_to_ctcb_ptr thread) = Some ko'; ctcb_relation ko ko'; ksPSpace \<sigma> thread = Some koa; is_aligned thread (objBitsKO koa); fst (projectKO koa \<sigma>) = {(obj, \<sigma>)}; obj = ko; ps_clear thread (objBitsKO koa) \<sigma>\<rbrakk> \<Longrightarrow> \<sigma> = \<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(thread \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) ko))\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x ko ko'. \<lbrakk>thread_' x = tcb_ptr_to_ctcb_ptr thread; reg_' x = register_from_H reg; (\<sigma>, x) \<in> rf_sr; cslift x (tcb_ptr_to_ctcb_ptr thread) = Some ko'; ctcb_relation ko ko'; ksPSpace \<sigma> thread = Some (KOTCB ko); is_aligned thread (objBitsKO (KOTCB ko)); ps_clear thread (objBitsKO (KOTCB ko)) \<sigma>\<rbrakk> \<Longrightarrow> \<sigma> = \<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(thread \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) ko))\<rparr> proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x ko ko' _. \<lbrakk>thread_' x = tcb_ptr_to_ctcb_ptr thread; reg_' x = register_from_H reg; (\<sigma>, x) \<in> rf_sr; cslift x (tcb_ptr_to_ctcb_ptr thread) = Some ko'; ctcb_relation ko ko'; ksPSpace \<sigma> thread = Some (KOTCB ko); is_aligned thread (objBitsKO (KOTCB ko)); ps_clear thread (objBitsKO (KOTCB ko)) \<sigma>\<rbrakk> \<Longrightarrow> ksPSpace \<sigma> thread = Some (KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) ko))
 2. \<And>\<sigma> x ko ko'. \<lbrakk>thread_' x = tcb_ptr_to_ctcb_ptr thread; reg_' x = register_from_H reg; (\<sigma>, x) \<in> rf_sr; cslift x (tcb_ptr_to_ctcb_ptr thread) = Some ko'; ctcb_relation ko ko'; ksPSpace \<sigma> thread = Some (KOTCB ko); is_aligned thread (objBitsKO (KOTCB ko)); ps_clear thread (objBitsKO (KOTCB ko)) \<sigma>\<rbrakk> \<Longrightarrow> \<sigma> = \<sigma>\<lparr>ksPSpace := ksPSpace \<sigma>\<rparr> proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x ko ko' _ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16. \<lbrakk>thread_' x = tcb_ptr_to_ctcb_ptr thread; reg_' x = register_from_H reg; (\<sigma>, x) \<in> rf_sr; cslift x (tcb_ptr_to_ctcb_ptr thread) = Some ko'; ctcb_relation ko ko'; ksPSpace \<sigma> thread = Some (KOTCB ko); is_aligned thread (objBitsKO (KOTCB ko)); ps_clear thread (objBitsKO (KOTCB ko)) \<sigma>; ko = Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16\<rbrakk> \<Longrightarrow> ksPSpace \<sigma> thread = Some (KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) ko))
 2. \<And>\<sigma> x ko ko'. \<lbrakk>thread_' x = tcb_ptr_to_ctcb_ptr thread; reg_' x = register_from_H reg; (\<sigma>, x) \<in> rf_sr; cslift x (tcb_ptr_to_ctcb_ptr thread) = Some ko'; ctcb_relation ko ko'; ksPSpace \<sigma> thread = Some (KOTCB ko); is_aligned thread (objBitsKO (KOTCB ko)); ps_clear thread (objBitsKO (KOTCB ko)) \<sigma>\<rbrakk> \<Longrightarrow> \<sigma> = \<sigma>\<lparr>ksPSpace := ksPSpace \<sigma>\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x ko ko'. \<lbrakk>thread_' x = tcb_ptr_to_ctcb_ptr thread; reg_' x = register_from_H reg; (\<sigma>, x) \<in> rf_sr; cslift x (tcb_ptr_to_ctcb_ptr thread) = Some ko'; ctcb_relation ko ko'; ksPSpace \<sigma> thread = Some (KOTCB ko); is_aligned thread (objBitsKO (KOTCB ko)); ps_clear thread (objBitsKO (KOTCB ko)) \<sigma>\<rbrakk> \<Longrightarrow> \<sigma> = \<sigma>\<lparr>ksPSpace := ksPSpace \<sigma>\<rparr> proof (prove)
goal:
No subgoals!