theory Interrupt_AI

lemma send_signal_interrupt_states[wp_unsafe]:
  "\<lbrace>\<lambda>s. P (interrupt_states s) \<and> valid_objs s\<rbrace> send_signal a b \<lbrace>\<lambda>_ s. P (interrupt_states s)\<rbrace>" apply (simp add: send_signal_def) apply (rule hoare_seq_ext [OF _ get_simple_ko_sp]) apply (rule hoare_pre) apply (wp cancel_ipc_noreply_interrupt_states gts_wp hoare_vcg_all_lift thread_get_wp | wpc | simp)+ apply (clarsimp) apply (erule (1) obj_at_valid_objsE) apply (clarsimp simp: valid_obj_def valid_ntfn_def obj_at_def is_tcb_def) apply (case_tac ko, simp_all) apply (auto simp: pred_tcb_at_def obj_at_def receive_blocked_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (interrupt_states s) \<and> valid_objs s\<rbrace> send_signal a b \<lbrace>\<lambda>_ s. P (interrupt_states s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (interrupt_states s) \<and> valid_objs s\<rbrace> do ntfn <- get_notification a;
case ntfn_obj ntfn of IdleNtfn \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> set_notification a $ ntfn_set_obj ntfn (ActiveNtfn b) | 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 b;
do_extended_op (possible_switch_to tcb)
od else set_notification a $ ntfn_set_obj ntfn (ActiveNtfn b)
od | WaitingNtfn queue \<Rightarrow> update_waiting_ntfn a queue (ntfn_bound_tcb ntfn) b | ActiveNtfn badge' \<Rightarrow> set_notification a $ ntfn_set_obj ntfn $ ActiveNtfn (combine_ntfn_badges b badge')
od \<lbrace>\<lambda>_ s. P (interrupt_states s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfn. \<lbrace>ko_at (Notification ntfn) a and (\<lambda>s. P (interrupt_states s) \<and> valid_objs s)\<rbrace> case ntfn_obj ntfn of IdleNtfn \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> set_notification a $ ntfn_set_obj ntfn (ActiveNtfn b) | 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 b;
do_extended_op (possible_switch_to tcb)
od else set_notification a $ ntfn_set_obj ntfn (ActiveNtfn b)
od | WaitingNtfn queue \<Rightarrow> update_waiting_ntfn a queue (ntfn_bound_tcb ntfn) b | ActiveNtfn badge' \<Rightarrow> set_notification a $ ntfn_set_obj ntfn $ ActiveNtfn (combine_ntfn_badges b badge') \<lbrace>\<lambda>_ s. P (interrupt_states s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ntfn. \<lbrace>?Q4 ntfn\<rbrace> case ntfn_obj ntfn of IdleNtfn \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> set_notification a $ ntfn_set_obj ntfn (ActiveNtfn b) | 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 b;
do_extended_op (possible_switch_to tcb)
od else set_notification a $ ntfn_set_obj ntfn (ActiveNtfn b)
od | WaitingNtfn queue \<Rightarrow> update_waiting_ntfn a queue (ntfn_bound_tcb ntfn) b | ActiveNtfn badge' \<Rightarrow> set_notification a $ ntfn_set_obj ntfn $ ActiveNtfn (combine_ntfn_badges b badge') \<lbrace>\<lambda>_ s. P (interrupt_states s)\<rbrace>
 2. \<And>ntfn s. (ko_at (Notification ntfn) a and (\<lambda>s. P (interrupt_states s) \<and> valid_objs s)) s \<Longrightarrow> ?Q4 ntfn s proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s. ko_at (Notification ntfn) a s \<and> P (interrupt_states s) \<and> valid_objs 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> st_tcb_at (\<lambda>st. st \<noteq> BlockedOnReply) x s)) proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s x st. \<lbrakk>ko_at (Notification ntfn) a s; P (interrupt_states s); valid_objs s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; st_tcb_at ((=) st) x s; receive_blocked st\<rbrakk> \<Longrightarrow> st_tcb_at (\<lambda>st. st \<noteq> BlockedOnReply) x s proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s x st ko. \<lbrakk>P (interrupt_states s); valid_objs s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; st_tcb_at ((=) st) x s; receive_blocked st; kheap s a = Some ko; Notification ntfn = ko; valid_obj a ko s\<rbrakk> \<Longrightarrow> st_tcb_at (\<lambda>st. st \<noteq> BlockedOnReply) x s proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s x st ko. \<lbrakk>P (interrupt_states s); valid_objs s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; st_tcb_at ((=) st) x s; receive_blocked st; kheap s a = Some (Notification ntfn); kheap s x = Some ko; case ko of TCB t \<Rightarrow> True | _ \<Rightarrow> False\<rbrakk> \<Longrightarrow> st_tcb_at (\<lambda>st. st \<noteq> BlockedOnReply) x s proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s x st ko x2. \<lbrakk>P (interrupt_states s); valid_objs s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; st_tcb_at ((=) st) x s; receive_blocked st; kheap s a = Some (Notification ntfn); kheap s x = Some (TCB x2); ko = TCB x2\<rbrakk> \<Longrightarrow> st_tcb_at (\<lambda>st. st \<noteq> BlockedOnReply) x s proof (prove)
goal:
No subgoals!