theory Ipc_IF

lemma receive_signal_globals_equiv:
  "\<lbrace>globals_equiv s and valid_objs and valid_arch_state and valid_global_refs
                    and pspace_distinct and (\<lambda>s. thread \<noteq> idle_thread s)\<rbrace>
   receive_signal thread cap is_blocking
   \<lbrace>\<lambda>_. globals_equiv s\<rbrace>" unfolding receive_signal_def fun_app_def do_nbrecv_failed_transfer_def apply (rule hoare_pre) apply (wpsimp wp: set_notification_globals_equiv set_thread_state_globals_equiv
                     as_user_globals_equiv get_simple_ko_wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and (\<lambda>s. thread \<noteq> idle_thread s)\<rbrace> receive_signal thread cap is_blocking \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and (\<lambda>s. thread \<noteq> idle_thread s)\<rbrace> do ntfnptr <- case cap of NotificationCap ntfnptr badge rights \<Rightarrow> return ntfnptr | _ \<Rightarrow> fail;
ntfn <- get_notification ntfnptr;
case ntfn_obj ntfn of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnNotification ntfnptr);
set_notification ntfnptr (ntfn_set_obj ntfn (WaitingNtfn [thread]))
od | False \<Rightarrow> do as_user thread (setRegister badge_register 0);
return ()
od | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnNotification ntfnptr);
set_notification ntfnptr (ntfn_set_obj ntfn (WaitingNtfn (queue @ [thread])))
od | False \<Rightarrow> do as_user thread (setRegister badge_register 0);
return ()
od | ActiveNtfn badge \<Rightarrow> do as_user thread (setRegister badge_register badge);
set_notification ntfnptr (ntfn_set_obj ntfn IdleNtfn)
od
od \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do ntfnptr <- case cap of NotificationCap ntfnptr badge rights \<Rightarrow> return ntfnptr | _ \<Rightarrow> fail;
ntfn <- get_notification ntfnptr;
case ntfn_obj ntfn of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnNotification ntfnptr);
set_notification ntfnptr (ntfn_set_obj ntfn (WaitingNtfn [thread]))
od | False \<Rightarrow> do as_user thread (setRegister badge_register 0);
return ()
od | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnNotification ntfnptr);
set_notification ntfnptr (ntfn_set_obj ntfn (WaitingNtfn (queue @ [thread])))
od | False \<Rightarrow> do as_user thread (setRegister badge_register 0);
return ()
od | ActiveNtfn badge \<Rightarrow> do as_user thread (setRegister badge_register badge);
set_notification ntfnptr (ntfn_set_obj ntfn IdleNtfn)
od
od \<lbrace>\<lambda>_. globals_equiv s\<rbrace>
 2. \<And>sa. (globals_equiv s and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and (\<lambda>s. thread \<noteq> idle_thread s)) sa \<Longrightarrow> ?Q sa proof (prove)
goal:
No subgoals!