theory Ipc_IF

lemma do_reply_transfer_globals_equiv:
  "\<lbrace>globals_equiv st and valid_objs and valid_arch_state and valid_global_refs
                     and pspace_distinct and pspace_aligned and valid_global_objs and valid_idle\<rbrace>
   do_reply_transfer sender receiver slot grant
   \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" unfolding do_reply_transfer_def apply (wp set_thread_state_globals_equiv cap_delete_one_globals_equiv do_ipc_transfer_globals_equiv
            thread_set_globals_equiv handle_fault_reply_globals_equiv dxo_wp_weak
         | wpc | simp split del: if_split)+ apply (rule_tac Q="\<lambda>_. globals_equiv st and valid_arch_state and valid_objs and valid_arch_state
                                             and valid_global_refs and pspace_distinct
                                             and pspace_aligned and valid_global_objs
                                             and (\<lambda>s. receiver \<noteq> idle_thread s) and valid_idle"
                  in hoare_strengthen_post) apply (wp gts_wp | fastforce simp: pred_tcb_at_def obj_at_def valid_idle_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and valid_idle\<rbrace> do_reply_transfer sender receiver slot grant \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and valid_idle\<rbrace> do state <- get_thread_state receiver;
assert (awaiting_reply state);
fault <- thread_get tcb_fault receiver;
case fault of None \<Rightarrow> do do_ipc_transfer sender None 0 grant receiver;
cap_delete_one slot;
set_thread_state receiver Running;
do_extended_op (possible_switch_to receiver)
od | Some f \<Rightarrow> do cap_delete_one slot;
mi <- get_message_info sender;
buf <- lookup_ipc_buffer False sender;
mrs <- get_mrs sender buf mi;
restart <- handle_fault_reply f receiver (mi_label mi) mrs;
thread_set (tcb_fault_update (\<lambda>_. None)) receiver;
set_thread_state receiver (if restart then Restart else Inactive);
when restart $ do_extended_op (possible_switch_to receiver);
return ()
od
od \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>state. \<lbrace>?B2 state ()\<rbrace> thread_get tcb_fault receiver \<lbrace>\<lambda>fault s. (fault = None \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_global_objs s \<and> receiver \<noteq> idle_thread s \<and> valid_arch_state s) \<and> ((\<exists>x. fault = Some x) \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> receiver \<noteq> idle_thread s \<and> valid_arch_state s)\<rbrace>
 2. \<And>state. \<lbrace>?B1 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B2 state\<rbrace>
 3. \<lbrace>?Q\<rbrace> get_thread_state receiver \<lbrace>?B1\<rbrace>
 4. \<And>s. (globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and valid_idle) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>state. \<lbrace>?B2 state ()\<rbrace> thread_get tcb_fault receiver \<lbrace>\<lambda>_. globals_equiv st and valid_arch_state and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and (\<lambda>s. receiver \<noteq> idle_thread s) and valid_idle\<rbrace>
 2. \<And>state rv s. (globals_equiv st and valid_arch_state and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and (\<lambda>s. receiver \<noteq> idle_thread s) and valid_idle) s \<Longrightarrow> (rv = None \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_global_objs s \<and> receiver \<noteq> idle_thread s \<and> valid_arch_state s) \<and> ((\<exists>x. rv = Some x) \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> receiver \<noteq> idle_thread s \<and> valid_arch_state s)
 3. \<And>state. \<lbrace>?B1 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B2 state\<rbrace>
 4. \<lbrace>?Q\<rbrace> get_thread_state receiver \<lbrace>?B1\<rbrace>
 5. \<And>s. (globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and valid_idle) s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!