theory Ipc_C

lemma copyMRs_register_loop_helper:
  fixes n
  defines regs: "regs \<equiv> take (unat n) ARM_H.msgRegisters"
  shows
  "\<forall>i. i<length regs \<longrightarrow>
   ccorres dc xfdc \<top> \<lbrace>\<acute>i = of_nat i\<rbrace> hs
     (do v \<leftarrow> asUser sender (getRegister (regs ! i));
         asUser receiver (setRegister (regs ! i) v)
      od)
     (Guard ArrayBounds \<lbrace>\<acute>i < 4\<rbrace>
      (\<acute>ret__unsigned_long :== CALL getRegister(tcb_ptr_to_ctcb_ptr sender,
               ucast (index msgRegistersC (unat \<acute>i))));;
      Guard ArrayBounds \<lbrace>\<acute>i < 4\<rbrace>
      (CALL setRegister(tcb_ptr_to_ctcb_ptr receiver,
               ucast (index msgRegistersC (unat \<acute>i)),
               \<acute>ret__unsigned_long)))" apply clarsimp apply (rule ccorres_guard_imp) apply ctac apply ctac apply wp apply vcg apply simp apply (clarsimp simp: regs msgRegistersC_def msgRegisters_unfold) apply (simp |
         (case_tac i,
          clarsimp simp: fupdate_def Kernel_C.R2_def
                         Kernel_C.R3_def Kernel_C.R4_def Kernel_C.R5_def
                         Kernel_C.R6_def Kernel_C.R7_def,
          rename_tac i))+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>i<length regs. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>i = word_of_nat i\<rbrace> hs (do v <- asUser sender (getRegister (regs ! i));
asUser receiver (setRegister (regs ! i) v)
od) (Guard ArrayBounds \<lbrace>\<acute>i < 4\<rbrace> (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,UCAST(32 \<rightarrow> 32) (kernel_all_global_addresses.msgRegisters.[unat \<acute>i])));;
Guard ArrayBounds \<lbrace>\<acute>i < 4\<rbrace> (CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr receiver,UCAST(32 \<rightarrow> 32) (kernel_all_global_addresses.msgRegisters.[unat \<acute>i]),\<acute>ret__unsigned_long))) proof (prove)
goal (1 subgoal):
 1. \<And>i. i < length regs \<Longrightarrow> ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>i = word_of_nat i\<rbrace> hs (do v <- asUser sender (getRegister (regs ! i));
asUser receiver (setRegister (regs ! i) v)
od) (Guard ArrayBounds \<lbrace>\<acute>i < 4\<rbrace> (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,kernel_all_global_addresses.msgRegisters.[unat \<acute>i]));;
Guard ArrayBounds \<lbrace>\<acute>i < 4\<rbrace> (CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr receiver,kernel_all_global_addresses.msgRegisters.[unat \<acute>i],\<acute>ret__unsigned_long))) proof (prove)
goal (3 subgoals):
 1. \<And>i. i < length regs \<Longrightarrow> ccorres dc xfdc (?Q10 i) (?Q'10 i) hs (do v <- asUser sender (getRegister (regs ! i));
asUser receiver (setRegister (regs ! i) v)
od) (Guard ArrayBounds \<lbrace>\<acute>i < 4\<rbrace> (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,kernel_all_global_addresses.msgRegisters.[unat \<acute>i]));;
Guard ArrayBounds \<lbrace>\<acute>i < 4\<rbrace> (CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr receiver,kernel_all_global_addresses.msgRegisters.[unat \<acute>i],\<acute>ret__unsigned_long)))
 2. \<And>i s. \<lbrakk>i < length regs; True\<rbrakk> \<Longrightarrow> ?Q10 i s
 3. \<And>i s. \<lbrakk>i < length regs; s \<in> \<lbrace>\<acute>i = word_of_nat i\<rbrace>\<rbrakk> \<Longrightarrow> s \<in> ?Q'10 i proof (prove)
goal (5 subgoals):
 1. \<And>i rv ret__unsigned_long. \<lbrakk>i < length regs; rv = ret__unsigned_long\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q17 i rv) (?Q'17 i rv ret__unsigned_long) hs (asUser receiver (setRegister (regs ! i) rv)) (Guard ArrayBounds \<lbrace>\<acute>i < 4\<rbrace> (CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr receiver,kernel_all_global_addresses.msgRegisters.[unat \<acute>i],ret__unsigned_long)))
 2. \<And>i. i < length regs \<Longrightarrow> \<lbrace>?R17 i\<rbrace> asUser sender (getRegister (regs ! i)) \<lbrace>?Q17 i\<rbrace>
 3. \<And>i. i < length regs \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'17 i) \<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,kernel_all_global_addresses.msgRegisters.[unat \<acute>i]) {s. \<forall>rv. rv = ret__unsigned_long_' s \<longrightarrow> s \<in> ?Q'17 i rv (ret__unsigned_long_' s)}
 4. \<And>i s. \<lbrakk>i < length regs; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R17 i) s
 5. \<And>i s. \<lbrakk>i < length regs; s \<in> \<lbrace>\<acute>i = word_of_nat i\<rbrace>\<rbrakk> \<Longrightarrow> s \<in> {s. reg_'_update (\<lambda>_. kernel_all_global_addresses.msgRegisters.[unat (i_' s)]) (thread_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr sender) s) \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr sender\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H (regs ! i)\<rbrace>} \<inter> ?R'17 i \<inter> \<lbrace>\<acute>i < 4\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>i. i < length regs \<Longrightarrow> \<lbrace>?R17 i\<rbrace> asUser sender (getRegister (regs ! i)) \<lbrace>\<lambda>rv _. True\<rbrace>
 2. \<And>i. i < length regs \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'17 i) \<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,kernel_all_global_addresses.msgRegisters.[unat \<acute>i]) {s. \<forall>rv. rv = ret__unsigned_long_' s \<longrightarrow> s \<in> {sa. w_'_update (\<lambda>_. ret__unsigned_long_' s) (reg_'_update (\<lambda>_. kernel_all_global_addresses.msgRegisters.[unat (i_' sa)]) (thread_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr receiver) sa)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H (regs ! i)\<rbrace> \<inter> \<lbrace>\<acute>w = rv\<rbrace>} \<inter> \<lbrace>\<acute>i < 4\<rbrace>}
 3. \<And>i s. \<lbrakk>i < length regs; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R17 i) s
 4. \<And>i s. \<lbrakk>i < length regs; s \<in> \<lbrace>\<acute>i = word_of_nat i\<rbrace>\<rbrakk> \<Longrightarrow> s \<in> {s. reg_'_update (\<lambda>_. kernel_all_global_addresses.msgRegisters.[unat (i_' s)]) (thread_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr sender) s) \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr sender\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H (regs ! i)\<rbrace>} \<inter> ?R'17 i \<inter> \<lbrace>\<acute>i < 4\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>i. i < length regs \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'17 i) \<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,kernel_all_global_addresses.msgRegisters.[unat \<acute>i]) {s. \<forall>rv. rv = ret__unsigned_long_' s \<longrightarrow> s \<in> {sa. w_'_update (\<lambda>_. ret__unsigned_long_' s) (reg_'_update (\<lambda>_. kernel_all_global_addresses.msgRegisters.[unat (i_' sa)]) (thread_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr receiver) sa)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H (regs ! i)\<rbrace> \<inter> \<lbrace>\<acute>w = rv\<rbrace>} \<inter> \<lbrace>\<acute>i < 4\<rbrace>}
 2. \<And>i s. \<lbrakk>i < length regs; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True)) s
 3. \<And>i s. \<lbrakk>i < length regs; s \<in> \<lbrace>\<acute>i = word_of_nat i\<rbrace>\<rbrakk> \<Longrightarrow> s \<in> {s. reg_'_update (\<lambda>_. kernel_all_global_addresses.msgRegisters.[unat (i_' s)]) (thread_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr sender) s) \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr sender\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H (regs ! i)\<rbrace>} \<inter> ?R'17 i \<inter> \<lbrace>\<acute>i < 4\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>i s. \<lbrakk>i < length regs; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True)) s
 2. \<And>i s. \<lbrakk>i < length regs; s \<in> \<lbrace>\<acute>i = word_of_nat i\<rbrace>\<rbrakk> \<Longrightarrow> s \<in> {s. reg_'_update (\<lambda>_. kernel_all_global_addresses.msgRegisters.[unat (i_' s)]) (thread_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr sender) s) \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr sender\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H (regs ! i)\<rbrace>} \<inter> {s. kernel_all_global_addresses.msgRegisters.[unat (i_' s)] < SCAST(32 signed \<rightarrow> 32) 0x14 \<longrightarrow> s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender \<longrightarrow> kernel_all_global_addresses.msgRegisters.[unat (i_' s)] = register_from_H (regs ! i) \<and> i_' s < 4} \<inter> \<lbrace>\<acute>i < 4\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>i s. \<lbrakk>i < length regs; s \<in> \<lbrace>\<acute>i = word_of_nat i\<rbrace>\<rbrakk> \<Longrightarrow> s \<in> {s. reg_'_update (\<lambda>_. kernel_all_global_addresses.msgRegisters.[unat (i_' s)]) (thread_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr sender) s) \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr sender\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H (regs ! i)\<rbrace>} \<inter> {s. kernel_all_global_addresses.msgRegisters.[unat (i_' s)] < SCAST(32 signed \<rightarrow> 32) 0x14 \<longrightarrow> s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender \<longrightarrow> kernel_all_global_addresses.msgRegisters.[unat (i_' s)] = register_from_H (regs ! i) \<and> i_' s < 4} \<inter> \<lbrace>\<acute>i < 4\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>i s. \<lbrakk>i_' s = word_of_nat i; i < Suc (Suc (Suc (Suc 0))); i < unat n\<rbrakk> \<Longrightarrow> fupdate 3 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.R5) (fupdate 2 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.R4) (fupdate (Suc 0) (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.R3) (fupdate 0 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.R2) (ARRAY _. 0)))).[unat (word_of_nat i)] = register_from_H ([register.R2, register.R3, register.R4, register.R5] ! i) \<and> (fupdate 3 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.R5) (fupdate 2 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.R4) (fupdate (Suc 0) (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.R3) (fupdate 0 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.R2) (ARRAY _. 0)))).[unat (word_of_nat i)] < 0x14 \<longrightarrow> s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender \<longrightarrow> fupdate 3 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.R5) (fupdate 2 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.R4) (fupdate (Suc 0) (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.R3) (fupdate 0 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.R2) (ARRAY _. 0)))).[unat (word_of_nat i)] = register_from_H ([register.R2, register.R3, register.R4, register.R5] ! i) \<and> word_of_nat i < 4) \<and> word_of_nat i < 4 proof (prove)
goal:
No subgoals!