kings-crown/FVELER_Isabelle huggingface dataset:
theory Finalise_R

lemma clearUntypedFreeIndex_valid_pspace'[wp]:
  "\<lbrace>valid_pspace'\<rbrace> clearUntypedFreeIndex slot \<lbrace>\<lambda>rv. valid_pspace'\<rbrace>" apply (simp add: valid_pspace'_def) apply (rule hoare_pre) apply (wp | simp add: valid_mdb'_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_pspace'\<rbrace> clearUntypedFreeIndex slot \<lbrace>\<lambda>rv. valid_pspace'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb'\<rbrace> clearUntypedFreeIndex slot \<lbrace>\<lambda>rv. valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> clearUntypedFreeIndex slot \<lbrace>\<lambda>rv. valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb'\<rbrace>
 2. \<And>s. (valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb') s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory Finalise_R

lemma isFinalCapability_inv:
  "\<lbrace>P\<rbrace> isFinalCapability cap \<lbrace>\<lambda>_. P\<rbrace>" apply (simp add: isFinalCapability_def Let_def
              split del: if_split cong: if_cong) apply (rule hoare_pre, wp) apply (rule hoare_post_imp [where Q="\<lambda>s. P"], simp) apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> isFinalCapability cap \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> do prevIsSameObject <- if mdbPrev (cteMDBNode cap) = nullPointer then return False else do prev <- getCTE (mdbPrev (cteMDBNode cap));
return (global.sameObjectAs (cteCap prev) (cteCap cap))
od;
if prevIsSameObject then return False else if mdbNext (cteMDBNode cap) = nullPointer then return True else do next <- getCTE (mdbNext (cteMDBNode cap));
return (\<not> global.sameObjectAs (cteCap cap) (cteCap next))
od
od \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. mdbPrev (cteMDBNode cap) \<noteq> nullPointer \<Longrightarrow> \<lbrace>?R18\<rbrace> getCTE (mdbPrev (cteMDBNode cap)) \<lbrace>\<lambda>prev a. (global.sameObjectAs (cteCap prev) (cteCap cap) \<longrightarrow> P a) \<and> (\<not> global.sameObjectAs (cteCap prev) (cteCap cap) \<longrightarrow> (mdbNext (cteMDBNode cap) = nullPointer \<longrightarrow> P a) \<and> (mdbNext (cteMDBNode cap) \<noteq> nullPointer \<longrightarrow> P a))\<rbrace>
 2. \<And>s. P s \<Longrightarrow> (mdbPrev (cteMDBNode cap) = nullPointer \<longrightarrow> (False \<longrightarrow> P s) \<and> (\<not> False \<longrightarrow> (mdbNext (cteMDBNode cap) = nullPointer \<longrightarrow> P s) \<and> (mdbNext (cteMDBNode cap) \<noteq> nullPointer \<longrightarrow> P s))) \<and> (mdbPrev (cteMDBNode cap) \<noteq> nullPointer \<longrightarrow> ?R18 s) proof (prove)
goal (2 subgoals):
 1. mdbPrev (cteMDBNode cap) \<noteq> nullPointer \<Longrightarrow> \<lbrace>?R18\<rbrace> getCTE (mdbPrev (cteMDBNode cap)) \<lbrace>\<lambda>s. P\<rbrace>
 2. \<And>s. P s \<Longrightarrow> (mdbPrev (cteMDBNode cap) = nullPointer \<longrightarrow> (False \<longrightarrow> P s) \<and> (\<not> False \<longrightarrow> (mdbNext (cteMDBNode cap) = nullPointer \<longrightarrow> P s) \<and> (mdbNext (cteMDBNode cap) \<noteq> nullPointer \<longrightarrow> P s))) \<and> (mdbPrev (cteMDBNode cap) \<noteq> nullPointer \<longrightarrow> ?R18 s) proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> (mdbPrev (cteMDBNode cap) = nullPointer \<longrightarrow> (False \<longrightarrow> P s) \<and> (\<not> False \<longrightarrow> (mdbNext (cteMDBNode cap) = nullPointer \<longrightarrow> P s) \<and> (mdbNext (cteMDBNode cap) \<noteq> nullPointer \<longrightarrow> P s))) \<and> (mdbPrev (cteMDBNode cap) \<noteq> nullPointer \<longrightarrow> P s) proof (prove)
goal:
No subgoals!
theory Finalise_R

lemma final_matters_sameRegion_sameObject:
  "final_matters' cap \<Longrightarrow> sameRegionAs cap cap' = sameObjectAs cap cap'" apply (rule iffI) apply (erule sameRegionAsE) apply (simp add: sameObjectAs_def3) apply (clarsimp simp: isCap_simps sameObjectAs_sameRegionAs final_matters'_def
        split:capability.splits arch_capability.splits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. final_matters' cap \<Longrightarrow> global.sameRegionAs cap cap' = global.sameObjectAs cap cap' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>final_matters' cap; global.sameRegionAs cap cap'\<rbrakk> \<Longrightarrow> global.sameObjectAs cap cap'
 2. \<lbrakk>final_matters' cap; global.sameObjectAs cap cap'\<rbrakk> \<Longrightarrow> global.sameRegionAs cap cap' proof (prove)
goal (5 subgoals):
 1. \<lbrakk>final_matters' cap; capMasterCap cap = capMasterCap cap'; \<not> isNullCap cap; \<not> isZombie cap; \<not> isUntypedCap cap; \<not> isArchPageCap cap\<rbrakk> \<Longrightarrow> global.sameObjectAs cap cap'
 2. \<lbrakk>final_matters' cap; capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isUntypedCap cap\<rbrakk> \<Longrightarrow> global.sameObjectAs cap cap'
 3. \<lbrakk>final_matters' cap; capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isArchPageCap cap; isArchPageCap cap'\<rbrakk> \<Longrightarrow> global.sameObjectAs cap cap'
 4. \<lbrakk>final_matters' cap; isIRQControlCap cap; isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> global.sameObjectAs cap cap'
 5. \<lbrakk>final_matters' cap; global.sameObjectAs cap cap'\<rbrakk> \<Longrightarrow> global.sameRegionAs cap cap' proof (prove)
goal (5 subgoals):
 1. \<lbrakk>final_matters' cap; capMasterCap cap = capMasterCap cap'; cap \<noteq> capability.NullCap; \<not> isZombie cap; \<not> isUntypedCap cap; \<not> isArchPageCap cap\<rbrakk> \<Longrightarrow> cap' \<noteq> capability.NullCap \<and> \<not> isZombie cap' \<and> \<not> isUntypedCap cap' \<and> (isArchPageCap cap' \<longrightarrow> capRange cap' \<noteq> {})
 2. \<lbrakk>final_matters' cap; capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isUntypedCap cap\<rbrakk> \<Longrightarrow> global.sameObjectAs cap cap'
 3. \<lbrakk>final_matters' cap; capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isArchPageCap cap; isArchPageCap cap'\<rbrakk> \<Longrightarrow> global.sameObjectAs cap cap'
 4. \<lbrakk>final_matters' cap; isIRQControlCap cap; isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> global.sameObjectAs cap cap'
 5. \<lbrakk>final_matters' cap; global.sameObjectAs cap cap'\<rbrakk> \<Longrightarrow> global.sameRegionAs cap cap' proof (prove)
goal:
No subgoals!
theory Finalise_R

lemma isFinal_no_descendants:
  "\<lbrakk> isFinal cap sl (cteCaps_of s); ctes_of s sl = Some (CTE cap n);
      valid_mdb' s; final_matters' cap \<rbrakk>
  \<Longrightarrow> descendants_of' sl (ctes_of s) = {}" apply (clarsimp simp add: descendants_of'_def cteCaps_of_def) apply (erule(3) vmdb.isFinal_no_subtree[rotated]) apply unfold_locales[1] apply (simp add: valid_mdb'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isFinal cap sl (cteCaps_of s); ctes_of s sl = Some (CTE cap n); valid_mdb' s; final_matters' cap\<rbrakk> \<Longrightarrow> descendants_of' sl (ctes_of s) = {} proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>isFinal cap sl (map_option cteCap \<circ> ctes_of s); ctes_of s sl = Some (CTE cap n); valid_mdb' s; final_matters' cap; ctes_of s \<turnstile> sl \<rightarrow> x\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>isFinal cap sl (map_option cteCap \<circ> ctes_of s); ctes_of s sl = Some (CTE cap n); valid_mdb' s; final_matters' cap\<rbrakk> \<Longrightarrow> vmdb (ctes_of s) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>isFinal cap sl (map_option cteCap \<circ> ctes_of s); ctes_of s sl = Some (CTE cap n); valid_mdb' s; final_matters' cap\<rbrakk> \<Longrightarrow> valid_mdb_ctes (ctes_of s) proof (prove)
goal:
No subgoals!
theory Finalise_R

lemma obj_refs_Master:
  "\<lbrakk> cap_relation cap cap'; P cap \<rbrakk>
      \<Longrightarrow> obj_refs cap =
           (if capClass (capMasterCap cap') = PhysicalClass
                  \<and> \<not> isUntypedCap (capMasterCap cap')
            then {capUntypedPtr (capMasterCap cap')} else {})" by (clarsimp simp: isCap_simps
              split: cap_relation_split_asm arch_cap.split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_relation cap cap'; P cap\<rbrakk> \<Longrightarrow> obj_refs cap = (if capClass (capMasterCap cap') = PhysicalClass \<and> \<not> isUntypedCap (capMasterCap cap') then {global.capUntypedPtr (capMasterCap cap')} else {})
theory Finalise_R

lemma ntfn_q_refs_of'_mult:
  "ntfn_q_refs_of' ntfn = (case ntfn of Structures_H.WaitingNtfn q \<Rightarrow> set q | _ \<Rightarrow> {}) \<times> {NTFNSignal}" by (cases ntfn, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ntfn_q_refs_of' ntfn = (case ntfn of Structures_H.ntfn.WaitingNtfn q \<Rightarrow> set q | _ \<Rightarrow> {}) \<times> {NTFNSignal}
theory Finalise_R

lemma tcb_st_not_Bound:
  "(p, NTFNBound) \<notin> tcb_st_refs_of' ts"
  "(p, TCBBound) \<notin> tcb_st_refs_of' ts" by (auto simp: tcb_st_refs_of'_def split: Structures_H.thread_state.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (p, NTFNBound) \<notin> tcb_st_refs_of' ts &&& (p, TCBBound) \<notin> tcb_st_refs_of' ts
theory Finalise_R

lemma ntfn_bound_tcb_at':
  "\<lbrakk>sym_refs (state_refs_of' s); valid_objs' s; ko_at' ntfn ntfnptr s;
    ntfnBoundTCB ntfn = Some tcbptr; P (Some ntfnptr)\<rbrakk>
  \<Longrightarrow> bound_tcb_at' P tcbptr s" apply (drule_tac x=ntfnptr in sym_refsD[rotated]) apply (clarsimp simp: obj_at'_def projectKOs) apply (fastforce simp: state_refs_of'_def) apply (auto simp: pred_tcb_at'_def obj_at'_def valid_obj'_def valid_ntfn'_def
                    state_refs_of'_def refs_of_rev' projectKOs
          simp del: refs_of_simps
             elim!: valid_objsE
             split: option.splits if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sym_refs (state_refs_of' s); valid_objs' s; ko_at' ntfn ntfnptr s; ntfnBoundTCB ntfn = Some tcbptr; P (Some ntfnptr)\<rbrakk> \<Longrightarrow> bound_tcb_at' P tcbptr s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_objs' s; ko_at' ntfn ntfnptr s; ntfnBoundTCB ntfn = Some tcbptr; P (Some ntfnptr)\<rbrakk> \<Longrightarrow> (?y, ?tp) \<in> state_refs_of' s ntfnptr
 2. \<lbrakk>valid_objs' s; ko_at' ntfn ntfnptr s; ntfnBoundTCB ntfn = Some tcbptr; P (Some ntfnptr); (ntfnptr, symreftype ?tp) \<in> state_refs_of' s ?y\<rbrakk> \<Longrightarrow> bound_tcb_at' P tcbptr s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_objs' s; ntfnBoundTCB ntfn = Some tcbptr; P (Some ntfnptr); ksPSpace s ntfnptr = Some (KONotification ntfn); is_aligned ntfnptr (objBitsKO (KONotification ntfn)); ps_clear ntfnptr (objBitsKO (KONotification ntfn)) s\<rbrakk> \<Longrightarrow> (?y, ?tp) \<in> state_refs_of' s ntfnptr
 2. \<lbrakk>valid_objs' s; ko_at' ntfn ntfnptr s; ntfnBoundTCB ntfn = Some tcbptr; P (Some ntfnptr); (ntfnptr, symreftype ?tp) \<in> state_refs_of' s ?y\<rbrakk> \<Longrightarrow> bound_tcb_at' P tcbptr s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs' s; ko_at' ntfn ntfnptr s; ntfnBoundTCB ntfn = Some tcbptr; P (Some ntfnptr); (ntfnptr, symreftype NTFNBound) \<in> state_refs_of' s tcbptr\<rbrakk> \<Longrightarrow> bound_tcb_at' P tcbptr s proof (prove)
goal:
No subgoals!
theory Finalise_R

lemma invalidateASIDEntry_valid_ap' [wp]:
  "\<lbrace>valid_asid_pool' p\<rbrace> invalidateASIDEntry asid \<lbrace>\<lambda>r. valid_asid_pool' p\<rbrace>" apply (simp add: invalidateASIDEntry_def invalidateASID_def
                   invalidateHWASIDEntry_def bind_assoc) apply (wp loadHWASID_wp | simp)+ apply (case_tac p) apply (clarsimp simp del: fun_upd_apply) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_asid_pool' p\<rbrace> invalidateASIDEntry asid \<lbrace>\<lambda>r. valid_asid_pool' p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_asid_pool' p\<rbrace> do maybeHWASID <- loadHWASID asid;
y <- when (\<exists>y. maybeHWASID = Some y) (do asidMap <- gets (armKSHWASIDTable \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSHWASIDTable_update (\<lambda>_. asidMap(the maybeHWASID := None)) (ksArchState s)\<rparr>)
od);
y <- findPDForASIDAssert asid;
asidMap <- gets (armKSASIDMap \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. asidMap(asid := None)) (ksArchState s)\<rparr>)
od \<lbrace>\<lambda>r. valid_asid_pool' p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_asid_pool' p s \<Longrightarrow> ((\<exists>y b. armKSASIDMap (ksArchState s) asid = Some (y, b)) \<longrightarrow> valid_asid_pool' p (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_ a. if a = asid then None else armKSASIDMap (ksArchState s) a) (armKSHWASIDTable_update (\<lambda>_ a. if a = the (map_option fst (armKSASIDMap (ksArchState s) asid)) then None else armKSHWASIDTable (ksArchState s) a) (ksArchState s))\<rparr>)) \<and> (armKSASIDMap (ksArchState s) asid = None \<longrightarrow> valid_asid_pool' p (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_ a. if a = asid then None else armKSASIDMap (ksArchState s) a) (ksArchState s)\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>valid_asid_pool' p s; p = asidpool.ASIDPool x\<rbrakk> \<Longrightarrow> ((\<exists>y b. armKSASIDMap (ksArchState s) asid = Some (y, b)) \<longrightarrow> valid_asid_pool' p (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_ a. if a = asid then None else armKSASIDMap (ksArchState s) a) (armKSHWASIDTable_update (\<lambda>_ a. if a = the (map_option fst (armKSASIDMap (ksArchState s) asid)) then None else armKSHWASIDTable (ksArchState s) a) (ksArchState s))\<rparr>)) \<and> (armKSASIDMap (ksArchState s) asid = None \<longrightarrow> valid_asid_pool' p (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_ a. if a = asid then None else armKSASIDMap (ksArchState s) a) (ksArchState s)\<rparr>)) proof (prove)
goal:
No subgoals!
theory Finalise_R

lemma isZombie_Null:
  "\<not> isZombie NullCap" by (simp add: isCap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> isZombie capability.NullCap
theory Finalise_R

lemma prepares_delete_helper'':
  assumes x: "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv. ko_wp_at' (Not \<circ> live') p\<rbrace>"
  shows      "\<lbrace>P and K ((\<forall>x. cte_refs' cap x = {})
                          \<and> zobj_refs' cap = {p}
                          \<and> threadCapRefs cap = {})\<rbrace>
                 f \<lbrace>\<lambda>rv s. removeable' sl s cap\<rbrace>" apply (rule hoare_gen_asm) apply (rule hoare_strengthen_post [OF x]) apply (clarsimp simp: removeable'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P and K ((\<forall>x. cte_refs' cap x = {}) \<and> zobj_refs' cap = {p} \<and> threadCapRefs cap = {})\<rbrace> f \<lbrace>\<lambda>rv s. removeable' sl s cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<forall>x. cte_refs' cap x = {}) \<and> zobj_refs' cap = {p} \<and> threadCapRefs cap = {} \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. removeable' sl s cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<lbrakk>(\<forall>x. cte_refs' cap x = {}) \<and> zobj_refs' cap = {p} \<and> threadCapRefs cap = {}; ko_wp_at' (Not \<circ> live') p s\<rbrakk> \<Longrightarrow> removeable' sl s cap proof (prove)
goal:
No subgoals!
theory Finalise_R

lemma cteDeleteOne_isFinal:
  "\<lbrace>\<lambda>s. isFinal cap slot (cteCaps_of s)\<rbrace>
     cteDeleteOne p
   \<lbrace>\<lambda>rv s. isFinal cap slot (cteCaps_of s)\<rbrace>" apply (wp cteDeleteOne_cteCaps_of) apply (clarsimp simp: isFinal_def sameObjectAs_def2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. isFinal cap slot (cteCaps_of s)\<rbrace> cteDeleteOne p \<lbrace>\<lambda>rv s. isFinal cap slot (cteCaps_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. isFinal cap slot (cteCaps_of s) \<Longrightarrow> cte_wp_at' (\<lambda>cte. \<exists>final. global.finaliseCap (cteCap cte) final True \<noteq> fail) p s \<longrightarrow> isFinal cap slot ((cteCaps_of s)(p \<mapsto> capability.NullCap)) proof (prove)
goal:
No subgoals!
theory Finalise_R

lemma isThreadCap_threadCapRefs_tcbptr:
  "isThreadCap cap \<Longrightarrow> threadCapRefs cap = {capTCBPtr cap}" by (clarsimp simp: isCap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isThreadCap cap \<Longrightarrow> threadCapRefs cap = {capTCBPtr cap}
theory Finalise_R

lemma isArchObjectCap_Cap_capCap:
  "isArchObjectCap cap \<Longrightarrow> ArchObjectCap (capCap cap) = cap" by (clarsimp simp: isCap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isArchObjectCap cap \<Longrightarrow> capability.ArchObjectCap (capCap cap) = cap
theory Finalise_R

lemma cteDeleteOne_deletes[wp]:
  "\<lbrace>\<top>\<rbrace> cteDeleteOne p \<lbrace>\<lambda>rv s. cte_wp_at' (\<lambda>c. cteCap c = NullCap) p s\<rbrace>" apply (subst tree_cte_cteCap_eq[unfolded o_def]) apply (wp cteDeleteOne_cteCaps_of) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> cteDeleteOne p \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> cteDeleteOne p \<lbrace>\<lambda>rv s. case cteCaps_of s p of None \<Rightarrow> False | Some a \<Rightarrow> a = capability.NullCap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> cte_wp_at' (\<lambda>cte. \<exists>final. global.finaliseCap (cteCap cte) final True \<noteq> fail) p s \<longrightarrow> (case ((cteCaps_of s)(p \<mapsto> capability.NullCap)) p of None \<Rightarrow> False | Some a \<Rightarrow> a = capability.NullCap) proof (prove)
goal:
No subgoals!
theory Finalise_R

lemma deletingIRQHandler_final:
  "\<lbrace>\<lambda>s. isFinal cap slot (cteCaps_of s)
             \<and> (\<forall>final. finaliseCap cap final True = fail)\<rbrace>
     deletingIRQHandler irq
   \<lbrace>\<lambda>rv s. isFinal cap slot (cteCaps_of s)\<rbrace>" apply (simp add: deletingIRQHandler_def isFinal_def getIRQSlot_def
                   getInterruptState_def locateSlot_conv getSlotCap_def) apply (wp cteDeleteOne_cteCaps_of getCTE_wp') apply (auto simp: sameObjectAs_def3) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. isFinal cap slot (cteCaps_of s) \<and> (\<forall>final. global.finaliseCap cap final True = fail)\<rbrace> deletingIRQHandler irq \<lbrace>\<lambda>rv s. isFinal cap slot (cteCaps_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> isUntypedCap cap \<and> (\<forall>p' c. cteCaps_of s p' = Some c \<longrightarrow> slot \<noteq> p' \<longrightarrow> \<not> isUntypedCap c \<longrightarrow> \<not> global.sameObjectAs cap c) \<and> (\<forall>final. global.finaliseCap cap final True = fail)\<rbrace> do node <- liftM intStateIRQNode (gets ksInterruptState);
cte <- getCTE (node + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) irq);
y <- assert (isNotificationCap (cteCap cte) \<or> cteCap cte = capability.NullCap);
cteDeleteOne (node + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) irq)
od \<lbrace>\<lambda>rv s. \<not> isUntypedCap cap \<and> (\<forall>p' c. cteCaps_of s p' = Some c \<longrightarrow> slot \<noteq> p' \<longrightarrow> \<not> isUntypedCap c \<longrightarrow> \<not> global.sameObjectAs cap c)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<not> isUntypedCap cap \<and> (\<forall>p' c. cteCaps_of s p' = Some c \<longrightarrow> slot \<noteq> p' \<longrightarrow> \<not> isUntypedCap c \<longrightarrow> \<not> global.sameObjectAs cap c) \<and> (\<forall>final. global.finaliseCap cap final True = fail) \<Longrightarrow> ((\<lambda>node s. \<forall>cte. cte_wp_at' ((=) cte) (node + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) irq) s \<longrightarrow> isNotificationCap (cteCap cte) \<or> cteCap cte = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>cte. \<exists>final. global.finaliseCap (cteCap cte) final True \<noteq> fail) (node + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) irq) s \<longrightarrow> \<not> isUntypedCap cap \<and> (\<forall>p' c. ((cteCaps_of s)(node + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) irq \<mapsto> capability.NullCap)) p' = Some c \<longrightarrow> slot \<noteq> p' \<longrightarrow> \<not> isUntypedCap c \<longrightarrow> \<not> global.sameObjectAs cap c)) \<circ> intStateIRQNode) (ksInterruptState s) s proof (prove)
goal:
No subgoals!
theory Finalise_R

lemma unbindNotification_valid_objs'_helper:
  "valid_tcb' tcb s \<longrightarrow> valid_tcb' (tcbBoundNotification_update (\<lambda>_. None) tcb) s " by (clarsimp simp: valid_bound_ntfn'_def valid_tcb'_def tcb_cte_cases_def
                  split: option.splits ntfn.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_tcb' tcb s \<longrightarrow> valid_tcb' (tcbBoundNotification_update (\<lambda>_. None) tcb) s
theory Finalise_R

lemma unbindNotification_valid_objs'_helper':
  "valid_ntfn' tcb s \<longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) tcb) s " by (clarsimp simp: valid_bound_tcb'_def valid_ntfn'_def
                  split: option.splits ntfn.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_ntfn' tcb s \<longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) tcb) s
theory Finalise_R

lemma unbindNotification_valid_objs'[wp]:
  "\<lbrace>valid_objs'\<rbrace>
     unbindNotification t
   \<lbrace>\<lambda>rv. valid_objs'\<rbrace>" apply (simp add: unbindNotification_def) apply (rule hoare_pre) apply (wp threadSet_valid_objs' gbn_wp' set_ntfn_valid_objs' hoare_vcg_all_lift
            setNotification_valid_tcb' getNotification_wp
        | wpc | clarsimp simp: setBoundNotification_def unbindNotification_valid_objs'_helper)+ apply (clarsimp elim!: obj_atE' simp: projectKOs) apply (rule valid_objsE', assumption+) apply (clarsimp simp: valid_obj'_def unbindNotification_valid_objs'_helper') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs'\<rbrace> unbindNotification t \<lbrace>\<lambda>rv. valid_objs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs'\<rbrace> do ntfnPtr <- getBoundNotification t;
case ntfnPtr of None \<Rightarrow> return () | Some ntfnPtr' \<Rightarrow> do ntfn <- getNotification ntfnPtr';
y <- setNotification ntfnPtr' (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None t
od
od \<lbrace>\<lambda>rv. valid_objs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q4\<rbrace> do ntfnPtr <- getBoundNotification t;
case ntfnPtr of None \<Rightarrow> return () | Some ntfnPtr' \<Rightarrow> do ntfn <- getNotification ntfnPtr';
y <- setNotification ntfnPtr' (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None t
od
od \<lbrace>\<lambda>rv. valid_objs'\<rbrace>
 2. \<And>s. valid_objs' s \<Longrightarrow> ?Q4 s proof (prove)
goal (1 subgoal):
 1. \<And>s x ntfna. \<lbrakk>valid_objs' s; bound_tcb_at' ((=) (Some x)) t s; ko_at' ntfna x s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) ntfna) s proof (prove)
goal (1 subgoal):
 1. \<And>s x ntfna. \<lbrakk>valid_objs' s; bound_tcb_at' ((=) (Some x)) t s; ksPSpace s x = Some (KONotification ntfna); is_aligned x (objBitsKO (KONotification ntfna)); ps_clear x (objBitsKO (KONotification ntfna)) s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) ntfna) s proof (prove)
goal (1 subgoal):
 1. \<And>s x ntfna. \<lbrakk>valid_objs' s; bound_tcb_at' ((=) (Some x)) t s; ksPSpace s x = Some (KONotification ntfna); is_aligned x (objBitsKO (KONotification ntfna)); ps_clear x (objBitsKO (KONotification ntfna)) s; valid_obj' (KONotification ntfna) s\<rbrakk> \<Longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) ntfna) s proof (prove)
goal:
No subgoals!