kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchRetype_AI

lemma caps_region_kernel_window_imp:
  "caps_of_state s p = Some cap
    \<Longrightarrow> cap_refs_in_kernel_window s
    \<Longrightarrow> S \<subseteq> cap_range cap
    \<Longrightarrow> region_in_kernel_window S s" apply (simp add: region_in_kernel_window_def) apply (drule(1) cap_refs_in_kernel_windowD) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some cap; cap_refs_in_kernel_window s; S \<subseteq> cap_range cap\<rbrakk> \<Longrightarrow> region_in_kernel_window S s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some cap; cap_refs_in_kernel_window s; S \<subseteq> cap_range cap\<rbrakk> \<Longrightarrow> \<forall>x\<in>S. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_refs_in_kernel_window s; S \<subseteq> cap_range cap; \<forall>ref\<in>cap_range cap. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow\<rbrakk> \<Longrightarrow> \<forall>x\<in>S. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow proof (prove)
goal:
No subgoals!
theory ArchRetype_AI

lemma valid_arch_mdb_detype:
  "valid_arch_mdb (is_original_cap s) (caps_of_state s) \<Longrightarrow>
            valid_arch_mdb (is_original_cap (detype (untyped_range cap) s))
         (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p)" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_arch_mdb (is_original_cap s) (caps_of_state s) \<Longrightarrow> valid_arch_mdb (is_original_cap (detype (untyped_range cap) s)) (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p)
theory Finalise_AI

lemma update_restart_pc_caps_of_state[wp]:
  "\<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> update_restart_pc t \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>" by (simp add: update_restart_pc_def as_user_caps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> update_restart_pc t \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>
theory Finalise_AI

lemma halted_emptyable:
  "\<And>ref. halted_if_tcb t s \<Longrightarrow> emptyable (t, ref) s" by (simp add: halted_if_tcb_def emptyable_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>ref. halted_if_tcb t s \<Longrightarrow> emptyable (t, ref) s
theory Finalise_AI

lemma emptyable_valid_NullCapD:
  "\<lbrakk> emptyable sl s; valid_objs s \<rbrakk> \<Longrightarrow> tcb_cap_valid cap.NullCap sl s" apply (clarsimp simp: emptyable_def tcb_cap_valid_def
                        valid_ipc_buffer_cap_def) apply (clarsimp simp: pred_tcb_at_def obj_at_def is_tcb split: option.split) apply (erule(1) valid_objsE) apply (clarsimp simp: valid_obj_def valid_tcb_def tcb_cap_cases_def
                 split: Structures_A.thread_state.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>emptyable sl s; valid_objs s\<rbrakk> \<Longrightarrow> tcb_cap_valid NullCap sl s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>snd sl = tcb_cnode_index 2 \<longrightarrow> st_tcb_at halted (fst sl) s; valid_objs s; tcb_at (fst sl) s\<rbrakk> \<Longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd sl) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst sl) st NullCap) (fst sl) s proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>snd sl = tcb_cnode_index 2 \<longrightarrow> halted (tcb_state tcb); valid_objs s; kheap s (fst sl) = Some (TCB tcb)\<rbrakk> \<Longrightarrow> \<exists>tcba. (tcb_cap_cases (snd sl) = None \<longrightarrow> tcb = tcba) \<and> (\<forall>a aa b. tcb_cap_cases (snd sl) = Some (a, aa, b) \<longrightarrow> tcb = tcba \<and> b (fst sl) (tcb_state tcba) NullCap) proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>snd sl = tcb_cnode_index 2 \<longrightarrow> halted (tcb_state tcb); kheap s (fst sl) = Some (TCB tcb); valid_obj (fst sl) (TCB tcb) s\<rbrakk> \<Longrightarrow> \<exists>tcba. (tcb_cap_cases (snd sl) = None \<longrightarrow> tcb = tcba) \<and> (\<forall>a aa b. tcb_cap_cases (snd sl) = Some (a, aa, b) \<longrightarrow> tcb = tcba \<and> b (fst sl) (tcb_state tcba) NullCap) proof (prove)
goal:
No subgoals!
theory Finalise_AI

lemma emptyable_valid_NullCap_strg:
  "emptyable sl s \<and> valid_objs s \<longrightarrow> tcb_cap_valid cap.NullCap sl s" by (simp add: emptyable_valid_NullCapD)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. emptyable sl s \<and> valid_objs s \<longrightarrow> tcb_cap_valid NullCap sl s
theory Finalise_AI

lemma tcb_cap_valid_pspaceI[intro]:
  "\<lbrakk> tcb_cap_valid cap sl s; kheap s = kheap s' \<rbrakk> \<Longrightarrow> tcb_cap_valid cap sl s'" by (clarsimp simp: tcb_cap_valid_def obj_at_def pred_tcb_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_cap_valid cap sl s; kheap s = kheap s'\<rbrakk> \<Longrightarrow> tcb_cap_valid cap sl s'
theory Finalise_AI

lemma emptyable_rvk[simp]:
  "emptyable sl (is_original_cap_update f s) = emptyable sl s" by (simp add: emptyable_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. emptyable sl (is_original_cap_update f s) = emptyable sl s
theory Finalise_AI

lemma set_cdt_emptyable[wp]:
  "\<lbrace>emptyable sl\<rbrace> set_cdt m \<lbrace>\<lambda>rv. emptyable sl\<rbrace>" by (simp add: set_cdt_def emptyable_def | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>emptyable sl\<rbrace> set_cdt m \<lbrace>\<lambda>rv. emptyable sl\<rbrace>
theory Finalise_AI

lemma emptyable_more_update[simp]:
  "emptyable sl (trans_state f s) = emptyable sl s" by (simp add: emptyable_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. emptyable sl (trans_state f s) = emptyable sl s
theory Finalise_AI

lemma tcb_cp_valid_trans_state_update[simp]: "tcb_cap_valid cap sl
         (trans_state f s) = tcb_cap_valid cap sl s" apply (simp add: tcb_cap_valid_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_cap_valid cap sl (trans_state f s) = tcb_cap_valid cap sl s proof (prove)
goal:
No subgoals!
theory Finalise_AI

lemma empty_slot_valid_objs[wp]:
  "\<lbrace>valid_objs and emptyable sl\<rbrace> empty_slot sl irqopt \<lbrace>\<lambda>rv. valid_objs\<rbrace>" apply (simp add: empty_slot_def) apply (rule hoare_pre) apply (wp set_cap_valid_objs set_cdt_valid_objs set_cdt_valid_cap
                 | simp add: trans_state_update[symmetric] del: trans_state_update| wpcw
                 | strengthen emptyable_valid_NullCap_strg
                 | wp (once) hoare_drop_imps)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and emptyable sl\<rbrace> empty_slot sl irqopt \<lbrace>\<lambda>rv. valid_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and emptyable sl\<rbrace> do cap <- get_cap sl;
if cap = NullCap then return () else do slot_p <- gets (\<lambda>s. cdt s sl);
cdt <- gets cdt;
parent <- return $ cdt sl;
set_cdt ((\<lambda>p. if cdt p = Some sl then parent else cdt p)(sl := None));
do_extended_op (empty_slot_ext sl slot_p);
set_original sl False;
set_cap NullCap sl;
post_cap_deletion irqopt
od
od \<lbrace>\<lambda>rv. valid_objs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do cap <- get_cap sl;
if cap = NullCap then return () else do slot_p <- gets (\<lambda>s. cdt s sl);
cdt <- gets cdt;
parent <- return $ cdt sl;
set_cdt ((\<lambda>p. if cdt p = Some sl then parent else cdt p)(sl := None));
do_extended_op (empty_slot_ext sl slot_p);
set_original sl False;
set_cap NullCap sl;
post_cap_deletion irqopt
od
od \<lbrace>\<lambda>rv. valid_objs\<rbrace>
 2. \<And>s. (valid_objs and emptyable sl) s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory Finalise_AI

lemma (in mdb_empty_abs) descendants:
  "descendants_of p n =
  (if p = slot then {} else descendants_of p m - {slot})" by (auto simp add: descendants_of_def parency)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. descendants_of p n = (if p = slot then {} else descendants_of p m - {slot})
theory Finalise_AI

lemma (in mdb_empty_abs) no_mloop_n:
  "no_mloop n" by (simp add: no_mloop_def parency)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_mloop n
theory Finalise_AI

lemma final_mdb_update[simp]:
  "is_final_cap' cap (cdt_update f s) = is_final_cap' cap s" by (clarsimp simp: is_final_cap'_def2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_final_cap' cap (cdt_update f s) = is_final_cap' cap s
theory Finalise_AI

lemma no_cap_to_obj_with_diff_cdt_update[simp]:
  "no_cap_to_obj_with_diff_ref cap S (cdt_update f s)
        = no_cap_to_obj_with_diff_ref cap S s" by (simp add: no_cap_to_obj_with_diff_ref_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_cap_to_obj_with_diff_ref cap S (cdt_update f s) = no_cap_to_obj_with_diff_ref cap S s
theory Finalise_AI

lemma no_cap_to_obj_with_diff_rvk_update[simp]:
  "no_cap_to_obj_with_diff_ref cap S (is_original_cap_update f s)
        = no_cap_to_obj_with_diff_ref cap S s" by (simp add: no_cap_to_obj_with_diff_ref_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_cap_to_obj_with_diff_ref cap S (is_original_cap_update f s) = no_cap_to_obj_with_diff_ref cap S s
theory Finalise_AI

lemma zombies_final_cdt_update[simp]:
  "zombies_final (cdt_update f s) = zombies_final s" by (fastforce elim!: zombies_final_pspaceI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. zombies_final (cdt_update f s) = zombies_final s
theory Finalise_AI

lemma post_cap_deletion_invs:
  "\<lbrace>\<lambda>s. invs s \<and> (info \<noteq> NullCap \<longrightarrow> post_cap_delete_pre info (caps_of_state s))\<rbrace>
     post_cap_deletion info
   \<lbrace>\<lambda>rv. invs\<rbrace>" unfolding post_cap_deletion_def deleted_irq_handler_def apply (rule hoare_pre) apply (wp arch_post_cap_deletion_invs | wpc)+ apply (clarsimp simp: post_cap_delete_pre_def split: cap.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. invs s \<and> (info \<noteq> NullCap \<longrightarrow> post_cap_delete_pre info (caps_of_state s))\<rbrace> post_cap_deletion info \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. invs s \<and> (info \<noteq> NullCap \<longrightarrow> post_cap_delete_pre info (caps_of_state s))\<rbrace> case info of IRQHandlerCap irq \<Rightarrow> set_irq_state IRQInactive irq | ArchObjectCap acap \<Rightarrow> arch_post_cap_deletion acap | _ \<Rightarrow> return () \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> case info of IRQHandlerCap irq \<Rightarrow> set_irq_state IRQInactive irq | ArchObjectCap acap \<Rightarrow> arch_post_cap_deletion acap | _ \<Rightarrow> return () \<lbrace>\<lambda>rv. invs\<rbrace>
 2. \<And>s. invs s \<and> (info \<noteq> NullCap \<longrightarrow> post_cap_delete_pre info (caps_of_state s)) \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. invs s \<and> (info \<noteq> NullCap \<longrightarrow> post_cap_delete_pre info (caps_of_state s)) \<Longrightarrow> (info = NullCap \<longrightarrow> invs s) \<and> (\<forall>x xa xb xc. info = UntypedCap x xa xb xc \<longrightarrow> invs s) \<and> (\<forall>x xa xb. info = EndpointCap x xa xb \<longrightarrow> invs s) \<and> (\<forall>x xa xb. info = NotificationCap x xa xb \<longrightarrow> invs s) \<and> (\<forall>x xa xb. info = ReplyCap x xa xb \<longrightarrow> invs s) \<and> (\<forall>x xa xb. info = CNodeCap x xa xb \<longrightarrow> invs s) \<and> (\<forall>x. info = ThreadCap x \<longrightarrow> invs s) \<and> (info = DomainCap \<longrightarrow> invs s) \<and> (info = IRQControlCap \<longrightarrow> invs s) \<and> (\<forall>x. info = IRQHandlerCap x \<longrightarrow> invs s \<and> (IRQInactive \<noteq> IRQSignal \<longrightarrow> IRQHandlerCap x \<notin> ran (caps_of_state s))) \<and> (\<forall>x xa xb. info = Zombie x xa xb \<longrightarrow> invs s) \<and> (\<forall>x. info = ArchObjectCap x \<longrightarrow> (invs and (\<lambda>s. arch_post_cap_delete_pre (ArchObjectCap x) (caps_of_state s))) s) proof (prove)
goal:
No subgoals!
theory Finalise_AI

lemma empty_slot_deletes[wp]:
  "\<lbrace>\<top>\<rbrace> empty_slot sl opt \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>c. c = cap.NullCap) sl\<rbrace>" apply (simp add: empty_slot_def) apply (wp set_cap_sets get_cap_wp opt_return_pres_lift|simp)+ apply (clarsimp elim!: cte_wp_at_weakenE) done

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

lemma empty_slot_final_cap_at:
  "\<lbrace>(\<lambda>s. cte_wp_at (\<lambda>c. is_final_cap' c s) p s) and K (p \<noteq> p')\<rbrace>
      empty_slot p' opt \<lbrace>\<lambda>rv s. cte_wp_at (\<lambda>c. is_final_cap' c s) p s\<rbrace>" apply (rule hoare_gen_asm) apply (simp add: empty_slot_def final_cap_at_eq cte_wp_at_conj cte_wp_at_caps_of_state) apply (wpsimp wp: opt_return_pres_lift get_cap_wp) apply (fastforce simp: )? done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. cte_wp_at (\<lambda>c. is_final_cap' c s) p s) and K (p \<noteq> p')\<rbrace> empty_slot p' opt \<lbrace>\<lambda>rv s. cte_wp_at (\<lambda>c. is_final_cap' c s) p s\<rbrace> proof (prove)
goal (1 subgoal):
 1. p \<noteq> p' \<Longrightarrow> \<lbrace>\<lambda>s. cte_wp_at (\<lambda>c. is_final_cap' c s) p s\<rbrace> empty_slot p' opt \<lbrace>\<lambda>rv s. cte_wp_at (\<lambda>c. is_final_cap' c s) p s\<rbrace> proof (prove)
goal (1 subgoal):
 1. p \<noteq> p' \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>cp. caps_of_state s p = Some cp \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs 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>cp. caps_of_state s p = Some cp \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {}))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s cp cap a b capa. \<lbrakk>p \<noteq> p'; caps_of_state s p = Some cp; gen_obj_refs cp \<noteq> {}; \<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {}); cte_wp_at ((=) cap) p' s; cap \<noteq> NullCap; (a, b) \<noteq> p'; (a, b) \<noteq> p; caps_of_state s (a, b) = Some capa\<rbrakk> \<Longrightarrow> gen_obj_refs cp \<inter> gen_obj_refs capa = {} proof (prove)
goal:
No subgoals!
theory Finalise_AI

lemma tcb_cap_cases_lt:
  "n < 5 \<Longrightarrow> tcb_cap_cases (nat_to_cref 3 n) \<noteq> None" unfolding tcb_cnode_index_def2[symmetric] by (simp add: tcb_cap_cases_def
         | erule less_handy_casesE)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n < 5 \<Longrightarrow> tcb_cap_cases (nat_to_cref 3 n) \<noteq> None proof (prove)
goal (1 subgoal):
 1. n < 5 \<Longrightarrow> tcb_cap_cases (tcb_cnode_index n) \<noteq> None
theory Finalise_AI

lemma cte_refs_CNode_Zombie_helper[simp]:
  "{xs. length xs = n \<and> unat (of_bl xs :: word32) < 2 ^ n}
     = {xs. length xs = n}" apply safe apply (rule unat_of_bl_length) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {xs. length xs = n \<and> unat (of_bl xs) < 2 ^ n} = {xs. length xs = n} proof (prove)
goal (1 subgoal):
 1. \<And>x. n = length x \<Longrightarrow> unat (of_bl x) < 2 ^ length x proof (prove)
goal:
No subgoals!
theory Finalise_AI

lemma empty_slot_caps_of_state:
  "\<lbrace>\<lambda>s. P ((caps_of_state s) (slot \<mapsto> cap.NullCap))\<rbrace>
     empty_slot slot opt
   \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace>" apply (simp add: empty_slot_def set_cdt_def) apply (wp get_cap_wp opt_return_pres_lift | simp)+ apply (clarsimp simp: cte_wp_at_caps_of_state
                        fun_upd_def[symmetric]
                        fun_upd_idem) done

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

lemma suspend_caps_of_state:
  "\<lbrace>\<lambda>s. (\<forall>p. cte_wp_at can_fast_finalise p s
           \<longrightarrow> P ((caps_of_state s) (p \<mapsto> cap.NullCap)))
           \<and> P (caps_of_state s)\<rbrace>
     suspend t
   \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace>" by (wpsimp wp: cancel_ipc_caps_of_state simp: suspend_def fun_upd_def[symmetric])+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>p. cte_wp_at can_fast_finalise p s \<longrightarrow> P ((caps_of_state s)(p \<mapsto> NullCap))) \<and> P (caps_of_state s)\<rbrace> suspend t \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace>
theory Finalise_AI

lemma deleting_irq_handler_final:
  "\<lbrace>is_final_cap' cap and cte_wp_at ((=) cap) slot
          and K (\<not> can_fast_finalise cap)\<rbrace>
      deleting_irq_handler irq
   \<lbrace>\<lambda>rv. is_final_cap' cap\<rbrace>" apply  (rule hoare_gen_asm) apply (simp add: deleting_irq_handler_def) apply (wp cap_delete_one_final_cap[where slot=slot]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>is_final_cap' cap and cte_wp_at ((=) cap) slot and K (\<not> can_fast_finalise cap)\<rbrace> deleting_irq_handler irq \<lbrace>\<lambda>rv. is_final_cap' cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<not> can_fast_finalise cap \<Longrightarrow> \<lbrace>is_final_cap' cap and cte_wp_at ((=) cap) slot\<rbrace> deleting_irq_handler irq \<lbrace>\<lambda>rv. is_final_cap' cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<not> can_fast_finalise cap \<Longrightarrow> \<lbrace>is_final_cap' cap and cte_wp_at ((=) cap) slot\<rbrace> get_irq_slot irq >>= cap_delete_one \<lbrace>\<lambda>rv. is_final_cap' cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<not> can_fast_finalise cap; (is_final_cap' cap and cte_wp_at ((=) cap) slot) s\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) slot s \<and> \<not> can_fast_finalise cap \<and> is_final_cap' cap s proof (prove)
goal:
No subgoals!
theory Finalise_AI

lemma unbind_notification_cte_wp_at[wp]:
  "\<lbrace>\<lambda>s. cte_wp_at P slot s\<rbrace> unbind_notification t \<lbrace>\<lambda>rv s. cte_wp_at P slot s\<rbrace>" by (wp thread_set_cte_wp_at_trivial hoare_drop_imp | wpc | simp add: unbind_notification_def tcb_cap_cases_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at P slot\<rbrace> unbind_notification t \<lbrace>\<lambda>rv. cte_wp_at P slot\<rbrace>
theory Finalise_AI

lemma is_final_cap'_objrefsE:
  "\<lbrakk> is_final_cap' cap s; gen_obj_refs cap = gen_obj_refs cap' \<rbrakk>
     \<Longrightarrow> is_final_cap' cap' s" by (simp add: is_final_cap'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_final_cap' cap s; gen_obj_refs cap = gen_obj_refs cap'\<rbrakk> \<Longrightarrow> is_final_cap' cap' s
theory Finalise_AI

lemma unbind_notification_valid_cap[wp]:
  "\<lbrace>valid_cap cap\<rbrace> unbind_notification t \<lbrace>\<lambda>rv. valid_cap cap\<rbrace>" unfolding unbind_notification_def by (wp abs_typ_at_lifts hoare_drop_imps | wpc | clarsimp)+

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

lemma refs_in_ntfn_q_refs:
  "(x, ref) \<in> ntfn_q_refs_of ntfn \<Longrightarrow> ref = NTFNSignal" by (clarsimp simp: ntfn_q_refs_of_def split: ntfn.splits)

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

lemma ntfn_q_refs_no_TCBSignal:
  "(x, TCBSignal) \<notin> ntfn_q_refs_of ntfn" by (clarsimp simp: ntfn_q_refs_of_def split: ntfn.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x, TCBSignal) \<notin> ntfn_q_refs_of ntfn
theory Finalise_AI

lemma tcb_st_refs_no_TCBBound:
  "(x, TCBBound) \<notin> tcb_st_refs_of ts" by (clarsimp simp: tcb_st_refs_of_def split: thread_state.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x, TCBBound) \<notin> tcb_st_refs_of ts
theory Finalise_AI

lemma cnode_at_unlive[elim!]:
  "s \<turnstile> cap.CNodeCap ptr bits gd \<Longrightarrow> obj_at (\<lambda>ko. \<not> live ko) ptr s" by (clarsimp simp: live_def valid_cap_def is_cap_table
              elim!: obj_at_weakenE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<turnstile> CNodeCap ptr bits gd \<Longrightarrow> obj_at (\<lambda>ko. \<not> live ko) ptr s
theory Finalise_AI

lemma set_thread_state_final_cap[wp]:
  "\<lbrace>is_final_cap' cap\<rbrace> set_thread_state st t \<lbrace>\<lambda>rv. is_final_cap' cap\<rbrace>" by (simp add: is_final_cap'_def2 cte_wp_at_caps_of_state, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>is_final_cap' cap\<rbrace> set_thread_state st t \<lbrace>\<lambda>rv. is_final_cap' cap\<rbrace>