theory Fastpath_C

lemma fastpath_copy_mrs_ccorres:
notes nat_min_simps [simp del]
shows
  "ccorres dc xfdc (\<top> and (\<lambda>_. len <= length ARM_H.msgRegisters))
     (UNIV \<inter> {s. unat (length___unsigned_long_' s) = len}
           \<inter> {s. src_' s = tcb_ptr_to_ctcb_ptr src}
           \<inter> {s. dest_' s = tcb_ptr_to_ctcb_ptr dest}) []
     (forM_x (take len ARM_H.msgRegisters)
             (\<lambda>r. do v \<leftarrow> asUser src (getRegister r);
                    asUser dest (setRegister r v) od))
     (Call fastpath_copy_mrs_'proc)" apply (rule ccorres_gen_asm) apply (cinit' lift: length___unsigned_long_' src_' dest_' simp: word_sle_def word_sless_def) apply (unfold whileAnno_def) apply (rule ccorres_rel_imp) apply (rule_tac F="K \<top>" in ccorres_mapM_x_while) apply clarsimp apply (rule ccorres_guard_imp2) apply (rule ccorres_rhs_assoc)+ apply (rule_tac xf'="i_'" in ccorres_abstract, ceqv) apply csymbr apply (ctac(no_vcg)) apply ctac apply wp apply (clarsimp simp: rf_sr_ksCurThread) apply (simp add: msgRegisters_ccorres[symmetric] length_msgRegisters) apply (simp add: n_msgRegisters_def msgRegisters_unfold) apply (drule(1) order_less_le_trans) apply ((clarsimp simp: "StrictC'_register_defs" msgRegistersC_def fupdate_def
                | drule nat_less_cases' | erule disjE)+)[2] apply (rule allI, rule conseqPre, vcg) apply (simp) apply (simp add: length_msgRegisters n_msgRegisters_def word_bits_def hoare_TrueI)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc ((\<lambda>_. True) and (\<lambda>_. len \<le> length TCB_H.msgRegisters)) (UNIV \<inter> \<lbrace>unat \<acute>length___unsigned_long = len\<rbrace> \<inter> \<lbrace>\<acute>src = tcb_ptr_to_ctcb_ptr src\<rbrace> \<inter> \<lbrace>\<acute>dest = tcb_ptr_to_ctcb_ptr dest\<rbrace>) [] (forM_x (take len TCB_H.msgRegisters) (\<lambda>r. do v <- asUser src (getRegister r);
asUser dest (setRegister r v)
od)) (Call fastpath_copy_mrs_'proc) proof (prove)
goal (1 subgoal):
 1. len \<le> length TCB_H.msgRegisters \<Longrightarrow> ccorres dc xfdc (\<lambda>_. True) (UNIV \<inter> \<lbrace>unat \<acute>length___unsigned_long = len\<rbrace> \<inter> \<lbrace>\<acute>src = tcb_ptr_to_ctcb_ptr src\<rbrace> \<inter> \<lbrace>\<acute>dest = tcb_ptr_to_ctcb_ptr dest\<rbrace>) [] (forM_x (take len TCB_H.msgRegisters) (\<lambda>r. do v <- asUser src (getRegister r);
asUser dest (setRegister r v)
od)) (Call fastpath_copy_mrs_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>desta srca length___unsigned_long. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q553 desta srca length___unsigned_long) (?Q'553 desta srca length___unsigned_long) [SKIP] (mapM_x (\<lambda>r. do v <- asUser src (getRegister r);
asUser dest (setRegister r v)
od) (take len TCB_H.msgRegisters)) (\<acute>i :== 0;;
WHILE \<acute>i < length___unsigned_long DO
  \<acute>reg :== kernel_all_global_addresses.msgRegisters.[0] + \<acute>i;;
\<acute>ret__unsigned_long :== CALL getRegister_'proc(srca,\<acute>reg);;
CALL setRegister_'proc(desta,\<acute>reg,\<acute>ret__unsigned_long);;
\<acute>i :== \<acute>i + 1
OD)
 2. \<And>desta srca length___unsigned_long s s'. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q553 desta srca length___unsigned_long s \<and> s' \<in> ?Q'553 desta srca length___unsigned_long proof (prove)
goal (2 subgoals):
 1. \<And>desta srca length___unsigned_long. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q553 desta srca length___unsigned_long) (?Q'553 desta srca length___unsigned_long) [SKIP] (mapM_x (\<lambda>r. do v <- asUser src (getRegister r);
asUser dest (setRegister r v)
od) (take len TCB_H.msgRegisters)) (\<acute>i :== 0;;
While \<lbrace>\<acute>i < length___unsigned_long\<rbrace> (\<acute>reg :== kernel_all_global_addresses.msgRegisters.[0] + \<acute>i;;
\<acute>ret__unsigned_long :== CALL getRegister_'proc(srca,\<acute>reg);;
CALL setRegister_'proc(desta,\<acute>reg,\<acute>ret__unsigned_long);;
\<acute>i :== \<acute>i + 1))
 2. \<And>desta srca length___unsigned_long s s'. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q553 desta srca length___unsigned_long s \<and> s' \<in> ?Q'553 desta srca length___unsigned_long proof (prove)
goal (3 subgoals):
 1. \<And>desta srca length___unsigned_long. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len\<rbrakk> \<Longrightarrow> ccorres (?r'559 desta srca length___unsigned_long) (?xf'559 desta srca length___unsigned_long) (?Q553 desta srca length___unsigned_long) (?Q'553 desta srca length___unsigned_long) [SKIP] (mapM_x (\<lambda>r. do v <- asUser src (getRegister r);
asUser dest (setRegister r v)
od) (take len TCB_H.msgRegisters)) (\<acute>i :== 0;;
While \<lbrace>\<acute>i < length___unsigned_long\<rbrace> (\<acute>reg :== kernel_all_global_addresses.msgRegisters.[0] + \<acute>i;;
\<acute>ret__unsigned_long :== CALL getRegister_'proc(srca,\<acute>reg);;
CALL setRegister_'proc(desta,\<acute>reg,\<acute>ret__unsigned_long);;
\<acute>i :== \<acute>i + 1))
 2. \<And>desta srca length___unsigned_long x y. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len; ?r'559 desta srca length___unsigned_long x (?xf'559 desta srca length___unsigned_long y)\<rbrakk> \<Longrightarrow> dc x (xfdc y)
 3. \<And>desta srca length___unsigned_long s s'. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q553 desta srca length___unsigned_long s \<and> s' \<in> ?Q'553 desta srca length___unsigned_long proof (prove)
goal (7 subgoals):
 1. \<And>desta srca length___unsigned_long. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len\<rbrakk> \<Longrightarrow> \<forall>n<length (take len TCB_H.msgRegisters). ccorres dc xfdc (K (\<lambda>_. True) n) \<lbrace>\<acute>i = word_of_nat n\<rbrace> [SKIP] (do v <- asUser src (getRegister (take len TCB_H.msgRegisters ! n));
asUser dest (setRegister (take len TCB_H.msgRegisters ! n) v)
od) (\<acute>reg :== kernel_all_global_addresses.msgRegisters.[0] + \<acute>i;;
\<acute>ret__unsigned_long :== CALL getRegister_'proc(srca,\<acute>reg);;
CALL setRegister_'proc(desta,\<acute>reg,\<acute>ret__unsigned_long))
 2. \<And>desta srca length___unsigned_long n. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len\<rbrakk> \<Longrightarrow> (n < length___unsigned_long) = (n < word_of_nat (length (take len TCB_H.msgRegisters)))
 3. \<And>desta srca length___unsigned_long. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len\<rbrakk> \<Longrightarrow> \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} \<acute>reg :== kernel_all_global_addresses.msgRegisters.[0] + \<acute>i;;
\<acute>ret__unsigned_long :== CALL getRegister_'proc(srca,\<acute>reg);;
CALL setRegister_'proc(desta,\<acute>reg,\<acute>ret__unsigned_long) \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>
 4. \<And>desta srca length___unsigned_long n. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len; Suc n < length (take len TCB_H.msgRegisters)\<rbrakk> \<Longrightarrow> \<lbrace>K (\<lambda>_. True) n\<rbrace> do v <- asUser src (getRegister (take len TCB_H.msgRegisters ! n));
asUser dest (setRegister (take len TCB_H.msgRegisters ! n) v)
od \<lbrace>\<lambda>_. K (\<lambda>_. True) (Suc n)\<rbrace>
 5. \<And>desta srca length___unsigned_long. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len\<rbrakk> \<Longrightarrow> length (take len TCB_H.msgRegisters) < 2 ^ word_bits
 6. \<And>desta srca length___unsigned_long x y. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len; i_' y = word_of_nat (length (take len TCB_H.msgRegisters))\<rbrakk> \<Longrightarrow> dc x (xfdc y)
 7. \<And>desta srca length___unsigned_long s s'. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> K (\<lambda>_. True) 0 s \<and> s' \<in> UNIV proof (prove)
goal (7 subgoals):
 1. \<And>length___unsigned_long n. \<lbrakk>unat length___unsigned_long \<le> length TCB_H.msgRegisters; len = unat length___unsigned_long; n < unat length___unsigned_long\<rbrakk> \<Longrightarrow> ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>i = word_of_nat n\<rbrace> [SKIP] (do v <- asUser src (getRegister (TCB_H.msgRegisters ! n));
asUser dest (setRegister (TCB_H.msgRegisters ! n) v)
od) (\<acute>reg :== kernel_all_global_addresses.msgRegisters.[0] + \<acute>i;;
\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr src);;
CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr dest,\<acute>ret__unsigned_long))
 2. \<And>desta srca length___unsigned_long n. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len\<rbrakk> \<Longrightarrow> (n < length___unsigned_long) = (n < word_of_nat (length (take len TCB_H.msgRegisters)))
 3. \<And>desta srca length___unsigned_long. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len\<rbrakk> \<Longrightarrow> \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} \<acute>reg :== kernel_all_global_addresses.msgRegisters.[0] + \<acute>i;;
\<acute>ret__unsigned_long :== CALL getRegister_'proc(srca,\<acute>reg);;
CALL setRegister_'proc(desta,\<acute>reg,\<acute>ret__unsigned_long) \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>
 4. \<And>desta srca length___unsigned_long n. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len; Suc n < length (take len TCB_H.msgRegisters)\<rbrakk> \<Longrightarrow> \<lbrace>K (\<lambda>_. True) n\<rbrace> do v <- asUser src (getRegister (take len TCB_H.msgRegisters ! n));
asUser dest (setRegister (take len TCB_H.msgRegisters ! n) v)
od \<lbrace>\<lambda>_. K (\<lambda>_. True) (Suc n)\<rbrace>
 5. \<And>desta srca length___unsigned_long. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len\<rbrakk> \<Longrightarrow> length (take len TCB_H.msgRegisters) < 2 ^ word_bits
 6. \<And>desta srca length___unsigned_long x y. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len; i_' y = word_of_nat (length (take len TCB_H.msgRegisters))\<rbrakk> \<Longrightarrow> dc x (xfdc y)
 7. \<And>desta srca length___unsigned_long s s'. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> K (\<lambda>_. True) 0 s \<and> s' \<in> UNIV proof (prove)
goal (8 subgoals):
 1. \<And>length___unsigned_long n. \<lbrakk>unat length___unsigned_long \<le> length TCB_H.msgRegisters; len = unat length___unsigned_long; n < unat length___unsigned_long\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q574 length___unsigned_long n) (?Q'574 length___unsigned_long n) [SKIP] (do v <- asUser src (getRegister (TCB_H.msgRegisters ! n));
asUser dest (setRegister (TCB_H.msgRegisters ! n) v)
od) (\<acute>reg :== kernel_all_global_addresses.msgRegisters.[0] + \<acute>i;;
\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr src);;
CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr dest,\<acute>ret__unsigned_long))
 2. \<And>length___unsigned_long n s s'. \<lbrakk>unat length___unsigned_long \<le> length TCB_H.msgRegisters; len = unat length___unsigned_long; n < unat length___unsigned_long; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>i = word_of_nat n\<rbrace>\<rbrakk> \<Longrightarrow> ?Q574 length___unsigned_long n s \<and> s' \<in> ?Q'574 length___unsigned_long n
 3. \<And>desta srca length___unsigned_long n. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len\<rbrakk> \<Longrightarrow> (n < length___unsigned_long) = (n < word_of_nat (length (take len TCB_H.msgRegisters)))
 4. \<And>desta srca length___unsigned_long. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len\<rbrakk> \<Longrightarrow> \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} \<acute>reg :== kernel_all_global_addresses.msgRegisters.[0] + \<acute>i;;
\<acute>ret__unsigned_long :== CALL getRegister_'proc(srca,\<acute>reg);;
CALL setRegister_'proc(desta,\<acute>reg,\<acute>ret__unsigned_long) \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>
 5. \<And>desta srca length___unsigned_long n. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len; Suc n < length (take len TCB_H.msgRegisters)\<rbrakk> \<Longrightarrow> \<lbrace>K (\<lambda>_. True) n\<rbrace> do v <- asUser src (getRegister (take len TCB_H.msgRegisters ! n));
asUser dest (setRegister (take len TCB_H.msgRegisters ! n) v)
od \<lbrace>\<lambda>_. K (\<lambda>_. True) (Suc n)\<rbrace>
 6. \<And>desta srca length___unsigned_long. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len\<rbrakk> \<Longrightarrow> length (take len TCB_H.msgRegisters) < 2 ^ word_bits
 7. \<And>desta srca length___unsigned_long x y. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len; i_' y = word_of_nat (length (take len TCB_H.msgRegisters))\<rbrakk> \<Longrightarrow> dc x (xfdc y)
 8. \<And>desta srca length___unsigned_long s s'. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> K (\<lambda>_. True) 0 s \<and> s' \<in> UNIV proof (prove)
goal (8 subgoals):
 1. \<And>length___unsigned_long n. \<lbrakk>unat length___unsigned_long \<le> length TCB_H.msgRegisters; len = unat length___unsigned_long; n < unat length___unsigned_long\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q574 length___unsigned_long n) (?Q'574 length___unsigned_long n) [SKIP] (do v <- asUser src (getRegister (TCB_H.msgRegisters ! n));
asUser dest (setRegister (TCB_H.msgRegisters ! n) v)
od) (\<acute>reg :== kernel_all_global_addresses.msgRegisters.[0] + \<acute>i;;
(\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr src);;
CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr dest,\<acute>ret__unsigned_long)))
 2. \<And>length___unsigned_long n s s'. \<lbrakk>unat length___unsigned_long \<le> length TCB_H.msgRegisters; len = unat length___unsigned_long; n < unat length___unsigned_long; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>i = word_of_nat n\<rbrace>\<rbrakk> \<Longrightarrow> ?Q574 length___unsigned_long n s \<and> s' \<in> ?Q'574 length___unsigned_long n
 3. \<And>desta srca length___unsigned_long n. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len\<rbrakk> \<Longrightarrow> (n < length___unsigned_long) = (n < word_of_nat (length (take len TCB_H.msgRegisters)))
 4. \<And>desta srca length___unsigned_long. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len\<rbrakk> \<Longrightarrow> \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} \<acute>reg :== kernel_all_global_addresses.msgRegisters.[0] + \<acute>i;;
\<acute>ret__unsigned_long :== CALL getRegister_'proc(srca,\<acute>reg);;
CALL setRegister_'proc(desta,\<acute>reg,\<acute>ret__unsigned_long) \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>
 5. \<And>desta srca length___unsigned_long n. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len; Suc n < length (take len TCB_H.msgRegisters)\<rbrakk> \<Longrightarrow> \<lbrace>K (\<lambda>_. True) n\<rbrace> do v <- asUser src (getRegister (take len TCB_H.msgRegisters ! n));
asUser dest (setRegister (take len TCB_H.msgRegisters ! n) v)
od \<lbrace>\<lambda>_. K (\<lambda>_. True) (Suc n)\<rbrace>
 6. \<And>desta srca length___unsigned_long. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len\<rbrakk> \<Longrightarrow> length (take len TCB_H.msgRegisters) < 2 ^ word_bits
 7. \<And>desta srca length___unsigned_long x y. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len; i_' y = word_of_nat (length (take len TCB_H.msgRegisters))\<rbrakk> \<Longrightarrow> dc x (xfdc y)
 8. \<And>desta srca length___unsigned_long s s'. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> K (\<lambda>_. True) 0 s \<and> s' \<in> UNIV proof (prove)
goal (8 subgoals):
 1. \<And>length___unsigned_long n rv'. \<lbrakk>unat length___unsigned_long \<le> length TCB_H.msgRegisters; len = unat length___unsigned_long; n < unat length___unsigned_long\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q574 length___unsigned_long n) (?G'579 length___unsigned_long n rv') [SKIP] (do v <- asUser src (getRegister (TCB_H.msgRegisters ! n));
asUser dest (setRegister (TCB_H.msgRegisters ! n) v)
od) (\<acute>reg :== kernel_all_global_addresses.msgRegisters.[0] + rv';;
(\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr src,\<acute>reg);;
CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr dest,\<acute>ret__unsigned_long,\<acute>reg)))
 2. \<And>length___unsigned_long n s s'. \<lbrakk>unat length___unsigned_long \<le> length TCB_H.msgRegisters; len = unat length___unsigned_long; n < unat length___unsigned_long; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>i = word_of_nat n\<rbrace>\<rbrakk> \<Longrightarrow> ?Q574 length___unsigned_long n s \<and> s' \<in> {s. s \<in> ?G'579 length___unsigned_long n (i_' s)}
 3. \<And>desta srca length___unsigned_long n. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len\<rbrakk> \<Longrightarrow> (n < length___unsigned_long) = (n < word_of_nat (length (take len TCB_H.msgRegisters)))
 4. \<And>desta srca length___unsigned_long. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len\<rbrakk> \<Longrightarrow> \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} \<acute>reg :== kernel_all_global_addresses.msgRegisters.[0] + \<acute>i;;
\<acute>ret__unsigned_long :== CALL getRegister_'proc(srca,\<acute>reg);;
CALL setRegister_'proc(desta,\<acute>reg,\<acute>ret__unsigned_long) \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>
 5. \<And>desta srca length___unsigned_long n. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len; Suc n < length (take len TCB_H.msgRegisters)\<rbrakk> \<Longrightarrow> \<lbrace>K (\<lambda>_. True) n\<rbrace> do v <- asUser src (getRegister (take len TCB_H.msgRegisters ! n));
asUser dest (setRegister (take len TCB_H.msgRegisters ! n) v)
od \<lbrace>\<lambda>_. K (\<lambda>_. True) (Suc n)\<rbrace>
 6. \<And>desta srca length___unsigned_long. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len\<rbrakk> \<Longrightarrow> length (take len TCB_H.msgRegisters) < 2 ^ word_bits
 7. \<And>desta srca length___unsigned_long x y. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len; i_' y = word_of_nat (length (take len TCB_H.msgRegisters))\<rbrakk> \<Longrightarrow> dc x (xfdc y)
 8. \<And>desta srca length___unsigned_long s s'. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> K (\<lambda>_. True) 0 s \<and> s' \<in> UNIV proof (prove)
goal (8 subgoals):
 1. \<And>length___unsigned_long n rv'. \<lbrakk>unat length___unsigned_long \<le> length TCB_H.msgRegisters; len = unat length___unsigned_long; n < unat length___unsigned_long\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q574 length___unsigned_long n) (?G'652 length___unsigned_long n rv') [SKIP] (do v <- asUser src (getRegister (TCB_H.msgRegisters ! n));
asUser dest (setRegister (TCB_H.msgRegisters ! n) v)
od) (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr src,kernel_all_global_addresses.msgRegisters.[0] + rv');;
CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr dest,\<acute>ret__unsigned_long,kernel_all_global_addresses.msgRegisters.[0] + rv'))
 2. \<And>length___unsigned_long n s s'. \<lbrakk>unat length___unsigned_long \<le> length TCB_H.msgRegisters; len = unat length___unsigned_long; n < unat length___unsigned_long; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>i = word_of_nat n\<rbrace>\<rbrakk> \<Longrightarrow> ?Q574 length___unsigned_long n s \<and> s' \<in> {s. s \<in> {sa. reg_'_update (\<lambda>_. kernel_all_global_addresses.msgRegisters.[0] + i_' s) sa \<in> ?G'652 length___unsigned_long n (i_' s)}}
 3. \<And>desta srca length___unsigned_long n. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len\<rbrakk> \<Longrightarrow> (n < length___unsigned_long) = (n < word_of_nat (length (take len TCB_H.msgRegisters)))
 4. \<And>desta srca length___unsigned_long. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len\<rbrakk> \<Longrightarrow> \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} \<acute>reg :== kernel_all_global_addresses.msgRegisters.[0] + \<acute>i;;
\<acute>ret__unsigned_long :== CALL getRegister_'proc(srca,\<acute>reg);;
CALL setRegister_'proc(desta,\<acute>reg,\<acute>ret__unsigned_long) \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>
 5. \<And>desta srca length___unsigned_long n. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len; Suc n < length (take len TCB_H.msgRegisters)\<rbrakk> \<Longrightarrow> \<lbrace>K (\<lambda>_. True) n\<rbrace> do v <- asUser src (getRegister (take len TCB_H.msgRegisters ! n));
asUser dest (setRegister (take len TCB_H.msgRegisters ! n) v)
od \<lbrace>\<lambda>_. K (\<lambda>_. True) (Suc n)\<rbrace>
 6. \<And>desta srca length___unsigned_long. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len\<rbrakk> \<Longrightarrow> length (take len TCB_H.msgRegisters) < 2 ^ word_bits
 7. \<And>desta srca length___unsigned_long x y. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len; i_' y = word_of_nat (length (take len TCB_H.msgRegisters))\<rbrakk> \<Longrightarrow> dc x (xfdc y)
 8. \<And>desta srca length___unsigned_long s s'. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> K (\<lambda>_. True) 0 s \<and> s' \<in> UNIV proof (prove)
goal (9 subgoals):
 1. \<And>length___unsigned_long n rv' rv ret__unsigned_long. \<lbrakk>unat length___unsigned_long \<le> length TCB_H.msgRegisters; len = unat length___unsigned_long; n < unat length___unsigned_long; rv = ret__unsigned_long\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q714 length___unsigned_long n rv' rv) (?Q'714 length___unsigned_long n rv' rv ret__unsigned_long) [SKIP] (asUser dest (setRegister (TCB_H.msgRegisters ! n) rv)) (CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr dest,ret__unsigned_long,kernel_all_global_addresses.msgRegisters.[0] + rv'))
 2. \<And>length___unsigned_long n rv'. \<lbrakk>unat length___unsigned_long \<le> length TCB_H.msgRegisters; len = unat length___unsigned_long; n < unat length___unsigned_long\<rbrakk> \<Longrightarrow> \<lbrace>?R716 length___unsigned_long n\<rbrace> asUser src (getRegister (TCB_H.msgRegisters ! n)) \<lbrace>?Q714 length___unsigned_long n rv'\<rbrace>
 3. \<And>length___unsigned_long n s s'. \<lbrakk>unat length___unsigned_long \<le> length TCB_H.msgRegisters; len = unat length___unsigned_long; n < unat length___unsigned_long; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>i = word_of_nat n\<rbrace>\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R716 length___unsigned_long n) s \<and> s' \<in> {s. s \<in> {sa. reg_'_update (\<lambda>_. kernel_all_global_addresses.msgRegisters.[0] + i_' s) sa \<in> {sa. reg_'_update (\<lambda>x. kernel_all_global_addresses.msgRegisters.[0] + i_' s) (thread_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr src) sa) \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr src\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H (TCB_H.msgRegisters ! n)\<rbrace>} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> s'\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> ?Q'714 length___unsigned_long n (i_' s) rv (ret__unsigned_long_' t)}}}
 4. \<And>desta srca length___unsigned_long n. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len\<rbrakk> \<Longrightarrow> (n < length___unsigned_long) = (n < word_of_nat (length (take len TCB_H.msgRegisters)))
 5. \<And>desta srca length___unsigned_long. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len\<rbrakk> \<Longrightarrow> \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} \<acute>reg :== kernel_all_global_addresses.msgRegisters.[0] + \<acute>i;;
\<acute>ret__unsigned_long :== CALL getRegister_'proc(srca,\<acute>reg);;
CALL setRegister_'proc(desta,\<acute>reg,\<acute>ret__unsigned_long) \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>
 6. \<And>desta srca length___unsigned_long n. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len; Suc n < length (take len TCB_H.msgRegisters)\<rbrakk> \<Longrightarrow> \<lbrace>K (\<lambda>_. True) n\<rbrace> do v <- asUser src (getRegister (take len TCB_H.msgRegisters ! n));
asUser dest (setRegister (take len TCB_H.msgRegisters ! n) v)
od \<lbrace>\<lambda>_. K (\<lambda>_. True) (Suc n)\<rbrace>
 7. \<And>desta srca length___unsigned_long. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len\<rbrakk> \<Longrightarrow> length (take len TCB_H.msgRegisters) < 2 ^ word_bits
 8. \<And>desta srca length___unsigned_long x y. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len; i_' y = word_of_nat (length (take len TCB_H.msgRegisters))\<rbrakk> \<Longrightarrow> dc x (xfdc y)
 9. \<And>desta srca length___unsigned_long s s'. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> K (\<lambda>_. True) 0 s \<and> s' \<in> UNIV proof (prove)
goal (8 subgoals):
 1. \<And>length___unsigned_long n rv'. \<lbrakk>unat length___unsigned_long \<le> length TCB_H.msgRegisters; len = unat length___unsigned_long; n < unat length___unsigned_long\<rbrakk> \<Longrightarrow> \<lbrace>?R716 length___unsigned_long n\<rbrace> asUser src (getRegister (TCB_H.msgRegisters ! n)) \<lbrace>\<lambda>rv _. True\<rbrace>
 2. \<And>length___unsigned_long n s s'. \<lbrakk>unat length___unsigned_long \<le> length TCB_H.msgRegisters; len = unat length___unsigned_long; n < unat length___unsigned_long; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>i = word_of_nat n\<rbrace>\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R716 length___unsigned_long n) s \<and> s' \<in> {s. s \<in> {sa. reg_'_update (\<lambda>_. kernel_all_global_addresses.msgRegisters.[0] + i_' s) sa \<in> {sa. reg_'_update (\<lambda>x. kernel_all_global_addresses.msgRegisters.[0] + i_' s) (thread_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr src) sa) \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr src\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H (TCB_H.msgRegisters ! n)\<rbrace>} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> s'\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> {sa. reg_'_update (\<lambda>x. kernel_all_global_addresses.msgRegisters.[0] + i_' s) (w_'_update (\<lambda>_. ret__unsigned_long_' t) (thread_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr dest) sa)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr dest\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H (TCB_H.msgRegisters ! n)\<rbrace> \<inter> \<lbrace>\<acute>w = rv\<rbrace>}}}}
 3. \<And>desta srca length___unsigned_long n. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len\<rbrakk> \<Longrightarrow> (n < length___unsigned_long) = (n < word_of_nat (length (take len TCB_H.msgRegisters)))
 4. \<And>desta srca length___unsigned_long. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len\<rbrakk> \<Longrightarrow> \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} \<acute>reg :== kernel_all_global_addresses.msgRegisters.[0] + \<acute>i;;
\<acute>ret__unsigned_long :== CALL getRegister_'proc(srca,\<acute>reg);;
CALL setRegister_'proc(desta,\<acute>reg,\<acute>ret__unsigned_long) \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>
 5. \<And>desta srca length___unsigned_long n. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len; Suc n < length (take len TCB_H.msgRegisters)\<rbrakk> \<Longrightarrow> \<lbrace>K (\<lambda>_. True) n\<rbrace> do v <- asUser src (getRegister (take len TCB_H.msgRegisters ! n));
asUser dest (setRegister (take len TCB_H.msgRegisters ! n) v)
od \<lbrace>\<lambda>_. K (\<lambda>_. True) (Suc n)\<rbrace>
 6. \<And>desta srca length___unsigned_long. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len\<rbrakk> \<Longrightarrow> length (take len TCB_H.msgRegisters) < 2 ^ word_bits
 7. \<And>desta srca length___unsigned_long x y. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len; i_' y = word_of_nat (length (take len TCB_H.msgRegisters))\<rbrakk> \<Longrightarrow> dc x (xfdc y)
 8. \<And>desta srca length___unsigned_long s s'. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> K (\<lambda>_. True) 0 s \<and> s' \<in> UNIV proof (prove)
goal (7 subgoals):
 1. \<And>length___unsigned_long n s s'. \<lbrakk>unat length___unsigned_long \<le> length TCB_H.msgRegisters; len = unat length___unsigned_long; n < unat length___unsigned_long; (s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>i = word_of_nat n\<rbrace>\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True)) s \<and> s' \<in> {s. s \<in> {sa. reg_'_update (\<lambda>_. kernel_all_global_addresses.msgRegisters.[0] + i_' s) sa \<in> {sa. reg_'_update (\<lambda>x. kernel_all_global_addresses.msgRegisters.[0] + i_' s) (thread_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr src) sa) \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr src\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H (TCB_H.msgRegisters ! n)\<rbrace>} \<inter> {s'. \<forall>t rv. rv = ret__unsigned_long_' t \<longrightarrow> s'\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> {sa. reg_'_update (\<lambda>x. kernel_all_global_addresses.msgRegisters.[0] + i_' s) (w_'_update (\<lambda>_. ret__unsigned_long_' t) (thread_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr dest) sa)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr dest\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H (TCB_H.msgRegisters ! n)\<rbrace> \<inter> \<lbrace>\<acute>w = rv\<rbrace>}}}}
 2. \<And>desta srca length___unsigned_long n. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len\<rbrakk> \<Longrightarrow> (n < length___unsigned_long) = (n < word_of_nat (length (take len TCB_H.msgRegisters)))
 3. \<And>desta srca length___unsigned_long. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len\<rbrakk> \<Longrightarrow> \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} \<acute>reg :== kernel_all_global_addresses.msgRegisters.[0] + \<acute>i;;
\<acute>ret__unsigned_long :== CALL getRegister_'proc(srca,\<acute>reg);;
CALL setRegister_'proc(desta,\<acute>reg,\<acute>ret__unsigned_long) \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>
 4. \<And>desta srca length___unsigned_long n. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len; Suc n < length (take len TCB_H.msgRegisters)\<rbrakk> \<Longrightarrow> \<lbrace>K (\<lambda>_. True) n\<rbrace> do v <- asUser src (getRegister (take len TCB_H.msgRegisters ! n));
asUser dest (setRegister (take len TCB_H.msgRegisters ! n) v)
od \<lbrace>\<lambda>_. K (\<lambda>_. True) (Suc n)\<rbrace>
 5. \<And>desta srca length___unsigned_long. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len\<rbrakk> \<Longrightarrow> length (take len TCB_H.msgRegisters) < 2 ^ word_bits
 6. \<And>desta srca length___unsigned_long x y. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len; i_' y = word_of_nat (length (take len TCB_H.msgRegisters))\<rbrakk> \<Longrightarrow> dc x (xfdc y)
 7. \<And>desta srca length___unsigned_long s s'. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> K (\<lambda>_. True) 0 s \<and> s' \<in> UNIV proof (prove)
goal (7 subgoals):
 1. \<And>length___unsigned_long n s s'. \<lbrakk>unat length___unsigned_long \<le> length TCB_H.msgRegisters; len = unat length___unsigned_long; n < unat length___unsigned_long; (s, s') \<in> rf_sr; i_' s' = word_of_nat n\<rbrakk> \<Longrightarrow> kernel_all_global_addresses.msgRegisters.[0] + word_of_nat n = register_from_H (TCB_H.msgRegisters ! n)
 2. \<And>desta srca length___unsigned_long n. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len\<rbrakk> \<Longrightarrow> (n < length___unsigned_long) = (n < word_of_nat (length (take len TCB_H.msgRegisters)))
 3. \<And>desta srca length___unsigned_long. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len\<rbrakk> \<Longrightarrow> \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} \<acute>reg :== kernel_all_global_addresses.msgRegisters.[0] + \<acute>i;;
\<acute>ret__unsigned_long :== CALL getRegister_'proc(srca,\<acute>reg);;
CALL setRegister_'proc(desta,\<acute>reg,\<acute>ret__unsigned_long) \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>
 4. \<And>desta srca length___unsigned_long n. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len; Suc n < length (take len TCB_H.msgRegisters)\<rbrakk> \<Longrightarrow> \<lbrace>K (\<lambda>_. True) n\<rbrace> do v <- asUser src (getRegister (take len TCB_H.msgRegisters ! n));
asUser dest (setRegister (take len TCB_H.msgRegisters ! n) v)
od \<lbrace>\<lambda>_. K (\<lambda>_. True) (Suc n)\<rbrace>
 5. \<And>desta srca length___unsigned_long. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len\<rbrakk> \<Longrightarrow> length (take len TCB_H.msgRegisters) < 2 ^ word_bits
 6. \<And>desta srca length___unsigned_long x y. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len; i_' y = word_of_nat (length (take len TCB_H.msgRegisters))\<rbrakk> \<Longrightarrow> dc x (xfdc y)
 7. \<And>desta srca length___unsigned_long s s'. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> K (\<lambda>_. True) 0 s \<and> s' \<in> UNIV proof (prove)
goal (7 subgoals):
 1. \<And>length___unsigned_long n s s'. \<lbrakk>unat length___unsigned_long \<le> unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters); len = unat length___unsigned_long; n < unat length___unsigned_long; (s, s') \<in> rf_sr; i_' s' = word_of_nat n\<rbrakk> \<Longrightarrow> kernel_all_global_addresses.msgRegisters.[0] + word_of_nat n = register_from_H (TCB_H.msgRegisters ! n)
 2. \<And>desta srca length___unsigned_long n. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len\<rbrakk> \<Longrightarrow> (n < length___unsigned_long) = (n < word_of_nat (length (take len TCB_H.msgRegisters)))
 3. \<And>desta srca length___unsigned_long. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len\<rbrakk> \<Longrightarrow> \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} \<acute>reg :== kernel_all_global_addresses.msgRegisters.[0] + \<acute>i;;
\<acute>ret__unsigned_long :== CALL getRegister_'proc(srca,\<acute>reg);;
CALL setRegister_'proc(desta,\<acute>reg,\<acute>ret__unsigned_long) \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>
 4. \<And>desta srca length___unsigned_long n. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len; Suc n < length (take len TCB_H.msgRegisters)\<rbrakk> \<Longrightarrow> \<lbrace>K (\<lambda>_. True) n\<rbrace> do v <- asUser src (getRegister (take len TCB_H.msgRegisters ! n));
asUser dest (setRegister (take len TCB_H.msgRegisters ! n) v)
od \<lbrace>\<lambda>_. K (\<lambda>_. True) (Suc n)\<rbrace>
 5. \<And>desta srca length___unsigned_long. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len\<rbrakk> \<Longrightarrow> length (take len TCB_H.msgRegisters) < 2 ^ word_bits
 6. \<And>desta srca length___unsigned_long x y. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len; i_' y = word_of_nat (length (take len TCB_H.msgRegisters))\<rbrakk> \<Longrightarrow> dc x (xfdc y)
 7. \<And>desta srca length___unsigned_long s s'. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> K (\<lambda>_. True) 0 s \<and> s' \<in> UNIV proof (prove)
goal (7 subgoals):
 1. \<And>length___unsigned_long n s s'. \<lbrakk>unat length___unsigned_long \<le> 4; len = unat length___unsigned_long; n < unat length___unsigned_long; (s, s') \<in> rf_sr; i_' s' = word_of_nat n\<rbrakk> \<Longrightarrow> kernel_all_global_addresses.msgRegisters.[0] + word_of_nat n = register_from_H ([register.R2, register.R3, register.R4, register.R5] ! n)
 2. \<And>desta srca length___unsigned_long n. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len\<rbrakk> \<Longrightarrow> (n < length___unsigned_long) = (n < word_of_nat (length (take len TCB_H.msgRegisters)))
 3. \<And>desta srca length___unsigned_long. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len\<rbrakk> \<Longrightarrow> \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} \<acute>reg :== kernel_all_global_addresses.msgRegisters.[0] + \<acute>i;;
\<acute>ret__unsigned_long :== CALL getRegister_'proc(srca,\<acute>reg);;
CALL setRegister_'proc(desta,\<acute>reg,\<acute>ret__unsigned_long) \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>
 4. \<And>desta srca length___unsigned_long n. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len; Suc n < length (take len TCB_H.msgRegisters)\<rbrakk> \<Longrightarrow> \<lbrace>K (\<lambda>_. True) n\<rbrace> do v <- asUser src (getRegister (take len TCB_H.msgRegisters ! n));
asUser dest (setRegister (take len TCB_H.msgRegisters ! n) v)
od \<lbrace>\<lambda>_. K (\<lambda>_. True) (Suc n)\<rbrace>
 5. \<And>desta srca length___unsigned_long. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len\<rbrakk> \<Longrightarrow> length (take len TCB_H.msgRegisters) < 2 ^ word_bits
 6. \<And>desta srca length___unsigned_long x y. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len; i_' y = word_of_nat (length (take len TCB_H.msgRegisters))\<rbrakk> \<Longrightarrow> dc x (xfdc y)
 7. \<And>desta srca length___unsigned_long s s'. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> K (\<lambda>_. True) 0 s \<and> s' \<in> UNIV proof (prove)
goal (7 subgoals):
 1. \<And>length___unsigned_long n s s'. \<lbrakk>unat length___unsigned_long \<le> 4; len = unat length___unsigned_long; (s, s') \<in> rf_sr; i_' s' = word_of_nat n; n < 4\<rbrakk> \<Longrightarrow> kernel_all_global_addresses.msgRegisters.[0] + word_of_nat n = register_from_H ([register.R2, register.R3, register.R4, register.R5] ! n)
 2. \<And>desta srca length___unsigned_long n. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len\<rbrakk> \<Longrightarrow> (n < length___unsigned_long) = (n < word_of_nat (length (take len TCB_H.msgRegisters)))
 3. \<And>desta srca length___unsigned_long. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len\<rbrakk> \<Longrightarrow> \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} \<acute>reg :== kernel_all_global_addresses.msgRegisters.[0] + \<acute>i;;
\<acute>ret__unsigned_long :== CALL getRegister_'proc(srca,\<acute>reg);;
CALL setRegister_'proc(desta,\<acute>reg,\<acute>ret__unsigned_long) \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>
 4. \<And>desta srca length___unsigned_long n. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len; Suc n < length (take len TCB_H.msgRegisters)\<rbrakk> \<Longrightarrow> \<lbrace>K (\<lambda>_. True) n\<rbrace> do v <- asUser src (getRegister (take len TCB_H.msgRegisters ! n));
asUser dest (setRegister (take len TCB_H.msgRegisters ! n) v)
od \<lbrace>\<lambda>_. K (\<lambda>_. True) (Suc n)\<rbrace>
 5. \<And>desta srca length___unsigned_long. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len\<rbrakk> \<Longrightarrow> length (take len TCB_H.msgRegisters) < 2 ^ word_bits
 6. \<And>desta srca length___unsigned_long x y. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len; i_' y = word_of_nat (length (take len TCB_H.msgRegisters))\<rbrakk> \<Longrightarrow> dc x (xfdc y)
 7. \<And>desta srca length___unsigned_long s s'. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> K (\<lambda>_. True) 0 s \<and> s' \<in> UNIV proof (prove)
goal (5 subgoals):
 1. \<And>desta srca length___unsigned_long. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len\<rbrakk> \<Longrightarrow> \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} \<acute>reg :== kernel_all_global_addresses.msgRegisters.[0] + \<acute>i;;
\<acute>ret__unsigned_long :== CALL getRegister_'proc(srca,\<acute>reg);;
CALL setRegister_'proc(desta,\<acute>reg,\<acute>ret__unsigned_long) \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>
 2. \<And>desta srca length___unsigned_long n. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len; Suc n < length (take len TCB_H.msgRegisters)\<rbrakk> \<Longrightarrow> \<lbrace>K (\<lambda>_. True) n\<rbrace> do v <- asUser src (getRegister (take len TCB_H.msgRegisters ! n));
asUser dest (setRegister (take len TCB_H.msgRegisters ! n) v)
od \<lbrace>\<lambda>_. K (\<lambda>_. True) (Suc n)\<rbrace>
 3. \<And>desta srca length___unsigned_long. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len\<rbrakk> \<Longrightarrow> length (take len TCB_H.msgRegisters) < 2 ^ word_bits
 4. \<And>desta srca length___unsigned_long x y. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len; i_' y = word_of_nat (length (take len TCB_H.msgRegisters))\<rbrakk> \<Longrightarrow> dc x (xfdc y)
 5. \<And>desta srca length___unsigned_long s s'. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> K (\<lambda>_. True) 0 s \<and> s' \<in> UNIV proof (prove)
goal (5 subgoals):
 1. \<And>desta srca length___unsigned_long s. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len\<rbrakk> \<Longrightarrow> {s} \<subseteq> {sa. kernel_all_global_addresses.msgRegisters.[0] + i_' sa < SCAST(32 signed \<rightarrow> 32) 0x14 \<longrightarrow> sa \<Turnstile>\<^sub>c srca \<longrightarrow> kernel_all_global_addresses.msgRegisters.[0] + i_' sa < SCAST(32 signed \<rightarrow> 32) 0x14 \<longrightarrow> sa \<Turnstile>\<^sub>c desta \<longrightarrow> i_' sa = i_' s}
 2. \<And>desta srca length___unsigned_long n. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len; Suc n < length (take len TCB_H.msgRegisters)\<rbrakk> \<Longrightarrow> \<lbrace>K (\<lambda>_. True) n\<rbrace> do v <- asUser src (getRegister (take len TCB_H.msgRegisters ! n));
asUser dest (setRegister (take len TCB_H.msgRegisters ! n) v)
od \<lbrace>\<lambda>_. K (\<lambda>_. True) (Suc n)\<rbrace>
 3. \<And>desta srca length___unsigned_long. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len\<rbrakk> \<Longrightarrow> length (take len TCB_H.msgRegisters) < 2 ^ word_bits
 4. \<And>desta srca length___unsigned_long x y. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len; i_' y = word_of_nat (length (take len TCB_H.msgRegisters))\<rbrakk> \<Longrightarrow> dc x (xfdc y)
 5. \<And>desta srca length___unsigned_long s s'. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> K (\<lambda>_. True) 0 s \<and> s' \<in> UNIV proof (prove)
goal (4 subgoals):
 1. \<And>desta srca length___unsigned_long n. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len; Suc n < length (take len TCB_H.msgRegisters)\<rbrakk> \<Longrightarrow> \<lbrace>K (\<lambda>_. True) n\<rbrace> do v <- asUser src (getRegister (take len TCB_H.msgRegisters ! n));
asUser dest (setRegister (take len TCB_H.msgRegisters ! n) v)
od \<lbrace>\<lambda>_. K (\<lambda>_. True) (Suc n)\<rbrace>
 2. \<And>desta srca length___unsigned_long. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len\<rbrakk> \<Longrightarrow> length (take len TCB_H.msgRegisters) < 2 ^ word_bits
 3. \<And>desta srca length___unsigned_long x y. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len; i_' y = word_of_nat (length (take len TCB_H.msgRegisters))\<rbrakk> \<Longrightarrow> dc x (xfdc y)
 4. \<And>desta srca length___unsigned_long s s'. \<lbrakk>len \<le> length TCB_H.msgRegisters; desta = tcb_ptr_to_ctcb_ptr dest; srca = tcb_ptr_to_ctcb_ptr src; unat length___unsigned_long = len; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> K (\<lambda>_. True) 0 s \<and> s' \<in> UNIV proof (prove)
goal:
No subgoals!