kings-crown/FVELER_Isabelle huggingface dataset:
theory Finalise_AC

lemma cap_delete_pas_refined':
  "\<lbrace>pas_refined aag and einvs and simple_sched_action
                    and emptyable slot and K(is_subject aag (fst slot))\<rbrace>
   cap_delete slot
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" by (wp cap_delete_pas_refined) fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and einvs and simple_sched_action and emptyable slot and K (is_subject aag (fst slot))\<rbrace> cap_delete slot \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
theory Finalise_AC

lemma empty_slot_cte_wp_at:
  "\<lbrace>\<lambda>s. (p = slot \<longrightarrow> P NullCap) \<and> (p \<noteq> slot \<longrightarrow> cte_wp_at P p s)\<rbrace>
   empty_slot slot free_irq
   \<lbrace>\<lambda>_. cte_wp_at P p\<rbrace>" unfolding cte_wp_at_caps_of_state by (wpsimp wp: empty_slot_caps_of_state)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (p = slot \<longrightarrow> P NullCap) \<and> (p \<noteq> slot \<longrightarrow> cte_wp_at P p s)\<rbrace> empty_slot slot free_irq \<lbrace>\<lambda>_. cte_wp_at P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (p = slot \<longrightarrow> P NullCap) \<and> (p \<noteq> slot \<longrightarrow> (\<exists>cap. caps_of_state s p = Some cap \<and> P cap))\<rbrace> empty_slot slot free_irq \<lbrace>\<lambda>_ s. \<exists>cap. caps_of_state s p = Some cap \<and> P cap\<rbrace>
theory Finalise_AC

lemma deleting_irq_handler_caps_of_state_nullinv:
  "\<lbrace>\<lambda>s. \<forall>p. P ((caps_of_state s)(p \<mapsto> NullCap))\<rbrace>
     deleting_irq_handler irq
   \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>" unfolding deleting_irq_handler_def including no_pre apply (wp cap_delete_one_caps_of_state hoare_drop_imps) apply (rule hoare_post_imp [OF _ get_irq_slot_inv]) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>p. P ((caps_of_state s)(p \<mapsto> NullCap))\<rbrace> deleting_irq_handler irq \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>p. P ((caps_of_state s)(p \<mapsto> NullCap))\<rbrace> get_irq_slot irq >>= cap_delete_one \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>p. P ((caps_of_state s)(p \<mapsto> NullCap))\<rbrace> get_irq_slot irq >>= cap_delete_one \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>p. P ((caps_of_state s)(p \<mapsto> NullCap))\<rbrace> get_irq_slot irq \<lbrace>\<lambda>rv s. P ((caps_of_state s)(rv \<mapsto> NullCap))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<forall>p. P ((caps_of_state s)(p \<mapsto> NullCap)) \<Longrightarrow> P ((caps_of_state s)(rv \<mapsto> NullCap)) proof (prove)
goal:
No subgoals!
theory Finalise_AC

lemma finalise_cap_cte_wp_at_nullinv:
  "\<lbrace>\<lambda>s :: det_ext state. P NullCap \<and> cte_wp_at P p s\<rbrace>
   finalise_cap cap final
   \<lbrace>\<lambda>_ s. cte_wp_at P p s\<rbrace>" apply (simp add: cte_wp_at_caps_of_state) apply (wp finalise_cap_caps_of_state_nullinv) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P NullCap \<and> cte_wp_at P p s\<rbrace> finalise_cap cap final \<lbrace>\<lambda>_. cte_wp_at P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P NullCap \<and> (\<exists>cap. caps_of_state s p = Some cap \<and> P cap)\<rbrace> finalise_cap cap final \<lbrace>\<lambda>_ s. \<exists>cap. caps_of_state s p = Some cap \<and> P cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P NullCap \<and> (\<exists>cap. caps_of_state s p = Some cap \<and> P cap) \<Longrightarrow> (\<exists>cap. caps_of_state s p = Some cap \<and> P cap) \<and> (\<forall>pa. \<exists>cap. ((caps_of_state s)(pa \<mapsto> NullCap)) p = Some cap \<and> P cap) proof (prove)
goal:
No subgoals!
theory Finalise_AC

lemma rec_del_preserves_cte_zombie_null_insts:
  assumes P_Null: "P (NullCap)"
  assumes P_Zombie: "\<And>word x y. P (Zombie word x y)"
  shows "\<lbrace>\<lambda>s :: det_ext state. cte_wp_at P p s\<rbrace>
         rec_del (FinaliseSlotCall slot True)
         \<lbrace>\<lambda>_. cte_wp_at P p\<rbrace>,-"
  and "\<lbrace>\<lambda>s :: det_ext state. cte_wp_at P p s\<rbrace> cap_delete slot \<lbrace>\<lambda>_. cte_wp_at P p\<rbrace>,-" by (simp add: validE_R_def P_Null P_Zombie cap_delete_def
      | rule use_spec spec_strengthen_postE[OF hoare_pre_spec_validE
                            [OF rec_del_preserves_cte_zombie_null[where P=P]]]
      | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at P p\<rbrace> rec_del (FinaliseSlotCall slot True) \<lbrace>\<lambda>_. cte_wp_at P p\<rbrace>, - &&& \<lbrace>cte_wp_at P p\<rbrace> cap_delete slot \<lbrace>\<lambda>_. cte_wp_at P p\<rbrace>, -
theory Finalise_AC

lemma set_cap_cte_wp_at_separation:
  "\<lbrace>cte_wp_at P slot and K (slot \<noteq> slot')\<rbrace>
   set_cap cap slot'
   \<lbrace>\<lambda>_. cte_wp_at P slot \<rbrace>" by (wpsimp simp: cte_wp_at_caps_of_state[abs_def])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at P slot and K (slot \<noteq> slot')\<rbrace> set_cap cap slot' \<lbrace>\<lambda>_. cte_wp_at P slot\<rbrace>
theory Finalise_AC

lemma cap_move_cte_wp_at_separation:
  "\<lbrace>cte_wp_at P slot and K(slot \<noteq> src \<and> slot \<noteq> dest)\<rbrace>
   cap_move cap src dest
   \<lbrace>\<lambda>_. cte_wp_at P slot\<rbrace>" by (wpsimp wp: dxo_wp_weak set_cdt_cte_wp_at set_cap_cte_wp_at_separation
           simp: cap_move_def cte_wp_at_caps_of_state)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at P slot and K (slot \<noteq> src \<and> slot \<noteq> dest)\<rbrace> cap_move cap src dest \<lbrace>\<lambda>_. cte_wp_at P slot\<rbrace>
theory Finalise_AC

lemma cap_move_empty_src_slot:
  "\<lbrace>K (src \<noteq> dest)\<rbrace>
   cap_move cap src dest
   \<lbrace>\<lambda>_. cte_wp_at ((=) NullCap) src \<rbrace>" unfolding cap_move_def by (wpsimp wp: dxo_wp_weak set_cdt_cte_wp_at set_cap_sets_wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (src \<noteq> dest)\<rbrace> cap_move cap src dest \<lbrace>\<lambda>_. cte_wp_at ((=) NullCap) src\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (src \<noteq> dest)\<rbrace> do set_cap cap dest;
set_cap NullCap src;
src_p <- gets (\<lambda>s. cdt s src);
dest_p <- gets (\<lambda>s. cdt s dest);
cdt <- gets cdt;
parent <- return $ cdt src;
cdt' <- return $ cdt(dest := parent, src := None);
set_cdt (\<lambda>r. if cdt' r = Some src then Some dest else cdt' r);
do_extended_op (cap_move_ext src dest src_p dest_p);
is_original <- gets is_original_cap;
set_original dest (is_original src);
set_original src False
od \<lbrace>\<lambda>_. cte_wp_at ((=) NullCap) src\<rbrace>
theory ArchFinalise_AC

lemma sbn_st_vrefs[Finalise_AC_assms, wp]:
  "set_bound_notification t st \<lbrace>\<lambda>s. P (state_vrefs s)\<rbrace>" apply (simp add: set_bound_notification_def) apply (wpsimp wp: set_object_wp dxo_wp_weak) apply (clarsimp simp: state_vrefs_def vs_refs_no_global_pts_def
                 elim!: rsubst[where P=P, OF _ ext]
                 dest!: get_tcb_SomeD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (state_vrefs s)\<rbrace> set_bound_notification t st \<lbrace>\<lambda>_ s. P (state_vrefs s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (state_vrefs s)\<rbrace> do tcb <- gets_the (get_tcb t);
set_object t (TCB (tcb\<lparr>tcb_bound_notification := st\<rparr>))
od \<lbrace>\<lambda>_ s. P (state_vrefs s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>P (state_vrefs s); get_tcb t s = Some y\<rbrakk> \<Longrightarrow> P (state_vrefs (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (y\<lparr>tcb_bound_notification := st\<rparr>))\<rparr>)) proof (prove)
goal:
No subgoals!
theory ArchFinalise_AC

lemma arch_finalise_cap_auth'[Finalise_AC_assms]:
   "\<lbrace>pas_refined aag\<rbrace> arch_finalise_cap x12 final \<lbrace>\<lambda>rv s. pas_cap_cur_auth aag (fst rv)\<rbrace>" unfolding arch_finalise_cap_def by (wp | wpc | simp add: comp_def hoare_post_taut[where P = \<top>] split del: if_split)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag\<rbrace> arch_finalise_cap x12 final \<lbrace>\<lambda>rv s. pas_cap_cur_auth aag (fst rv)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag\<rbrace> case (x12, final) of (ASIDPoolCap ptr b, True) \<Rightarrow> do delete_asid_pool b ptr;
return (NullCap, NullCap)
od | (ASIDPoolCap ptr b, False) \<Rightarrow> return (NullCap, NullCap) | (ASIDControlCap, xb) \<Rightarrow> return (NullCap, NullCap) | (PageCap x ptr xa s None, xb) \<Rightarrow> return (NullCap, NullCap) | (PageCap x ptr xa s (Some (a, v)), xb) \<Rightarrow> do unmap_page s a v ptr;
return (NullCap, NullCap)
od | (PageTableCap ptr None, xb) \<Rightarrow> return (NullCap, NullCap) | (PageTableCap ptr (Some (a, v)), True) \<Rightarrow> do unmap_page_table a v ptr;
return (NullCap, NullCap)
od | (PageTableCap ptr (Some (a, v)), False) \<Rightarrow> return (NullCap, NullCap) | (PageDirectoryCap ptr None, xb) \<Rightarrow> return (NullCap, NullCap) | (PageDirectoryCap ptr (Some a), True) \<Rightarrow> do delete_asid a ptr;
return (NullCap, NullCap)
od | (PageDirectoryCap ptr (Some a), False) \<Rightarrow> return (NullCap, NullCap) \<lbrace>\<lambda>rv s. pas_cap_cur_auth aag (fst rv)\<rbrace>
theory ArchFinalise_AC

lemma arch_finalise_cap_obj_refs[Finalise_AC_assms]:
  "\<lbrace>\<lambda>s. \<forall>x \<in> aobj_ref' acap. P x\<rbrace>
   arch_finalise_cap acap slot
   \<lbrace>\<lambda>rv s. \<forall>x \<in> obj_refs_ac (fst rv). P x\<rbrace>" by (wpsimp simp: arch_finalise_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>x\<in>aobj_ref' acap. P x\<rbrace> arch_finalise_cap acap slot \<lbrace>\<lambda>rv s. \<forall>x\<in>obj_refs_ac (fst rv). P x\<rbrace>
theory ArchFinalise_AC

lemma arch_finalise_cap_makes_halted[Finalise_AC_assms]:
  "\<lbrace>\<top>\<rbrace> arch_finalise_cap arch_cap ex \<lbrace>\<lambda>rv s. \<forall>t\<in>obj_refs_ac (fst rv). halted_if_tcb t s\<rbrace>" apply (case_tac arch_cap, simp_all add: arch_finalise_cap_def) by (wpsimp simp: valid_cap_def split: option.split bool.split)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> arch_finalise_cap arch_cap ex \<lbrace>\<lambda>rv s. \<forall>t\<in>obj_refs_ac (fst rv). halted_if_tcb t s\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x11 x12. arch_cap = ASIDPoolCap x11 x12 \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> case ex of True \<Rightarrow> do delete_asid_pool x12 x11;
return (NullCap, NullCap)
od | False \<Rightarrow> return (NullCap, NullCap) \<lbrace>\<lambda>rv s. \<forall>t\<in>obj_refs_ac (fst rv). halted_if_tcb t s\<rbrace>
 2. arch_cap = ASIDControlCap \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>rv s. \<forall>t\<in>obj_refs_ac (fst rv). halted_if_tcb t s\<rbrace>
 3. \<And>x31 x32 x33 x34 x35. arch_cap = PageCap x31 x32 x33 x34 x35 \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> case x35 of None \<Rightarrow> return (NullCap, NullCap) | Some (a, v) \<Rightarrow> do y <- unmap_page x34 a v x32;
return (NullCap, NullCap)
od \<lbrace>\<lambda>rv s. \<forall>t\<in>obj_refs_ac (fst rv). halted_if_tcb t s\<rbrace>
 4. \<And>x41 x42. arch_cap = PageTableCap x41 x42 \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> case x42 of None \<Rightarrow> return (NullCap, NullCap) | Some (a, v) \<Rightarrow> case ex of True \<Rightarrow> do unmap_page_table a v x41;
return (NullCap, NullCap)
od | False \<Rightarrow> return (NullCap, NullCap) \<lbrace>\<lambda>rv s. \<forall>t\<in>obj_refs_ac (fst rv). halted_if_tcb t s\<rbrace>
 5. \<And>x51 x52. arch_cap = PageDirectoryCap x51 x52 \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> case x52 of None \<Rightarrow> return (NullCap, NullCap) | Some a \<Rightarrow> case ex of True \<Rightarrow> do delete_asid a x51;
return (NullCap, NullCap)
od | False \<Rightarrow> return (NullCap, NullCap) \<lbrace>\<lambda>rv s. \<forall>t\<in>obj_refs_ac (fst rv). halted_if_tcb t s\<rbrace>
theory ArchFinalise_AC

lemma arch_cap_cleanup_wf[Finalise_AC_assms]:
  "\<lbrakk> arch_cap_cleanup_opt acap \<noteq> NullCap; \<not> is_arch_cap (arch_cap_cleanup_opt acap) \<rbrakk>
     \<Longrightarrow> (\<exists>irq. arch_cap_cleanup_opt acap = IRQHandlerCap irq \<and> is_subject_irq aag irq)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>arch_cap_cleanup_opt acap \<noteq> NullCap; \<not> is_arch_cap (arch_cap_cleanup_opt acap)\<rbrakk> \<Longrightarrow> \<exists>irq. arch_cap_cleanup_opt acap = IRQHandlerCap irq \<and> is_subject_irq aag irq
theory ArchFinalise_AC

lemma finalise_cap_caps_of_state_nullinv[Finalise_AC_assms]:
  "\<lbrace>\<lambda>s. P (caps_of_state s) \<and> (\<forall>p. P ((caps_of_state s)(p \<mapsto> NullCap)))\<rbrace>
   finalise_cap cap final
   \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>" by (cases cap;
      wpsimp wp: suspend_caps_of_state unbind_notification_caps_of_state
                 unbind_notification_cte_wp_at
                 hoare_vcg_all_lift hoare_drop_imps
                 deleting_irq_handler_caps_of_state_nullinv
           simp: fun_upd_def[symmetric] if_apply_def2 split_del: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (caps_of_state s) \<and> (\<forall>p. P ((caps_of_state s)(p \<mapsto> NullCap)))\<rbrace> finalise_cap cap final \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>
theory Ipc_AC

lemma send_signal_caps_of_state[wp]:
  "send_signal ntfnptr badge \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace>" apply (clarsimp simp: send_signal_def) apply (rule hoare_seq_ext[OF _ get_simple_ko_sp]) apply (wpsimp wp: dxo_wp_weak cancel_ipc_receive_blocked_caps_of_state gts_wp hoare_weak_lift_imp
               simp: update_waiting_ntfn_def) apply (clarsimp simp: fun_upd_def[symmetric] st_tcb_def2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> send_signal ntfnptr badge \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> do ntfn <- get_notification ntfnptr;
case ntfn_obj ntfn of IdleNtfn \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn (ActiveNtfn badge) | 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 badge;
do_extended_op (possible_switch_to tcb)
od else set_notification ntfnptr $ ntfn_set_obj ntfn (ActiveNtfn badge)
od | WaitingNtfn queue \<Rightarrow> update_waiting_ntfn ntfnptr queue (ntfn_bound_tcb ntfn) badge | ActiveNtfn badge' \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn $ ActiveNtfn (combine_ntfn_badges badge badge')
od \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfn. \<lbrace>ko_at (Notification ntfn) ntfnptr and (\<lambda>s. P (caps_of_state s))\<rbrace> case ntfn_obj ntfn of IdleNtfn \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn (ActiveNtfn badge) | 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 badge;
do_extended_op (possible_switch_to tcb)
od else set_notification ntfnptr $ ntfn_set_obj ntfn (ActiveNtfn badge)
od | WaitingNtfn queue \<Rightarrow> update_waiting_ntfn ntfnptr queue (ntfn_bound_tcb ntfn) badge | ActiveNtfn badge' \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn $ ActiveNtfn (combine_ntfn_badges badge badge') \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s x st. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; P (caps_of_state 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 receive_blocked x s proof (prove)
goal:
No subgoals!
theory Ipc_AC

lemma update_waiting_ntfn_pas_refined:
  "\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state
                    and ko_at (Notification ntfn) ntfnptr and K (ntfn_obj ntfn = WaitingNtfn queue)\<rbrace>
   update_waiting_ntfn ntfnptr queue badge val
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" by (wpsimp wp: set_thread_state_pas_refined set_simple_ko_pas_refined simp: update_waiting_ntfn_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and ko_at (Notification ntfn) ntfnptr and K (ntfn_obj ntfn = WaitingNtfn queue)\<rbrace> update_waiting_ntfn ntfnptr queue badge val \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
theory Ipc_AC

lemma cancel_ipc_receive_blocked_pas_refined:
  "\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs
                    and valid_arch_state and st_tcb_at receive_blocked t\<rbrace>
   cancel_ipc t
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" apply (clarsimp simp: cancel_ipc_def) apply (rule hoare_seq_ext[OF _ gts_sp]) apply (wp gts_wp | wpc | simp)+ apply (clarsimp simp: st_tcb_def2 receive_blocked_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and st_tcb_at receive_blocked t\<rbrace> cancel_ipc t \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and st_tcb_at receive_blocked t\<rbrace> do state <- get_thread_state t;
case state of BlockedOnReceive x y \<Rightarrow> blocked_cancel_ipc state t | BlockedOnSend x y \<Rightarrow> blocked_cancel_ipc state t | BlockedOnReply \<Rightarrow> reply_cancel_ipc t | BlockedOnNotification event \<Rightarrow> cancel_signal t event | _ \<Rightarrow> return ()
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>state. \<lbrace>st_tcb_at ((=) state) t and (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and st_tcb_at receive_blocked t)\<rbrace> case state of BlockedOnReceive x y \<Rightarrow> blocked_cancel_ipc state t | BlockedOnSend x y \<Rightarrow> blocked_cancel_ipc state t | BlockedOnReply \<Rightarrow> reply_cancel_ipc t | BlockedOnNotification event \<Rightarrow> cancel_signal t event | _ \<Rightarrow> return () \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>state s. st_tcb_at ((=) state) t s \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> st_tcb_at receive_blocked t s \<Longrightarrow> awaiting_reply state \<longrightarrow> invs s \<and> tcb_at t s \<and> is_subject aag t proof (prove)
goal:
No subgoals!
theory Ipc_AC

lemma send_signal_pas_refined:
  "\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\<rbrace>
   send_signal ntfnptr badge
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" apply (simp add: send_signal_def) apply (rule hoare_seq_ext[OF _ get_simple_ko_sp]) apply (wpsimp wp: set_simple_ko_pas_refined update_waiting_ntfn_pas_refined gts_wp
                    set_thread_state_pas_refined cancel_ipc_receive_blocked_pas_refined) apply (fastforce simp: st_tcb_def2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\<rbrace> send_signal ntfnptr badge \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\<rbrace> do ntfn <- get_notification ntfnptr;
case ntfn_obj ntfn of IdleNtfn \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn (ActiveNtfn badge) | 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 badge;
do_extended_op (possible_switch_to tcb)
od else set_notification ntfnptr $ ntfn_set_obj ntfn (ActiveNtfn badge)
od | WaitingNtfn queue \<Rightarrow> update_waiting_ntfn ntfnptr queue (ntfn_bound_tcb ntfn) badge | ActiveNtfn badge' \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn $ ActiveNtfn (combine_ntfn_badges badge badge')
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfn. \<lbrace>ko_at (Notification ntfn) ntfnptr and (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state)\<rbrace> case ntfn_obj ntfn of IdleNtfn \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn (ActiveNtfn badge) | 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 badge;
do_extended_op (possible_switch_to tcb)
od else set_notification ntfnptr $ ntfn_set_obj ntfn (ActiveNtfn badge)
od | WaitingNtfn queue \<Rightarrow> update_waiting_ntfn ntfnptr queue (ntfn_bound_tcb ntfn) badge | ActiveNtfn badge' \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn $ ActiveNtfn (combine_ntfn_badges badge badge') \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s\<rbrakk> \<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 receive_blocked x s))) \<and> (\<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> ko_at (Notification (?ntfn98 ntfn x)) ntfnptr s \<and> ntfn_obj (?ntfn98 ntfn x) = WaitingNtfn x) proof (prove)
goal:
No subgoals!
theory Ipc_AC

lemma st_tcb_at_tcb_states_of_state:
  "(st_tcb_at stf p s) = (\<exists>st. tcb_states_of_state s p = Some st \<and> stf st)" unfolding tcb_states_of_state_def st_tcb_def2 by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. st_tcb_at stf p s = (\<exists>st. tcb_states_of_state s p = Some st \<and> stf st) proof (prove)
goal (1 subgoal):
 1. (\<exists>tcb. get_tcb p s = Some tcb \<and> stf (tcb_state tcb)) = (\<exists>st. map_option tcb_state (get_tcb p s) = Some st \<and> stf st)
theory Ipc_AC

lemma st_tcb_at_tcb_states_of_state_eq:
  "(st_tcb_at ((=) st) p s) = (tcb_states_of_state s p = Some st)" unfolding tcb_states_of_state_def st_tcb_def2 by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. st_tcb_at ((=) st) p s = (tcb_states_of_state s p = Some st) proof (prove)
goal (1 subgoal):
 1. (\<exists>tcb. get_tcb p s = Some tcb \<and> st = tcb_state tcb) = (map_option tcb_state (get_tcb p s) = Some st)
theory Ipc_AC

lemma ipc_buffer_has_auth_None [simp]:
  "ipc_buffer_has_auth aag receiver None" unfolding ipc_buffer_has_auth_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ipc_buffer_has_auth aag receiver None proof (prove)
goal (1 subgoal):
 1. case None of None \<Rightarrow> True | Some p \<Rightarrow> is_aligned p msg_align_bits \<and> (\<forall>x\<in>ptr_range p msg_align_bits. (pasObjectAbs aag receiver, Write, pasObjectAbs aag x) \<in> pasPolicy aag)