kings-crown/FVELER_Isabelle huggingface dataset:
theory Finalise_AI

lemma tcb_cap_valid_imp':
  "((\<forall>(get, set, restr)\<in>ran tcb_cap_cases.
          \<forall>ptr st. restr ptr st cap \<longrightarrow> restr ptr st newcap)
            \<and> (\<forall>ptr. valid_ipc_buffer_cap cap ptr
                       \<longrightarrow> valid_ipc_buffer_cap newcap ptr))
     \<longrightarrow> (tcb_cap_valid cap sl s \<longrightarrow> tcb_cap_valid newcap sl s)" by (fastforce simp: tcb_cap_valid_def elim!: pred_tcb_weakenE
              split: option.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<forall>(get, set, restr)\<in>ran tcb_cap_cases. \<forall>ptr st. restr ptr st cap \<longrightarrow> restr ptr st newcap) \<and> (\<forall>ptr. valid_ipc_buffer_cap cap ptr \<longrightarrow> valid_ipc_buffer_cap newcap ptr) \<longrightarrow> tcb_cap_valid cap sl s \<longrightarrow> tcb_cap_valid newcap sl s
theory Finalise_AI

lemma tcb_cap_valid_imp_NullCap:
  "(\<not> is_master_reply_cap cap)
     \<longrightarrow> (tcb_cap_valid cap sl s \<longrightarrow> tcb_cap_valid cap.NullCap sl s)" apply (strengthen tcb_cap_valid_imp') apply (clarsimp simp: ran_tcb_cap_cases valid_ipc_buffer_cap_def
                 split: Structures_A.thread_state.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> is_master_reply_cap cap \<longrightarrow> tcb_cap_valid cap sl s \<longrightarrow> tcb_cap_valid NullCap sl s proof (prove)
goal (1 subgoal):
 1. \<not> is_master_reply_cap cap \<longrightarrow> (\<forall>(get, set, restr)\<in>ran tcb_cap_cases. \<forall>ptr st. restr ptr st cap \<longrightarrow> restr ptr st NullCap) \<and> (\<forall>ptr. valid_ipc_buffer_cap cap ptr \<longrightarrow> valid_ipc_buffer_cap NullCap ptr) proof (prove)
goal:
No subgoals!
theory Finalise_AI

lemma pred_tcb_at_def2:
  "pred_tcb_at proj P t \<equiv> \<lambda>s. \<exists>tcb. ko_at (TCB tcb) t s \<and> P (proj (tcb_to_itcb tcb))" by (rule eq_reflection, rule ext) (fastforce simp: pred_tcb_at_def obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pred_tcb_at proj P t \<equiv> \<lambda>s. \<exists>tcb. ko_at (TCB tcb) t s \<and> P (proj (tcb_to_itcb tcb))
theory Finalise_AI

lemma deleting_irq_handler_empty:
  "\<lbrace>\<top>\<rbrace>
     deleting_irq_handler irq
   \<lbrace>\<lambda>rv s. cte_wp_at ((=) cap.NullCap) (interrupt_irq_node s irq, []) s\<rbrace>" apply (simp add: deleting_irq_handler_def cte_wp_at_caps_of_state
                   get_irq_slot_def) apply (wp hoare_use_eq_irq_node [OF cap_delete_one_irq_node cap_delete_one_caps_of_state]) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> deleting_irq_handler irq \<lbrace>\<lambda>rv s. cte_wp_at ((=) NullCap) (interrupt_irq_node s irq, []) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> gets (\<lambda>st. (interrupt_irq_node st irq, [])) >>= cap_delete_one \<lbrace>\<lambda>rv s. caps_of_state s (interrupt_irq_node s irq, []) = Some NullCap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> cte_wp_at can_fast_finalise (interrupt_irq_node s irq, []) s \<longrightarrow> ((caps_of_state s)((interrupt_irq_node s irq, []) \<mapsto> NullCap)) (interrupt_irq_node s irq, []) = Some NullCap proof (prove)
goal:
No subgoals!
theory Finalise_AI

lemma cnode_zombie_thread_appropriate[simp]:
  "appropriate_cte_cap cp (cap.CNodeCap a b c)"
  "appropriate_cte_cap cp (cap.ThreadCap f)"
  "appropriate_cte_cap cp (cap.Zombie h i j)" by (simp add: appropriate_cte_cap_def split: cap.splits)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. appropriate_cte_cap cp (CNodeCap a b c) &&& appropriate_cte_cap cp (ThreadCap f) &&& appropriate_cte_cap cp (Zombie h i j)
theory Finalise_AI

lemma unbind_maybe_notification_not_bound:
   "\<lbrace>\<lambda>s. ntfn_at ntfnptr s \<and> valid_objs s \<and> sym_refs (state_refs_of s)\<rbrace>
      unbind_maybe_notification ntfnptr
    \<lbrace>\<lambda>_. obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None) ntfnptr\<rbrace>" apply (simp add: unbind_maybe_notification_def) apply (rule hoare_pre) apply (wp get_simple_ko_wp sbn_obj_at_impossible simple_obj_set_prop_at | wpc | simp)+ apply (clarsimp simp: obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. ntfn_at ntfnptr s \<and> valid_objs s \<and> sym_refs (state_refs_of s)\<rbrace> unbind_maybe_notification ntfnptr \<lbrace>\<lambda>_. obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None) ntfnptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. ntfn_at ntfnptr s \<and> valid_objs s \<and> sym_refs (state_refs_of s)\<rbrace> do ntfn <- get_notification ntfnptr;
case ntfn_bound_tcb ntfn of None \<Rightarrow> return () | Some t \<Rightarrow> do_unbind_notification ntfnptr ntfn t
od \<lbrace>\<lambda>_. obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None) ntfnptr\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do ntfn <- get_notification ntfnptr;
case ntfn_bound_tcb ntfn of None \<Rightarrow> return () | Some t \<Rightarrow> do_unbind_notification ntfnptr ntfn t
od \<lbrace>\<lambda>_. obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None) ntfnptr\<rbrace>
 2. \<And>s. ntfn_at ntfnptr s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. ntfn_at ntfnptr s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<Longrightarrow> \<forall>ntfn. ko_at (Notification ntfn) ntfnptr s \<longrightarrow> ntfn_bound_tcb ntfn = None \<longrightarrow> obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None) ntfnptr s proof (prove)
goal:
No subgoals!
theory Finalise_AI

lemma unbind_notification_bound_tcb_at[wp]:
  "\<lbrace>\<top>\<rbrace> unbind_notification tcbptr \<lbrace>\<lambda>_. bound_tcb_at ((=) None) tcbptr\<rbrace>" apply (simp add: unbind_notification_def) apply (wpsimp wp: sbn_bound_tcb_at') apply (rule gbn_bound_tcb[THEN hoare_strengthen_post]) apply clarsimp apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> unbind_notification tcbptr \<lbrace>\<lambda>_. bound_tcb_at ((=) None) tcbptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do ntfnptr <- get_bound_notification tcbptr;
case ntfnptr of None \<Rightarrow> return () | Some ntfnptr' \<Rightarrow> do ntfn <- get_notification ntfnptr';
do_unbind_notification ntfnptr' ntfn tcbptr
od
od \<lbrace>\<lambda>_. bound_tcb_at ((=) None) tcbptr\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q1\<rbrace> get_bound_notification tcbptr \<lbrace>\<lambda>ntfnptr s. ntfnptr = None \<longrightarrow> bound_tcb_at ((=) None) tcbptr s\<rbrace>
 2. \<And>s. True \<Longrightarrow> ?Q1 s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. bound_tcb_at ((=) rv) tcbptr s \<Longrightarrow> rv = None \<longrightarrow> bound_tcb_at ((=) None) tcbptr s
 2. \<And>s. True \<Longrightarrow> True proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> True proof (prove)
goal:
No subgoals!
theory Finalise_AI

lemma unbind_notification_no_cap_to_obj_ref[wp]:
  "\<lbrace>no_cap_to_obj_with_diff_ref cap S\<rbrace>
     unbind_notification tcbptr
   \<lbrace>\<lambda>_. no_cap_to_obj_with_diff_ref cap S\<rbrace>" apply (simp add: no_cap_to_obj_with_diff_ref_def cte_wp_at_caps_of_state) apply (wp unbind_notification_caps_of_state) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_cap_to_obj_with_diff_ref cap S\<rbrace> unbind_notification tcbptr \<lbrace>\<lambda>_. no_cap_to_obj_with_diff_ref cap S\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>p\<in>UNIV - S. \<forall>capa. obj_refs capa = obj_refs cap \<longrightarrow> caps_of_state s p = Some capa \<longrightarrow> table_cap_ref capa = table_cap_ref cap\<rbrace> unbind_notification tcbptr \<lbrace>\<lambda>_ s. \<forall>p\<in>UNIV - S. \<forall>capa. obj_refs capa = obj_refs cap \<longrightarrow> caps_of_state s p = Some capa \<longrightarrow> table_cap_ref capa = table_cap_ref cap\<rbrace> proof (prove)
goal:
No subgoals!
theory Finalise_AI

lemma empty_slot_cte_wp_elsewhere:
  "\<lbrace>(\<lambda>s. cte_wp_at P p s) and K (p \<noteq> p')\<rbrace> empty_slot p' opt \<lbrace>\<lambda>rv s. cte_wp_at P p s\<rbrace>" apply (rule hoare_gen_asm) apply (simp add: empty_slot_def cte_wp_at_caps_of_state) apply (wp opt_return_pres_lift | simp split del: if_split)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at P p and K (p \<noteq> p')\<rbrace> empty_slot p' opt \<lbrace>\<lambda>rv. cte_wp_at P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. p \<noteq> p' \<Longrightarrow> \<lbrace>cte_wp_at P p\<rbrace> empty_slot p' opt \<lbrace>\<lambda>rv. cte_wp_at P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. p \<noteq> p' \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>cap. caps_of_state s p = Some cap \<and> P cap\<rbrace> do cap <- get_cap p';
if cap = NullCap then return () else do slot_p <- gets (\<lambda>s. cdt s p');
cdt <- gets cdt;
parent <- return $ cdt p';
set_cdt ((\<lambda>p. if cdt p = Some p' then parent else cdt p)(p' := None));
do_extended_op (empty_slot_ext p' slot_p);
set_original p' False;
set_cap NullCap p';
post_cap_deletion opt
od
od \<lbrace>\<lambda>rv s. \<exists>cap. caps_of_state s p = Some cap \<and> P cap\<rbrace> proof (prove)
goal:
No subgoals!
theory Finalise_AI

lemma fast_finalise_lift:
  assumes ep:"\<And>r. \<lbrace>P\<rbrace>cancel_all_ipc r \<lbrace>\<lambda>r s. P s\<rbrace>"
  and ntfn:"\<And>r. \<lbrace>P\<rbrace>cancel_all_signals r \<lbrace>\<lambda>r s. P s\<rbrace>"
  and unbind:"\<And>r. \<lbrace>P\<rbrace> unbind_notification r \<lbrace> \<lambda>r s. P s\<rbrace>"
  and unbind2: "\<And>r. \<lbrace>P\<rbrace> unbind_maybe_notification r \<lbrace> \<lambda>r s. P s\<rbrace>"
  shows "\<lbrace>P\<rbrace> fast_finalise cap final \<lbrace>\<lambda>r s. P s\<rbrace>" apply (case_tac cap,simp_all) apply (wp ep ntfn unbind unbind2 hoare_drop_imps | clarsimp | wpc)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> fast_finalise cap final \<lbrace>\<lambda>r. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x31 x32 x33. cap = EndpointCap x31 x32 x33 \<Longrightarrow> \<lbrace>P\<rbrace> when final (cancel_all_ipc x31) \<lbrace>\<lambda>r. P\<rbrace>
 2. \<And>x41 x42 x43. cap = NotificationCap x41 x42 x43 \<Longrightarrow> \<lbrace>P\<rbrace> when final (do y <- unbind_maybe_notification x41;
cancel_all_signals x41
od) \<lbrace>\<lambda>r. P\<rbrace> proof (prove)
goal:
No subgoals!
theory Finalise_AI

lemma cap_delete_one_cte_wp_at_preserved:
  assumes x: "\<And>cap. P cap \<Longrightarrow> \<not> can_fast_finalise cap"
  shows "\<lbrace>cte_wp_at P p\<rbrace> cap_delete_one ptr \<lbrace>\<lambda>rv s. cte_wp_at P p s\<rbrace>" apply (simp add: cte_wp_at_caps_of_state) apply (wp cap_delete_one_caps_of_state) apply (clarsimp simp: cte_wp_at_caps_of_state x) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at P p\<rbrace> cap_delete_one ptr \<lbrace>\<lambda>rv. cte_wp_at P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at P p\<rbrace> cap_delete_one ptr \<lbrace>\<lambda>rv s. \<exists>cap. caps_of_state s p = Some cap \<and> P cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cte_wp_at P p s \<Longrightarrow> cte_wp_at can_fast_finalise ptr s \<longrightarrow> (\<exists>cap. ((caps_of_state s)(ptr \<mapsto> NullCap)) p = Some cap \<and> P cap) proof (prove)
goal:
No subgoals!
theory Finalise_AI

lemma (in Finalise_AI_1) finalise_cap_equal_cap[wp]:
  "\<lbrace>cte_wp_at ((=) cap) sl\<rbrace>
     finalise_cap cap fin
   \<lbrace>\<lambda>rv. cte_wp_at ((=) cap) sl :: 'a state \<Rightarrow> bool\<rbrace>" apply (cases cap, simp_all split del: if_split) apply (wp suspend_cte_wp_at_preserved
                 deleting_irq_handler_cte_preserved prepare_thread_delete_cte_wp_at
                 hoare_drop_imp thread_set_cte_wp_at_trivial
               | clarsimp simp: can_fast_finalise_def unbind_maybe_notification_def
                                unbind_notification_def
                                tcb_cap_cases_def
               | wpc )+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at ((=) cap) sl\<rbrace> finalise_cap cap fin \<lbrace>\<lambda>rv. cte_wp_at ((=) cap) sl\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x31 x32 x33. cap = EndpointCap x31 x32 x33 \<Longrightarrow> \<lbrace>cte_wp_at ((=) (EndpointCap x31 x32 x33)) sl\<rbrace> liftM (\<lambda>y. (NullCap, NullCap)) (when fin (cancel_all_ipc x31)) \<lbrace>\<lambda>rv. cte_wp_at ((=) (EndpointCap x31 x32 x33)) sl\<rbrace>
 2. \<And>x41 x42 x43. cap = NotificationCap x41 x42 x43 \<Longrightarrow> \<lbrace>cte_wp_at ((=) (NotificationCap x41 x42 x43)) sl\<rbrace> liftM (\<lambda>y. (NullCap, NullCap)) (when fin (do y <- unbind_maybe_notification x41;
cancel_all_signals x41
od)) \<lbrace>\<lambda>rv. cte_wp_at ((=) (NotificationCap x41 x42 x43)) sl\<rbrace>
 3. \<And>x7. cap = ThreadCap x7 \<Longrightarrow> \<lbrace>cte_wp_at ((=) (ThreadCap x7)) sl\<rbrace> do y <- when fin (unbind_notification x7);
y <- when fin (suspend x7);
y <- when fin (prepare_thread_delete x7);
return (if fin then Zombie x7 None 5 else NullCap, NullCap)
od \<lbrace>\<lambda>rv. cte_wp_at ((=) (ThreadCap x7)) sl\<rbrace>
 4. \<And>x10. cap = IRQHandlerCap x10 \<Longrightarrow> \<lbrace>cte_wp_at ((=) (IRQHandlerCap x10)) sl\<rbrace> if fin then do y <- deleting_irq_handler x10;
return (NullCap, IRQHandlerCap x10)
od else return (NullCap, NullCap) \<lbrace>\<lambda>rv. cte_wp_at ((=) (IRQHandlerCap x10)) sl\<rbrace>
 5. \<And>x111 x112 x113. cap = Zombie x111 x112 x113 \<Longrightarrow> \<lbrace>cte_wp_at ((=) (Zombie x111 x112 x113)) sl\<rbrace> do y <- assert fin;
return (Zombie x111 x112 x113, NullCap)
od \<lbrace>\<lambda>rv. cte_wp_at ((=) (Zombie x111 x112 x113)) sl\<rbrace>
 6. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> \<lbrace>cte_wp_at ((=) (ArchObjectCap x12)) sl\<rbrace> arch_finalise_cap x12 fin \<lbrace>\<lambda>rv. cte_wp_at ((=) (ArchObjectCap x12)) sl\<rbrace> proof (prove)
goal:
No subgoals!
theory Finalise_AI

lemma sts_emptyable:
  "\<lbrace>emptyable sl and st_tcb_at (\<lambda>st. \<not> halted st) t\<rbrace>
    set_thread_state t st
   \<lbrace>\<lambda>rv. emptyable sl\<rbrace>" apply (simp add: emptyable_def) apply (subst imp_conv_disj)+ apply (wp hoare_vcg_disj_lift sts_st_tcb_at_cases | simp add: tcb_at_typ)+ apply (clarsimp simp: pred_tcb_at_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>emptyable sl and st_tcb_at (\<lambda>st. \<not> halted st) t\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. emptyable sl\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. tcb_at (fst sl) s \<and> snd sl = tcb_cnode_index 2 \<longrightarrow> st_tcb_at halted (fst sl) s) and st_tcb_at (\<lambda>st. \<not> halted st) t\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv s. tcb_at (fst sl) s \<and> snd sl = tcb_cnode_index 2 \<longrightarrow> st_tcb_at halted (fst sl) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<not> (tcb_at (fst sl) s \<and> snd sl = tcb_cnode_index 2) \<or> st_tcb_at halted (fst sl) s) and st_tcb_at (\<lambda>st. \<not> halted st) t\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv s. \<not> (tcb_at (fst sl) s \<and> snd sl = tcb_cnode_index 2) \<or> st_tcb_at halted (fst sl) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (typ_at ATCB (fst sl) s \<longrightarrow> snd sl = tcb_cnode_index 2 \<longrightarrow> st_tcb_at halted (fst sl) s) \<and> st_tcb_at (\<lambda>st. \<not> halted st) t s \<Longrightarrow> typ_at ATCB (fst sl) s \<longrightarrow> snd sl = tcb_cnode_index 2 \<longrightarrow> t = fst sl \<longrightarrow> halted st proof (prove)
goal:
No subgoals!
theory Finalise_AI

lemma cancel_all_emptyable_helper:
  "\<lbrace>emptyable sl and (\<lambda>s. \<forall>t \<in> set q. st_tcb_at (\<lambda>st. \<not> halted st) t s)\<rbrace>
     mapM_x (\<lambda>t. do y \<leftarrow> set_thread_state t Structures_A.Restart;
                    do_extended_op (tcb_sched_enqueue_ext t) od) q
   \<lbrace>\<lambda>rv. emptyable sl\<rbrace>" apply (rule hoare_strengthen_post) apply (rule mapM_x_wp [where S="set q", simplified]) apply (wp, simp, wp hoare_vcg_const_Ball_lift sts_emptyable sts_st_tcb_at_cases) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>emptyable sl and (\<lambda>s. \<forall>t\<in>set q. st_tcb_at (\<lambda>st. \<not> halted st) t s)\<rbrace> mapM_x (\<lambda>t. do y <- set_thread_state t Restart;
do_extended_op (tcb_sched_enqueue_ext t)
od) q \<lbrace>\<lambda>rv. emptyable sl\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>emptyable sl and (\<lambda>s. \<forall>t\<in>set q. st_tcb_at (\<lambda>st. \<not> halted st) t s)\<rbrace> mapM_x (\<lambda>t. do y <- set_thread_state t Restart;
do_extended_op (tcb_sched_enqueue_ext t)
od) q \<lbrace>?Q\<rbrace>
 2. \<And>rv s. ?Q rv s \<Longrightarrow> emptyable sl s proof (prove)
goal (3 subgoals):
 1. \<And>x. x \<in> set q \<Longrightarrow> \<lbrace>emptyable sl and (\<lambda>s. \<forall>t\<in>set q. st_tcb_at (\<lambda>st. \<not> halted st) t s)\<rbrace> do y <- set_thread_state x Restart;
do_extended_op (tcb_sched_enqueue_ext x)
od \<lbrace>\<lambda>rv. emptyable sl and (\<lambda>s. \<forall>t\<in>set q. st_tcb_at (\<lambda>st. \<not> halted st) t s)\<rbrace>
 2. set q \<subseteq> set q
 3. \<And>rv s. (emptyable sl and (\<lambda>s. \<forall>t\<in>set q. st_tcb_at (\<lambda>st. \<not> halted st) t s)) s \<Longrightarrow> emptyable sl s proof (prove)
goal (3 subgoals):
 1. \<And>x s. \<lbrakk>x \<in> set q; (emptyable sl and (\<lambda>s. \<forall>t\<in>set q. st_tcb_at (\<lambda>st. \<not> halted st) t s)) s\<rbrakk> \<Longrightarrow> (emptyable sl and st_tcb_at (\<lambda>st. \<not> halted st) x) s \<and> (\<forall>xa\<in>set q. (x = xa \<longrightarrow> \<not> halted Restart) \<and> (x \<noteq> xa \<longrightarrow> st_tcb_at (\<lambda>st. \<not> halted st) xa s))
 2. set q \<subseteq> set q
 3. \<And>rv s. (emptyable sl and (\<lambda>s. \<forall>t\<in>set q. st_tcb_at (\<lambda>st. \<not> halted st) t s)) s \<Longrightarrow> emptyable sl s proof (prove)
goal:
No subgoals!
theory Finalise_AI

lemma unbind_notification_emptyable[wp]:
  "\<lbrace> emptyable sl \<rbrace> unbind_notification t \<lbrace> \<lambda>rv. emptyable sl\<rbrace>" unfolding unbind_notification_def apply (wp emptyable_lift hoare_drop_imps thread_set_no_change_tcb_state | wpc |simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>emptyable sl\<rbrace> unbind_notification t \<lbrace>\<lambda>rv. emptyable sl\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>emptyable sl\<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. emptyable sl\<rbrace> proof (prove)
goal:
No subgoals!
theory Finalise_AI

lemma unbind_maybe_notification_emptyable[wp]:
  "\<lbrace> emptyable sl \<rbrace> unbind_maybe_notification r \<lbrace> \<lambda>rv. emptyable sl\<rbrace>" unfolding unbind_maybe_notification_def apply (wp emptyable_lift hoare_drop_imps thread_set_no_change_tcb_state | wpc |simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>emptyable sl\<rbrace> unbind_maybe_notification r \<lbrace>\<lambda>rv. emptyable sl\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>emptyable sl\<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. emptyable sl\<rbrace> proof (prove)
goal:
No subgoals!
theory Finalise_AI

lemma cancel_all_signals_emptyable[wp]:
  "\<lbrace>invs and emptyable sl\<rbrace> cancel_all_signals ptr \<lbrace>\<lambda>_. emptyable sl\<rbrace>" unfolding cancel_all_signals_def unbind_maybe_notification_def apply (rule hoare_seq_ext[OF _ get_simple_ko_sp]) apply (rule hoare_pre) apply (wp cancel_all_emptyable_helper
            hoare_vcg_const_Ball_lift
       | wpc
       | simp)+ apply (auto elim: ntfn_queued_st_tcb_at) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and emptyable sl\<rbrace> cancel_all_signals ptr \<lbrace>\<lambda>_. emptyable sl\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and emptyable sl\<rbrace> do ntfn <- get_notification ptr;
case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> do _ <- set_notification ptr $ 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>_. emptyable sl\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfn. \<lbrace>ko_at (Notification ntfn) ptr and (invs and emptyable sl)\<rbrace> case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> do _ <- set_notification ptr $ 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 () \<lbrace>\<lambda>_. emptyable sl\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ntfn. \<lbrace>?Q4 ntfn\<rbrace> case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> do _ <- set_notification ptr $ 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 () \<lbrace>\<lambda>_. emptyable sl\<rbrace>
 2. \<And>ntfn s. (ko_at (Notification ntfn) ptr and (invs and emptyable sl)) s \<Longrightarrow> ?Q4 ntfn s proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s. ko_at (Notification ntfn) ptr s \<and> invs s \<and> emptyable sl s \<Longrightarrow> \<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> (\<forall>x\<in>set x. st_tcb_at (\<lambda>st. \<not> halted st) x s) proof (prove)
goal:
No subgoals!
theory Finalise_AI

lemma (in Finalise_AI_1) fast_finalise_emptyable[wp]:
  "\<lbrace>invs and emptyable sl\<rbrace> fast_finalise cap fin \<lbrace>\<lambda>rv. emptyable sl\<rbrace>" apply (simp add: fast_finalise_def2) apply (case_tac cap, simp_all add: can_fast_finalise_def) apply (wp unbind_maybe_notification_invs hoare_drop_imps | simp add: o_def  | wpc)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and emptyable sl\<rbrace> fast_finalise cap fin \<lbrace>\<lambda>rv. emptyable sl\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and emptyable sl\<rbrace> do y <- assert (can_fast_finalise cap);
result <- finalise_cap cap fin;
assert (result = (NullCap, NullCap))
od \<lbrace>\<lambda>rv. emptyable sl\<rbrace> proof (prove)
goal (4 subgoals):
 1. cap = NullCap \<Longrightarrow> \<lbrace>invs and emptyable sl\<rbrace> return () \<lbrace>\<lambda>rv. emptyable sl\<rbrace>
 2. \<And>x31 x32 x33. cap = EndpointCap x31 x32 x33 \<Longrightarrow> \<lbrace>invs and emptyable sl\<rbrace> do result <- liftM (\<lambda>y. (NullCap, NullCap)) (when fin (cancel_all_ipc x31));
assert (result = (NullCap, NullCap))
od \<lbrace>\<lambda>rv. emptyable sl\<rbrace>
 3. \<And>x41 x42 x43. cap = NotificationCap x41 x42 x43 \<Longrightarrow> \<lbrace>invs and emptyable sl\<rbrace> do result <- liftM (\<lambda>y. (NullCap, NullCap)) (when fin (do y <- unbind_maybe_notification x41;
cancel_all_signals x41
od));
assert (result = (NullCap, NullCap))
od \<lbrace>\<lambda>rv. emptyable sl\<rbrace>
 4. \<And>x51 x52 x53. cap = ReplyCap x51 x52 x53 \<Longrightarrow> \<lbrace>invs and emptyable sl\<rbrace> return () \<lbrace>\<lambda>rv. emptyable sl\<rbrace> proof (prove)
goal:
No subgoals!