theory Ipc_IF

lemma do_fault_transfer_globals_equiv:
  "\<lbrace>globals_equiv s and valid_arch_state and (\<lambda>sa. receiver \<noteq> idle_thread sa)\<rbrace>
   do_fault_transfer badge sender receiver buf
   \<lbrace>\<lambda>_. globals_equiv s\<rbrace>" unfolding do_fault_transfer_def apply (wp) apply (simp add: split_def) apply (wp as_user_globals_equiv set_message_info_globals_equiv
               set_mrs_globals_equiv | wpc)+ apply (clarsimp) apply (rule hoare_drop_imps) apply (wp thread_get_inv, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and valid_arch_state and (\<lambda>sa. receiver \<noteq> idle_thread sa)\<rbrace> do_fault_transfer badge sender receiver buf \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and valid_arch_state and (\<lambda>sa. receiver \<noteq> idle_thread sa)\<rbrace> do fault <- thread_get tcb_fault sender;
f <- case fault of None \<Rightarrow> fail | Some f \<Rightarrow> return f;
(label, msg) <- make_fault_msg f sender;
sent <- set_mrs receiver buf msg;
set_message_info receiver $ MI sent 0 0 label;
as_user receiver $ setRegister badge_register badge
od \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>fault f x. \<lbrace>?B3 fault f x\<rbrace> case x of (label, msg) \<Rightarrow> do sent <- set_mrs receiver buf msg;
set_message_info receiver $ MI sent 0 0 label;
as_user receiver $ setRegister badge_register badge
od \<lbrace>\<lambda>_. globals_equiv s\<rbrace>
 2. \<And>fault f. \<lbrace>?B2 fault f\<rbrace> make_fault_msg f sender \<lbrace>?B3 fault f\<rbrace>
 3. \<And>fault. \<lbrace>?B1 fault\<rbrace> case fault of None \<Rightarrow> fail | Some f \<Rightarrow> return f \<lbrace>?B2 fault\<rbrace>
 4. \<lbrace>?Q\<rbrace> thread_get tcb_fault sender \<lbrace>?B1\<rbrace>
 5. \<And>sa. (globals_equiv s and valid_arch_state and (\<lambda>sa. receiver \<noteq> idle_thread sa)) sa \<Longrightarrow> ?Q sa proof (prove)
goal (5 subgoals):
 1. \<And>fault f x. \<lbrace>?B3 fault f x\<rbrace> do sent <- set_mrs receiver buf (snd x);
y <- set_message_info receiver (MI sent 0 0 (fst x));
as_user receiver (setRegister badge_register badge)
od \<lbrace>\<lambda>_. globals_equiv s\<rbrace>
 2. \<And>fault f. \<lbrace>?B2 fault f\<rbrace> make_fault_msg f sender \<lbrace>?B3 fault f\<rbrace>
 3. \<And>fault. \<lbrace>?B1 fault\<rbrace> case fault of None \<Rightarrow> fail | Some f \<Rightarrow> return f \<lbrace>?B2 fault\<rbrace>
 4. \<lbrace>?Q\<rbrace> thread_get tcb_fault sender \<lbrace>?B1\<rbrace>
 5. \<And>sa. (globals_equiv s and valid_arch_state and (\<lambda>sa. receiver \<noteq> idle_thread sa)) sa \<Longrightarrow> ?Q sa proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> thread_get tcb_fault sender \<lbrace>\<lambda>fault sa. (fault = None \<longrightarrow> True) \<and> (\<forall>x. fault = Some x \<longrightarrow> globals_equiv s sa \<and> valid_arch_state sa \<and> receiver \<noteq> idle_thread sa \<and> valid_arch_state sa \<and> receiver \<noteq> idle_thread sa \<and> valid_arch_state sa \<and> receiver \<noteq> idle_thread sa)\<rbrace>
 2. \<And>sa. (globals_equiv s and valid_arch_state and (\<lambda>sa. receiver \<noteq> idle_thread sa)) sa \<Longrightarrow> ?Q sa proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> thread_get tcb_fault sender \<lbrace>\<lambda>fault sa. (\<exists>x. fault = Some x) \<longrightarrow> globals_equiv s sa \<and> valid_arch_state sa \<and> receiver \<noteq> idle_thread sa \<and> valid_arch_state sa \<and> receiver \<noteq> idle_thread sa \<and> valid_arch_state sa \<and> receiver \<noteq> idle_thread sa\<rbrace>
 2. \<And>sa. (globals_equiv s and valid_arch_state and (\<lambda>sa. receiver \<noteq> idle_thread sa)) sa \<Longrightarrow> ?Q sa proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> thread_get tcb_fault sender \<lbrace>\<lambda>rv sa. globals_equiv s sa \<and> valid_arch_state sa \<and> receiver \<noteq> idle_thread sa \<and> valid_arch_state sa \<and> receiver \<noteq> idle_thread sa \<and> valid_arch_state sa \<and> receiver \<noteq> idle_thread sa\<rbrace>
 2. \<And>sa. (globals_equiv s and valid_arch_state and (\<lambda>sa. receiver \<noteq> idle_thread sa)) sa \<Longrightarrow> ?Q sa proof (prove)
goal:
No subgoals!