theory Ipc_AI

lemma do_ipc_transfer_aobj_at:
  "arch_obj_pred P' \<Longrightarrow>
  \<lbrace>\<lambda>s. P (obj_at P' pd s)\<rbrace> do_ipc_transfer s ep bg grt r \<lbrace>\<lambda>r s :: 'state_ext state. P (obj_at P' pd s)\<rbrace>" unfolding
    do_ipc_transfer_def do_normal_transfer_def set_message_info_def transfer_caps_def
    copy_mrs_def do_fault_transfer_def apply (wpsimp wp: as_user.aobj_at set_mrs.aobj_at hoare_drop_imps mapM_wp' transfer_caps_loop_aobj_at) apply (case_tac f, simp split del: if_split) apply (wpsimp wp: as_user.aobj_at hoare_drop_imps)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arch_obj_pred P' \<Longrightarrow> \<lbrace>\<lambda>s. P (obj_at P' pd s)\<rbrace> do_ipc_transfer s ep bg grt r \<lbrace>\<lambda>r s. P (obj_at P' pd s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. arch_obj_pred P' \<Longrightarrow> \<lbrace>\<lambda>s. P (obj_at P' pd s)\<rbrace> do recv_buffer <- lookup_ipc_buffer True r;
fault <- thread_get tcb_fault s;
case fault of None \<Rightarrow> do send_buffer <- lookup_ipc_buffer False s;
mi <- get_message_info s;
caps <- if grt then lookup_extra_caps s send_buffer mi <catch> K (return []) else return [];
mrs_transferred <- do hardware_mrs <- return $ take (unat (mi_length mi)) msg_registers;
mapM (\<lambda>ra. do v <- as_user s $ getRegister ra;
as_user r $ setRegister ra v
od) hardware_mrs;
buf_mrs <- case (send_buffer, recv_buffer) 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 mi))];
return $ min (mi_length mi) $ nat_to_len $ length hardware_mrs + length buf_mrs
od;
mi' <- do dest_slots <- get_receive_slots r recv_buffer;
mi' <- return $ MI (mi_length mi) 0 0 (mi_label mi);
case recv_buffer of None \<Rightarrow> return mi' | Some receive_buffer \<Rightarrow> transfer_caps_loop ep receive_buffer 0 caps dest_slots mi'
od;
(\<lambda>info. as_user r $ setRegister msg_info_register $ message_info_to_data info) $ MI mrs_transferred (mi_extra_caps mi') (mi_caps_unwrapped mi') (mi_label mi);
as_user r $ setRegister badge_register bg
od | Some f \<Rightarrow> do fault <- thread_get tcb_fault s;
f <- case fault of None \<Rightarrow> fail | Some f \<Rightarrow> return f;
(label, msg) <- make_fault_msg f s;
sent <- set_mrs r recv_buffer msg;
(\<lambda>info. as_user r $ setRegister msg_info_register $ message_info_to_data info) $ MI sent 0 0 label;
as_user r $ setRegister badge_register bg
od
od \<lbrace>\<lambda>r s. P (obj_at P' pd s)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>recv_buffer x2 faulta f. arch_obj_pred P' \<Longrightarrow> \<lbrace>?B241 recv_buffer (Some x2) x2 faulta f\<rbrace> make_fault_msg f s \<lbrace>\<lambda>x s. P (obj_at P' pd s)\<rbrace>
 2. \<And>recv_buffer fault x2 faulta. \<lbrakk>arch_obj_pred P'; fault = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?B240 recv_buffer fault x2 faulta\<rbrace> case faulta of None \<Rightarrow> fail | Some f \<Rightarrow> return f \<lbrace>?B241 recv_buffer fault x2 faulta\<rbrace>
 3. \<And>recv_buffer fault x2. \<lbrakk>arch_obj_pred P'; fault = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R13 recv_buffer fault x2\<rbrace> thread_get tcb_fault s \<lbrace>?B240 recv_buffer fault x2\<rbrace>
 4. \<And>recv_buffer. arch_obj_pred P' \<Longrightarrow> \<lbrace>?B2 recv_buffer\<rbrace> thread_get tcb_fault s \<lbrace>\<lambda>fault s. (fault = None \<longrightarrow> P (obj_at P' pd s) \<and> P (obj_at P' pd s) \<and> P (obj_at P' pd s) \<and> P (obj_at P' pd s) \<and> (\<forall>x. recv_buffer = Some x \<longrightarrow> P (obj_at P' pd s)) \<and> P (obj_at P' pd s) \<and> P (obj_at P' pd s) \<and> P (obj_at P' pd s) \<and> P (obj_at P' pd s)) \<and> (\<forall>x. fault = Some x \<longrightarrow> ?R13 recv_buffer fault x s)\<rbrace>
 5. arch_obj_pred P' \<Longrightarrow> \<lbrace>?Q1\<rbrace> lookup_ipc_buffer True r \<lbrace>?B2\<rbrace>
 6. \<And>s. \<lbrakk>arch_obj_pred P'; P (obj_at P' pd s)\<rbrakk> \<Longrightarrow> ?Q1 s proof (prove)
goal (9 subgoals):
 1. \<And>recv_buffer x2 faulta f x11 x12 x13. \<lbrakk>arch_obj_pred P'; f = CapFault x11 x12 x13\<rbrakk> \<Longrightarrow> \<lbrace>?B241 recv_buffer (Some x2) x2 faulta (CapFault x11 x12 x13)\<rbrace> do pc <- as_user s getRestartPC;
return (1, pc # x11 # (if x12 then 1 else 0) # msg_from_lookup_failure x13)
od \<lbrace>\<lambda>x s. P (obj_at P' pd s)\<rbrace>
 2. \<And>recv_buffer x2 faulta f x2a. \<lbrakk>arch_obj_pred P'; f = UnknownSyscallException x2a\<rbrakk> \<Longrightarrow> \<lbrace>?B241 recv_buffer (Some x2) x2 faulta f\<rbrace> make_fault_msg f s \<lbrace>\<lambda>x s. P (obj_at P' pd s)\<rbrace>
 3. \<And>recv_buffer x2 faulta f x31 x32. \<lbrakk>arch_obj_pred P'; f = UserException x31 x32\<rbrakk> \<Longrightarrow> \<lbrace>?B241 recv_buffer (Some x2) x2 faulta f\<rbrace> make_fault_msg f s \<lbrace>\<lambda>x s. P (obj_at P' pd s)\<rbrace>
 4. \<And>recv_buffer x2 faulta f x4. \<lbrakk>arch_obj_pred P'; f = ArchFault x4\<rbrakk> \<Longrightarrow> \<lbrace>?B241 recv_buffer (Some x2) x2 faulta f\<rbrace> make_fault_msg f s \<lbrace>\<lambda>x s. P (obj_at P' pd s)\<rbrace>
 5. \<And>recv_buffer fault x2 faulta. \<lbrakk>arch_obj_pred P'; fault = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?B240 recv_buffer fault x2 faulta\<rbrace> case faulta of None \<Rightarrow> fail | Some f \<Rightarrow> return f \<lbrace>?B241 recv_buffer fault x2 faulta\<rbrace>
 6. \<And>recv_buffer fault x2. \<lbrakk>arch_obj_pred P'; fault = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R13 recv_buffer fault x2\<rbrace> thread_get tcb_fault s \<lbrace>?B240 recv_buffer fault x2\<rbrace>
 7. \<And>recv_buffer. arch_obj_pred P' \<Longrightarrow> \<lbrace>?B2 recv_buffer\<rbrace> thread_get tcb_fault s \<lbrace>\<lambda>fault s. (fault = None \<longrightarrow> P (obj_at P' pd s) \<and> P (obj_at P' pd s) \<and> P (obj_at P' pd s) \<and> P (obj_at P' pd s) \<and> (\<forall>x. recv_buffer = Some x \<longrightarrow> P (obj_at P' pd s)) \<and> P (obj_at P' pd s) \<and> P (obj_at P' pd s) \<and> P (obj_at P' pd s) \<and> P (obj_at P' pd s)) \<and> (\<forall>x. fault = Some x \<longrightarrow> ?R13 recv_buffer fault x s)\<rbrace>
 8. arch_obj_pred P' \<Longrightarrow> \<lbrace>?Q1\<rbrace> lookup_ipc_buffer True r \<lbrace>?B2\<rbrace>
 9. \<And>s. \<lbrakk>arch_obj_pred P'; P (obj_at P' pd s)\<rbrakk> \<Longrightarrow> ?Q1 s proof (prove)
goal:
No subgoals!