theory Arch_C

lemma setMR_as_setRegister_ccorres:
  "ccorres (\<lambda>rv rv'. rv' = of_nat offset + 1) ret__unsigned_'
      (tcb_at' thread and K (TCB_H.msgRegisters ! offset = reg \<and> offset < length msgRegisters))
      (UNIV \<inter> \<lbrace>\<acute>reg = val\<rbrace>
            \<inter> \<lbrace>\<acute>offset = of_nat offset\<rbrace>
            \<inter> \<lbrace>\<acute>receiver = tcb_ptr_to_ctcb_ptr thread\<rbrace>) hs
    (asUser thread (setRegister reg val))
    (Call setMR_'proc)" apply (rule ccorres_grab_asm) apply (cinit' lift:  reg_' offset_' receiver_') apply (clarsimp simp: length_msgRegisters) apply (rule ccorres_cond_false) apply (rule ccorres_move_const_guards) apply (rule ccorres_add_return2) apply (ctac add: setRegister_ccorres) apply (rule ccorres_from_vcg_throws[where P'=UNIV and P=\<top>]) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: return_def) apply (rule hoare_post_taut[of \<top>]) apply (vcg exspec=setRegister_modifies) apply (clarsimp simp: length_msgRegisters n_msgRegisters_def not_le conj_commute) apply (subst msgRegisters_ccorres[symmetric]) apply (clarsimp simp: n_msgRegisters_def unat_of_nat_eq) apply (clarsimp simp: word_less_nat_alt word_le_nat_alt unat_of_nat_eq not_le[symmetric]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (\<lambda>rv rv'. rv' = word_of_nat offset + 1) ret__unsigned_' (tcb_at' thread and K (TCB_H.msgRegisters ! offset = reg \<and> offset < length TCB_H.msgRegisters)) (UNIV \<inter> \<lbrace>\<acute>reg = val\<rbrace> \<inter> \<lbrace>\<acute>offset = word_of_nat offset\<rbrace> \<inter> \<lbrace>\<acute>receiver = tcb_ptr_to_ctcb_ptr thread\<rbrace>) hs (asUser thread (setRegister reg val)) (Call setMR_'proc) proof (prove)
goal (1 subgoal):
 1. TCB_H.msgRegisters ! offset = reg \<and> offset < length TCB_H.msgRegisters \<Longrightarrow> ccorres (\<lambda>rv rv'. rv' = word_of_nat offset + 1) ret__unsigned_' (tcb_at' thread) (UNIV \<inter> \<lbrace>\<acute>reg = val\<rbrace> \<inter> \<lbrace>\<acute>offset = word_of_nat offset\<rbrace> \<inter> \<lbrace>\<acute>receiver = tcb_ptr_to_ctcb_ptr thread\<rbrace>) hs (asUser thread (setRegister reg val)) (Call setMR_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>receiver offseta rega. \<lbrakk>TCB_H.msgRegisters ! offset = reg \<and> offset < length TCB_H.msgRegisters; receiver = tcb_ptr_to_ctcb_ptr thread; offseta = word_of_nat offset; rega = val\<rbrakk> \<Longrightarrow> ccorres (\<lambda>rv rv'. rv' = word_of_nat offset + 1) ret__unsigned_' (?Q443 receiver offseta rega) (?Q'443 receiver offseta rega) (SKIP # hs) (asUser thread (setRegister reg val)) (IF SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> offseta THEN
  IF \<acute>receiveIPCBuffer \<noteq> NULL THEN
  Guard MemorySafety \<lbrace>offseta + 1 = 0 \<or> array_assertion \<acute>receiveIPCBuffer (unat (offseta + 1)) (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c (receiveIPCBuffer_' s +\<^sub>p uint (offseta + 1))} (Guard MemorySafety \<lbrace>offseta + 1 = 0 \<or> array_assertion \<acute>receiveIPCBuffer (Suc (unat (offseta + 1))) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (\<acute>receiveIPCBuffer +\<^sub>p uint (offseta + 1)) rega)))));;
return_C ret__unsigned_'_update (\<lambda>s. offseta + 1)
ELSE
  return_C ret__unsigned_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) n_msgRegisters)
FI
ELSE
  Guard ArrayBounds \<lbrace>offseta < 4\<rbrace> (CALL setRegister_'proc(receiver,kernel_all_global_addresses.msgRegisters.[unat offseta],rega));;
return_C ret__unsigned_'_update (\<lambda>s. offseta + 1)
FI)
 2. \<And>receiver offseta rega s s'. \<lbrakk>TCB_H.msgRegisters ! offset = reg \<and> offset < length TCB_H.msgRegisters; receiver = tcb_ptr_to_ctcb_ptr thread; offseta = word_of_nat offset; rega = val; (s, s') \<in> rf_sr; tcb_at' thread s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q443 receiver offseta rega s \<and> s' \<in> ?Q'443 receiver offseta rega proof (prove)
goal (2 subgoals):
 1. \<lbrakk>offset < unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters); reg = TCB_H.msgRegisters ! offset\<rbrakk> \<Longrightarrow> ccorres (\<lambda>rv rv'. rv' = word_of_nat offset + 1) ret__unsigned_' (?Q443 (tcb_ptr_to_ctcb_ptr thread) (word_of_nat offset) val) (?Q'443 (tcb_ptr_to_ctcb_ptr thread) (word_of_nat offset) val) (SKIP # hs) (asUser thread (setRegister (TCB_H.msgRegisters ! offset) val)) (Cond (if SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> word_of_nat offset then UNIV else {}) (IF \<acute>receiveIPCBuffer \<noteq> NULL THEN
  Guard MemorySafety \<lbrace>word_of_nat offset + 1 = 0 \<or> array_assertion \<acute>receiveIPCBuffer (unat (word_of_nat offset + 1)) (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c (receiveIPCBuffer_' s +\<^sub>p uint (word_of_nat offset + 1))} (Guard MemorySafety \<lbrace>word_of_nat offset + 1 = 0 \<or> array_assertion \<acute>receiveIPCBuffer (Suc (unat (word_of_nat offset + 1))) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (\<acute>receiveIPCBuffer +\<^sub>p uint (word_of_nat offset + 1)) val)))));;
return_C ret__unsigned_'_update (\<lambda>s. word_of_nat offset + 1)
ELSE
  return_C ret__unsigned_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) n_msgRegisters)
FI) (Guard ArrayBounds (if word_of_nat offset < 4 then UNIV else {}) (CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr thread,kernel_all_global_addresses.msgRegisters.[unat (word_of_nat offset)],val));;
return_C ret__unsigned_'_update (\<lambda>s. word_of_nat offset + 1)))
 2. \<And>receiver offseta rega s s'. \<lbrakk>TCB_H.msgRegisters ! offset = reg \<and> offset < length TCB_H.msgRegisters; receiver = tcb_ptr_to_ctcb_ptr thread; offseta = word_of_nat offset; rega = val; (s, s') \<in> rf_sr; tcb_at' thread s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q443 receiver offseta rega s \<and> s' \<in> ?Q'443 receiver offseta rega proof (prove)
goal (2 subgoals):
 1. \<lbrakk>offset < unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters); reg = TCB_H.msgRegisters ! offset\<rbrakk> \<Longrightarrow> ccorres (\<lambda>rv rv'. rv' = word_of_nat offset + 1) ret__unsigned_' (?Q443 (tcb_ptr_to_ctcb_ptr thread) (word_of_nat offset) val) (?R'460 (tcb_ptr_to_ctcb_ptr thread) (word_of_nat offset) val) (SKIP # hs) (asUser thread (setRegister (TCB_H.msgRegisters ! offset) val)) (Guard ArrayBounds (if word_of_nat offset < 4 then UNIV else {}) (CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr thread,kernel_all_global_addresses.msgRegisters.[unat (word_of_nat offset)],val));;
return_C ret__unsigned_'_update (\<lambda>s. word_of_nat offset + 1))
 2. \<And>receiver offseta rega s s'. \<lbrakk>TCB_H.msgRegisters ! offset = reg \<and> offset < length TCB_H.msgRegisters; receiver = tcb_ptr_to_ctcb_ptr thread; offseta = word_of_nat offset; rega = val; (s, s') \<in> rf_sr; tcb_at' thread s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q443 receiver offseta rega s \<and> s' \<in> ?R'460 receiver offseta rega \<inter> - (if SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> offseta then UNIV else {}) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>offset < unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters); reg = TCB_H.msgRegisters ! offset\<rbrakk> \<Longrightarrow> ccorres (\<lambda>rv rv'. rv' = word_of_nat offset + 1) ret__unsigned_' (?P464 (tcb_ptr_to_ctcb_ptr thread) (word_of_nat offset) val) (?R'460 (tcb_ptr_to_ctcb_ptr thread) (word_of_nat offset) val) (SKIP # hs) (asUser thread (setRegister (TCB_H.msgRegisters ! offset) val)) (CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr thread,kernel_all_global_addresses.msgRegisters.[unat (word_of_nat offset)],val);;
return_C ret__unsigned_'_update (\<lambda>s. word_of_nat offset + 1))
 2. \<And>receiver offseta rega s s'. \<lbrakk>TCB_H.msgRegisters ! offset = reg \<and> offset < length TCB_H.msgRegisters; receiver = tcb_ptr_to_ctcb_ptr thread; offseta = word_of_nat offset; rega = val; (s, s') \<in> rf_sr; tcb_at' thread s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (?P464 receiver offseta rega and K (offseta < 4)) s \<and> s' \<in> ?R'460 receiver offseta rega \<inter> - (if SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> offseta then UNIV else {}) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>offset < unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters); reg = TCB_H.msgRegisters ! offset\<rbrakk> \<Longrightarrow> ccorres (\<lambda>rv rv'. rv' = word_of_nat offset + 1) ret__unsigned_' (?P464 (tcb_ptr_to_ctcb_ptr thread) (word_of_nat offset) val) (?R'460 (tcb_ptr_to_ctcb_ptr thread) (word_of_nat offset) val) (SKIP # hs) (asUser thread (setRegister (TCB_H.msgRegisters ! offset) val) >>= return) (CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr thread,kernel_all_global_addresses.msgRegisters.[unat (word_of_nat offset)],val);;
return_C ret__unsigned_'_update (\<lambda>s. word_of_nat offset + 1))
 2. \<And>receiver offseta rega s s'. \<lbrakk>TCB_H.msgRegisters ! offset = reg \<and> offset < length TCB_H.msgRegisters; receiver = tcb_ptr_to_ctcb_ptr thread; offseta = word_of_nat offset; rega = val; (s, s') \<in> rf_sr; tcb_at' thread s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (?P464 receiver offseta rega and K (offseta < 4)) s \<and> s' \<in> ?R'460 receiver offseta rega \<inter> - (if SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> offseta then UNIV else {}) proof (prove)
goal (4 subgoals):
 1. \<And>rv xfdc. \<lbrakk>offset < unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters); reg = TCB_H.msgRegisters ! offset; dc rv xfdc\<rbrakk> \<Longrightarrow> ccorres (\<lambda>rv rv'. rv' = word_of_nat offset + 1) ret__unsigned_' (?Q470 rv) (?Q'470 rv xfdc) (SKIP # hs) (return rv) (return_C ret__unsigned_'_update (\<lambda>s. word_of_nat offset + 1))
 2. \<lbrakk>offset < unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters); reg = TCB_H.msgRegisters ! offset\<rbrakk> \<Longrightarrow> \<lbrace>?R477 (tcb_ptr_to_ctcb_ptr thread) (word_of_nat offset) val\<rbrace> asUser thread (setRegister (TCB_H.msgRegisters ! offset) val) \<lbrace>?Q470\<rbrace>
 3. \<lbrakk>offset < unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters); reg = TCB_H.msgRegisters ! offset\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'472 (tcb_ptr_to_ctcb_ptr thread) (word_of_nat offset) val) CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr thread,kernel_all_global_addresses.msgRegisters.[unat (word_of_nat offset)],val) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> ?Q'470 rv (xfdc s)}
 4. \<And>receiver offseta rega s s'. \<lbrakk>TCB_H.msgRegisters ! offset = reg \<and> offset < length TCB_H.msgRegisters; receiver = tcb_ptr_to_ctcb_ptr thread; offseta = word_of_nat offset; rega = val; (s, s') \<in> rf_sr; tcb_at' thread s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?R477 receiver offseta rega and K (offseta < 4)) s \<and> s' \<in> {s. w_'_update (\<lambda>_. rega) (reg_'_update (\<lambda>_. kernel_all_global_addresses.msgRegisters.[unat offseta]) (thread_'_update (\<lambda>_. receiver) s)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = receiver\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H (TCB_H.msgRegisters ! offset)\<rbrace> \<inter> \<lbrace>\<acute>w = rega\<rbrace>} \<inter> ?R'472 receiver offseta rega \<inter> - (if SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> offseta then UNIV else {}) proof (prove)
goal (4 subgoals):
 1. \<And>rv xfdc. \<lbrakk>offset < unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters); reg = TCB_H.msgRegisters ! offset; dc rv xfdc\<rbrakk> \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} return_C ret__unsigned_'_update (\<lambda>s. word_of_nat offset + 1) {},{s. \<exists>(rv, \<sigma>')\<in>fst (return rv \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> ret__unsigned_' s = word_of_nat offset + 1}
 2. \<lbrakk>offset < unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters); reg = TCB_H.msgRegisters ! offset\<rbrakk> \<Longrightarrow> \<lbrace>?R477 (tcb_ptr_to_ctcb_ptr thread) (word_of_nat offset) val\<rbrace> asUser thread (setRegister (TCB_H.msgRegisters ! offset) val) \<lbrace>\<lambda>a b. True\<rbrace>
 3. \<lbrakk>offset < unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters); reg = TCB_H.msgRegisters ! offset\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'472 (tcb_ptr_to_ctcb_ptr thread) (word_of_nat offset) val) CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr thread,kernel_all_global_addresses.msgRegisters.[unat (word_of_nat offset)],val) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> UNIV}
 4. \<And>receiver offseta rega s s'. \<lbrakk>TCB_H.msgRegisters ! offset = reg \<and> offset < length TCB_H.msgRegisters; receiver = tcb_ptr_to_ctcb_ptr thread; offseta = word_of_nat offset; rega = val; (s, s') \<in> rf_sr; tcb_at' thread s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?R477 receiver offseta rega and K (offseta < 4)) s \<and> s' \<in> {s. w_'_update (\<lambda>_. rega) (reg_'_update (\<lambda>_. kernel_all_global_addresses.msgRegisters.[unat offseta]) (thread_'_update (\<lambda>_. receiver) s)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = receiver\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H (TCB_H.msgRegisters ! offset)\<rbrace> \<inter> \<lbrace>\<acute>w = rega\<rbrace>} \<inter> ?R'472 receiver offseta rega \<inter> - (if SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> offseta then UNIV else {}) proof (prove)
goal (4 subgoals):
 1. \<And>rv xfdc \<sigma>. \<lbrakk>offset < unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters); reg = TCB_H.msgRegisters ! offset; dc rv xfdc\<rbrakk> \<Longrightarrow> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (return rv \<sigma>). (\<sigma>', s\<lparr>ret__unsigned_' := word_of_nat offset + 1, global_exn_var_' := Return\<rparr>) \<in> rf_sr \<and> word_of_nat offset + 1 = word_of_nat offset + 1}
 2. \<lbrakk>offset < unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters); reg = TCB_H.msgRegisters ! offset\<rbrakk> \<Longrightarrow> \<lbrace>?R477 (tcb_ptr_to_ctcb_ptr thread) (word_of_nat offset) val\<rbrace> asUser thread (setRegister (TCB_H.msgRegisters ! offset) val) \<lbrace>\<lambda>a b. True\<rbrace>
 3. \<lbrakk>offset < unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters); reg = TCB_H.msgRegisters ! offset\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'472 (tcb_ptr_to_ctcb_ptr thread) (word_of_nat offset) val) CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr thread,kernel_all_global_addresses.msgRegisters.[unat (word_of_nat offset)],val) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> UNIV}
 4. \<And>receiver offseta rega s s'. \<lbrakk>TCB_H.msgRegisters ! offset = reg \<and> offset < length TCB_H.msgRegisters; receiver = tcb_ptr_to_ctcb_ptr thread; offseta = word_of_nat offset; rega = val; (s, s') \<in> rf_sr; tcb_at' thread s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?R477 receiver offseta rega and K (offseta < 4)) s \<and> s' \<in> {s. w_'_update (\<lambda>_. rega) (reg_'_update (\<lambda>_. kernel_all_global_addresses.msgRegisters.[unat offseta]) (thread_'_update (\<lambda>_. receiver) s)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = receiver\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H (TCB_H.msgRegisters ! offset)\<rbrace> \<inter> \<lbrace>\<acute>w = rega\<rbrace>} \<inter> ?R'472 receiver offseta rega \<inter> - (if SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> offseta then UNIV else {}) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>offset < unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters); reg = TCB_H.msgRegisters ! offset\<rbrakk> \<Longrightarrow> \<lbrace>?R477 (tcb_ptr_to_ctcb_ptr thread) (word_of_nat offset) val\<rbrace> asUser thread (setRegister (TCB_H.msgRegisters ! offset) val) \<lbrace>\<lambda>a b. True\<rbrace>
 2. \<lbrakk>offset < unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters); reg = TCB_H.msgRegisters ! offset\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'472 (tcb_ptr_to_ctcb_ptr thread) (word_of_nat offset) val) CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr thread,kernel_all_global_addresses.msgRegisters.[unat (word_of_nat offset)],val) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> UNIV}
 3. \<And>receiver offseta rega s s'. \<lbrakk>TCB_H.msgRegisters ! offset = reg \<and> offset < length TCB_H.msgRegisters; receiver = tcb_ptr_to_ctcb_ptr thread; offseta = word_of_nat offset; rega = val; (s, s') \<in> rf_sr; tcb_at' thread s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?R477 receiver offseta rega and K (offseta < 4)) s \<and> s' \<in> {s. w_'_update (\<lambda>_. rega) (reg_'_update (\<lambda>_. kernel_all_global_addresses.msgRegisters.[unat offseta]) (thread_'_update (\<lambda>_. receiver) s)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = receiver\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H (TCB_H.msgRegisters ! offset)\<rbrace> \<inter> \<lbrace>\<acute>w = rega\<rbrace>} \<inter> ?R'472 receiver offseta rega \<inter> - (if SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> offseta then UNIV else {}) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>offset < unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters); reg = TCB_H.msgRegisters ! offset\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'472 (tcb_ptr_to_ctcb_ptr thread) (word_of_nat offset) val) CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr thread,kernel_all_global_addresses.msgRegisters.[unat (word_of_nat offset)],val) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> UNIV}
 2. \<And>receiver offseta rega s s'. \<lbrakk>TCB_H.msgRegisters ! offset = reg \<and> offset < length TCB_H.msgRegisters; receiver = tcb_ptr_to_ctcb_ptr thread; offseta = word_of_nat offset; rega = val; (s, s') \<in> rf_sr; tcb_at' thread s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and (\<lambda>a. True) and K (offseta < 4)) s \<and> s' \<in> {s. w_'_update (\<lambda>_. rega) (reg_'_update (\<lambda>_. kernel_all_global_addresses.msgRegisters.[unat offseta]) (thread_'_update (\<lambda>_. receiver) s)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = receiver\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H (TCB_H.msgRegisters ! offset)\<rbrace> \<inter> \<lbrace>\<acute>w = rega\<rbrace>} \<inter> ?R'472 receiver offseta rega \<inter> - (if SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> offseta then UNIV else {}) proof (prove)
goal (1 subgoal):
 1. \<And>receiver offseta rega s s'. \<lbrakk>TCB_H.msgRegisters ! offset = reg \<and> offset < length TCB_H.msgRegisters; receiver = tcb_ptr_to_ctcb_ptr thread; offseta = word_of_nat offset; rega = val; (s, s') \<in> rf_sr; tcb_at' thread s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and (\<lambda>a. True) and K (offseta < 4)) s \<and> s' \<in> {s. w_'_update (\<lambda>_. rega) (reg_'_update (\<lambda>_. kernel_all_global_addresses.msgRegisters.[unat offseta]) (thread_'_update (\<lambda>_. receiver) s)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = receiver\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H (TCB_H.msgRegisters ! offset)\<rbrace> \<inter> \<lbrace>\<acute>w = rega\<rbrace>} \<inter> \<lbrace>True\<rbrace> \<inter> - (if SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<le> offseta then UNIV else {}) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; tcb_at' thread s; offset < 4; reg = TCB_H.msgRegisters ! offset\<rbrakk> \<Longrightarrow> word_of_nat offset < 4 \<and> kernel_all_global_addresses.msgRegisters.[unat (word_of_nat offset)] = register_from_H (TCB_H.msgRegisters ! offset) proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; tcb_at' thread s; offset < 4; reg = TCB_H.msgRegisters ! offset\<rbrakk> \<Longrightarrow> unat (word_of_nat offset) < unat n_msgRegisters
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; tcb_at' thread s; offset < 4; reg = TCB_H.msgRegisters ! offset\<rbrakk> \<Longrightarrow> word_of_nat offset < 4 \<and> register_from_H (TCB_H.msgRegisters ! unat (word_of_nat offset)) = register_from_H (TCB_H.msgRegisters ! offset) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; tcb_at' thread s; offset < 4; reg = TCB_H.msgRegisters ! offset\<rbrakk> \<Longrightarrow> word_of_nat offset < 4 \<and> register_from_H (TCB_H.msgRegisters ! unat (word_of_nat offset)) = register_from_H (TCB_H.msgRegisters ! offset) proof (prove)
goal:
No subgoals!