theory Invocation_DP

lemma send_signal_no_pending:
  "\<lbrace>P and no_pending\<rbrace>
     send_signal thread
  \<lbrace>\<lambda>r. P\<rbrace>" apply (simp add: send_signal_def send_signal_bound_def) apply (rule hoare_pre) apply (wp | wpc)+ apply (rule hoare_pre_cont) apply (rule_tac P = "waiters = {}" in hoare_gen_asm) apply (clarsimp simp: option_select_def) apply wp+ apply (rule hoare_pre_cont) apply wp+ apply (clarsimp simp: get_waiting_ntfn_recv_threads_def get_waiting_sync_bound_ntfn_threads_def
                        no_pending_def opt_cap_def) apply (intro allI impI conjI) apply (drule_tac x = x in spec) apply (clarsimp simp: slots_of_def object_slots_def is_pending_cap_def) apply (drule_tac x = x in spec) apply (clarsimp simp: slots_of_def object_slots_def is_pending_cap_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P and no_pending\<rbrace> send_signal thread \<lbrace>\<lambda>r. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P and no_pending\<rbrace> do waiters <- gets (get_waiting_ntfn_recv_threads thread);
t <- option_select waiters;
case t of None \<Rightarrow> return () | Some receiver \<Rightarrow> do_notification_transfer receiver
od \<sqinter> do bound_tcbs <- gets (get_waiting_sync_bound_ntfn_threads thread);
if bound_tcbs \<noteq> {} then do t <- select bound_tcbs;
set_cap (t, tcb_pending_op_slot) NullCap;
do_notification_transfer t
od else return ()
od \<lbrace>\<lambda>r. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do waiters <- gets (get_waiting_ntfn_recv_threads thread);
t <- option_select waiters;
case t of None \<Rightarrow> return () | Some receiver \<Rightarrow> do_notification_transfer receiver
od \<sqinter> do bound_tcbs <- gets (get_waiting_sync_bound_ntfn_threads thread);
if bound_tcbs \<noteq> {} then do t <- select bound_tcbs;
set_cap (t, tcb_pending_op_slot) NullCap;
do_notification_transfer t
od else return ()
od \<lbrace>\<lambda>r. P\<rbrace>
 2. \<And>s. (P and no_pending) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>waiters t x2. t = Some x2 \<Longrightarrow> \<lbrace>?R17 waiters t x2\<rbrace> do_notification_transfer x2 \<lbrace>\<lambda>r. P\<rbrace>
 2. \<And>waiters. \<lbrace>?B5 waiters\<rbrace> option_select waiters \<lbrace>\<lambda>t s. (t = None \<longrightarrow> P s) \<and> (\<forall>x. t = Some x \<longrightarrow> ?R17 waiters t x s)\<rbrace>
 3. \<lbrace>?P4\<rbrace> gets (get_waiting_ntfn_recv_threads thread) \<lbrace>?B5\<rbrace>
 4. \<lbrace>?P'4\<rbrace> do bound_tcbs <- gets (get_waiting_sync_bound_ntfn_threads thread);
if bound_tcbs \<noteq> {} then do t <- select bound_tcbs;
set_cap (t, tcb_pending_op_slot) NullCap;
do_notification_transfer t
od else return ()
od \<lbrace>\<lambda>r. P\<rbrace>
 5. \<And>s. (P and no_pending) s \<Longrightarrow> (?P4 and ?P'4) s proof (prove)
goal (4 subgoals):
 1. \<And>waiters. \<lbrace>?B5 waiters\<rbrace> option_select waiters \<lbrace>\<lambda>t s. (t = None \<longrightarrow> P s) \<and> (\<forall>x. t = Some x \<longrightarrow> False)\<rbrace>
 2. \<lbrace>?P4\<rbrace> gets (get_waiting_ntfn_recv_threads thread) \<lbrace>?B5\<rbrace>
 3. \<lbrace>?P'4\<rbrace> do bound_tcbs <- gets (get_waiting_sync_bound_ntfn_threads thread);
if bound_tcbs \<noteq> {} then do t <- select bound_tcbs;
set_cap (t, tcb_pending_op_slot) NullCap;
do_notification_transfer t
od else return ()
od \<lbrace>\<lambda>r. P\<rbrace>
 4. \<And>s. (P and no_pending) s \<Longrightarrow> (?P4 and ?P'4) s proof (prove)
goal (4 subgoals):
 1. \<And>waiters. waiters = {} \<Longrightarrow> \<lbrace>?P'23 waiters\<rbrace> option_select waiters \<lbrace>\<lambda>t s. (t = None \<longrightarrow> P s) \<and> (\<forall>x. t = Some x \<longrightarrow> False)\<rbrace>
 2. \<lbrace>?P4\<rbrace> gets (get_waiting_ntfn_recv_threads thread) \<lbrace>\<lambda>waiters. ?P'23 waiters and K (waiters = {})\<rbrace>
 3. \<lbrace>?P'4\<rbrace> do bound_tcbs <- gets (get_waiting_sync_bound_ntfn_threads thread);
if bound_tcbs \<noteq> {} then do t <- select bound_tcbs;
set_cap (t, tcb_pending_op_slot) NullCap;
do_notification_transfer t
od else return ()
od \<lbrace>\<lambda>r. P\<rbrace>
 4. \<And>s. (P and no_pending) s \<Longrightarrow> (?P4 and ?P'4) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?P'23 {}\<rbrace> return None \<lbrace>\<lambda>t s. (t = None \<longrightarrow> P s) \<and> t = None\<rbrace>
 2. \<lbrace>?P4\<rbrace> gets (get_waiting_ntfn_recv_threads thread) \<lbrace>\<lambda>waiters. ?P'23 waiters and K (waiters = {})\<rbrace>
 3. \<lbrace>?P'4\<rbrace> do bound_tcbs <- gets (get_waiting_sync_bound_ntfn_threads thread);
if bound_tcbs \<noteq> {} then do t <- select bound_tcbs;
set_cap (t, tcb_pending_op_slot) NullCap;
do_notification_transfer t
od else return ()
od \<lbrace>\<lambda>r. P\<rbrace>
 4. \<And>s. (P and no_pending) s \<Longrightarrow> (?P4 and ?P'4) s proof (prove)
goal (6 subgoals):
 1. \<And>bound_tcbs t x. bound_tcbs \<noteq> {} \<Longrightarrow> \<lbrace>?B38 bound_tcbs t x\<rbrace> do_notification_transfer t \<lbrace>\<lambda>r. P\<rbrace>
 2. \<And>bound_tcbs t. bound_tcbs \<noteq> {} \<Longrightarrow> \<lbrace>?B37 bound_tcbs t\<rbrace> set_cap (t, tcb_pending_op_slot) NullCap \<lbrace>?B38 bound_tcbs t\<rbrace>
 3. \<And>bound_tcbs. bound_tcbs \<noteq> {} \<Longrightarrow> \<lbrace>?Q36 bound_tcbs\<rbrace> select bound_tcbs \<lbrace>?B37 bound_tcbs\<rbrace>
 4. \<And>bound_tcbs. \<not> bound_tcbs \<noteq> {} \<Longrightarrow> \<lbrace>?R36 bound_tcbs\<rbrace> return () \<lbrace>\<lambda>r. P\<rbrace>
 5. \<lbrace>?P'4\<rbrace> gets (get_waiting_sync_bound_ntfn_threads thread) \<lbrace>\<lambda>bound_tcbs s. (bound_tcbs \<noteq> {} \<longrightarrow> ?Q36 bound_tcbs s) \<and> (\<not> bound_tcbs \<noteq> {} \<longrightarrow> ?R36 bound_tcbs s)\<rbrace>
 6. \<And>s. (P and no_pending) s \<Longrightarrow> ((\<lambda>s. ((\<lambda>a. (None = None \<longrightarrow> P a) \<and> None = None) and K (get_waiting_ntfn_recv_threads thread s = {})) s) and ?P'4) s proof (prove)
goal (5 subgoals):
 1. \<And>bound_tcbs t. bound_tcbs \<noteq> {} \<Longrightarrow> \<lbrace>?B37 bound_tcbs t\<rbrace> set_cap (t, tcb_pending_op_slot) NullCap \<lbrace>\<lambda>x _. False\<rbrace>
 2. \<And>bound_tcbs. bound_tcbs \<noteq> {} \<Longrightarrow> \<lbrace>?Q36 bound_tcbs\<rbrace> select bound_tcbs \<lbrace>?B37 bound_tcbs\<rbrace>
 3. \<And>bound_tcbs. \<not> bound_tcbs \<noteq> {} \<Longrightarrow> \<lbrace>?R36 bound_tcbs\<rbrace> return () \<lbrace>\<lambda>r. P\<rbrace>
 4. \<lbrace>?P'4\<rbrace> gets (get_waiting_sync_bound_ntfn_threads thread) \<lbrace>\<lambda>bound_tcbs s. (bound_tcbs \<noteq> {} \<longrightarrow> ?Q36 bound_tcbs s) \<and> (\<not> bound_tcbs \<noteq> {} \<longrightarrow> ?R36 bound_tcbs s)\<rbrace>
 5. \<And>s. (P and no_pending) s \<Longrightarrow> ((\<lambda>s. ((\<lambda>a. (None = None \<longrightarrow> P a) \<and> None = None) and K (get_waiting_ntfn_recv_threads thread s = {})) s) and ?P'4) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (P and no_pending) s \<Longrightarrow> ((\<lambda>s. ((\<lambda>a. (None = None \<longrightarrow> P a) \<and> None = None) and K (get_waiting_ntfn_recv_threads thread s = {})) s) and (\<lambda>s. (get_waiting_sync_bound_ntfn_threads thread s \<noteq> {} \<longrightarrow> (\<forall>x\<in>get_waiting_sync_bound_ntfn_threads thread s. False)) \<and> (\<not> get_waiting_sync_bound_ntfn_threads thread s \<noteq> {} \<longrightarrow> P s))) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>P s; \<forall>oid cap. slots_of oid s tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap\<rbrakk> \<Longrightarrow> (\<forall>x a. cdl_objects s x = Some (Tcb a) \<longrightarrow> cdl_tcb_caps a tcb_pending_op_slot \<noteq> Some (PendingNtfnRecvCap thread)) \<and> (\<forall>x a. cdl_objects s x = Some (Tcb a) \<longrightarrow> (\<forall>ep_id can_grant. cdl_tcb_caps a tcb_pending_op_slot \<noteq> Some (PendingSyncRecvCap ep_id False can_grant)) \<or> cdl_tcb_caps a tcb_boundntfn_slot \<noteq> Some (BoundNotificationCap thread)) proof (prove)
goal (2 subgoals):
 1. \<And>s x a. \<lbrakk>P s; \<forall>oid cap. slots_of oid s tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap; cdl_objects s x = Some (Tcb a)\<rbrakk> \<Longrightarrow> cdl_tcb_caps a tcb_pending_op_slot \<noteq> Some (PendingNtfnRecvCap thread)
 2. \<And>s x a. \<lbrakk>P s; \<forall>oid cap. slots_of oid s tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap; cdl_objects s x = Some (Tcb a)\<rbrakk> \<Longrightarrow> (\<forall>ep_id can_grant. cdl_tcb_caps a tcb_pending_op_slot \<noteq> Some (PendingSyncRecvCap ep_id False can_grant)) \<or> cdl_tcb_caps a tcb_boundntfn_slot \<noteq> Some (BoundNotificationCap thread) proof (prove)
goal (2 subgoals):
 1. \<And>s x a. \<lbrakk>P s; cdl_objects s x = Some (Tcb a); \<forall>cap. slots_of x s tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap\<rbrakk> \<Longrightarrow> cdl_tcb_caps a tcb_pending_op_slot \<noteq> Some (PendingNtfnRecvCap thread)
 2. \<And>s x a. \<lbrakk>P s; \<forall>oid cap. slots_of oid s tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap; cdl_objects s x = Some (Tcb a)\<rbrakk> \<Longrightarrow> (\<forall>ep_id can_grant. cdl_tcb_caps a tcb_pending_op_slot \<noteq> Some (PendingSyncRecvCap ep_id False can_grant)) \<or> cdl_tcb_caps a tcb_boundntfn_slot \<noteq> Some (BoundNotificationCap thread) proof (prove)
goal (1 subgoal):
 1. \<And>s x a. \<lbrakk>P s; \<forall>oid cap. slots_of oid s tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap; cdl_objects s x = Some (Tcb a)\<rbrakk> \<Longrightarrow> (\<forall>ep_id can_grant. cdl_tcb_caps a tcb_pending_op_slot \<noteq> Some (PendingSyncRecvCap ep_id False can_grant)) \<or> cdl_tcb_caps a tcb_boundntfn_slot \<noteq> Some (BoundNotificationCap thread) proof (prove)
goal (1 subgoal):
 1. \<And>s x a. \<lbrakk>P s; cdl_objects s x = Some (Tcb a); \<forall>cap. slots_of x s tcb_pending_op_slot = Some cap \<longrightarrow> \<not> is_pending_cap cap\<rbrakk> \<Longrightarrow> (\<forall>ep_id can_grant. cdl_tcb_caps a tcb_pending_op_slot \<noteq> Some (PendingSyncRecvCap ep_id False can_grant)) \<or> cdl_tcb_caps a tcb_boundntfn_slot \<noteq> Some (BoundNotificationCap thread) proof (prove)
goal:
No subgoals!