kings-crown/FVELER_Isabelle huggingface dataset:
theory FinalCaps

lemma cancel_ipc_indirect_silc_inv:
  "\<lbrace>silc_inv aag st and st_tcb_at receive_blocked t\<rbrace>
    cancel_ipc t
   \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" unfolding cancel_ipc_def apply (rule hoare_seq_ext[OF _ gts_sp]) apply (rule hoare_name_pre_state) apply (clarsimp simp: st_tcb_def2 receive_blocked_def) apply (simp add: blocked_cancel_ipc_def split: thread_state.splits) apply wpsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and st_tcb_at receive_blocked t\<rbrace> cancel_ipc t \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st 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>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>state. \<lbrace>st_tcb_at ((=) state) t and (silc_inv aag st 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>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>state s. (st_tcb_at ((=) state) t and (silc_inv aag st and st_tcb_at receive_blocked t)) s \<Longrightarrow> \<lbrace>(=) s\<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>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s tcb. \<lbrakk>silc_inv aag st s; get_tcb t s = Some tcb; case tcb_state tcb of BlockedOnReceive x xa \<Rightarrow> True | _ \<Rightarrow> False\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case tcb_state tcb of BlockedOnReceive x y \<Rightarrow> blocked_cancel_ipc (tcb_state tcb) t | BlockedOnSend x y \<Rightarrow> blocked_cancel_ipc (tcb_state tcb) t | BlockedOnReply \<Rightarrow> reply_cancel_ipc t | BlockedOnNotification x \<Rightarrow> cancel_signal t x | _ \<Rightarrow> return () \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s tcb x41 x42. \<lbrakk>silc_inv aag st s; get_tcb t s = Some tcb; tcb_state tcb = BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do epptr <- get_blocking_object (BlockedOnReceive x41 x42);
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>_. silc_inv aag st\<rbrace> proof (prove)
goal:
No subgoals!
theory FinalCaps

lemma intra_label_cap_machine_state[simp]:
  "intra_label_cap aag slot (s\<lparr>machine_state := X\<rparr>) = intra_label_cap aag slot s" by (simp add: intra_label_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. intra_label_cap aag slot (s\<lparr>machine_state := X\<rparr>) = intra_label_cap aag slot s
theory FinalCaps

lemma slots_holding_overlapping_caps_machine_state[simp]:
  "slots_holding_overlapping_caps cap (s\<lparr>machine_state := X\<rparr>) = slots_holding_overlapping_caps cap s" by (simp add: slots_holding_overlapping_caps_def2 ctes_wp_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. slots_holding_overlapping_caps cap (s\<lparr>machine_state := X\<rparr>) = slots_holding_overlapping_caps cap s
theory FinalCaps

lemma intra_label_cap_arch_state[simp]:
  "intra_label_cap aag slot (s\<lparr>arch_state := X\<rparr>) = intra_label_cap aag slot s" by (simp add: intra_label_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. intra_label_cap aag slot (s\<lparr>arch_state := X\<rparr>) = intra_label_cap aag slot s
theory FinalCaps

lemma slots_holding_overlapping_caps_arch_state[simp]:
  "slots_holding_overlapping_caps cap (s\<lparr>arch_state := X\<rparr>) = slots_holding_overlapping_caps cap s" by (simp add: slots_holding_overlapping_caps_def2 ctes_wp_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. slots_holding_overlapping_caps cap (s\<lparr>arch_state := X\<rparr>) = slots_holding_overlapping_caps cap s
theory FinalCaps

lemma is_subject_not_silc_inv:
  "\<lbrakk>silc_inv aag st s; is_subject aag ptr\<rbrakk> \<Longrightarrow> pasObjectAbs aag ptr \<noteq> SilcLabel" using silc_inv_not_subject by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>silc_inv aag st s; is_subject aag ptr\<rbrakk> \<Longrightarrow> pasObjectAbs aag ptr \<noteq> SilcLabel proof (prove)
using this:
silc_inv ?aag ?st ?s \<Longrightarrow> SilcLabel \<noteq> pasSubject ?aag

goal (1 subgoal):
 1. \<lbrakk>silc_inv aag st s; is_subject aag ptr\<rbrakk> \<Longrightarrow> pasObjectAbs aag ptr \<noteq> SilcLabel
theory FinalCaps

lemma validE_validE_R':
  "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, -" apply (rule validE_validE_R) apply (erule hoare_post_impErr) by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s. Q rv s \<Longrightarrow> Q rv s
 2. \<And>e s. R e s \<Longrightarrow> True
theory FinalCaps

lemma finalise_cap_ret_subset_cap_irqs:
  "\<lbrace>\<lambda>s. (cap_irqs cap) = X\<rbrace>
   finalise_cap cap blah
   \<lbrace>\<lambda>rv s :: det_state. (cap_irqs (fst rv)) \<subseteq> X\<rbrace>" apply (cases cap) by (wp arch_finalise_cap_rv | simp add: o_def split del: if_split | simp split: if_split)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cap_irqs cap = X\<rbrace> finalise_cap cap blah \<lbrace>\<lambda>rv s. cap_irqs (fst rv) \<subseteq> X\<rbrace> proof (prove)
goal (12 subgoals):
 1. cap = NullCap \<Longrightarrow> \<lbrace>\<lambda>s. cap_irqs cap = X\<rbrace> finalise_cap cap blah \<lbrace>\<lambda>rv s. cap_irqs (fst rv) \<subseteq> X\<rbrace>
 2. \<And>x21 x22 x23 x24. cap = UntypedCap x21 x22 x23 x24 \<Longrightarrow> \<lbrace>\<lambda>s. cap_irqs cap = X\<rbrace> finalise_cap cap blah \<lbrace>\<lambda>rv s. cap_irqs (fst rv) \<subseteq> X\<rbrace>
 3. \<And>x31 x32 x33. cap = EndpointCap x31 x32 x33 \<Longrightarrow> \<lbrace>\<lambda>s. cap_irqs cap = X\<rbrace> finalise_cap cap blah \<lbrace>\<lambda>rv s. cap_irqs (fst rv) \<subseteq> X\<rbrace>
 4. \<And>x41 x42 x43. cap = NotificationCap x41 x42 x43 \<Longrightarrow> \<lbrace>\<lambda>s. cap_irqs cap = X\<rbrace> finalise_cap cap blah \<lbrace>\<lambda>rv s. cap_irqs (fst rv) \<subseteq> X\<rbrace>
 5. \<And>x51 x52 x53. cap = ReplyCap x51 x52 x53 \<Longrightarrow> \<lbrace>\<lambda>s. cap_irqs cap = X\<rbrace> finalise_cap cap blah \<lbrace>\<lambda>rv s. cap_irqs (fst rv) \<subseteq> X\<rbrace>
 6. \<And>x61 x62 x63. cap = CNodeCap x61 x62 x63 \<Longrightarrow> \<lbrace>\<lambda>s. cap_irqs cap = X\<rbrace> finalise_cap cap blah \<lbrace>\<lambda>rv s. cap_irqs (fst rv) \<subseteq> X\<rbrace>
 7. \<And>x7. cap = ThreadCap x7 \<Longrightarrow> \<lbrace>\<lambda>s. cap_irqs cap = X\<rbrace> finalise_cap cap blah \<lbrace>\<lambda>rv s. cap_irqs (fst rv) \<subseteq> X\<rbrace>
 8. cap = DomainCap \<Longrightarrow> \<lbrace>\<lambda>s. cap_irqs cap = X\<rbrace> finalise_cap cap blah \<lbrace>\<lambda>rv s. cap_irqs (fst rv) \<subseteq> X\<rbrace>
 9. cap = IRQControlCap \<Longrightarrow> \<lbrace>\<lambda>s. cap_irqs cap = X\<rbrace> finalise_cap cap blah \<lbrace>\<lambda>rv s. cap_irqs (fst rv) \<subseteq> X\<rbrace>
 10. \<And>x10. cap = IRQHandlerCap x10 \<Longrightarrow> \<lbrace>\<lambda>s. cap_irqs cap = X\<rbrace> finalise_cap cap blah \<lbrace>\<lambda>rv s. cap_irqs (fst rv) \<subseteq> X\<rbrace>
A total of 12 subgoals...
theory FinalCaps

lemma finalise_cap_ret_subset_obj_refs:
  "\<lbrace>\<lambda>s. obj_refs cap = X\<rbrace>
   finalise_cap cap blah
   \<lbrace>\<lambda>rv s :: det_state. (obj_refs (fst rv)) \<subseteq> X\<rbrace>" apply (cases cap) by (wp arch_finalise_cap_rv | simp add: o_def split del: if_split | simp split: if_split)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. obj_refs cap = X\<rbrace> finalise_cap cap blah \<lbrace>\<lambda>rv s. obj_refs (fst rv) \<subseteq> X\<rbrace> proof (prove)
goal (12 subgoals):
 1. cap = NullCap \<Longrightarrow> \<lbrace>\<lambda>s. obj_refs cap = X\<rbrace> finalise_cap cap blah \<lbrace>\<lambda>rv s. obj_refs (fst rv) \<subseteq> X\<rbrace>
 2. \<And>x21 x22 x23 x24. cap = UntypedCap x21 x22 x23 x24 \<Longrightarrow> \<lbrace>\<lambda>s. obj_refs cap = X\<rbrace> finalise_cap cap blah \<lbrace>\<lambda>rv s. obj_refs (fst rv) \<subseteq> X\<rbrace>
 3. \<And>x31 x32 x33. cap = EndpointCap x31 x32 x33 \<Longrightarrow> \<lbrace>\<lambda>s. obj_refs cap = X\<rbrace> finalise_cap cap blah \<lbrace>\<lambda>rv s. obj_refs (fst rv) \<subseteq> X\<rbrace>
 4. \<And>x41 x42 x43. cap = NotificationCap x41 x42 x43 \<Longrightarrow> \<lbrace>\<lambda>s. obj_refs cap = X\<rbrace> finalise_cap cap blah \<lbrace>\<lambda>rv s. obj_refs (fst rv) \<subseteq> X\<rbrace>
 5. \<And>x51 x52 x53. cap = ReplyCap x51 x52 x53 \<Longrightarrow> \<lbrace>\<lambda>s. obj_refs cap = X\<rbrace> finalise_cap cap blah \<lbrace>\<lambda>rv s. obj_refs (fst rv) \<subseteq> X\<rbrace>
 6. \<And>x61 x62 x63. cap = CNodeCap x61 x62 x63 \<Longrightarrow> \<lbrace>\<lambda>s. obj_refs cap = X\<rbrace> finalise_cap cap blah \<lbrace>\<lambda>rv s. obj_refs (fst rv) \<subseteq> X\<rbrace>
 7. \<And>x7. cap = ThreadCap x7 \<Longrightarrow> \<lbrace>\<lambda>s. obj_refs cap = X\<rbrace> finalise_cap cap blah \<lbrace>\<lambda>rv s. obj_refs (fst rv) \<subseteq> X\<rbrace>
 8. cap = DomainCap \<Longrightarrow> \<lbrace>\<lambda>s. obj_refs cap = X\<rbrace> finalise_cap cap blah \<lbrace>\<lambda>rv s. obj_refs (fst rv) \<subseteq> X\<rbrace>
 9. cap = IRQControlCap \<Longrightarrow> \<lbrace>\<lambda>s. obj_refs cap = X\<rbrace> finalise_cap cap blah \<lbrace>\<lambda>rv s. obj_refs (fst rv) \<subseteq> X\<rbrace>
 10. \<And>x10. cap = IRQHandlerCap x10 \<Longrightarrow> \<lbrace>\<lambda>s. obj_refs cap = X\<rbrace> finalise_cap cap blah \<lbrace>\<lambda>rv s. obj_refs (fst rv) \<subseteq> X\<rbrace>
A total of 12 subgoals...
theory FinalCaps

lemma arch_finalise_cap_ret:
  "(rv, s') \<in> fst (arch_finalise_cap arch_cap final (s :: det_state)) \<Longrightarrow> rv = (NullCap, NullCap)" apply (erule use_valid) apply (wpsimp wp: arch_finalise_cap_rv)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (rv, s') \<in> fst (arch_finalise_cap arch_cap final s) \<Longrightarrow> rv = (NullCap, NullCap) proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P\<rbrace> arch_finalise_cap arch_cap final \<lbrace>\<lambda>a b. a = (NullCap, NullCap)\<rbrace>
 2. ?P s proof (prove)
goal:
No subgoals!
theory FinalCaps

lemma finalise_cap_ret:
  "(rv, s') \<in> fst (finalise_cap cap final (s :: det_state))
   \<Longrightarrow> case (fst rv) of NullCap \<Rightarrow> True | Zombie ptr bits n \<Rightarrow> True | _ \<Rightarrow> False" apply (case_tac cap, simp_all add: return_def) apply (fastforce simp: liftM_def when_def bind_def return_def split: if_split_asm)+ apply (drule arch_finalise_cap_ret) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (rv, s') \<in> fst (finalise_cap cap final s) \<Longrightarrow> case fst rv of NullCap \<Rightarrow> True | Zombie ptr bits n \<Rightarrow> True | _ \<Rightarrow> False proof (prove)
goal (6 subgoals):
 1. \<And>x31 x32 x33. \<lbrakk>(rv, s') \<in> fst (liftM (\<lambda>y. (NullCap, NullCap)) (when final (cancel_all_ipc x31)) s); cap = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> case fst rv of NullCap \<Rightarrow> True | Zombie ptr bits n \<Rightarrow> True | _ \<Rightarrow> False
 2. \<And>x41 x42 x43. \<lbrakk>(rv, s') \<in> fst (liftM (\<lambda>y. (NullCap, NullCap)) (when final (do y <- unbind_maybe_notification x41;
cancel_all_signals x41
od)) s); cap = NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> case fst rv of NullCap \<Rightarrow> True | Zombie ptr bits n \<Rightarrow> True | _ \<Rightarrow> False
 3. \<And>x7. \<lbrakk>(rv, s') \<in> fst ((do y <- when final (unbind_notification x7);
y <- when final (suspend x7);
y <- when final (prepare_thread_delete x7);
\<lambda>s. ({((if final then Zombie x7 None 5 else NullCap, NullCap), s)}, False)
od) s); cap = ThreadCap x7\<rbrakk> \<Longrightarrow> case fst rv of NullCap \<Rightarrow> True | Zombie ptr bits n \<Rightarrow> True | _ \<Rightarrow> False
 4. \<And>x10. \<lbrakk>(rv, s') \<in> fst ((if final then do y <- deleting_irq_handler x10;
\<lambda>s. ({((NullCap, IRQHandlerCap x10), s)}, False)
od else (\<lambda>s. ({((NullCap, NullCap), s)}, False))) s); cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> case fst rv of NullCap \<Rightarrow> True | Zombie ptr bits n \<Rightarrow> True | _ \<Rightarrow> False
 5. \<And>x111 x112 x113. \<lbrakk>(rv, s') \<in> fst ((do y <- assert final;
\<lambda>s. ({((Zombie x111 x112 x113, NullCap), s)}, False)
od) s); cap = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> case fst rv of NullCap \<Rightarrow> True | Zombie ptr bits n \<Rightarrow> True | _ \<Rightarrow> False
 6. \<And>x12. \<lbrakk>(rv, s') \<in> fst (arch_finalise_cap x12 final s); cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> case fst rv of NullCap \<Rightarrow> True | Zombie ptr bits n \<Rightarrow> True | _ \<Rightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x12. \<lbrakk>(rv, s') \<in> fst (arch_finalise_cap x12 final s); cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> case fst rv of NullCap \<Rightarrow> True | Zombie ptr bits n \<Rightarrow> True | _ \<Rightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x12. \<lbrakk>cap = ArchObjectCap x12; rv = (NullCap, NullCap)\<rbrakk> \<Longrightarrow> case fst rv of NullCap \<Rightarrow> True | Zombie ptr bits n \<Rightarrow> True | _ \<Rightarrow> False proof (prove)
goal:
No subgoals!
theory FinalCaps

lemma finalise_cap_ret_is_subject':
  "\<lbrace>K (is_cnode_cap rv \<or> is_thread_cap rv \<or> is_zombie rv \<longrightarrow> is_subject aag (obj_ref_of rv))\<rbrace>
   finalise_cap rv rva
   \<lbrace>\<lambda>rv s :: det_state. (is_zombie (fst rv) \<longrightarrow> is_subject aag (obj_ref_of (fst rv)))\<rbrace>" apply (clarsimp simp: valid_def) apply (drule use_valid[OF _ finalise_cap_ret_is_subject[where aag=aag]]) apply simp apply (case_tac a, simp_all add: is_zombie_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (is_cnode_cap rv \<or> is_thread_cap rv \<or> is_zombie rv \<longrightarrow> is_subject aag (obj_ref_of rv))\<rbrace> finalise_cap rv rva \<lbrace>\<lambda>rv s. is_zombie (fst rv) \<longrightarrow> is_subject aag (obj_ref_of (fst rv))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b ba. \<lbrakk>((a, b), ba) \<in> fst (finalise_cap rv rva s); is_cnode_cap rv \<longrightarrow> is_subject aag (obj_ref_of rv); is_thread_cap rv \<longrightarrow> is_subject aag (obj_ref_of rv); is_zombie rv \<longrightarrow> is_subject aag (obj_ref_of rv); is_zombie a\<rbrakk> \<Longrightarrow> is_subject aag (obj_ref_of a) proof (prove)
goal (2 subgoals):
 1. \<And>s a b ba. \<lbrakk>is_cnode_cap rv \<longrightarrow> is_subject aag (obj_ref_of rv); is_thread_cap rv \<longrightarrow> is_subject aag (obj_ref_of rv); is_zombie rv \<longrightarrow> is_subject aag (obj_ref_of rv); is_zombie a\<rbrakk> \<Longrightarrow> K (is_cnode_cap rv \<or> is_thread_cap rv \<or> is_zombie rv \<longrightarrow> is_subject aag (obj_ref_of rv)) s
 2. \<And>s a b ba. \<lbrakk>is_cnode_cap rv \<longrightarrow> is_subject aag (obj_ref_of rv); is_thread_cap rv \<longrightarrow> is_subject aag (obj_ref_of rv); is_zombie rv \<longrightarrow> is_subject aag (obj_ref_of rv); is_zombie a; case fst (a, b) of Zombie ptr bits n \<Rightarrow> is_subject aag (obj_ref_of (fst (a, b))) | _ \<Rightarrow> True\<rbrakk> \<Longrightarrow> is_subject aag (obj_ref_of a) proof (prove)
goal (1 subgoal):
 1. \<And>s a b ba. \<lbrakk>is_cnode_cap rv \<longrightarrow> is_subject aag (obj_ref_of rv); is_thread_cap rv \<longrightarrow> is_subject aag (obj_ref_of rv); is_zombie rv \<longrightarrow> is_subject aag (obj_ref_of rv); is_zombie a; case fst (a, b) of Zombie ptr bits n \<Rightarrow> is_subject aag (obj_ref_of (fst (a, b))) | _ \<Rightarrow> True\<rbrakk> \<Longrightarrow> is_subject aag (obj_ref_of a) proof (prove)
goal:
No subgoals!
theory FinalCaps

lemma ran_caps_of_state_cte_wp_at:
 "(\<forall>cap \<in> ran (caps_of_state s). P cap) \<Longrightarrow> (\<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> P cap)" by (fastforce simp: cte_wp_at_caps_of_state)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>cap\<in>ran (caps_of_state s). P cap \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> P cap
theory FinalCaps

lemma finalise_cap_ret':
  "\<lbrace>\<top>\<rbrace> finalise_cap cap final \<lbrace>\<lambda>rv s :: det_state. (is_zombie (fst rv) \<or> fst rv = NullCap)\<rbrace>" by (auto simp: valid_def dest!: finalise_cap_ret split: cap.splits simp: is_zombie_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> finalise_cap cap final \<lbrace>\<lambda>rv s. is_zombie (fst rv) \<or> fst rv = NullCap\<rbrace>
theory FinalCaps

lemma silc_inv_irq_state_independent_A[simp, intro!]:
  "irq_state_independent_A (silc_inv aag st)" by (simp add: silc_inv_def irq_state_independent_A_def silc_dom_equiv_def equiv_for_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. irq_state_independent_A (silc_inv aag st)
theory FinalCaps

lemma thread_set_tcb_registers_caps_merge_default_tcb_silc_inv[wp]:
  "\<lbrace>silc_inv aag st\<rbrace>
   thread_set (tcb_registers_caps_merge default_tcb) word
   \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" by (rule thread_set_silc_inv; simp add: tcb_cap_cases_def tcb_registers_caps_merge_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st\<rbrace> thread_set (tcb_registers_caps_merge default_tcb) word \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
theory FinalCaps

lemma cap_delete_silc_inv:
  "\<lbrace>silc_inv aag st and einvs and simple_sched_action and emptyable slot
                    and pas_refined aag and cdt_change_allowed' aag slot\<rbrace>
   cap_delete slot
   \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" unfolding cap_delete_def by (wp rec_del_silc_inv_CTEDelete_transferable' | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and einvs and simple_sched_action and emptyable slot and pas_refined aag and cdt_change_allowed' aag slot\<rbrace> cap_delete slot \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and einvs and simple_sched_action and emptyable slot and pas_refined aag and cdt_change_allowed' aag slot\<rbrace> doE rec_del (CTEDeleteCall slot True);
returnOk ()
odE \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
theory FinalCaps

lemma cap_revoke_silc_inv:
  "\<lbrace>silc_inv aag st and pas_refined aag and einvs
                    and simple_sched_action and K (is_subject aag (fst slot))\<rbrace>
   cap_revoke slot
   \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" apply (rule use_spec) apply (rule cap_revoke_silc_inv') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and pas_refined aag and einvs and simple_sched_action and K (is_subject aag (fst slot))\<rbrace> cap_revoke slot \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. s \<turnstile> \<lbrace>silc_inv aag st and pas_refined aag and einvs and simple_sched_action and K (is_subject aag (fst slot))\<rbrace> cap_revoke slot \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal:
No subgoals!
theory FinalCaps

lemma finalise_slot_silc_inv:
  "\<lbrace>silc_inv aag st and einvs and pas_refined aag and simple_sched_action
                    and emptyable slot and K (is_subject aag (fst slot))\<rbrace>
   finalise_slot slot blah
   \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" unfolding finalise_slot_def apply (rule validE_valid) apply (rule hoare_pre) apply (rule rec_del_silc_inv_not_transferable) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and einvs and pas_refined aag and simple_sched_action and emptyable slot and K (is_subject aag (fst slot))\<rbrace> finalise_slot slot blah \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and einvs and pas_refined aag and simple_sched_action and emptyable slot and K (is_subject aag (fst slot))\<rbrace> rec_del (FinaliseSlotCall slot blah) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and einvs and pas_refined aag and simple_sched_action and emptyable slot and K (is_subject aag (fst slot))\<rbrace> rec_del (FinaliseSlotCall slot blah) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q2\<rbrace> rec_del (FinaliseSlotCall slot blah) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>, \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. \<And>s. (silc_inv aag st and einvs and pas_refined aag and simple_sched_action and emptyable slot and K (is_subject aag (fst slot))) s \<Longrightarrow> ?Q2 s proof (prove)
goal (1 subgoal):
 1. \<And>s. (silc_inv aag st and einvs and pas_refined aag and simple_sched_action and emptyable slot and K (is_subject aag (fst slot))) s \<Longrightarrow> (silc_inv aag st and einvs and simple_sched_action and valid_rec_del_call (FinaliseSlotCall slot blah) and emptyable (slot_rdcall (FinaliseSlotCall slot blah)) and pas_refined aag and K (case FinaliseSlotCall slot blah of CTEDeleteCall slot x \<Rightarrow> is_subject aag (fst slot) | FinaliseSlotCall slot x \<Rightarrow> is_subject aag (fst slot) | ReduceZombieCall cap slot x \<Rightarrow> is_subject aag (fst slot) \<and> is_subject aag (obj_ref_of cap))) s proof (prove)
goal:
No subgoals!