theory TcbAcc_AI

lemma set_mrs_thread_set_dmo:
  assumes ts: "\<And>c. \<lbrace>P\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_set_registers (c tcb) (tcb_arch tcb)\<rparr>) r \<lbrace>\<lambda>rv. Q\<rbrace>"
  assumes dmo: "\<And>x y. \<lbrace>Q\<rbrace> do_machine_op (storeWord x y) \<lbrace>\<lambda>rv. Q\<rbrace>"
  shows "\<lbrace>P\<rbrace> set_mrs r t mrs \<lbrace>\<lambda>rv. Q\<rbrace>" apply (simp add: set_mrs_redux) apply (case_tac t) apply simp apply (wp ts) apply (simp add: zipWithM_x_mapM store_word_offs_def split_def
              split del: if_split) apply (wpsimp wp: ts mapM_wp' dmo) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> set_mrs r t mrs \<lbrace>\<lambda>rv. Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> do y <- thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>reg. if reg \<in> set (take (length mrs) msg_registers) then mrs ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch tcb) reg) (tcb_arch tcb)\<rparr>) r;
case t of None \<Rightarrow> return $ nat_to_len (min (length msg_registers) (length mrs)) | Some pptr \<Rightarrow> do zipWithM_x (store_word_offs pptr) [length msg_registers + 1..<Suc msg_max_length] (drop (length msg_registers) mrs);
return $ nat_to_len $ min (length mrs) msg_max_length
od
od \<lbrace>\<lambda>rv. Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. t = None \<Longrightarrow> \<lbrace>P\<rbrace> do y <- thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>reg. if reg \<in> set (take (length mrs) msg_registers) then mrs ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch tcb) reg) (tcb_arch tcb)\<rparr>) r;
case t of None \<Rightarrow> return $ nat_to_len (min (length msg_registers) (length mrs)) | Some pptr \<Rightarrow> do zipWithM_x (store_word_offs pptr) [length msg_registers + 1..<Suc msg_max_length] (drop (length msg_registers) mrs);
return $ nat_to_len $ min (length mrs) msg_max_length
od
od \<lbrace>\<lambda>rv. Q\<rbrace>
 2. \<And>a. t = Some a \<Longrightarrow> \<lbrace>P\<rbrace> do y <- thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>reg. if reg \<in> set (take (length mrs) msg_registers) then mrs ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch tcb) reg) (tcb_arch tcb)\<rparr>) r;
case t of None \<Rightarrow> return $ nat_to_len (min (length msg_registers) (length mrs)) | Some pptr \<Rightarrow> do zipWithM_x (store_word_offs pptr) [length msg_registers + 1..<Suc msg_max_length] (drop (length msg_registers) mrs);
return $ nat_to_len $ min (length mrs) msg_max_length
od
od \<lbrace>\<lambda>rv. Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. t = None \<Longrightarrow> \<lbrace>P\<rbrace> do y <- thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>reg. if reg \<in> set (take (length mrs) msg_registers) then mrs ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch tcb) reg) (tcb_arch tcb)\<rparr>) r;
return (nat_to_len (min (length msg_registers) (length mrs)))
od \<lbrace>\<lambda>rv. Q\<rbrace>
 2. \<And>a. t = Some a \<Longrightarrow> \<lbrace>P\<rbrace> do y <- thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>reg. if reg \<in> set (take (length mrs) msg_registers) then mrs ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch tcb) reg) (tcb_arch tcb)\<rparr>) r;
case t of None \<Rightarrow> return $ nat_to_len (min (length msg_registers) (length mrs)) | Some pptr \<Rightarrow> do zipWithM_x (store_word_offs pptr) [length msg_registers + 1..<Suc msg_max_length] (drop (length msg_registers) mrs);
return $ nat_to_len $ min (length mrs) msg_max_length
od
od \<lbrace>\<lambda>rv. Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a. t = Some a \<Longrightarrow> \<lbrace>P\<rbrace> do y <- thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>reg. if reg \<in> set (take (length mrs) msg_registers) then mrs ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch tcb) reg) (tcb_arch tcb)\<rparr>) r;
case t of None \<Rightarrow> return $ nat_to_len (min (length msg_registers) (length mrs)) | Some pptr \<Rightarrow> do zipWithM_x (store_word_offs pptr) [length msg_registers + 1..<Suc msg_max_length] (drop (length msg_registers) mrs);
return $ nat_to_len $ min (length mrs) msg_max_length
od
od \<lbrace>\<lambda>rv. Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a. t = Some a \<Longrightarrow> \<lbrace>P\<rbrace> do y <- thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>reg. if reg \<in> set (take (length mrs) msg_registers) then mrs ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch tcb) reg) (tcb_arch tcb)\<rparr>) r;
_ <- mapM (\<lambda>p. do s <- get;
y <- assert (in_user_frame (a + word_of_nat (fst p) * word_of_nat word_size) s);
do_machine_op (storeWord (a + word_of_nat (fst p) * word_of_nat word_size) (snd p))
od) (zip (if Suc (length msg_registers) \<le> msg_max_length then [Suc (length msg_registers)..<msg_max_length] @ [msg_max_length] else []) (drop (length msg_registers) mrs));
return (nat_to_len (min (length mrs) msg_max_length))
od \<lbrace>\<lambda>rv. Q\<rbrace> proof (prove)
goal:
No subgoals!