kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchSchedule_AI

lemma stit_activatable[Schedule_AI_asms]:
  "\<lbrace>invs\<rbrace> switch_to_idle_thread \<lbrace>\<lambda>rv . ct_in_state activatable\<rbrace>" apply (simp add: switch_to_idle_thread_def arch_switch_to_idle_thread_def) apply (wp | simp add: ct_in_state_def)+ apply (clarsimp simp: invs_def valid_state_def cur_tcb_def valid_idle_def
                 elim!: pred_tcb_weaken_strongerE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> switch_to_idle_thread \<lbrace>\<lambda>rv. ct_in_state activatable\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> do thread <- gets idle_thread;
y <- gets idle_thread >>= set_vm_root;
modify (cur_thread_update (\<lambda>_. thread))
od \<lbrace>\<lambda>rv. ct_in_state activatable\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. invs s \<Longrightarrow> st_tcb_at activatable (idle_thread s) s proof (prove)
goal:
No subgoals!
theory IpcCancel_AI

lemma blocked_cancel_ipc_simple:
  "\<lbrace>tcb_at t\<rbrace> blocked_cancel_ipc ts t \<lbrace>\<lambda>rv. st_tcb_at simple t\<rbrace>" by (simp add: blocked_cancel_ipc_def | wp sts_st_tcb_at')+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at t\<rbrace> blocked_cancel_ipc ts t \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t\<rbrace>
theory IpcCancel_AI

lemma cancel_signal_simple:
  "\<lbrace>\<top>\<rbrace> cancel_signal t ntfn \<lbrace>\<lambda>rv. st_tcb_at simple t\<rbrace>" by (simp add: cancel_signal_def | wp sts_st_tcb_at')+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> cancel_signal t ntfn \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t\<rbrace>
theory IpcCancel_AI

lemma unbind_notification_valid_objs_helper:
  "valid_ntfn ntfn s \<longrightarrow> valid_ntfn (ntfn_set_bound_tcb ntfn None) s " by (clarsimp simp: valid_bound_tcb_def valid_ntfn_def
                  split: option.splits ntfn.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_ntfn ntfn s \<longrightarrow> valid_ntfn (ntfn_set_bound_tcb ntfn None) s
theory IpcCancel_AI

lemma unbind_notification_valid_objs:
  "\<lbrace>valid_objs\<rbrace>
   unbind_notification ptr \<lbrace>\<lambda>rv. valid_objs\<rbrace>" unfolding unbind_notification_def apply (wp thread_set_valid_objs_triv set_simple_ko_valid_objs hoare_drop_imp | wpc
         | simp add: tcb_cap_cases_def
         | strengthen unbind_notification_valid_objs_helper)+ apply (wp thread_get_wp' | simp add:get_bound_notification_def)+ apply (clarsimp) apply (erule (1) obj_at_valid_objsE) apply (clarsimp simp:valid_obj_def valid_tcb_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> unbind_notification ptr \<lbrace>\<lambda>rv. valid_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> do ntfnptr <- get_bound_notification ptr;
case ntfnptr of None \<Rightarrow> return () | Some ntfnptr' \<Rightarrow> do ntfn <- get_notification ntfnptr';
do_unbind_notification ntfnptr' ntfn ptr
od
od \<lbrace>\<lambda>rv. valid_objs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'48\<rbrace> get_bound_notification ptr \<lbrace>\<lambda>rv s. \<forall>x. rv = Some x \<longrightarrow> valid_objs s \<and> ntfn_at x s\<rbrace>
 2. \<And>s. valid_objs s \<Longrightarrow> valid_objs s \<and> ?P'48 s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_objs s \<Longrightarrow> \<forall>tcb. ko_at (TCB tcb) ptr s \<longrightarrow> (\<forall>x. tcb_bound_notification tcb = Some x \<longrightarrow> ntfn_at x s) proof (prove)
goal (1 subgoal):
 1. \<And>s tcb x. \<lbrakk>valid_objs s; ko_at (TCB tcb) ptr s; tcb_bound_notification tcb = Some x\<rbrakk> \<Longrightarrow> ntfn_at x s proof (prove)
goal (1 subgoal):
 1. \<And>s tcb x ko. \<lbrakk>valid_objs s; tcb_bound_notification tcb = Some x; kheap s ptr = Some ko; TCB tcb = ko; valid_obj ptr ko s\<rbrakk> \<Longrightarrow> ntfn_at x s proof (prove)
goal:
No subgoals!
theory IpcCancel_AI

lemma get_ep_queue_inv[wp]:
  "\<lbrace>P\<rbrace> get_ep_queue ep \<lbrace>\<lambda>_. P\<rbrace>" by (cases ep, simp_all add: get_ep_queue_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> get_ep_queue ep \<lbrace>\<lambda>_. P\<rbrace>
theory IpcCancel_AI

lemma cancel_all_ipc_st_tcb_at:
  assumes x[simp]: "P Structures_A.Restart" shows
  "\<lbrace>st_tcb_at P t\<rbrace> cancel_all_ipc epptr \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace>" unfolding cancel_all_ipc_def by (wp ep_cases_weak_wp mapM_x_wp' sts_st_tcb_at_cases | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at P t\<rbrace> cancel_all_ipc epptr \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at P t\<rbrace> do ep <- get_endpoint epptr;
case ep of IdleEP \<Rightarrow> return () | _ \<Rightarrow> do queue <- get_ep_queue ep;
set_endpoint epptr IdleEP;
mapM_x (\<lambda>t. do set_thread_state t Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t)
od) $ queue;
do_extended_op reschedule_required
od
od \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace>
theory IpcCancel_AI

lemma unbind_notification_st_tcb_at[wp]:
  "\<lbrace>st_tcb_at P t\<rbrace> unbind_notification t' \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace>" unfolding unbind_notification_def by (wp thread_set_no_change_tcb_state hoare_drop_imps | wpc | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at P t\<rbrace> unbind_notification t' \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at P t\<rbrace> do ntfnptr <- get_bound_notification t';
case ntfnptr of None \<Rightarrow> return () | Some ntfnptr' \<Rightarrow> do ntfn <- get_notification ntfnptr';
do_unbind_notification ntfnptr' ntfn t'
od
od \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace>
theory IpcCancel_AI

lemma unbind_maybe_notification_st_tcb_at[wp]:
  "\<lbrace>st_tcb_at P t\<rbrace> unbind_maybe_notification r \<lbrace>\<lambda>rv. st_tcb_at P t \<rbrace>" unfolding unbind_maybe_notification_def apply (rule hoare_pre) apply (wp  thread_set_no_change_tcb_state hoare_drop_imps| wpc | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at P t\<rbrace> unbind_maybe_notification r \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at P t\<rbrace> do ntfn <- get_notification r;
case ntfn_bound_tcb ntfn of None \<Rightarrow> return () | Some t \<Rightarrow> do_unbind_notification r ntfn t
od \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do ntfn <- get_notification r;
case ntfn_bound_tcb ntfn of None \<Rightarrow> return () | Some t \<Rightarrow> do_unbind_notification r ntfn t
od \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace>
 2. \<And>s. st_tcb_at P t s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory IpcCancel_AI

lemma cancel_all_signals_st_tcb_at:
  assumes x[simp]: "P Structures_A.Restart" shows
  "\<lbrace>st_tcb_at P t\<rbrace> cancel_all_signals ntfnptr \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace>" unfolding cancel_all_signals_def unbind_maybe_notification_def by (wp ntfn_cases_weak_wp mapM_x_wp' sts_st_tcb_at_cases
         hoare_drop_imps unbind_notification_st_tcb_at
    | simp | wpc)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at P t\<rbrace> cancel_all_signals ntfnptr \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at P t\<rbrace> do ntfn <- get_notification ntfnptr;
case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> do _ <- set_notification ntfnptr $ ntfn_set_obj ntfn IdleNtfn;
mapM_x (\<lambda>t. do set_thread_state t Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t)
od) queue;
do_extended_op reschedule_required
od | _ \<Rightarrow> return ()
od \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace>
theory IpcCancel_AI

lemma get_blocking_object_inv[wp]:
  "\<lbrace>P\<rbrace> get_blocking_object st \<lbrace>\<lambda>_. P\<rbrace>" by (cases st, simp_all add: get_blocking_object_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> get_blocking_object st \<lbrace>\<lambda>_. P\<rbrace>
theory IpcCancel_AI

lemma blocked_ipc_st_tcb_at_general:
  "\<lbrace>st_tcb_at P t' and K (t = t' \<longrightarrow> P Structures_A.Inactive)\<rbrace>
     blocked_cancel_ipc st t
   \<lbrace>\<lambda>rv. st_tcb_at P t'\<rbrace>" apply (simp add: blocked_cancel_ipc_def) apply (wp sts_st_tcb_at_cases hoare_weak_lift_imp, simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at P t' and K (t = t' \<longrightarrow> P Inactive)\<rbrace> blocked_cancel_ipc st t \<lbrace>\<lambda>rv. st_tcb_at P t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at P t' and (\<lambda>y. t = t' \<longrightarrow> P Inactive)\<rbrace> do epptr <- get_blocking_object st;
ep <- get_endpoint epptr;
queue <- get_ep_queue ep;
y <- set_endpoint epptr (case remove1 t queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep (remove1 t queue));
set_thread_state t Inactive
od \<lbrace>\<lambda>rv. st_tcb_at P t'\<rbrace> proof (prove)
goal:
No subgoals!
theory IpcCancel_AI

lemma cancel_signal_st_tcb_at_general:
  "\<lbrace>st_tcb_at P t' and K (t = t' \<longrightarrow> (P Structures_A.Running \<and> P Structures_A.Inactive))\<rbrace>
     cancel_signal t ntfn
   \<lbrace>\<lambda>rv. st_tcb_at P t'\<rbrace>" apply (simp add: cancel_signal_def) apply (wp sts_st_tcb_at_cases ntfn_cases_weak_wp hoare_weak_lift_imp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at P t' and K (t = t' \<longrightarrow> P Running \<and> P Inactive)\<rbrace> cancel_signal t ntfn \<lbrace>\<lambda>rv. st_tcb_at P t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at P t' and (\<lambda>y. t = t' \<longrightarrow> P Running \<and> P Inactive)\<rbrace> do ntfna <- get_notification ntfn;
queue <- case ntfn_obj ntfna of WaitingNtfn queue \<Rightarrow> return queue | _ \<Rightarrow> fail;
y <- set_notification ntfn (ntfn_set_obj ntfna (case remove1 t queue of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn (remove1 t queue)));
set_thread_state t Inactive
od \<lbrace>\<lambda>rv. st_tcb_at P t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (st_tcb_at P t' and (\<lambda>y. t = t' \<longrightarrow> P Running \<and> P Inactive)) s \<Longrightarrow> ((\<lambda>s. (t = t' \<longrightarrow> True) \<and> (t \<noteq> t' \<longrightarrow> True)) and (\<lambda>s. (t = t' \<longrightarrow> P Inactive) \<and> (t \<noteq> t' \<longrightarrow> st_tcb_at P t' s)) and (\<lambda>s. (t = t' \<longrightarrow> True) \<and> (t \<noteq> t' \<longrightarrow> True))) s proof (prove)
goal:
No subgoals!
theory IpcCancel_AI

lemma fast_finalise_misc[wp]:
"\<lbrace>st_tcb_at simple t \<rbrace> fast_finalise a b \<lbrace>\<lambda>_. st_tcb_at simple t\<rbrace>" apply (case_tac a,simp_all) apply (wp|clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t\<rbrace> fast_finalise a b \<lbrace>\<lambda>_. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x31 x32 x33. a = EndpointCap x31 x32 x33 \<Longrightarrow> \<lbrace>st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t\<rbrace> when b (cancel_all_ipc x31) \<lbrace>\<lambda>_. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t\<rbrace>
 2. \<And>x41 x42 x43. a = NotificationCap x41 x42 x43 \<Longrightarrow> \<lbrace>st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t\<rbrace> when b (do y <- unbind_maybe_notification x41;
cancel_all_signals x41
od) \<lbrace>\<lambda>_. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t\<rbrace> proof (prove)
goal:
No subgoals!
theory IpcCancel_AI

lemma update_restart_pc_has_reply_cap[wp]:
  "\<lbrace>\<lambda>s. \<not> has_reply_cap t s\<rbrace> update_restart_pc t \<lbrace>\<lambda>_ s. \<not> has_reply_cap t s\<rbrace>" apply (simp add: has_reply_cap_def) apply (wp hoare_vcg_all_lift) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> has_reply_cap t s\<rbrace> update_restart_pc t \<lbrace>\<lambda>_ s. \<not> has_reply_cap t s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>a b. \<not> cte_wp_at (is_reply_cap_to t) (a, b) s\<rbrace> update_restart_pc t \<lbrace>\<lambda>_ s. \<forall>a b. \<not> cte_wp_at (is_reply_cap_to t) (a, b) s\<rbrace> proof (prove)
goal:
No subgoals!
theory IpcCancel_AI

lemma blocked_cancel_ipc_typ_at[wp]:
  "\<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> blocked_cancel_ipc st t \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>" apply (simp add: blocked_cancel_ipc_def get_blocking_object_def get_ep_queue_def
                   get_simple_ko_def) apply (wp get_object_wp|wpc)+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> blocked_cancel_ipc st t \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> do epptr <- case st of BlockedOnReceive epptr x \<Rightarrow> return epptr | BlockedOnSend epptr x \<Rightarrow> return epptr | _ \<Rightarrow> fail;
ep <- do kobj <- get_object epptr;
y <- assert (a_type kobj = AEndpoint \<or> a_type kobj = ANTFN);
case partial_inv Endpoint kobj of None \<Rightarrow> fail | Some x \<Rightarrow> return x
od;
queue <- case ep of IdleEP \<Rightarrow> fail | SendEP q \<Rightarrow> return q | RecvEP q \<Rightarrow> return q;
y <- set_endpoint epptr (case remove1 t queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep (remove1 t queue));
set_thread_state t Inactive
od \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (typ_at T p s) \<Longrightarrow> (st = Running \<longrightarrow> True) \<and> (inactive st \<longrightarrow> True) \<and> (st = Restart \<longrightarrow> True) \<and> (\<forall>x xa. st = BlockedOnReceive x xa \<longrightarrow> (\<forall>ko. ko_at ko x s \<longrightarrow> a_type ko = AEndpoint \<or> a_type ko = ANTFN \<longrightarrow> (partial_inv Endpoint ko = None \<longrightarrow> True) \<and> (\<forall>x. partial_inv Endpoint ko = Some x \<longrightarrow> (x = IdleEP \<longrightarrow> True) \<and> (\<forall>xa. x = SendEP xa \<longrightarrow> P (typ_at T p s)) \<and> (\<forall>xa. x = RecvEP xa \<longrightarrow> P (typ_at T p s))))) \<and> (\<forall>x xa. st = BlockedOnSend x xa \<longrightarrow> (\<forall>ko. ko_at ko x s \<longrightarrow> a_type ko = AEndpoint \<or> a_type ko = ANTFN \<longrightarrow> (partial_inv Endpoint ko = None \<longrightarrow> True) \<and> (\<forall>x. partial_inv Endpoint ko = Some x \<longrightarrow> (x = IdleEP \<longrightarrow> True) \<and> (\<forall>xa. x = SendEP xa \<longrightarrow> P (typ_at T p s)) \<and> (\<forall>xa. x = RecvEP xa \<longrightarrow> P (typ_at T p s))))) \<and> (awaiting_reply st \<longrightarrow> True) \<and> (\<forall>x. st = BlockedOnNotification x \<longrightarrow> True) \<and> (idle st \<longrightarrow> True) proof (prove)
goal:
No subgoals!
theory IpcCancel_AI

lemma blocked_cancel_ipc_tcb_at [wp]:
  "\<lbrace>tcb_at t\<rbrace> blocked_cancel_ipc st t' \<lbrace>\<lambda>rv. tcb_at t\<rbrace>" by (simp add: tcb_at_typ) wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at t\<rbrace> blocked_cancel_ipc st t' \<lbrace>\<lambda>rv. tcb_at t\<rbrace>
theory IpcCancel_AI

lemma cancel_ipc_tcb [wp]:
  "\<lbrace>tcb_at t\<rbrace> cancel_ipc t' \<lbrace>\<lambda>rv. (tcb_at t) :: 'a state \<Rightarrow> bool\<rbrace>" by (simp add: tcb_at_typ) wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at t\<rbrace> cancel_ipc t' \<lbrace>\<lambda>rv. tcb_at t\<rbrace>
theory IpcCancel_AI

lemma gbep_ret:
  "\<lbrakk> st = Structures_A.BlockedOnReceive epPtr pl' \<or>
     st = Structures_A.BlockedOnSend epPtr pl \<rbrakk> \<Longrightarrow>
  get_blocking_object st = return epPtr" by (auto simp add: get_blocking_object_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. st = BlockedOnReceive epPtr pl' \<or> st = BlockedOnSend epPtr pl \<Longrightarrow> get_blocking_object st = return epPtr
theory IpcCancel_AI

lemma st_tcb_at_valid_st2:
  "\<lbrakk> st_tcb_at ((=) st) t s; valid_objs s \<rbrakk> \<Longrightarrow> valid_tcb_state st s" apply (clarsimp simp add: valid_objs_def get_tcb_def pred_tcb_at_def
                  obj_at_def) apply (drule_tac x=t in bspec) apply (erule domI) apply (simp add: valid_obj_def valid_tcb_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>st_tcb_at ((=) st) t s; valid_objs s\<rbrakk> \<Longrightarrow> valid_tcb_state st s proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>\<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; kheap s t = Some (TCB tcb); st = tcb_state tcb\<rbrakk> \<Longrightarrow> valid_tcb_state (tcb_state tcb) s proof (prove)
goal (2 subgoals):
 1. \<And>tcb. \<lbrakk>kheap s t = Some (TCB tcb); st = tcb_state tcb\<rbrakk> \<Longrightarrow> t \<in> dom (kheap s)
 2. \<And>tcb. \<lbrakk>kheap s t = Some (TCB tcb); st = tcb_state tcb; \<exists>obj. kheap s t = Some obj \<and> valid_obj t obj s\<rbrakk> \<Longrightarrow> valid_tcb_state (tcb_state tcb) s proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>kheap s t = Some (TCB tcb); st = tcb_state tcb; \<exists>obj. kheap s t = Some obj \<and> valid_obj t obj s\<rbrakk> \<Longrightarrow> valid_tcb_state (tcb_state tcb) s proof (prove)
goal:
No subgoals!
theory IpcCancel_AI

lemma reply_master_no_descendants_no_reply:
  "\<lbrakk> valid_mdb s; valid_reply_masters s; tcb_at t s \<rbrakk> \<Longrightarrow>
   descendants_of (t, tcb_cnode_index 2) (cdt s) = {} \<longrightarrow> \<not> has_reply_cap t s" by (fastforce simp: invs_def valid_state_def valid_mdb_def has_reply_cap_def
                     cte_wp_at_caps_of_state reply_mdb_def is_reply_cap_to_def
                     reply_caps_mdb_def descendants_of_def cdt_parent_defs
               dest: reply_master_caps_of_stateD tranclD)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_mdb s; valid_reply_masters s; tcb_at t s\<rbrakk> \<Longrightarrow> descendants_of (t, tcb_cnode_index 2) (cdt s) = {} \<longrightarrow> \<not> has_reply_cap t s
theory IpcCancel_AI

lemma reply_master_one_descendant:
  "\<lbrakk> invs s; tcb_at t s; descendants_of (t, tcb_cnode_index 2) (cdt s) \<noteq> {} \<rbrakk>
   \<Longrightarrow> \<exists>sl. descendants_of (t, tcb_cnode_index 2) (cdt s) = {sl}" by (fastforce elim: construct_singleton dest: reply_cap_unique_descendant)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; tcb_at t s; descendants_of (t, tcb_cnode_index 2) (cdt s) \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>sl. descendants_of (t, tcb_cnode_index 2) (cdt s) = {sl}
theory IpcCancel_AI

lemma ep_redux_simps2:
  "ep \<noteq> Structures_A.IdleEP \<Longrightarrow>
   valid_ep (case xs of [] \<Rightarrow> Structures_A.endpoint.IdleEP
            | a # list \<Rightarrow> update_ep_queue ep xs)
     = (\<lambda>s. distinct xs \<and> (\<forall>t\<in>set xs. tcb_at t s))"
  "ep \<noteq> Structures_A.IdleEP \<Longrightarrow>
   ep_q_refs_of (case xs of [] \<Rightarrow> Structures_A.endpoint.IdleEP
                   | a # list \<Rightarrow> update_ep_queue ep xs)
     = (set xs \<times> {case ep of Structures_A.SendEP xs \<Rightarrow> EPSend | Structures_A.RecvEP xs \<Rightarrow> EPRecv})" by (cases ep, simp_all cong: list.case_cong add: ep_redux_simps)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (ep \<noteq> IdleEP \<Longrightarrow> valid_ep (case xs of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep xs) = (\<lambda>s. distinct xs \<and> (\<forall>t\<in>set xs. tcb_at t s))) &&& (ep \<noteq> IdleEP \<Longrightarrow> ep_q_refs_of (case xs of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep xs) = set xs \<times> {case ep of SendEP xs \<Rightarrow> EPSend | RecvEP xs \<Rightarrow> EPRecv})
theory IpcCancel_AI

lemma gbi_ep_sp:
  "\<lbrace>P\<rbrace>
     get_blocking_object st
   \<lbrace>\<lambda>ep. P and K ((\<exists>d. st = Structures_A.BlockedOnReceive ep d)
                    \<or> (\<exists>d. st = Structures_A.BlockedOnSend ep d))\<rbrace>" apply (cases st, simp_all add: get_blocking_object_def) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> get_blocking_object st \<lbrace>\<lambda>ep. P and K ((\<exists>d. st = BlockedOnReceive ep d) \<or> (\<exists>d. st = BlockedOnSend ep d))\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x41 x42. st = BlockedOnReceive x41 x42 \<Longrightarrow> \<lbrace>P\<rbrace> return x41 \<lbrace>\<lambda>ep. P and (\<lambda>y. x41 = ep)\<rbrace>
 2. \<And>x51 x52. st = BlockedOnSend x51 x52 \<Longrightarrow> \<lbrace>P\<rbrace> return x51 \<lbrace>\<lambda>ep. P and (\<lambda>y. x51 = ep)\<rbrace> proof (prove)
goal:
No subgoals!
theory IpcCancel_AI

lemma get_epq_sp:
  "\<lbrace>P\<rbrace>
  get_ep_queue ep
  \<lbrace>\<lambda>q. P and K (ep \<in> {Structures_A.SendEP q, Structures_A.RecvEP q})\<rbrace>" apply (simp add: get_ep_queue_def) apply (cases ep) apply (wp|simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> get_ep_queue ep \<lbrace>\<lambda>q. P and K (ep \<in> {SendEP q, RecvEP q})\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> case ep of IdleEP \<Rightarrow> fail | SendEP q \<Rightarrow> return q | RecvEP q \<Rightarrow> return q \<lbrace>\<lambda>q. P and (\<lambda>y. ep = SendEP q \<or> ep = RecvEP q)\<rbrace> proof (prove)
goal (3 subgoals):
 1. ep = IdleEP \<Longrightarrow> \<lbrace>P\<rbrace> case ep of IdleEP \<Rightarrow> fail | SendEP q \<Rightarrow> return q | RecvEP q \<Rightarrow> return q \<lbrace>\<lambda>q. P and (\<lambda>y. ep = SendEP q \<or> ep = RecvEP q)\<rbrace>
 2. \<And>x2. ep = SendEP x2 \<Longrightarrow> \<lbrace>P\<rbrace> case ep of IdleEP \<Rightarrow> fail | SendEP q \<Rightarrow> return q | RecvEP q \<Rightarrow> return q \<lbrace>\<lambda>q. P and (\<lambda>y. ep = SendEP q \<or> ep = RecvEP q)\<rbrace>
 3. \<And>x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>P\<rbrace> case ep of IdleEP \<Rightarrow> fail | SendEP q \<Rightarrow> return q | RecvEP q \<Rightarrow> return q \<lbrace>\<lambda>q. P and (\<lambda>y. ep = SendEP q \<or> ep = RecvEP q)\<rbrace> proof (prove)
goal:
No subgoals!
theory IpcCancel_AI

lemma refs_in_tcb_bound_refs:
  "(x, ref) \<in> tcb_bound_refs ntfn \<Longrightarrow> ref = TCBBound" by (auto simp: tcb_bound_refs_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x, ref) \<in> tcb_bound_refs ntfn \<Longrightarrow> ref = TCBBound
theory IpcCancel_AI

lemma refs_in_ntfn_bound_refs:
  "(x, ref) \<in> ntfn_bound_refs tcb \<Longrightarrow> ref = NTFNBound" by (auto simp: ntfn_bound_refs_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x, ref) \<in> ntfn_bound_refs tcb \<Longrightarrow> ref = NTFNBound
theory IpcCancel_AI

lemma symreftype_inverse':
  "symreftype ref = ref' \<Longrightarrow> ref = symreftype ref'" by (cases ref) simp_all

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. symreftype ref = ref' \<Longrightarrow> ref = symreftype ref'