theory Ipc_DR

lemma ipc_buffer_wp_at_copy_mrs[wp]:
  "\<lbrace>ipc_buffer_wp_at buf t \<rbrace>
     copy_mrs send rva recv rv (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch obj') msg_info_register)))
   \<lbrace>\<lambda>r. ipc_buffer_wp_at buf t\<rbrace>" unfolding copy_mrs_def apply (wp|wpc)+ apply (wp mapM_wp) apply (simp add:store_word_offs_def ipc_buffer_wp_at_def) apply wp+ prefer 2 apply fastforce apply (clarsimp simp:ipc_buffer_wp_at_def) apply (rule_tac Q="\<lambda>rv. ipc_buffer_wp_at buf t" in hoare_strengthen_post) apply (wp mapM_wp) apply fastforce apply (clarsimp) apply wp apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ipc_buffer_wp_at buf t\<rbrace> copy_mrs send rva recv rv (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch obj') msg_info_register))) \<lbrace>\<lambda>r. ipc_buffer_wp_at buf t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ipc_buffer_wp_at buf t\<rbrace> do hardware_mrs <- return $ take (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch obj') msg_info_register)))) msg_registers;
mapM (\<lambda>r. do v <- as_user send $ getRegister r;
as_user recv $ setRegister r v
od) hardware_mrs;
buf_mrs <- case (rva, rv) of (None, b) \<Rightarrow> return [] | (Some sb_ptr, None) \<Rightarrow> return [] | (Some sb_ptr, Some rb_ptr) \<Rightarrow> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [length msg_registers + 1..<Suc (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch obj') msg_info_register))))];
return $ min (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch obj') msg_info_register))) $ nat_to_len $ length hardware_mrs + length buf_mrs
od \<lbrace>\<lambda>r. ipc_buffer_wp_at buf t\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>hardware_mrs x x2 x2a. \<lbrakk>rva = Some x2; rv = Some x2a\<rbrakk> \<Longrightarrow> \<lbrace>?R31 hardware_mrs x x2 x2a\<rbrace> mapM (\<lambda>x. load_word_offs x2 x >>= store_word_offs x2a x) [length msg_registers + 1..<Suc (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch obj') msg_info_register))))] \<lbrace>\<lambda>buf_mrs. ipc_buffer_wp_at buf t\<rbrace>
 2. \<And>hardware_mrs. \<lbrace>?B1 hardware_mrs\<rbrace> mapM (\<lambda>r. do v <- as_user send $ getRegister r;
as_user recv $ setRegister r v
od) hardware_mrs \<lbrace>\<lambda>x s. (rva = None \<longrightarrow> ipc_buffer_wp_at buf t s) \<and> (\<forall>xa. rva = Some xa \<longrightarrow> (rv = None \<longrightarrow> ipc_buffer_wp_at buf t s) \<and> (\<forall>xb. rv = Some xb \<longrightarrow> ?R31 hardware_mrs x xa xb s))\<rbrace>
 3. \<lbrace>?Q\<rbrace> return $ take (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch obj') msg_info_register)))) msg_registers \<lbrace>?B1\<rbrace>
 4. \<And>s. ipc_buffer_wp_at buf t s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>hardware_mrs x x2 x2a xa v. \<lbrakk>rva = Some x2; rv = Some x2a; xa \<in> ?S37 hardware_mrs x x2 x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B38 hardware_mrs x x2 x2a xa v\<rbrace> store_word_offs x2a xa v \<lbrace>\<lambda>buf_mrs. ipc_buffer_wp_at buf t\<rbrace>
 2. \<And>hardware_mrs x x2 x2a xa. \<lbrakk>rva = Some x2; rv = Some x2a; xa \<in> ?S37 hardware_mrs x x2 x2a\<rbrakk> \<Longrightarrow> \<lbrace>ipc_buffer_wp_at buf t\<rbrace> load_word_offs x2 xa \<lbrace>?B38 hardware_mrs x x2 x2a xa\<rbrace>
 3. \<And>hardware_mrs x x2 x2a. \<lbrakk>rva = Some x2; rv = Some x2a\<rbrakk> \<Longrightarrow> set [length msg_registers + 1..<Suc (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch obj') msg_info_register))))] \<subseteq> ?S37 hardware_mrs x x2 x2a
 4. \<And>hardware_mrs. \<lbrace>?B1 hardware_mrs\<rbrace> mapM (\<lambda>r. do v <- as_user send $ getRegister r;
as_user recv $ setRegister r v
od) hardware_mrs \<lbrace>\<lambda>x s. (rva = None \<longrightarrow> ipc_buffer_wp_at buf t s) \<and> (\<forall>x. rva = Some x \<longrightarrow> (rv = None \<longrightarrow> ipc_buffer_wp_at buf t s) \<and> (\<forall>x. rv = Some x \<longrightarrow> ipc_buffer_wp_at buf t s))\<rbrace>
 5. \<lbrace>?Q\<rbrace> return $ take (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch obj') msg_info_register)))) msg_registers \<lbrace>?B1\<rbrace>
 6. \<And>s. ipc_buffer_wp_at buf t s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>hardware_mrs x x2 x2a xa v. \<lbrakk>rva = Some x2; rv = Some x2a; xa \<in> ?S37 hardware_mrs x x2 x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B38 hardware_mrs x x2 x2a xa v\<rbrace> do s <- get;
y <- assert (in_user_frame (x2a + word_of_nat xa * word_of_nat word_size) s);
do_machine_op (storeWord (x2a + word_of_nat xa * word_of_nat word_size) v)
od \<lbrace>\<lambda>buf_mrs. obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> tcb_ipc_buffer tcb = buf) t\<rbrace>
 2. \<And>hardware_mrs x x2 x2a xa. \<lbrakk>rva = Some x2; rv = Some x2a; xa \<in> ?S37 hardware_mrs x x2 x2a\<rbrakk> \<Longrightarrow> \<lbrace>ipc_buffer_wp_at buf t\<rbrace> load_word_offs x2 xa \<lbrace>?B38 hardware_mrs x x2 x2a xa\<rbrace>
 3. \<And>hardware_mrs x x2 x2a. \<lbrakk>rva = Some x2; rv = Some x2a\<rbrakk> \<Longrightarrow> set [length msg_registers + 1..<Suc (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch obj') msg_info_register))))] \<subseteq> ?S37 hardware_mrs x x2 x2a
 4. \<And>hardware_mrs. \<lbrace>?B1 hardware_mrs\<rbrace> mapM (\<lambda>r. do v <- as_user send $ getRegister r;
as_user recv $ setRegister r v
od) hardware_mrs \<lbrace>\<lambda>x s. (rva = None \<longrightarrow> ipc_buffer_wp_at buf t s) \<and> (\<forall>x. rva = Some x \<longrightarrow> (rv = None \<longrightarrow> ipc_buffer_wp_at buf t s) \<and> (\<forall>x. rv = Some x \<longrightarrow> ipc_buffer_wp_at buf t s))\<rbrace>
 5. \<lbrace>?Q\<rbrace> return $ take (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch obj') msg_info_register)))) msg_registers \<lbrace>?B1\<rbrace>
 6. \<And>s. ipc_buffer_wp_at buf t s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>hardware_mrs x x2 x2a xa s. \<lbrakk>rva = Some x2; rv = Some x2a; xa \<in> ?S37 hardware_mrs x x2 x2a; ipc_buffer_wp_at buf t s\<rbrakk> \<Longrightarrow> in_user_frame (x2a + word_of_nat xa * word_of_nat word_size) s \<longrightarrow> obj_at (\<lambda>a. \<exists>tcb. a = TCB tcb \<and> tcb_ipc_buffer tcb = buf) t s
 2. \<And>hardware_mrs x x2 x2a. \<lbrakk>rva = Some x2; rv = Some x2a\<rbrakk> \<Longrightarrow> set [length msg_registers + 1..<Suc (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch obj') msg_info_register))))] \<subseteq> ?S37 hardware_mrs x x2 x2a
 3. \<And>hardware_mrs. \<lbrace>?B1 hardware_mrs\<rbrace> mapM (\<lambda>r. do v <- as_user send $ getRegister r;
as_user recv $ setRegister r v
od) hardware_mrs \<lbrace>\<lambda>x s. (rva = None \<longrightarrow> ipc_buffer_wp_at buf t s) \<and> (\<forall>x. rva = Some x \<longrightarrow> (rv = None \<longrightarrow> ipc_buffer_wp_at buf t s) \<and> (\<forall>x. rv = Some x \<longrightarrow> ipc_buffer_wp_at buf t s))\<rbrace>
 4. \<lbrace>?Q\<rbrace> return $ take (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch obj') msg_info_register)))) msg_registers \<lbrace>?B1\<rbrace>
 5. \<And>s. ipc_buffer_wp_at buf t s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>hardware_mrs x x2 x2a. \<lbrakk>rva = Some x2; rv = Some x2a\<rbrakk> \<Longrightarrow> set [length msg_registers + 1..<Suc (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch obj') msg_info_register))))] \<subseteq> ?S37 hardware_mrs x x2 x2a
 2. \<And>hardware_mrs x x2 x2a xa s. \<lbrakk>rva = Some x2; rv = Some x2a; xa \<in> ?S37 hardware_mrs x x2 x2a; ipc_buffer_wp_at buf t s\<rbrakk> \<Longrightarrow> in_user_frame (x2a + word_of_nat xa * word_of_nat word_size) s \<longrightarrow> obj_at (\<lambda>a. \<exists>tcb. a = TCB tcb \<and> tcb_ipc_buffer tcb = buf) t s
 3. \<And>hardware_mrs. \<lbrace>?B1 hardware_mrs\<rbrace> mapM (\<lambda>r. do v <- as_user send $ getRegister r;
as_user recv $ setRegister r v
od) hardware_mrs \<lbrace>\<lambda>x s. (rva = None \<longrightarrow> ipc_buffer_wp_at buf t s) \<and> (\<forall>x. rva = Some x \<longrightarrow> (rv = None \<longrightarrow> ipc_buffer_wp_at buf t s) \<and> (\<forall>x. rv = Some x \<longrightarrow> ipc_buffer_wp_at buf t s))\<rbrace>
 4. \<lbrace>?Q\<rbrace> return $ take (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch obj') msg_info_register)))) msg_registers \<lbrace>?B1\<rbrace>
 5. \<And>s. ipc_buffer_wp_at buf t s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>hardware_mrs x x2 x2a xa s. \<lbrakk>rva = Some x2; rv = Some x2a; xa \<in> dom (\<lambda>a. Some (?y63 hardware_mrs x x2 x2a a)); ipc_buffer_wp_at buf t s\<rbrakk> \<Longrightarrow> in_user_frame (x2a + word_of_nat xa * word_of_nat word_size) s \<longrightarrow> obj_at (\<lambda>a. \<exists>tcb. a = TCB tcb \<and> tcb_ipc_buffer tcb = buf) t s
 2. \<And>hardware_mrs. \<lbrace>?B1 hardware_mrs\<rbrace> mapM (\<lambda>r. do v <- as_user send $ getRegister r;
as_user recv $ setRegister r v
od) hardware_mrs \<lbrace>\<lambda>x s. (rva = None \<longrightarrow> ipc_buffer_wp_at buf t s) \<and> (\<forall>x. rva = Some x \<longrightarrow> (rv = None \<longrightarrow> ipc_buffer_wp_at buf t s) \<and> (\<forall>x. rv = Some x \<longrightarrow> ipc_buffer_wp_at buf t s))\<rbrace>
 3. \<lbrace>?Q\<rbrace> return $ take (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch obj') msg_info_register)))) msg_registers \<lbrace>?B1\<rbrace>
 4. \<And>s. ipc_buffer_wp_at buf t s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>hardware_mrs. \<lbrace>?B1 hardware_mrs\<rbrace> mapM (\<lambda>r. do v <- as_user send $ getRegister r;
as_user recv $ setRegister r v
od) hardware_mrs \<lbrace>\<lambda>x s. (rva = None \<longrightarrow> ipc_buffer_wp_at buf t s) \<and> (\<forall>x. rva = Some x \<longrightarrow> (rv = None \<longrightarrow> ipc_buffer_wp_at buf t s) \<and> (\<forall>x. rv = Some x \<longrightarrow> ipc_buffer_wp_at buf t s))\<rbrace>
 2. \<lbrace>?Q\<rbrace> return $ take (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch obj') msg_info_register)))) msg_registers \<lbrace>?B1\<rbrace>
 3. \<And>s. ipc_buffer_wp_at buf t s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>hardware_mrs. \<lbrace>?B1 hardware_mrs\<rbrace> mapM (\<lambda>r. do v <- as_user send $ getRegister r;
as_user recv $ setRegister r v
od) hardware_mrs \<lbrace>\<lambda>rv. ipc_buffer_wp_at buf t\<rbrace>
 2. \<And>hardware_mrs rvb s. ipc_buffer_wp_at buf t s \<Longrightarrow> (rva = None \<longrightarrow> ipc_buffer_wp_at buf t s) \<and> (\<forall>x. rva = Some x \<longrightarrow> (rv = None \<longrightarrow> ipc_buffer_wp_at buf t s) \<and> (\<forall>x. rv = Some x \<longrightarrow> ipc_buffer_wp_at buf t s))
 3. \<lbrace>?Q\<rbrace> return $ take (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch obj') msg_info_register)))) msg_registers \<lbrace>?B1\<rbrace>
 4. \<And>s. ipc_buffer_wp_at buf t s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>hardware_mrs. set hardware_mrs \<subseteq> ?S70 hardware_mrs
 2. \<And>hardware_mrs rvb s. ipc_buffer_wp_at buf t s \<Longrightarrow> (rva = None \<longrightarrow> ipc_buffer_wp_at buf t s) \<and> (\<forall>x. rva = Some x \<longrightarrow> (rv = None \<longrightarrow> ipc_buffer_wp_at buf t s) \<and> (\<forall>x. rv = Some x \<longrightarrow> ipc_buffer_wp_at buf t s))
 3. \<lbrace>?Q\<rbrace> return $ take (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch obj') msg_info_register)))) msg_registers \<lbrace>\<lambda>hardware_mrs. ipc_buffer_wp_at buf t\<rbrace>
 4. \<And>s. ipc_buffer_wp_at buf t s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>hardware_mrs rvb s. ipc_buffer_wp_at buf t s \<Longrightarrow> (rva = None \<longrightarrow> ipc_buffer_wp_at buf t s) \<and> (\<forall>x. rva = Some x \<longrightarrow> (rv = None \<longrightarrow> ipc_buffer_wp_at buf t s) \<and> (\<forall>x. rv = Some x \<longrightarrow> ipc_buffer_wp_at buf t s))
 2. \<lbrace>?Q\<rbrace> return $ take (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch obj') msg_info_register)))) msg_registers \<lbrace>\<lambda>hardware_mrs. ipc_buffer_wp_at buf t\<rbrace>
 3. \<And>s. ipc_buffer_wp_at buf t s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> return $ take (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch obj') msg_info_register)))) msg_registers \<lbrace>\<lambda>hardware_mrs. ipc_buffer_wp_at buf t\<rbrace>
 2. \<And>s. ipc_buffer_wp_at buf t s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. ipc_buffer_wp_at buf t s \<Longrightarrow> ipc_buffer_wp_at buf t s proof (prove)
goal:
No subgoals!