theory Syscall_S

lemma send_signal_separate_state [wp]:
  "\<lbrace>separate_state\<rbrace> send_signal a b \<lbrace>\<lambda>_. separate_state\<rbrace>" unfolding send_signal_def cancel_ipc_def apply (rule separate_state_pres) apply (rule hoare_pre) apply (wp gts_wp get_simple_ko_wp hoare_pre_cont[where f="reply_cancel_ipc x" for x]
        | wpc | wps
        | simp add: update_waiting_ntfn_def)+ apply (clarsimp) apply (simp add: receive_blocked_def) apply (case_tac st; clarsimp) apply (clarsimp simp add: pred_tcb_at_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>separate_state\<rbrace> send_signal a b \<lbrace>\<lambda>_. separate_state\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>separate_state\<rbrace> do ntfn <- get_notification a;
case (ntfn_obj ntfn, ntfn_bound_tcb ntfn) of (IdleNtfn, None) \<Rightarrow> set_notification a $ ntfn_set_obj ntfn (ActiveNtfn b) | (IdleNtfn, Some tcb) \<Rightarrow> do st <- get_thread_state tcb;
if receive_blocked st then do do state <- get_thread_state tcb;
case state of BlockedOnReceive x y \<Rightarrow> blocked_cancel_ipc state tcb | BlockedOnSend x y \<Rightarrow> blocked_cancel_ipc state tcb | BlockedOnReply \<Rightarrow> reply_cancel_ipc tcb | BlockedOnNotification event \<Rightarrow> cancel_signal tcb event | _ \<Rightarrow> return ()
od;
set_thread_state tcb Running;
as_user tcb $ setRegister badge_register b;
do_extended_op (possible_switch_to tcb)
od else set_notification a $ ntfn_set_obj ntfn (ActiveNtfn b)
od | (WaitingNtfn queue, bound_tcb) \<Rightarrow> update_waiting_ntfn a queue bound_tcb b | (ActiveNtfn badge', bound_tcb) \<Rightarrow> set_notification a $ ntfn_set_obj ntfn $ ActiveNtfn (combine_ntfn_badges b badge')
od \<lbrace>\<lambda>_. separate_state\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P t p. \<lbrace>\<lambda>s. P (typ_at t p s) (caps_of_state s)\<rbrace> do ntfn <- get_notification a;
case (ntfn_obj ntfn, ntfn_bound_tcb ntfn) of (IdleNtfn, None) \<Rightarrow> set_notification a $ ntfn_set_obj ntfn (ActiveNtfn b) | (IdleNtfn, Some tcb) \<Rightarrow> do st <- get_thread_state tcb;
if receive_blocked st then do do state <- get_thread_state tcb;
case state of BlockedOnReceive x y \<Rightarrow> blocked_cancel_ipc state tcb | BlockedOnSend x y \<Rightarrow> blocked_cancel_ipc state tcb | BlockedOnReply \<Rightarrow> reply_cancel_ipc tcb | BlockedOnNotification event \<Rightarrow> cancel_signal tcb event | _ \<Rightarrow> return ()
od;
set_thread_state tcb Running;
as_user tcb $ setRegister badge_register b;
do_extended_op (possible_switch_to tcb)
od else set_notification a $ ntfn_set_obj ntfn (ActiveNtfn b)
od | (WaitingNtfn queue, bound_tcb) \<Rightarrow> update_waiting_ntfn a queue bound_tcb b | (ActiveNtfn badge', bound_tcb) \<Rightarrow> set_notification a $ ntfn_set_obj ntfn $ ActiveNtfn (combine_ntfn_badges b badge')
od \<lbrace>\<lambda>_ s. P (typ_at t p s) (caps_of_state s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>P t p. \<lbrace>?Q2 P t p\<rbrace> do ntfn <- get_notification a;
case (ntfn_obj ntfn, ntfn_bound_tcb ntfn) of (IdleNtfn, None) \<Rightarrow> set_notification a $ ntfn_set_obj ntfn (ActiveNtfn b) | (IdleNtfn, Some tcb) \<Rightarrow> do st <- get_thread_state tcb;
if receive_blocked st then do do state <- get_thread_state tcb;
case state of BlockedOnReceive x y \<Rightarrow> blocked_cancel_ipc state tcb | BlockedOnSend x y \<Rightarrow> blocked_cancel_ipc state tcb | BlockedOnReply \<Rightarrow> reply_cancel_ipc tcb | BlockedOnNotification event \<Rightarrow> cancel_signal tcb event | _ \<Rightarrow> return ()
od;
set_thread_state tcb Running;
as_user tcb $ setRegister badge_register b;
do_extended_op (possible_switch_to tcb)
od else set_notification a $ ntfn_set_obj ntfn (ActiveNtfn b)
od | (WaitingNtfn queue, bound_tcb) \<Rightarrow> update_waiting_ntfn a queue bound_tcb b | (ActiveNtfn badge', bound_tcb) \<Rightarrow> set_notification a $ ntfn_set_obj ntfn $ ActiveNtfn (combine_ntfn_badges b badge')
od \<lbrace>\<lambda>_ s. P (typ_at t p s) (caps_of_state s)\<rbrace>
 2. \<And>P t p s. P (typ_at t p s) (caps_of_state s) \<Longrightarrow> ?Q2 P t p s proof (prove)
goal (1 subgoal):
 1. \<And>P t p s. P (typ_at t p s) (caps_of_state s) \<Longrightarrow> \<forall>ntfn. ko_at (Notification ntfn) a s \<longrightarrow> ntfn_obj ntfn = IdleNtfn \<longrightarrow> (\<forall>x. ntfn_bound_tcb ntfn = Some x \<longrightarrow> (\<forall>st. st_tcb_at ((=) st) x s \<longrightarrow> receive_blocked st \<longrightarrow> (\<forall>st. st_tcb_at ((=) st) x s \<longrightarrow> st \<noteq> BlockedOnReply))) proof (prove)
goal (1 subgoal):
 1. \<And>P t p s ntfn x st. \<lbrakk>P (typ_at t p s) (caps_of_state s); ko_at (Notification ntfn) a s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; st_tcb_at ((=) st) x s; receive_blocked st; st_tcb_at ((=) BlockedOnReply) x s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>P t p s ntfn x st. \<lbrakk>P (typ_at t p s) (caps_of_state s); ko_at (Notification ntfn) a s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; st_tcb_at ((=) st) x s; case st of BlockedOnReceive x xa \<Rightarrow> True | _ \<Rightarrow> False; st_tcb_at ((=) BlockedOnReply) x s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>P t p s ntfn x x41 x42. \<lbrakk>P (typ_at t p s) (caps_of_state s); ko_at (Notification ntfn) a s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; st_tcb_at ((=) (BlockedOnReceive x41 x42)) x s; st_tcb_at ((=) BlockedOnReply) x s\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!