theory Intent_DR

lemma get_tcb_mrs_wp:
  "\<lbrace>(=) sa and ko_at (TCB obj) thread and K_bind (evalMonad (lookup_ipc_buffer False thread) sa = Some (op_buf))\<rbrace>
    get_mrs thread (op_buf) (data_to_message_info (arch_tcb_context_get (tcb_arch obj) msg_info_register))
            \<lbrace>\<lambda>rv s. rv = get_tcb_mrs (machine_state sa) obj\<rbrace>" apply (case_tac op_buf) apply (clarsimp simp:get_mrs_def thread_get_def gets_the_def) apply (wp|wpc)+ apply (clarsimp simp:get_tcb_mrs_def Let_def) apply (clarsimp simp:Suc_leI[OF msg_registers_lt_msg_max_length] split del:if_split) apply (clarsimp simp:get_tcb_message_info_def get_ipc_buffer_words_empty) apply (clarsimp dest!:get_tcb_SomeD simp:obj_at_def arch_tcb_get_registers_def) apply (clarsimp simp:get_mrs_def thread_get_def gets_the_def arch_tcb_get_registers_def) apply (clarsimp simp:Suc_leI[OF msg_registers_lt_msg_max_length] split del:if_split) apply (wp|wpc)+ apply (rule_tac P = "tcb = obj" in hoare_gen_asm) apply (clarsimp simp: get_tcb_mrs_def Let_def get_tcb_message_info_def Suc_leI[OF msg_registers_lt_msg_max_length]
                   split del:if_split) apply (rule_tac Q="\<lambda>buf_mrs s. buf_mrs =
      (get_ipc_buffer_words (machine_state sa) obj ([Suc (length msg_registers)..<msg_max_length] @ [msg_max_length]))"
      in hoare_strengthen_post) apply (rule get_ipc_buffer_words[where thread=thread ]) apply simp apply wp apply (fastforce simp:get_tcb_SomeD obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(=) sa and ko_at (TCB obj) thread and K_bind (evalMonad (lookup_ipc_buffer False thread) sa = Some op_buf)\<rbrace> get_mrs thread op_buf (data_to_message_info (arch_tcb_context_get (tcb_arch obj) msg_info_register)) \<lbrace>\<lambda>rv s. rv = get_tcb_mrs (machine_state sa) obj\<rbrace> proof (prove)
goal (2 subgoals):
 1. op_buf = None \<Longrightarrow> \<lbrace>(=) sa and ko_at (TCB obj) thread and K_bind (evalMonad (lookup_ipc_buffer False thread) sa = Some op_buf)\<rbrace> get_mrs thread op_buf (data_to_message_info (arch_tcb_context_get (tcb_arch obj) msg_info_register)) \<lbrace>\<lambda>rv s. rv = get_tcb_mrs (machine_state sa) obj\<rbrace>
 2. \<And>a. op_buf = Some a \<Longrightarrow> \<lbrace>(=) sa and ko_at (TCB obj) thread and K_bind (evalMonad (lookup_ipc_buffer False thread) sa = Some op_buf)\<rbrace> get_mrs thread op_buf (data_to_message_info (arch_tcb_context_get (tcb_arch obj) msg_info_register)) \<lbrace>\<lambda>rv s. rv = get_tcb_mrs (machine_state sa) obj\<rbrace> proof (prove)
goal (2 subgoals):
 1. op_buf = None \<Longrightarrow> \<lbrace>(=) sa and ko_at (TCB obj) thread and (\<lambda>y. evalMonad (lookup_ipc_buffer False thread) sa = Some None)\<rbrace> do tcb <- gets (get_tcb thread) >>= assert_opt;
return (take (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch obj) msg_info_register)))) (map (arch_tcb_get_registers (tcb_arch tcb)) msg_registers))
od \<lbrace>\<lambda>rv s. rv = get_tcb_mrs (machine_state sa) obj\<rbrace>
 2. \<And>a. op_buf = Some a \<Longrightarrow> \<lbrace>(=) sa and ko_at (TCB obj) thread and K_bind (evalMonad (lookup_ipc_buffer False thread) sa = Some op_buf)\<rbrace> get_mrs thread op_buf (data_to_message_info (arch_tcb_context_get (tcb_arch obj) msg_info_register)) \<lbrace>\<lambda>rv s. rv = get_tcb_mrs (machine_state sa) obj\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>op_buf = None; ((=) sa and ko_at (TCB obj) thread and (\<lambda>y. evalMonad (lookup_ipc_buffer False thread) sa = Some None)) s\<rbrakk> \<Longrightarrow> get_tcb thread s \<noteq> None \<longrightarrow> take (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch obj) msg_info_register)))) (map (arch_tcb_get_registers (tcb_arch (the (get_tcb thread s)))) msg_registers) = get_tcb_mrs (machine_state sa) obj
 2. \<And>a. op_buf = Some a \<Longrightarrow> \<lbrace>(=) sa and ko_at (TCB obj) thread and K_bind (evalMonad (lookup_ipc_buffer False thread) sa = Some op_buf)\<rbrace> get_mrs thread op_buf (data_to_message_info (arch_tcb_context_get (tcb_arch obj) msg_info_register)) \<lbrace>\<lambda>rv s. rv = get_tcb_mrs (machine_state sa) obj\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>op_buf = None; ko_at (TCB obj) thread sa; evalMonad (lookup_ipc_buffer False thread) sa = Some None\<rbrakk> \<Longrightarrow> (Suc (length msg_registers) \<le> msg_max_length \<longrightarrow> (\<exists>y. get_tcb thread sa = Some y) \<longrightarrow> take (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch obj) msg_info_register)))) (map (arch_tcb_get_registers (tcb_arch (the (get_tcb thread sa)))) msg_registers) = take (unat (mi_length (get_tcb_message_info obj))) (map (arch_tcb_context_get (tcb_arch obj)) msg_registers) @ take (unat (mi_length (get_tcb_message_info obj)) - length msg_registers) (get_ipc_buffer_words (machine_state sa) obj ([Suc (length msg_registers)..<msg_max_length] @ [msg_max_length]))) \<and> (\<not> Suc (length msg_registers) \<le> msg_max_length \<longrightarrow> (\<exists>y. get_tcb thread sa = Some y) \<longrightarrow> take (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch obj) msg_info_register)))) (map (arch_tcb_get_registers (tcb_arch (the (get_tcb thread sa)))) msg_registers) = take (unat (mi_length (get_tcb_message_info obj))) (map (arch_tcb_context_get (tcb_arch obj)) msg_registers) @ take (unat (mi_length (get_tcb_message_info obj)) - length msg_registers) (get_ipc_buffer_words (machine_state sa) obj []))
 2. \<And>a. op_buf = Some a \<Longrightarrow> \<lbrace>(=) sa and ko_at (TCB obj) thread and K_bind (evalMonad (lookup_ipc_buffer False thread) sa = Some op_buf)\<rbrace> get_mrs thread op_buf (data_to_message_info (arch_tcb_context_get (tcb_arch obj) msg_info_register)) \<lbrace>\<lambda>rv s. rv = get_tcb_mrs (machine_state sa) obj\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>op_buf = None; ko_at (TCB obj) thread sa; evalMonad (lookup_ipc_buffer False thread) sa = Some None; get_tcb thread sa = Some y\<rbrakk> \<Longrightarrow> take (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch obj) msg_info_register)))) (map (arch_tcb_get_registers (tcb_arch y)) msg_registers) = take (unat (mi_length (get_tcb_message_info obj))) (map (arch_tcb_context_get (tcb_arch obj)) msg_registers) @ take (unat (mi_length (get_tcb_message_info obj)) - length msg_registers) (get_ipc_buffer_words (machine_state sa) obj ([Suc (length msg_registers)..<msg_max_length] @ [msg_max_length]))
 2. \<And>a. op_buf = Some a \<Longrightarrow> \<lbrace>(=) sa and ko_at (TCB obj) thread and K_bind (evalMonad (lookup_ipc_buffer False thread) sa = Some op_buf)\<rbrace> get_mrs thread op_buf (data_to_message_info (arch_tcb_context_get (tcb_arch obj) msg_info_register)) \<lbrace>\<lambda>rv s. rv = get_tcb_mrs (machine_state sa) obj\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>op_buf = None; ko_at (TCB obj) thread sa; evalMonad (lookup_ipc_buffer False thread) sa = Some None; get_tcb thread sa = Some y\<rbrakk> \<Longrightarrow> take (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch obj) msg_info_register)))) (map (arch_tcb_get_registers (tcb_arch y)) msg_registers) = take (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch obj) msg_info_register)))) (map (arch_tcb_context_get (tcb_arch obj)) msg_registers)
 2. \<And>a. op_buf = Some a \<Longrightarrow> \<lbrace>(=) sa and ko_at (TCB obj) thread and K_bind (evalMonad (lookup_ipc_buffer False thread) sa = Some op_buf)\<rbrace> get_mrs thread op_buf (data_to_message_info (arch_tcb_context_get (tcb_arch obj) msg_info_register)) \<lbrace>\<lambda>rv s. rv = get_tcb_mrs (machine_state sa) obj\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a. op_buf = Some a \<Longrightarrow> \<lbrace>(=) sa and ko_at (TCB obj) thread and K_bind (evalMonad (lookup_ipc_buffer False thread) sa = Some op_buf)\<rbrace> get_mrs thread op_buf (data_to_message_info (arch_tcb_context_get (tcb_arch obj) msg_info_register)) \<lbrace>\<lambda>rv s. rv = get_tcb_mrs (machine_state sa) obj\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a. op_buf = Some a \<Longrightarrow> (Suc (length msg_registers) \<le> msg_max_length \<longrightarrow> \<lbrace>(=) sa and ko_at (TCB obj) thread and (\<lambda>y. evalMonad (lookup_ipc_buffer False thread) sa = Some (Some a))\<rbrace> do tcb <- gets (get_tcb thread) >>= assert_opt;
buf_mrs <- mapM (load_word_offs a) ([Suc (length msg_registers)..<msg_max_length] @ [msg_max_length]);
return (take (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch obj) msg_info_register)))) (map (arch_tcb_context_get (tcb_arch tcb)) msg_registers) @ take (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch obj) msg_info_register))) - length msg_registers) buf_mrs)
od \<lbrace>\<lambda>rv s. rv = get_tcb_mrs (machine_state sa) obj\<rbrace>) \<and> (\<not> Suc (length msg_registers) \<le> msg_max_length \<longrightarrow> \<lbrace>(=) sa and ko_at (TCB obj) thread and (\<lambda>y. evalMonad (lookup_ipc_buffer False thread) sa = Some (Some a))\<rbrace> do tcb <- gets (get_tcb thread) >>= assert_opt;
buf_mrs <- mapM (load_word_offs a) [];
return (take (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch obj) msg_info_register)))) (map (arch_tcb_context_get (tcb_arch tcb)) msg_registers) @ take (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch obj) msg_info_register))) - length msg_registers) buf_mrs)
od \<lbrace>\<lambda>rv s. rv = get_tcb_mrs (machine_state sa) obj\<rbrace>) proof (prove)
goal (1 subgoal):
 1. \<And>a. op_buf = Some a \<Longrightarrow> \<lbrace>(=) sa and ko_at (TCB obj) thread and (\<lambda>y. evalMonad (lookup_ipc_buffer False thread) sa = Some (Some a))\<rbrace> do tcb <- gets (get_tcb thread) >>= assert_opt;
buf_mrs <- mapM (load_word_offs a) ([Suc (length msg_registers)..<msg_max_length] @ [msg_max_length]);
return (take (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch obj) msg_info_register)))) (map (arch_tcb_context_get (tcb_arch tcb)) msg_registers) @ take (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch obj) msg_info_register))) - length msg_registers) buf_mrs)
od \<lbrace>\<lambda>rv s. rv = get_tcb_mrs (machine_state sa) obj\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>a tcb. op_buf = Some a \<Longrightarrow> \<lbrace>?B32 a tcb\<rbrace> mapM (load_word_offs a) ([Suc (length msg_registers)..<msg_max_length] @ [msg_max_length]) \<lbrace>\<lambda>buf_mrs a. take (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch obj) msg_info_register)))) (map (arch_tcb_context_get (tcb_arch tcb)) msg_registers) @ take (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch obj) msg_info_register))) - length msg_registers) buf_mrs = get_tcb_mrs (machine_state sa) obj\<rbrace>
 2. \<And>a. op_buf = Some a \<Longrightarrow> \<lbrace>?Q31 a\<rbrace> gets (get_tcb thread) >>= assert_opt \<lbrace>?B32 a\<rbrace>
 3. \<And>a s. \<lbrakk>op_buf = Some a; ((=) sa and ko_at (TCB obj) thread and (\<lambda>y. evalMonad (lookup_ipc_buffer False thread) sa = Some (Some a))) s\<rbrakk> \<Longrightarrow> ?Q31 a s proof (prove)
goal (3 subgoals):
 1. \<And>a tcb. \<lbrakk>op_buf = Some a; tcb = obj\<rbrakk> \<Longrightarrow> \<lbrace>?P'35 a tcb\<rbrace> mapM (load_word_offs a) ([Suc (length msg_registers)..<msg_max_length] @ [msg_max_length]) \<lbrace>\<lambda>buf_mrs a. take (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch obj) msg_info_register)))) (map (arch_tcb_context_get (tcb_arch tcb)) msg_registers) @ take (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch obj) msg_info_register))) - length msg_registers) buf_mrs = get_tcb_mrs (machine_state sa) obj\<rbrace>
 2. \<And>a. op_buf = Some a \<Longrightarrow> \<lbrace>?Q31 a\<rbrace> gets (get_tcb thread) >>= assert_opt \<lbrace>\<lambda>tcb. ?P'35 a tcb and K (tcb = obj)\<rbrace>
 3. \<And>a s. \<lbrakk>op_buf = Some a; ((=) sa and ko_at (TCB obj) thread and (\<lambda>y. evalMonad (lookup_ipc_buffer False thread) sa = Some (Some a))) s\<rbrakk> \<Longrightarrow> ?Q31 a s proof (prove)
goal (3 subgoals):
 1. \<And>a. op_buf = Some a \<Longrightarrow> \<lbrace>?P'35 a obj\<rbrace> mapM (load_word_offs a) ([Suc (length msg_registers)..<msg_max_length] @ [msg_max_length]) \<lbrace>\<lambda>buf_mrs a. take (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch obj) msg_info_register))) - length msg_registers) buf_mrs = take (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch obj) msg_info_register))) - length msg_registers) (get_ipc_buffer_words (machine_state sa) obj ([Suc (length msg_registers)..<msg_max_length] @ [msg_max_length]))\<rbrace>
 2. \<And>a. op_buf = Some a \<Longrightarrow> \<lbrace>?Q31 a\<rbrace> gets (get_tcb thread) >>= assert_opt \<lbrace>\<lambda>tcb. ?P'35 a tcb and K (tcb = obj)\<rbrace>
 3. \<And>a s. \<lbrakk>op_buf = Some a; ((=) sa and ko_at (TCB obj) thread and (\<lambda>y. evalMonad (lookup_ipc_buffer False thread) sa = Some (Some a))) s\<rbrakk> \<Longrightarrow> ?Q31 a s proof (prove)
goal (4 subgoals):
 1. \<And>a. op_buf = Some a \<Longrightarrow> \<lbrace>?P'35 a obj\<rbrace> mapM (load_word_offs a) ([Suc (length msg_registers)..<msg_max_length] @ [msg_max_length]) \<lbrace>\<lambda>buf_mrs s. buf_mrs = get_ipc_buffer_words (machine_state sa) obj ([Suc (length msg_registers)..<msg_max_length] @ [msg_max_length])\<rbrace>
 2. \<And>a rv s. \<lbrakk>op_buf = Some a; rv = get_ipc_buffer_words (machine_state sa) obj ([Suc (length msg_registers)..<msg_max_length] @ [msg_max_length])\<rbrakk> \<Longrightarrow> take (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch obj) msg_info_register))) - length msg_registers) rv = take (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch obj) msg_info_register))) - length msg_registers) (get_ipc_buffer_words (machine_state sa) obj ([Suc (length msg_registers)..<msg_max_length] @ [msg_max_length]))
 3. \<And>a. op_buf = Some a \<Longrightarrow> \<lbrace>?Q31 a\<rbrace> gets (get_tcb thread) >>= assert_opt \<lbrace>\<lambda>tcb. ?P'35 a tcb and K (tcb = obj)\<rbrace>
 4. \<And>a s. \<lbrakk>op_buf = Some a; ((=) sa and ko_at (TCB obj) thread and (\<lambda>y. evalMonad (lookup_ipc_buffer False thread) sa = Some (Some a))) s\<rbrakk> \<Longrightarrow> ?Q31 a s proof (prove)
goal (3 subgoals):
 1. \<And>a rv s. \<lbrakk>op_buf = Some a; rv = get_ipc_buffer_words (machine_state sa) obj ([Suc (length msg_registers)..<msg_max_length] @ [msg_max_length])\<rbrakk> \<Longrightarrow> take (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch obj) msg_info_register))) - length msg_registers) rv = take (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch obj) msg_info_register))) - length msg_registers) (get_ipc_buffer_words (machine_state sa) obj ([Suc (length msg_registers)..<msg_max_length] @ [msg_max_length]))
 2. \<And>a. op_buf = Some a \<Longrightarrow> \<lbrace>?Q31 a\<rbrace> gets (get_tcb thread) >>= assert_opt \<lbrace>\<lambda>tcb. (=) sa and ko_at (TCB tcb) thread and K_bind (evalMonad (lookup_ipc_buffer (?in_receive45 a tcb) thread) sa = Some (Some a)) and K (tcb = obj)\<rbrace>
 3. \<And>a s. \<lbrakk>op_buf = Some a; ((=) sa and ko_at (TCB obj) thread and (\<lambda>y. evalMonad (lookup_ipc_buffer False thread) sa = Some (Some a))) s\<rbrakk> \<Longrightarrow> ?Q31 a s proof (prove)
goal (2 subgoals):
 1. \<And>a. op_buf = Some a \<Longrightarrow> \<lbrace>?Q31 a\<rbrace> gets (get_tcb thread) >>= assert_opt \<lbrace>\<lambda>tcb. (=) sa and ko_at (TCB tcb) thread and K_bind (evalMonad (lookup_ipc_buffer (?in_receive45 a tcb) thread) sa = Some (Some a)) and K (tcb = obj)\<rbrace>
 2. \<And>a s. \<lbrakk>op_buf = Some a; ((=) sa and ko_at (TCB obj) thread and (\<lambda>y. evalMonad (lookup_ipc_buffer False thread) sa = Some (Some a))) s\<rbrakk> \<Longrightarrow> ?Q31 a s proof (prove)
goal (1 subgoal):
 1. \<And>a s. \<lbrakk>op_buf = Some a; ((=) sa and ko_at (TCB obj) thread and (\<lambda>y. evalMonad (lookup_ipc_buffer False thread) sa = Some (Some a))) s\<rbrakk> \<Longrightarrow> get_tcb thread s \<noteq> None \<longrightarrow> ((=) sa and ko_at (TCB (the (get_tcb thread s))) thread and K_bind (evalMonad (lookup_ipc_buffer (?in_receive45 a (the (get_tcb thread s))) thread) sa = Some (Some a)) and K (the (get_tcb thread s) = obj)) s proof (prove)
goal:
No subgoals!