theory Ipc_AC

lemma receive_signal_integrity_autarch:
  "\<lbrace>integrity aag X st and pas_refined aag and valid_objs and
    K ((\<forall>ntfnptr \<in> obj_refs_ac cap. aag_has_auth_to aag Receive ntfnptr) \<and> is_subject aag thread)\<rbrace>
   receive_signal thread cap is_blocking
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (simp add: receive_signal_def) apply (cases cap, simp_all) apply (rule hoare_seq_ext [OF _ get_simple_ko_sp]) apply (wpsimp wp: set_notification_respects[where auth=Receive]
                    set_thread_state_integrity_autarch as_user_integrity_autarch
              simp: do_nbrecv_failed_transfer_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and valid_objs and K ((\<forall>ntfnptr\<in>obj_refs_ac cap. (pasSubject aag, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag) \<and> is_subject aag thread)\<rbrace> receive_signal thread cap is_blocking \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and valid_objs and (\<lambda>y. (\<forall>ntfnptr\<in>obj_refs_ac cap. (pasSubject aag, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag) \<and> is_subject aag thread)\<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_nbrecv_failed_transfer thread | 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_nbrecv_failed_transfer thread | ActiveNtfn badge \<Rightarrow> do as_user thread $ setRegister badge_register badge;
set_notification ntfnptr $ ntfn_set_obj ntfn IdleNtfn
od
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x41 x42 x43. cap = NotificationCap x41 x42 x43 \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and valid_objs and (\<lambda>y. (pasSubject aag, Receive, pasObjectAbs aag x41) \<in> pasPolicy aag \<and> is_subject aag thread)\<rbrace> do ntfn <- get_notification x41;
case ntfn_obj ntfn of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnNotification x41);
set_notification x41 $ ntfn_set_obj ntfn $ WaitingNtfn [thread]
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnNotification x41);
set_notification x41 $ ntfn_set_obj ntfn $ WaitingNtfn (queue @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | ActiveNtfn badge \<Rightarrow> do as_user thread $ setRegister badge_register badge;
set_notification x41 $ ntfn_set_obj ntfn IdleNtfn
od
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x41 x42 x43 x. cap = NotificationCap x41 x42 x43 \<Longrightarrow> \<lbrace>ko_at (Notification x) x41 and (integrity aag X st and pas_refined aag and valid_objs and (\<lambda>y. (pasSubject aag, Receive, pasObjectAbs aag x41) \<in> pasPolicy aag \<and> is_subject aag thread))\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnNotification x41);
set_notification x41 $ ntfn_set_obj x $ WaitingNtfn [thread]
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnNotification x41);
set_notification x41 $ ntfn_set_obj x $ WaitingNtfn (queue @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | ActiveNtfn badge \<Rightarrow> do as_user thread $ setRegister badge_register badge;
set_notification x41 $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal:
No subgoals!