theory VSpace_C

lemma setRegister_ccorres:
  "ccorres dc xfdc \<top>
       (UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H reg\<rbrace>
             \<inter> {s. w_' s = val}) []
       (asUser thread (setRegister reg val))
       (Call setRegister_'proc)" apply (cinit' lift: thread_' reg_' w_') apply (simp add: asUser_def split_def) apply (rule ccorres_pre_threadGet) apply (rule ccorres_Guard) apply (simp add: setRegister_def simpler_modify_def exec_select_f_singleton) apply (rule_tac P="\<lambda>tcb. (atcbContextGet o tcbArch) tcb = uc"
                in threadSet_ccorres_lemma2) apply vcg apply (clarsimp simp: setRegister_def HaskellLib_H.runState_def
                         simpler_modify_def typ_heap_simps) apply (subst StateSpace.state.fold_congs[OF refl refl]) apply (rule globals.fold_congs[OF refl refl]) apply (rule heap_update_field_hrs, simp) apply (fastforce intro: typ_heap_simps) apply simp apply (erule(1) rf_sr_tcb_update_no_queue2,
               (simp add: typ_heap_simps')+) apply (rule ball_tcb_cte_casesI, simp+) apply (clarsimp simp: ctcb_relation_def ccontext_relation_def
                         atcbContextSet_def atcbContextGet_def
                         carch_tcb_relation_def
                  split: if_split) apply (clarsimp simp: Collect_const_mem
                        register_from_H_less) apply (auto intro: typ_heap_simps elim: obj_at'_weakenE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (\<lambda>_. True) (UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H reg\<rbrace> \<inter> \<lbrace>\<acute>w = val\<rbrace>) [] (asUser thread (setRegister reg val)) (Call setRegister_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>w rega threada. \<lbrakk>w = val; rega = register_from_H reg; threada = tcb_ptr_to_ctcb_ptr thread\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q91 w rega threada) (?Q'91 w rega threada) [SKIP] (asUser thread (setRegister reg val)) (Guard ArrayBounds \<lbrace>rega < 0x14\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c threada} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word[20]) &(PTR(user_context_C) &(PTR(arch_tcb_C) &(threada\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])\<rightarrow>[''registers_C''])) (Arrays.update (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[20]) &(PTR(user_context_C) &(PTR(arch_tcb_C) &(threada\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])\<rightarrow>[''registers_C'']))) (unat rega) w))))))
 2. \<And>w rega threada s s'. \<lbrakk>w = val; rega = register_from_H reg; threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q91 w rega threada s \<and> s' \<in> ?Q'91 w rega threada proof (prove)
goal (2 subgoals):
 1. \<And>w rega threada. \<lbrakk>w = val; rega = register_from_H reg; threada = tcb_ptr_to_ctcb_ptr thread\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q91 val (register_from_H reg) (tcb_ptr_to_ctcb_ptr thread)) (?Q'91 val (register_from_H reg) (tcb_ptr_to_ctcb_ptr thread)) [SKIP] (do uc <- threadGet (atcbContextGet \<circ> tcbArch) thread;
p <- select_f (setRegister reg val uc);
threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet (snd p) (tcbArch tcb)) tcb) thread
od) (Guard ArrayBounds (if register_from_H reg < 0x14 then UNIV else {}) (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (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''])) (Arrays.update (h_val (hrs_mem \<acute>t_hrs) (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)) val))))))
 2. \<And>w rega threada s s'. \<lbrakk>w = val; rega = register_from_H reg; threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q91 w rega threada s \<and> s' \<in> ?Q'91 w rega threada proof (prove)
goal (2 subgoals):
 1. \<And>w rega threada uc. \<lbrakk>w = val; rega = register_from_H reg; threada = tcb_ptr_to_ctcb_ptr thread\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?P104 uc) (?P'103 uc) [SKIP] (do p <- select_f (setRegister reg val uc);
threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet (snd p) (tcbArch tcb)) tcb) thread
od) (Guard ArrayBounds (if register_from_H reg < 0x14 then UNIV else {}) (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (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''])) (Arrays.update (h_val (hrs_mem \<acute>t_hrs) (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)) val))))))
 2. \<And>w rega threada s s'. \<lbrakk>w = val; rega = register_from_H reg; threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb thread s \<longrightarrow> ?P101 w rega threada s tcb) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' threada = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> ?P'102 w rega threada tcb}
flex-flex pairs:
\<lambda>s tcb. ?P104 ((atcbContextGet \<circ> tcbArch) tcb) s \<equiv>\<^sup>? ?P101 val (register_from_H reg) (tcb_ptr_to_ctcb_ptr thread)
\<lambda>tcb. ?P'103 ((atcbContextGet \<circ> tcbArch) tcb) \<equiv>\<^sup>? ?P'102 val (register_from_H reg) (tcb_ptr_to_ctcb_ptr thread) proof (prove)
goal (2 subgoals):
 1. \<And>w rega threada uc. \<lbrakk>w = val; rega = register_from_H reg; threada = tcb_ptr_to_ctcb_ptr thread\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?P104 uc) (?C'110 uc) [SKIP] (do p <- select_f (setRegister reg val uc);
threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet (snd p) (tcbArch tcb)) tcb) thread
od) (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (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''])) (Arrays.update (h_val (hrs_mem \<acute>t_hrs) (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)) val)))))
 2. \<And>w rega threada s s'. \<lbrakk>w = val; rega = register_from_H reg; threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb thread s \<longrightarrow> ?P101 w rega threada s tcb) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' threada = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> ?C'108 w rega threada tcb \<inter> (if rega < 0x14 then UNIV else {})}
flex-flex pairs:
\<lambda>tcb. ?C'110 ((atcbContextGet \<circ> tcbArch) tcb) \<equiv>\<^sup>? ?C'108 val (register_from_H reg) (tcb_ptr_to_ctcb_ptr thread)
\<lambda>s tcb. ?P104 ((atcbContextGet \<circ> tcbArch) tcb) s \<equiv>\<^sup>? ?P101 val (register_from_H reg) (tcb_ptr_to_ctcb_ptr thread) proof (prove)
goal (2 subgoals):
 1. \<And>w rega threada uc. \<lbrakk>w = val; rega = register_from_H reg; threada = tcb_ptr_to_ctcb_ptr thread\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?P104 uc) (?C'110 uc) [SKIP] (threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet (uc(reg := val)) (tcbArch tcb)) tcb) thread) (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (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''])) (Arrays.update (h_val (hrs_mem \<acute>t_hrs) (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)) val)))))
 2. \<And>w rega threada s s'. \<lbrakk>w = val; rega = register_from_H reg; threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb thread s \<longrightarrow> ?P101 w rega threada s tcb) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' threada = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> ?C'108 w rega threada tcb \<inter> (if rega < 0x14 then UNIV else {})}
flex-flex pairs:
\<lambda>tcb. ?C'110 ((atcbContextGet \<circ> tcbArch) tcb) \<equiv>\<^sup>? ?C'108 val (register_from_H reg) (tcb_ptr_to_ctcb_ptr thread)
\<lambda>s tcb. ?P104 ((atcbContextGet \<circ> tcbArch) tcb) s \<equiv>\<^sup>? ?P101 val (register_from_H reg) (tcb_ptr_to_ctcb_ptr thread) proof (prove)
goal (3 subgoals):
 1. \<And>w rega threada uc s tcb. \<lbrakk>w = val; rega = register_from_H reg; threada = tcb_ptr_to_ctcb_ptr thread\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q117 w rega threada uc s tcb) Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (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''])) (Arrays.update (h_val (hrs_mem \<acute>t_hrs) (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)) val)))) {s'. (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> injectKOS (tcbArch_update (\<lambda>_. atcbContextSet (uc(reg := val)) (tcbArch tcb)) tcb))\<rparr>, s') \<in> rf_sr}
 2. \<And>w rega threada uc s s' tcb tcb'. \<lbrakk>w = val; rega = register_from_H reg; threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (atcbContextGet \<circ> tcbArch) tcb = uc; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> s' \<in> ?Q117 w rega threada uc s tcb
 3. \<And>w rega threada s s'. \<lbrakk>w = val; rega = register_from_H reg; threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb thread s \<longrightarrow> (obj_at' (\<lambda>tcba. (atcbContextGet \<circ> tcbArch) tcba = (atcbContextGet \<circ> tcbArch) tcb) thread and (\<lambda>_. True)) s) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' threada = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> UNIV \<inter> (if rega < 0x14 then UNIV else {})} proof (prove)
goal (2 subgoals):
 1. \<And>w rega threada uc s s' tcb tcb'. \<lbrakk>w = val; rega = register_from_H reg; threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (atcbContextGet \<circ> tcbArch) tcb = uc; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> s' \<in> {sa. sa \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<and> (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> injectKOS (tcbArch_update (\<lambda>_. atcbContextSet (uc(reg := val)) (tcbArch tcb)) tcb))\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (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''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals sa))) (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)) val)))) sa) \<in> rf_sr}
 2. \<And>w rega threada s s'. \<lbrakk>w = val; rega = register_from_H reg; threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb thread s \<longrightarrow> (obj_at' (\<lambda>tcba. (atcbContextGet \<circ> tcbArch) tcba = (atcbContextGet \<circ> tcbArch) tcb) thread and (\<lambda>_. True)) s) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' threada = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> UNIV \<inter> (if rega < 0x14 then UNIV else {})} proof (prove)
goal (2 subgoals):
 1. \<And>s s' tcb tcb'. \<lbrakk>(s, s') \<in> rf_sr; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'\<rbrakk> \<Longrightarrow> (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet ((atcbContextGet (tcbArch tcb))(reg := val)) (tcbArch tcb)) tcb))\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (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''])) (Arrays.update (registers_C (tcbContext_C (tcbArch_C tcb'))) (unat (register_from_H reg)) val)))) s') \<in> rf_sr
 2. \<And>w rega threada s s'. \<lbrakk>w = val; rega = register_from_H reg; threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb thread s \<longrightarrow> (obj_at' (\<lambda>tcba. (atcbContextGet \<circ> tcbArch) tcba = (atcbContextGet \<circ> tcbArch) tcb) thread and (\<lambda>_. True)) s) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' threada = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> UNIV \<inter> (if rega < 0x14 then UNIV else {})} proof (prove)
goal (3 subgoals):
 1. \<And>s s' tcb tcb' v. \<lbrakk>(s, s') \<in> rf_sr; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; globals s' = v\<rbrakk> \<Longrightarrow> t_hrs_'_update (hrs_mem_update (heap_update (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''])) (Arrays.update (registers_C (tcbContext_C (tcbArch_C tcb'))) (unat (register_from_H reg)) val))) v = ?f'134 s s' tcb tcb' v
 2. \<And>s s' tcb tcb'. \<lbrakk>(s, s') \<in> rf_sr; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'\<rbrakk> \<Longrightarrow> (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet ((atcbContextGet (tcbArch tcb))(reg := val)) (tcbArch tcb)) tcb))\<rparr>, globals_update (?f'134 s s' tcb tcb') s') \<in> rf_sr
 3. \<And>w rega threada s s'. \<lbrakk>w = val; rega = register_from_H reg; threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb thread s \<longrightarrow> (obj_at' (\<lambda>tcba. (atcbContextGet \<circ> tcbArch) tcba = (atcbContextGet \<circ> tcbArch) tcb) thread and (\<lambda>_. True)) s) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' threada = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> UNIV \<inter> (if rega < 0x14 then UNIV else {})} proof (prove)
goal (3 subgoals):
 1. \<And>s s' tcb tcb' v va. \<lbrakk>(s, s') \<in> rf_sr; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; globals s' = v; t_hrs_' v = va\<rbrakk> \<Longrightarrow> hrs_mem_update (heap_update (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''])) (Arrays.update (registers_C (tcbContext_C (tcbArch_C tcb'))) (unat (register_from_H reg)) val)) va = ?f'136 s s' tcb tcb' v va
 2. \<And>s s' tcb tcb'. \<lbrakk>(s, s') \<in> rf_sr; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'\<rbrakk> \<Longrightarrow> (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet ((atcbContextGet (tcbArch tcb))(reg := val)) (tcbArch tcb)) tcb))\<rparr>, globals_update (\<lambda>v. t_hrs_'_update (?f'136 s s' tcb tcb' v) v) s') \<in> rf_sr
 3. \<And>w rega threada s s'. \<lbrakk>w = val; rega = register_from_H reg; threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb thread s \<longrightarrow> (obj_at' (\<lambda>tcba. (atcbContextGet \<circ> tcbArch) tcba = (atcbContextGet \<circ> tcbArch) tcb) thread and (\<lambda>_. True)) s) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' threada = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> UNIV \<inter> (if rega < 0x14 then UNIV else {})} proof (prove)
goal (4 subgoals):
 1. \<And>s s' tcb tcb' v va. \<lbrakk>(s, s') \<in> rf_sr; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; globals s' = v; t_hrs_' v = va\<rbrakk> \<Longrightarrow> c_guard (PTR(user_context_C) &(PTR(arch_tcb_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C'']))
 2. \<And>s s' tcb tcb' v va. \<lbrakk>(s, s') \<in> rf_sr; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; globals s' = v; t_hrs_' v = va\<rbrakk> \<Longrightarrow> export_uinfo (adjust_ti (typ_info_t TYPE(32 word[20])) registers_C (registers_C_update \<circ> (\<lambda>x _. x))) = export_uinfo (typ_info_t TYPE(32 word[20]))
 3. \<And>s s' tcb tcb'. \<lbrakk>(s, s') \<in> rf_sr; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'\<rbrakk> \<Longrightarrow> (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet ((atcbContextGet (tcbArch tcb))(reg := val)) (tcbArch tcb)) tcb))\<rparr>, globals_update (t_hrs_'_update (\<lambda>va. hrs_mem_update (heap_update (PTR(user_context_C) &(PTR(arch_tcb_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])) (update_ti_t (adjust_ti (typ_info_t TYPE(32 word[20])) registers_C (registers_C_update \<circ> (\<lambda>x _. x))) (to_bytes_p (Arrays.update (registers_C (tcbContext_C (tcbArch_C tcb'))) (unat (register_from_H reg)) val)) (h_val (hrs_mem va) (PTR(user_context_C) &(PTR(arch_tcb_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C'']))))) va)) s') \<in> rf_sr
 4. \<And>w rega threada s s'. \<lbrakk>w = val; rega = register_from_H reg; threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb thread s \<longrightarrow> (obj_at' (\<lambda>tcba. (atcbContextGet \<circ> tcbArch) tcba = (atcbContextGet \<circ> tcbArch) tcb) thread and (\<lambda>_. True)) s) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' threada = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> UNIV \<inter> (if rega < 0x14 then UNIV else {})} proof (prove)
goal (3 subgoals):
 1. \<And>s s' tcb tcb' v va. \<lbrakk>(s, s') \<in> rf_sr; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; globals s' = v; t_hrs_' v = va\<rbrakk> \<Longrightarrow> export_uinfo (adjust_ti (typ_info_t TYPE(32 word[20])) registers_C (registers_C_update \<circ> (\<lambda>x _. x))) = export_uinfo (typ_info_t TYPE(32 word[20]))
 2. \<And>s s' tcb tcb'. \<lbrakk>(s, s') \<in> rf_sr; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'\<rbrakk> \<Longrightarrow> (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet ((atcbContextGet (tcbArch tcb))(reg := val)) (tcbArch tcb)) tcb))\<rparr>, globals_update (t_hrs_'_update (\<lambda>va. hrs_mem_update (heap_update (PTR(user_context_C) &(PTR(arch_tcb_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])) (update_ti_t (adjust_ti (typ_info_t TYPE(32 word[20])) registers_C (registers_C_update \<circ> (\<lambda>x _. x))) (to_bytes_p (Arrays.update (registers_C (tcbContext_C (tcbArch_C tcb'))) (unat (register_from_H reg)) val)) (h_val (hrs_mem va) (PTR(user_context_C) &(PTR(arch_tcb_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C'']))))) va)) s') \<in> rf_sr
 3. \<And>w rega threada s s'. \<lbrakk>w = val; rega = register_from_H reg; threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb thread s \<longrightarrow> (obj_at' (\<lambda>tcba. (atcbContextGet \<circ> tcbArch) tcba = (atcbContextGet \<circ> tcbArch) tcb) thread and (\<lambda>_. True)) s) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' threada = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> UNIV \<inter> (if rega < 0x14 then UNIV else {})} proof (prove)
goal (2 subgoals):
 1. \<And>s s' tcb tcb'. \<lbrakk>(s, s') \<in> rf_sr; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'\<rbrakk> \<Longrightarrow> (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet ((atcbContextGet (tcbArch tcb))(reg := val)) (tcbArch tcb)) tcb))\<rparr>, globals_update (t_hrs_'_update (\<lambda>va. hrs_mem_update (heap_update (PTR(user_context_C) &(PTR(arch_tcb_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])) (update_ti_t (adjust_ti (typ_info_t TYPE(32 word[20])) registers_C (registers_C_update \<circ> (\<lambda>x _. x))) (to_bytes_p (Arrays.update (registers_C (tcbContext_C (tcbArch_C tcb'))) (unat (register_from_H reg)) val)) (h_val (hrs_mem va) (PTR(user_context_C) &(PTR(arch_tcb_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C'']))))) va)) s') \<in> rf_sr
 2. \<And>w rega threada s s'. \<lbrakk>w = val; rega = register_from_H reg; threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb thread s \<longrightarrow> (obj_at' (\<lambda>tcba. (atcbContextGet \<circ> tcbArch) tcba = (atcbContextGet \<circ> tcbArch) tcb) thread and (\<lambda>_. True)) s) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' threada = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> UNIV \<inter> (if rega < 0x14 then UNIV else {})} proof (prove)
goal (3 subgoals):
 1. \<And>s s' tcb tcb'. \<lbrakk>ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'\<rbrakk> \<Longrightarrow> \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> getF (tcbArch_update (\<lambda>_. atcbContextSet ((atcbContextGet (tcbArch tcb))(reg := val)) (tcbArch tcb)) tcb) = getF tcb
 2. \<And>s s' tcb tcb'. \<lbrakk>ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'\<rbrakk> \<Longrightarrow> ctcb_relation (tcbArch_update (\<lambda>_. atcbContextSet ((atcbContextGet (tcbArch tcb))(reg := val)) (tcbArch tcb)) tcb) (tcbArch_C_update (\<lambda>_. tcbContext_C_update (\<lambda>_. registers_C_update (\<lambda>_. Arrays.update (registers_C (tcbContext_C (tcbArch_C tcb'))) (unat (register_from_H reg)) val) (tcbContext_C (tcbArch_C tcb'))) (tcbArch_C tcb')) tcb')
 3. \<And>w rega threada s s'. \<lbrakk>w = val; rega = register_from_H reg; threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb thread s \<longrightarrow> (obj_at' (\<lambda>tcba. (atcbContextGet \<circ> tcbArch) tcba = (atcbContextGet \<circ> tcbArch) tcb) thread and (\<lambda>_. True)) s) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' threada = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> UNIV \<inter> (if rega < 0x14 then UNIV else {})} proof (prove)
goal (2 subgoals):
 1. \<And>s s' tcb tcb'. \<lbrakk>ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'\<rbrakk> \<Longrightarrow> ctcb_relation (tcbArch_update (\<lambda>_. atcbContextSet ((atcbContextGet (tcbArch tcb))(reg := val)) (tcbArch tcb)) tcb) (tcbArch_C_update (\<lambda>_. tcbContext_C_update (\<lambda>_. registers_C_update (\<lambda>_. Arrays.update (registers_C (tcbContext_C (tcbArch_C tcb'))) (unat (register_from_H reg)) val) (tcbContext_C (tcbArch_C tcb'))) (tcbArch_C tcb')) tcb')
 2. \<And>w rega threada s s'. \<lbrakk>w = val; rega = register_from_H reg; threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb thread s \<longrightarrow> (obj_at' (\<lambda>tcba. (atcbContextGet \<circ> tcbArch) tcba = (atcbContextGet \<circ> tcbArch) tcb) thread and (\<lambda>_. True)) s) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' threada = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> UNIV \<inter> (if rega < 0x14 then UNIV else {})} proof (prove)
goal (1 subgoal):
 1. \<And>w rega threada s s'. \<lbrakk>w = val; rega = register_from_H reg; threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>tcb. ko_at' tcb thread s \<longrightarrow> (obj_at' (\<lambda>tcba. (atcbContextGet \<circ> tcbArch) tcba = (atcbContextGet \<circ> tcbArch) tcb) thread and (\<lambda>_. True)) s) \<and> s' \<in> {s'. \<forall>tcb ctcb. cslift s' threada = Some ctcb \<and> ctcb_relation tcb ctcb \<longrightarrow> s' \<in> UNIV \<inter> (if rega < 0x14 then UNIV else {})} proof (prove)
goal (1 subgoal):
 1. \<And>s s' tcb. \<lbrakk>(s, s') \<in> rf_sr; ko_at' tcb thread s\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>tcba. atcbContextGet (tcbArch tcba) = atcbContextGet (tcbArch tcb)) thread s proof (prove)
goal:
No subgoals!