theory Ipc_AI

lemma sai_invs[wp]:
  "\<lbrace>invs and ex_nonz_cap_to ntfn\<rbrace> send_signal ntfn bdg \<lbrace>\<lambda>rv. invs\<rbrace>" apply (simp add: send_signal_def) apply (rule hoare_seq_ext [OF _ get_simple_ko_sp]) apply (case_tac "ntfn_obj ntfna", simp_all) apply (case_tac "ntfn_bound_tcb ntfna", simp_all) apply (wp set_ntfn_minor_invs) apply (clarsimp simp: obj_at_def is_ntfn invs_def valid_pspace_def
                           valid_state_def valid_obj_def valid_ntfn_def) apply (rule hoare_seq_ext [OF _ gts_sp]) apply (rule hoare_pre) apply (rule hoare_vcg_if_split) apply (wp sts_invs_minor | clarsimp split: thread_state.splits)+ apply (rule hoare_vcg_conj_lift[OF hoare_strengthen_post[OF cancel_ipc_simple]]) apply (fastforce elim: st_tcb_weakenE) apply (wp cancel_ipc_ex_nonz_cap_to_tcb cancel_ipc_simple2 set_ntfn_minor_invs
                hoare_disjI2 cancel_ipc_cte_wp_at_not_reply_state)+ apply (clarsimp simp: invs_def valid_state_def valid_pspace_def
                          st_tcb_at_tcb_at receive_blocked_def
                          st_tcb_at_reply_cap_valid) apply (rule conjI, rule impI) apply (clarsimp simp: idle_no_ex_cap st_tcb_at_reply_cap_valid
                    split: thread_state.splits) apply (frule (1) st_tcb_ex_cap, fastforce split:thread_state.splits) apply (auto simp: st_tcb_at_def obj_at_def idle_no_ex_cap)[1] apply (clarsimp simp: valid_ntfn_def obj_at_def is_ntfn_def st_tcb_at_def is_tcb
                   elim!: obj_at_weakenE) apply (wp update_waiting_invs, simp) apply blast apply (wp set_ntfn_minor_invs, simp) apply (clarsimp simp add: valid_ntfn_def obj_at_def is_ntfn_def
                     elim!: obj_at_weakenE) apply (erule(1) valid_objsE[OF invs_valid_objs]) apply (clarsimp simp: valid_obj_def valid_ntfn_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and ex_nonz_cap_to ntfn\<rbrace> send_signal ntfn bdg \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and ex_nonz_cap_to ntfn\<rbrace> do ntfna <- get_notification ntfn;
case ntfn_obj ntfna of IdleNtfn \<Rightarrow> case ntfn_bound_tcb ntfna of None \<Rightarrow> set_notification ntfn $ ntfn_set_obj ntfna (ActiveNtfn bdg) | Some tcb \<Rightarrow> do st <- get_thread_state tcb;
if receive_blocked st then do cancel_ipc tcb;
set_thread_state tcb Running;
as_user tcb $ setRegister badge_register bdg;
do_extended_op (possible_switch_to tcb)
od else set_notification ntfn $ ntfn_set_obj ntfna (ActiveNtfn bdg)
od | WaitingNtfn queue \<Rightarrow> update_waiting_ntfn ntfn queue (ntfn_bound_tcb ntfna) bdg | ActiveNtfn badge' \<Rightarrow> set_notification ntfn $ ntfn_set_obj ntfna $ ActiveNtfn (combine_ntfn_badges bdg badge')
od \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfna. \<lbrace>ko_at (Notification ntfna) ntfn and (invs and ex_nonz_cap_to ntfn)\<rbrace> case ntfn_obj ntfna of IdleNtfn \<Rightarrow> case ntfn_bound_tcb ntfna of None \<Rightarrow> set_notification ntfn $ ntfn_set_obj ntfna (ActiveNtfn bdg) | Some tcb \<Rightarrow> do st <- get_thread_state tcb;
if receive_blocked st then do cancel_ipc tcb;
set_thread_state tcb Running;
as_user tcb $ setRegister badge_register bdg;
do_extended_op (possible_switch_to tcb)
od else set_notification ntfn $ ntfn_set_obj ntfna (ActiveNtfn bdg)
od | WaitingNtfn queue \<Rightarrow> update_waiting_ntfn ntfn queue (ntfn_bound_tcb ntfna) bdg | ActiveNtfn badge' \<Rightarrow> set_notification ntfn $ ntfn_set_obj ntfna $ ActiveNtfn (combine_ntfn_badges bdg badge') \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ntfna. ntfn_obj ntfna = IdleNtfn \<Longrightarrow> \<lbrace>ko_at (Notification ntfna) ntfn and (invs and ex_nonz_cap_to ntfn)\<rbrace> case ntfn_bound_tcb ntfna of None \<Rightarrow> set_notification ntfn $ ntfn_set_obj ntfna (ActiveNtfn bdg) | Some tcb \<Rightarrow> do st <- get_thread_state tcb;
if receive_blocked st then do cancel_ipc tcb;
set_thread_state tcb Running;
as_user tcb $ setRegister badge_register bdg;
do_extended_op (possible_switch_to tcb)
od else set_notification ntfn $ ntfn_set_obj ntfna (ActiveNtfn bdg)
od \<lbrace>\<lambda>rv. invs\<rbrace>
 2. \<And>ntfna x2. ntfn_obj ntfna = WaitingNtfn x2 \<Longrightarrow> \<lbrace>ko_at (Notification ntfna) ntfn and (invs and ex_nonz_cap_to ntfn)\<rbrace> update_waiting_ntfn ntfn x2 (ntfn_bound_tcb ntfna) bdg \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>ntfna x3. ntfn_obj ntfna = ActiveNtfn x3 \<Longrightarrow> \<lbrace>ko_at (Notification ntfna) ntfn and (invs and ex_nonz_cap_to ntfn)\<rbrace> set_notification ntfn (ntfn_set_obj ntfna (ActiveNtfn (combine_ntfn_badges bdg x3))) \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>ntfna. \<lbrakk>ntfn_obj ntfna = IdleNtfn; ntfn_bound_tcb ntfna = None\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification ntfna) ntfn and (invs and ex_nonz_cap_to ntfn)\<rbrace> set_notification ntfn (ntfn_set_obj ntfna (ActiveNtfn bdg)) \<lbrace>\<lambda>rv. invs\<rbrace>
 2. \<And>ntfna a. \<lbrakk>ntfn_obj ntfna = IdleNtfn; ntfn_bound_tcb ntfna = Some a\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification ntfna) ntfn and (invs and ex_nonz_cap_to ntfn)\<rbrace> do st <- get_thread_state a;
if receive_blocked st then do y <- cancel_ipc a;
y <- set_thread_state a Running;
y <- as_user a (setRegister badge_register bdg);
do_extended_op (possible_switch_to a)
od else set_notification ntfn (ntfn_set_obj ntfna (ActiveNtfn bdg))
od \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>ntfna x2. ntfn_obj ntfna = WaitingNtfn x2 \<Longrightarrow> \<lbrace>ko_at (Notification ntfna) ntfn and (invs and ex_nonz_cap_to ntfn)\<rbrace> update_waiting_ntfn ntfn x2 (ntfn_bound_tcb ntfna) bdg \<lbrace>\<lambda>rv. invs\<rbrace>
 4. \<And>ntfna x3. ntfn_obj ntfna = ActiveNtfn x3 \<Longrightarrow> \<lbrace>ko_at (Notification ntfna) ntfn and (invs and ex_nonz_cap_to ntfn)\<rbrace> set_notification ntfn (ntfn_set_obj ntfna (ActiveNtfn (combine_ntfn_badges bdg x3))) \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>ntfna s. \<lbrakk>ntfn_obj ntfna = IdleNtfn; ntfn_bound_tcb ntfna = None; (ko_at (Notification ntfna) ntfn and (invs and ex_nonz_cap_to ntfn)) s\<rbrakk> \<Longrightarrow> (invs and ntfn_at ntfn and obj_at (\<lambda>ko. refs_of ko = ntfn_q_refs_of (ntfn_obj (ntfn_set_obj ntfna (ActiveNtfn bdg))) \<union> ntfn_bound_refs (ntfn_bound_tcb (ntfn_set_obj ntfna (ActiveNtfn bdg)))) ntfn and valid_ntfn (ntfn_set_obj ntfna (ActiveNtfn bdg)) and (\<lambda>s. \<forall>typ. (idle_thread s, typ) \<notin> ntfn_q_refs_of (ntfn_obj (ntfn_set_obj ntfna (ActiveNtfn bdg)))) and (\<lambda>s. live (Notification (ntfn_set_obj ntfna (ActiveNtfn bdg))) \<longrightarrow> ex_nonz_cap_to ntfn s)) s
 2. \<And>ntfna a. \<lbrakk>ntfn_obj ntfna = IdleNtfn; ntfn_bound_tcb ntfna = Some a\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification ntfna) ntfn and (invs and ex_nonz_cap_to ntfn)\<rbrace> do st <- get_thread_state a;
if receive_blocked st then do y <- cancel_ipc a;
y <- set_thread_state a Running;
y <- as_user a (setRegister badge_register bdg);
do_extended_op (possible_switch_to a)
od else set_notification ntfn (ntfn_set_obj ntfna (ActiveNtfn bdg))
od \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>ntfna x2. ntfn_obj ntfna = WaitingNtfn x2 \<Longrightarrow> \<lbrace>ko_at (Notification ntfna) ntfn and (invs and ex_nonz_cap_to ntfn)\<rbrace> update_waiting_ntfn ntfn x2 (ntfn_bound_tcb ntfna) bdg \<lbrace>\<lambda>rv. invs\<rbrace>
 4. \<And>ntfna x3. ntfn_obj ntfna = ActiveNtfn x3 \<Longrightarrow> \<lbrace>ko_at (Notification ntfna) ntfn and (invs and ex_nonz_cap_to ntfn)\<rbrace> set_notification ntfn (ntfn_set_obj ntfna (ActiveNtfn (combine_ntfn_badges bdg x3))) \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ntfna a. \<lbrakk>ntfn_obj ntfna = IdleNtfn; ntfn_bound_tcb ntfna = Some a\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification ntfna) ntfn and (invs and ex_nonz_cap_to ntfn)\<rbrace> do st <- get_thread_state a;
if receive_blocked st then do y <- cancel_ipc a;
y <- set_thread_state a Running;
y <- as_user a (setRegister badge_register bdg);
do_extended_op (possible_switch_to a)
od else set_notification ntfn (ntfn_set_obj ntfna (ActiveNtfn bdg))
od \<lbrace>\<lambda>rv. invs\<rbrace>
 2. \<And>ntfna x2. ntfn_obj ntfna = WaitingNtfn x2 \<Longrightarrow> \<lbrace>ko_at (Notification ntfna) ntfn and (invs and ex_nonz_cap_to ntfn)\<rbrace> update_waiting_ntfn ntfn x2 (ntfn_bound_tcb ntfna) bdg \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>ntfna x3. ntfn_obj ntfna = ActiveNtfn x3 \<Longrightarrow> \<lbrace>ko_at (Notification ntfna) ntfn and (invs and ex_nonz_cap_to ntfn)\<rbrace> set_notification ntfn (ntfn_set_obj ntfna (ActiveNtfn (combine_ntfn_badges bdg x3))) \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ntfna a st. \<lbrakk>ntfn_obj ntfna = IdleNtfn; ntfn_bound_tcb ntfna = Some a\<rbrakk> \<Longrightarrow> \<lbrace>st_tcb_at ((=) st) a and (ko_at (Notification ntfna) ntfn and (invs and ex_nonz_cap_to ntfn))\<rbrace> if receive_blocked st then do y <- cancel_ipc a;
y <- set_thread_state a Running;
y <- as_user a (setRegister badge_register bdg);
do_extended_op (possible_switch_to a)
od else set_notification ntfn (ntfn_set_obj ntfna (ActiveNtfn bdg)) \<lbrace>\<lambda>rv. invs\<rbrace>
 2. \<And>ntfna x2. ntfn_obj ntfna = WaitingNtfn x2 \<Longrightarrow> \<lbrace>ko_at (Notification ntfna) ntfn and (invs and ex_nonz_cap_to ntfn)\<rbrace> update_waiting_ntfn ntfn x2 (ntfn_bound_tcb ntfna) bdg \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>ntfna x3. ntfn_obj ntfna = ActiveNtfn x3 \<Longrightarrow> \<lbrace>ko_at (Notification ntfna) ntfn and (invs and ex_nonz_cap_to ntfn)\<rbrace> set_notification ntfn (ntfn_set_obj ntfna (ActiveNtfn (combine_ntfn_badges bdg x3))) \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>ntfna a st. \<lbrakk>ntfn_obj ntfna = IdleNtfn; ntfn_bound_tcb ntfna = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?Q40 ntfna a st\<rbrace> if receive_blocked st then do y <- cancel_ipc a;
y <- set_thread_state a Running;
y <- as_user a (setRegister badge_register bdg);
do_extended_op (possible_switch_to a)
od else set_notification ntfn (ntfn_set_obj ntfna (ActiveNtfn bdg)) \<lbrace>\<lambda>rv. invs\<rbrace>
 2. \<And>ntfna a st s. \<lbrakk>ntfn_obj ntfna = IdleNtfn; ntfn_bound_tcb ntfna = Some a; (st_tcb_at ((=) st) a and (ko_at (Notification ntfna) ntfn and (invs and ex_nonz_cap_to ntfn))) s\<rbrakk> \<Longrightarrow> ?Q40 ntfna a st s
 3. \<And>ntfna x2. ntfn_obj ntfna = WaitingNtfn x2 \<Longrightarrow> \<lbrace>ko_at (Notification ntfna) ntfn and (invs and ex_nonz_cap_to ntfn)\<rbrace> update_waiting_ntfn ntfn x2 (ntfn_bound_tcb ntfna) bdg \<lbrace>\<lambda>rv. invs\<rbrace>
 4. \<And>ntfna x3. ntfn_obj ntfna = ActiveNtfn x3 \<Longrightarrow> \<lbrace>ko_at (Notification ntfna) ntfn and (invs and ex_nonz_cap_to ntfn)\<rbrace> set_notification ntfn (ntfn_set_obj ntfna (ActiveNtfn (combine_ntfn_badges bdg x3))) \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>ntfn a st. \<lbrakk>ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some a; receive_blocked st\<rbrakk> \<Longrightarrow> \<lbrace>?Q43 ntfn a st\<rbrace> do y <- cancel_ipc a;
y <- set_thread_state a Running;
y <- as_user a (setRegister badge_register bdg);
do_extended_op (possible_switch_to a)
od \<lbrace>\<lambda>rv. invs\<rbrace>
 2. \<And>ntfna a st. \<lbrakk>ntfn_obj ntfna = IdleNtfn; ntfn_bound_tcb ntfna = Some a; \<not> receive_blocked st\<rbrakk> \<Longrightarrow> \<lbrace>?R43 ntfna a st\<rbrace> set_notification ntfn (ntfn_set_obj ntfna (ActiveNtfn bdg)) \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>ntfna a st s. \<lbrakk>ntfn_obj ntfna = IdleNtfn; ntfn_bound_tcb ntfna = Some a; (st_tcb_at ((=) st) a and (ko_at (Notification ntfna) ntfn and (invs and ex_nonz_cap_to ntfn))) s\<rbrakk> \<Longrightarrow> (receive_blocked st \<longrightarrow> ?Q43 ntfna a st s) \<and> (\<not> receive_blocked st \<longrightarrow> ?R43 ntfna a st s)
 4. \<And>ntfna x2. ntfn_obj ntfna = WaitingNtfn x2 \<Longrightarrow> \<lbrace>ko_at (Notification ntfna) ntfn and (invs and ex_nonz_cap_to ntfn)\<rbrace> update_waiting_ntfn ntfn x2 (ntfn_bound_tcb ntfna) bdg \<lbrace>\<lambda>rv. invs\<rbrace>
 5. \<And>ntfna x3. ntfn_obj ntfna = ActiveNtfn x3 \<Longrightarrow> \<lbrace>ko_at (Notification ntfna) ntfn and (invs and ex_nonz_cap_to ntfn)\<rbrace> set_notification ntfn (ntfn_set_obj ntfna (ActiveNtfn (combine_ntfn_badges bdg x3))) \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>ntfn a st. \<lbrakk>ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some a; receive_blocked st\<rbrakk> \<Longrightarrow> \<lbrace>?Q43 ntfn a st\<rbrace> cancel_ipc a \<lbrace>\<lambda>y s. st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = {}) a s \<and> ex_nonz_cap_to a s \<and> a \<noteq> idle_thread s \<and> (st_tcb_at (\<lambda>st. st \<noteq> Inactive \<and> st \<noteq> IdleThreadState) a s \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = a) (a, tcb_cnode_index 2) s) \<and> \<not> has_reply_cap a s \<and> invs s\<rbrace>
 2. \<And>ntfna a st. \<lbrakk>ntfn_obj ntfna = IdleNtfn; ntfn_bound_tcb ntfna = Some a; \<not> receive_blocked st\<rbrakk> \<Longrightarrow> \<lbrace>?R43 ntfna a st\<rbrace> set_notification ntfn (ntfn_set_obj ntfna (ActiveNtfn bdg)) \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>ntfna a st s. \<lbrakk>ntfn_obj ntfna = IdleNtfn; ntfn_bound_tcb ntfna = Some a; (st_tcb_at ((=) st) a and (ko_at (Notification ntfna) ntfn and (invs and ex_nonz_cap_to ntfn))) s\<rbrakk> \<Longrightarrow> (receive_blocked st \<longrightarrow> ?Q43 ntfna a st s) \<and> (\<not> receive_blocked st \<longrightarrow> ?R43 ntfna a st s)
 4. \<And>ntfna x2. ntfn_obj ntfna = WaitingNtfn x2 \<Longrightarrow> \<lbrace>ko_at (Notification ntfna) ntfn and (invs and ex_nonz_cap_to ntfn)\<rbrace> update_waiting_ntfn ntfn x2 (ntfn_bound_tcb ntfna) bdg \<lbrace>\<lambda>rv. invs\<rbrace>
 5. \<And>ntfna x3. ntfn_obj ntfna = ActiveNtfn x3 \<Longrightarrow> \<lbrace>ko_at (Notification ntfna) ntfn and (invs and ex_nonz_cap_to ntfn)\<rbrace> set_notification ntfn (ntfn_set_obj ntfna (ActiveNtfn (combine_ntfn_badges bdg x3))) \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>ntfn a st y s. \<lbrakk>ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some a; receive_blocked st; st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) a s\<rbrakk> \<Longrightarrow> st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = {}) a s
 2. \<And>ntfn a st. \<lbrakk>ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some a; receive_blocked st\<rbrakk> \<Longrightarrow> \<lbrace>?P'83 ntfn a st\<rbrace> cancel_ipc a \<lbrace>\<lambda>rv s. ex_nonz_cap_to a s \<and> a \<noteq> idle_thread s \<and> (st_tcb_at (\<lambda>st. st \<noteq> Inactive \<and> st \<noteq> IdleThreadState) a s \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = a) (a, tcb_cnode_index 2) s) \<and> \<not> has_reply_cap a s \<and> invs s\<rbrace>
 3. \<And>ntfna a st. \<lbrakk>ntfn_obj ntfna = IdleNtfn; ntfn_bound_tcb ntfna = Some a; \<not> receive_blocked st\<rbrakk> \<Longrightarrow> \<lbrace>?R43 ntfna a st\<rbrace> set_notification ntfn (ntfn_set_obj ntfna (ActiveNtfn bdg)) \<lbrace>\<lambda>rv. invs\<rbrace>
 4. \<And>ntfna a st s. \<lbrakk>ntfn_obj ntfna = IdleNtfn; ntfn_bound_tcb ntfna = Some a; (st_tcb_at ((=) st) a and (ko_at (Notification ntfna) ntfn and (invs and ex_nonz_cap_to ntfn))) s\<rbrakk> \<Longrightarrow> (receive_blocked st \<longrightarrow> True \<and> ?P'83 ntfna a st s) \<and> (\<not> receive_blocked st \<longrightarrow> ?R43 ntfna a st s)
 5. \<And>ntfna x2. ntfn_obj ntfna = WaitingNtfn x2 \<Longrightarrow> \<lbrace>ko_at (Notification ntfna) ntfn and (invs and ex_nonz_cap_to ntfn)\<rbrace> update_waiting_ntfn ntfn x2 (ntfn_bound_tcb ntfna) bdg \<lbrace>\<lambda>rv. invs\<rbrace>
 6. \<And>ntfna x3. ntfn_obj ntfna = ActiveNtfn x3 \<Longrightarrow> \<lbrace>ko_at (Notification ntfna) ntfn and (invs and ex_nonz_cap_to ntfn)\<rbrace> set_notification ntfn (ntfn_set_obj ntfna (ActiveNtfn (combine_ntfn_badges bdg x3))) \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>ntfn a st. \<lbrakk>ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some a; receive_blocked st\<rbrakk> \<Longrightarrow> \<lbrace>?P'83 ntfn a st\<rbrace> cancel_ipc a \<lbrace>\<lambda>rv s. ex_nonz_cap_to a s \<and> a \<noteq> idle_thread s \<and> (st_tcb_at (\<lambda>st. st \<noteq> Inactive \<and> st \<noteq> IdleThreadState) a s \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = a) (a, tcb_cnode_index 2) s) \<and> \<not> has_reply_cap a s \<and> invs s\<rbrace>
 2. \<And>ntfna a st. \<lbrakk>ntfn_obj ntfna = IdleNtfn; ntfn_bound_tcb ntfna = Some a; \<not> receive_blocked st\<rbrakk> \<Longrightarrow> \<lbrace>?R43 ntfna a st\<rbrace> set_notification ntfn (ntfn_set_obj ntfna (ActiveNtfn bdg)) \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>ntfna a st s. \<lbrakk>ntfn_obj ntfna = IdleNtfn; ntfn_bound_tcb ntfna = Some a; (st_tcb_at ((=) st) a and (ko_at (Notification ntfna) ntfn and (invs and ex_nonz_cap_to ntfn))) s\<rbrakk> \<Longrightarrow> (receive_blocked st \<longrightarrow> True \<and> ?P'83 ntfna a st s) \<and> (\<not> receive_blocked st \<longrightarrow> ?R43 ntfna a st s)
 4. \<And>ntfna x2. ntfn_obj ntfna = WaitingNtfn x2 \<Longrightarrow> \<lbrace>ko_at (Notification ntfna) ntfn and (invs and ex_nonz_cap_to ntfn)\<rbrace> update_waiting_ntfn ntfn x2 (ntfn_bound_tcb ntfna) bdg \<lbrace>\<lambda>rv. invs\<rbrace>
 5. \<And>ntfna x3. ntfn_obj ntfna = ActiveNtfn x3 \<Longrightarrow> \<lbrace>ko_at (Notification ntfna) ntfn and (invs and ex_nonz_cap_to ntfn)\<rbrace> set_notification ntfn (ntfn_set_obj ntfna (ActiveNtfn (combine_ntfn_badges bdg x3))) \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ntfna a st s. \<lbrakk>ntfn_obj ntfna = IdleNtfn; ntfn_bound_tcb ntfna = Some a; (st_tcb_at ((=) st) a and (ko_at (Notification ntfna) ntfn and (invs and ex_nonz_cap_to ntfn))) s\<rbrakk> \<Longrightarrow> (receive_blocked st \<longrightarrow> True \<and> (ex_nonz_cap_to a s \<and> valid_objs s \<and> tcb_at a s) \<and> a \<noteq> idle_thread s \<and> (st_tcb_at ((\<noteq>) BlockedOnReply) a and cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = a) (a, tcb_cnode_index 2)) s \<and> (invs and tcb_at a) s \<and> invs s) \<and> (\<not> receive_blocked st \<longrightarrow> (invs and ntfn_at ntfn and obj_at (\<lambda>ko. refs_of ko = ntfn_q_refs_of (ntfn_obj (ntfn_set_obj ntfna (ActiveNtfn bdg))) \<union> ntfn_bound_refs (ntfn_bound_tcb (ntfn_set_obj ntfna (ActiveNtfn bdg)))) ntfn and valid_ntfn (ntfn_set_obj ntfna (ActiveNtfn bdg)) and (\<lambda>s. \<forall>typ. (idle_thread s, typ) \<notin> ntfn_q_refs_of (ntfn_obj (ntfn_set_obj ntfna (ActiveNtfn bdg)))) and (\<lambda>s. live (Notification (ntfn_set_obj ntfna (ActiveNtfn bdg))) \<longrightarrow> ex_nonz_cap_to ntfn s)) s)
 2. \<And>ntfna x2. ntfn_obj ntfna = WaitingNtfn x2 \<Longrightarrow> \<lbrace>ko_at (Notification ntfna) ntfn and (invs and ex_nonz_cap_to ntfn)\<rbrace> update_waiting_ntfn ntfn x2 (ntfn_bound_tcb ntfna) bdg \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>ntfna x3. ntfn_obj ntfna = ActiveNtfn x3 \<Longrightarrow> \<lbrace>ko_at (Notification ntfna) ntfn and (invs and ex_nonz_cap_to ntfn)\<rbrace> set_notification ntfn (ntfn_set_obj ntfna (ActiveNtfn (combine_ntfn_badges bdg x3))) \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ntfna a st s. \<lbrakk>ntfn_obj ntfna = IdleNtfn; ntfn_bound_tcb ntfna = Some a; st_tcb_at ((=) st) a s; ko_at (Notification ntfna) ntfn s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ex_nonz_cap_to ntfn s\<rbrakk> \<Longrightarrow> ((case st of BlockedOnReceive x xa \<Rightarrow> True | _ \<Rightarrow> False) \<longrightarrow> ex_nonz_cap_to a s \<and> a \<noteq> idle_thread s \<and> st_tcb_at ((\<noteq>) BlockedOnReply) a s \<and> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = a) (a, tcb_cnode_index 2) s) \<and> (\<not> (case st of BlockedOnReceive x xa \<Rightarrow> True | _ \<Rightarrow> False) \<longrightarrow> ntfn_at ntfn s \<and> obj_at (\<lambda>ko. refs_of ko = {(a, NTFNBound)}) ntfn s \<and> valid_ntfn (ntfn_set_obj ntfna (ActiveNtfn bdg)) s)
 2. \<And>ntfna x2. ntfn_obj ntfna = WaitingNtfn x2 \<Longrightarrow> \<lbrace>ko_at (Notification ntfna) ntfn and (invs and ex_nonz_cap_to ntfn)\<rbrace> update_waiting_ntfn ntfn x2 (ntfn_bound_tcb ntfna) bdg \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>ntfna x3. ntfn_obj ntfna = ActiveNtfn x3 \<Longrightarrow> \<lbrace>ko_at (Notification ntfna) ntfn and (invs and ex_nonz_cap_to ntfn)\<rbrace> set_notification ntfn (ntfn_set_obj ntfna (ActiveNtfn (combine_ntfn_badges bdg x3))) \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>ntfna a st s. \<lbrakk>ntfn_obj ntfna = IdleNtfn; ntfn_bound_tcb ntfna = Some a; st_tcb_at ((=) st) a s; ko_at (Notification ntfna) ntfn s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ex_nonz_cap_to ntfn s; case st of BlockedOnReceive x xa \<Rightarrow> True | _ \<Rightarrow> False\<rbrakk> \<Longrightarrow> ex_nonz_cap_to a s \<and> a \<noteq> idle_thread s \<and> st_tcb_at ((\<noteq>) BlockedOnReply) a s \<and> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = a) (a, tcb_cnode_index 2) s
 2. \<And>ntfna a st s. \<lbrakk>ntfn_obj ntfna = IdleNtfn; ntfn_bound_tcb ntfna = Some a; st_tcb_at ((=) st) a s; ko_at (Notification ntfna) ntfn s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ex_nonz_cap_to ntfn s\<rbrakk> \<Longrightarrow> \<not> (case st of BlockedOnReceive x xa \<Rightarrow> True | _ \<Rightarrow> False) \<longrightarrow> ntfn_at ntfn s \<and> obj_at (\<lambda>ko. refs_of ko = {(a, NTFNBound)}) ntfn s \<and> valid_ntfn (ntfn_set_obj ntfna (ActiveNtfn bdg)) s
 3. \<And>ntfna x2. ntfn_obj ntfna = WaitingNtfn x2 \<Longrightarrow> \<lbrace>ko_at (Notification ntfna) ntfn and (invs and ex_nonz_cap_to ntfn)\<rbrace> update_waiting_ntfn ntfn x2 (ntfn_bound_tcb ntfna) bdg \<lbrace>\<lambda>rv. invs\<rbrace>
 4. \<And>ntfna x3. ntfn_obj ntfna = ActiveNtfn x3 \<Longrightarrow> \<lbrace>ko_at (Notification ntfna) ntfn and (invs and ex_nonz_cap_to ntfn)\<rbrace> set_notification ntfn (ntfn_set_obj ntfna (ActiveNtfn (combine_ntfn_badges bdg x3))) \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>ntfna a s x41 x42. \<lbrakk>ntfn_obj ntfna = IdleNtfn; ntfn_bound_tcb ntfna = Some a; st_tcb_at ((=) (BlockedOnReceive x41 x42)) a s; ko_at (Notification ntfna) ntfn s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ex_nonz_cap_to ntfn s\<rbrakk> \<Longrightarrow> ex_nonz_cap_to a s \<and> a \<noteq> idle_thread s \<and> st_tcb_at ((\<noteq>) BlockedOnReply) a s
 2. \<And>ntfna a st s. \<lbrakk>ntfn_obj ntfna = IdleNtfn; ntfn_bound_tcb ntfna = Some a; st_tcb_at ((=) st) a s; ko_at (Notification ntfna) ntfn s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ex_nonz_cap_to ntfn s\<rbrakk> \<Longrightarrow> \<not> (case st of BlockedOnReceive x xa \<Rightarrow> True | _ \<Rightarrow> False) \<longrightarrow> ntfn_at ntfn s \<and> obj_at (\<lambda>ko. refs_of ko = {(a, NTFNBound)}) ntfn s \<and> valid_ntfn (ntfn_set_obj ntfna (ActiveNtfn bdg)) s
 3. \<And>ntfna x2. ntfn_obj ntfna = WaitingNtfn x2 \<Longrightarrow> \<lbrace>ko_at (Notification ntfna) ntfn and (invs and ex_nonz_cap_to ntfn)\<rbrace> update_waiting_ntfn ntfn x2 (ntfn_bound_tcb ntfna) bdg \<lbrace>\<lambda>rv. invs\<rbrace>
 4. \<And>ntfna x3. ntfn_obj ntfna = ActiveNtfn x3 \<Longrightarrow> \<lbrace>ko_at (Notification ntfna) ntfn and (invs and ex_nonz_cap_to ntfn)\<rbrace> set_notification ntfn (ntfn_set_obj ntfna (ActiveNtfn (combine_ntfn_badges bdg x3))) \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>ntfna a s x41 x42. \<lbrakk>ntfn_obj ntfna = IdleNtfn; ntfn_bound_tcb ntfna = Some a; st_tcb_at ((=) (BlockedOnReceive x41 x42)) a s; ko_at (Notification ntfna) ntfn s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ex_nonz_cap_to ntfn s; ex_nonz_cap_to a s\<rbrakk> \<Longrightarrow> ex_nonz_cap_to a s \<and> a \<noteq> idle_thread s \<and> st_tcb_at ((\<noteq>) BlockedOnReply) a s
 2. \<And>ntfna a st s. \<lbrakk>ntfn_obj ntfna = IdleNtfn; ntfn_bound_tcb ntfna = Some a; st_tcb_at ((=) st) a s; ko_at (Notification ntfna) ntfn s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ex_nonz_cap_to ntfn s\<rbrakk> \<Longrightarrow> \<not> (case st of BlockedOnReceive x xa \<Rightarrow> True | _ \<Rightarrow> False) \<longrightarrow> ntfn_at ntfn s \<and> obj_at (\<lambda>ko. refs_of ko = {(a, NTFNBound)}) ntfn s \<and> valid_ntfn (ntfn_set_obj ntfna (ActiveNtfn bdg)) s
 3. \<And>ntfna x2. ntfn_obj ntfna = WaitingNtfn x2 \<Longrightarrow> \<lbrace>ko_at (Notification ntfna) ntfn and (invs and ex_nonz_cap_to ntfn)\<rbrace> update_waiting_ntfn ntfn x2 (ntfn_bound_tcb ntfna) bdg \<lbrace>\<lambda>rv. invs\<rbrace>
 4. \<And>ntfna x3. ntfn_obj ntfna = ActiveNtfn x3 \<Longrightarrow> \<lbrace>ko_at (Notification ntfna) ntfn and (invs and ex_nonz_cap_to ntfn)\<rbrace> set_notification ntfn (ntfn_set_obj ntfna (ActiveNtfn (combine_ntfn_badges bdg x3))) \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ntfna a st s. \<lbrakk>ntfn_obj ntfna = IdleNtfn; ntfn_bound_tcb ntfna = Some a; st_tcb_at ((=) st) a s; ko_at (Notification ntfna) ntfn s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ex_nonz_cap_to ntfn s\<rbrakk> \<Longrightarrow> \<not> (case st of BlockedOnReceive x xa \<Rightarrow> True | _ \<Rightarrow> False) \<longrightarrow> ntfn_at ntfn s \<and> obj_at (\<lambda>ko. refs_of ko = {(a, NTFNBound)}) ntfn s \<and> valid_ntfn (ntfn_set_obj ntfna (ActiveNtfn bdg)) s
 2. \<And>ntfna x2. ntfn_obj ntfna = WaitingNtfn x2 \<Longrightarrow> \<lbrace>ko_at (Notification ntfna) ntfn and (invs and ex_nonz_cap_to ntfn)\<rbrace> update_waiting_ntfn ntfn x2 (ntfn_bound_tcb ntfna) bdg \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>ntfna x3. ntfn_obj ntfna = ActiveNtfn x3 \<Longrightarrow> \<lbrace>ko_at (Notification ntfna) ntfn and (invs and ex_nonz_cap_to ntfn)\<rbrace> set_notification ntfn (ntfn_set_obj ntfna (ActiveNtfn (combine_ntfn_badges bdg x3))) \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ntfna x2. ntfn_obj ntfna = WaitingNtfn x2 \<Longrightarrow> \<lbrace>ko_at (Notification ntfna) ntfn and (invs and ex_nonz_cap_to ntfn)\<rbrace> update_waiting_ntfn ntfn x2 (ntfn_bound_tcb ntfna) bdg \<lbrace>\<lambda>rv. invs\<rbrace>
 2. \<And>ntfna x3. ntfn_obj ntfna = ActiveNtfn x3 \<Longrightarrow> \<lbrace>ko_at (Notification ntfna) ntfn and (invs and ex_nonz_cap_to ntfn)\<rbrace> set_notification ntfn (ntfn_set_obj ntfna (ActiveNtfn (combine_ntfn_badges bdg x3))) \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ntfna x2 s. \<lbrakk>ntfn_obj ntfna = WaitingNtfn x2; ko_at (Notification ntfna) ntfn s \<and> invs s \<and> ex_nonz_cap_to ntfn s\<rbrakk> \<Longrightarrow> ko_at (Notification (?ntfn229 ntfna x2)) ntfn s \<and> ntfn_obj (?ntfn229 ntfna x2) = WaitingNtfn x2 \<and> ntfn_bound_tcb (?ntfn229 ntfna x2) = ntfn_bound_tcb ntfna
 2. \<And>ntfna x3. ntfn_obj ntfna = ActiveNtfn x3 \<Longrightarrow> \<lbrace>ko_at (Notification ntfna) ntfn and (invs and ex_nonz_cap_to ntfn)\<rbrace> set_notification ntfn (ntfn_set_obj ntfna (ActiveNtfn (combine_ntfn_badges bdg x3))) \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfna x3. ntfn_obj ntfna = ActiveNtfn x3 \<Longrightarrow> \<lbrace>ko_at (Notification ntfna) ntfn and (invs and ex_nonz_cap_to ntfn)\<rbrace> set_notification ntfn (ntfn_set_obj ntfna (ActiveNtfn (combine_ntfn_badges bdg x3))) \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfna x3 s. \<lbrakk>ntfn_obj ntfna = ActiveNtfn x3; ko_at (Notification ntfna) ntfn s \<and> invs s \<and> ex_nonz_cap_to ntfn s\<rbrakk> \<Longrightarrow> ntfn_at ntfn s \<and> obj_at (\<lambda>ko. refs_of ko = ntfn_bound_refs (ntfn_bound_tcb ntfna)) ntfn s \<and> valid_ntfn (ntfn_set_obj ntfna (ActiveNtfn (combine_ntfn_badges bdg x3))) s proof (prove)
goal (1 subgoal):
 1. \<And>ntfna x3 s. \<lbrakk>ntfn_obj ntfna = ActiveNtfn x3; kheap s ntfn = Some (Notification ntfna); invs s; ex_nonz_cap_to ntfn s\<rbrakk> \<Longrightarrow> valid_bound_tcb (ntfn_bound_tcb ntfna) s proof (prove)
goal (1 subgoal):
 1. \<And>ntfna x3 s. \<lbrakk>ntfn_obj ntfna = ActiveNtfn x3; kheap s ntfn = Some (Notification ntfna); ex_nonz_cap_to ntfn s; valid_obj ntfn (Notification ntfna) s\<rbrakk> \<Longrightarrow> valid_bound_tcb (ntfn_bound_tcb ntfna) s proof (prove)
goal:
No subgoals!