kings-crown/FVELER_Isabelle huggingface dataset:
theory Finalise_R

lemma to_slot_eq [simp]:
  "m \<turnstile> p \<leadsto> slot = (p = mdbPrev s_node \<and> p \<noteq> 0)" apply (rule iffI) apply (frule dlist_nextD0, simp) apply (clarsimp simp: mdb_prev_def slot mdb_next_unfold) apply (clarsimp intro!: prev_slot_next) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> p \<leadsto> slot = (p = mdbPrev s_node \<and> p \<noteq> 0) proof (prove)
goal (2 subgoals):
 1. m \<turnstile> p \<leadsto> slot \<Longrightarrow> p = mdbPrev s_node \<and> p \<noteq> 0
 2. p = mdbPrev s_node \<and> p \<noteq> 0 \<Longrightarrow> m \<turnstile> p \<leadsto> slot proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> p \<leadsto> slot; m \<turnstile> p \<leftarrow> slot\<rbrakk> \<Longrightarrow> p = mdbPrev s_node \<and> p \<noteq> 0
 2. p = mdbPrev s_node \<and> p \<noteq> 0 \<Longrightarrow> m \<turnstile> p \<leadsto> slot proof (prove)
goal (1 subgoal):
 1. p = mdbPrev s_node \<and> p \<noteq> 0 \<Longrightarrow> m \<turnstile> p \<leadsto> slot proof (prove)
goal:
No subgoals!
theory Finalise_R

lemma parency:
  "n \<turnstile> p \<rightarrow> p' = (p \<noteq> slot \<and> p' \<noteq> slot \<and> m \<turnstile> p \<rightarrow> p')" by (auto dest!: parency_n parency_m)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<turnstile> p \<rightarrow> p' = (p \<noteq> slot \<and> p' \<noteq> slot \<and> m \<turnstile> p \<rightarrow> p')
theory Finalise_R

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

(* 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_R

lemma n_rtrancl_eq:
  "n \<turnstile> p \<leadsto>\<^sup>* p' =
  (m \<turnstile> p \<leadsto>\<^sup>* p' \<and>
   (p = slot \<longrightarrow> p' = 0 \<or> p' = slot) \<and>
   (p' = slot \<longrightarrow> p = slot))" by (auto simp: rtrancl_eq_or_trancl n_trancl_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<turnstile> p \<leadsto>\<^sup>* p' = (m \<turnstile> p \<leadsto>\<^sup>* p' \<and> (p = slot \<longrightarrow> p' = 0 \<or> p' = slot) \<and> (p' = slot \<longrightarrow> p = slot))
theory Finalise_R

lemma mdb_chain_0_n:
  "mdb_chain_0 n" using chain apply (clarsimp simp: mdb_chain_0_def) apply (drule bspec) apply (fastforce simp: n_def modify_map_if split: if_split_asm) apply (simp add: n_trancl_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdb_chain_0 n proof (prove)
using this:
mdb_chain_0 m

goal (1 subgoal):
 1. mdb_chain_0 n proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<forall>x\<in>dom m. m \<turnstile> x \<leadsto>\<^sup>+ 0; n x = Some y\<rbrakk> \<Longrightarrow> n \<turnstile> x \<leadsto>\<^sup>+ 0 proof (prove)
goal (2 subgoals):
 1. \<And>x y. n x = Some y \<Longrightarrow> ?x6 x y \<in> dom m
 2. \<And>x y. \<lbrakk>n x = Some y; m \<turnstile> ?x6 x y \<leadsto>\<^sup>+ 0\<rbrakk> \<Longrightarrow> n \<turnstile> x \<leadsto>\<^sup>+ 0 proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>n x = Some y; m \<turnstile> x \<leadsto>\<^sup>+ 0\<rbrakk> \<Longrightarrow> n \<turnstile> x \<leadsto>\<^sup>+ 0 proof (prove)
goal:
No subgoals!
theory Finalise_R

lemma ut_rev_n: "ut_revocable' n" apply(insert valid) apply(clarsimp simp: ut_revocable'_def) apply(frule n_cap) apply(drule n_revokable) apply(clarsimp simp: isCap_simps split: if_split_asm) apply(simp add: valid_mdb_ctes_def ut_revocable'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ut_revocable' n proof (prove)
goal (1 subgoal):
 1. valid_mdb_ctes m \<Longrightarrow> ut_revocable' n proof (prove)
goal (1 subgoal):
 1. \<And>p cap na. \<lbrakk>valid_mdb_ctes m; n p = Some (CTE cap na); isUntypedCap cap\<rbrakk> \<Longrightarrow> mdbRevocable na proof (prove)
goal (1 subgoal):
 1. \<And>p cap na. \<lbrakk>valid_mdb_ctes m; n p = Some (CTE cap na); isUntypedCap cap; \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then cap = capability.NullCap else cap' = cap)\<rbrakk> \<Longrightarrow> mdbRevocable na proof (prove)
goal (1 subgoal):
 1. \<And>p cap n. \<lbrakk>valid_mdb_ctes m; isUntypedCap cap; \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then cap = capability.NullCap else cap' = cap); \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then \<not> mdbRevocable n else mdbRevocable n = mdbRevocable node')\<rbrakk> \<Longrightarrow> mdbRevocable n proof (prove)
goal (1 subgoal):
 1. \<And>p n d node' v0 v1 f. \<lbrakk>valid_mdb_ctes m; m p = Some (CTE (capability.UntypedCap d v0 v1 f) node'); p \<noteq> slot; \<not> mdbRevocable n; \<not> mdbRevocable node'\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Finalise_R

lemma distinct_zombies_m: "distinct_zombies m" using valid by (simp add: valid_mdb_ctes_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. distinct_zombies m proof (prove)
using this:
valid_mdb_ctes m

goal (1 subgoal):
 1. distinct_zombies m
theory Finalise_R

lemma reply_masters_rvk_fb_m: "reply_masters_rvk_fb m" using valid by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reply_masters_rvk_fb m proof (prove)
using this:
valid_mdb_ctes m

goal (1 subgoal):
 1. reply_masters_rvk_fb m
theory Finalise_R

lemma vmdb_n: "valid_mdb_ctes n" by (simp add: valid_mdb_ctes_def valid_dlist_n
                no_0_n mdb_chain_0_n valid_badges_n
                caps_contained_n mdb_chunked_n
                untyped_mdb_n untyped_inc_n
                nullcaps_n ut_rev_n class_links_n)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_mdb_ctes n
theory Finalise_R

lemma if_live_then_nonz_cap'_def2:
  "if_live_then_nonz_cap' = (\<lambda>s. \<forall>ptr. ko_wp_at' live' ptr s
                               \<longrightarrow> (\<exists>p zr. (option_map zobj_refs' o cteCaps_of s) p = Some zr \<and> ptr \<in> zr))" by (fastforce intro!: ext
                 simp: if_live_then_nonz_cap'_def ex_nonz_cap_to'_def
                       cte_wp_at_ctes_of cteCaps_of_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. if_live_then_nonz_cap' = (\<lambda>s. \<forall>ptr. ko_wp_at' live' ptr s \<longrightarrow> (\<exists>p zr. (map_option zobj_refs' \<circ> cteCaps_of s) p = Some zr \<and> ptr \<in> zr))
theory Finalise_R

lemma updateMDB_ko_wp_at_live[wp]:
  "\<lbrace>\<lambda>s. P (ko_wp_at' live' p' s)\<rbrace>
      updateMDB p m
   \<lbrace>\<lambda>rv s. P (ko_wp_at' live' p' s)\<rbrace>" unfolding updateMDB_def Let_def apply (rule hoare_pre, wp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ko_wp_at' live' p' s)\<rbrace> updateMDB p m \<lbrace>\<lambda>rv s. P (ko_wp_at' live' p' s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ko_wp_at' live' p' s)\<rbrace> if p = 0 then return () else do cte <- getCTE p;
mdb <- return (cteMDBNode cte);
mdb' <- return (m mdb);
return (cteMDBNode_update (\<lambda>_. mdb') cte) >>= setCTE p
od \<lbrace>\<lambda>rv s. P (ko_wp_at' live' p' s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (ko_wp_at' live' p' s) \<Longrightarrow> (p = 0 \<longrightarrow> P (ko_wp_at' live' p' s)) \<and> (p \<noteq> 0 \<longrightarrow> P (ko_wp_at' live' p' s)) proof (prove)
goal:
No subgoals!
theory Finalise_R

lemma updateCap_ko_wp_at_live[wp]:
  "\<lbrace>\<lambda>s. P (ko_wp_at' live' p' s)\<rbrace>
      updateCap p cap
   \<lbrace>\<lambda>rv s. P (ko_wp_at' live' p' s)\<rbrace>" unfolding updateCap_def by wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ko_wp_at' live' p' s)\<rbrace> updateCap p cap \<lbrace>\<lambda>rv s. P (ko_wp_at' live' p' s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ko_wp_at' live' p' s)\<rbrace> do cte <- getCTE p;
setCTE p (cteCap_update (\<lambda>_. cap) cte)
od \<lbrace>\<lambda>rv s. P (ko_wp_at' live' p' s)\<rbrace>
theory Finalise_R

lemma not_FinalE:
  "\<lbrakk> \<not> isFinal cap sl cps; isUntypedCap cap \<Longrightarrow> P;
     \<And>p c. \<lbrakk> cps p = Some c; p \<noteq> sl; \<not> isUntypedCap c; sameObjectAs cap c \<rbrakk> \<Longrightarrow> P
    \<rbrakk> \<Longrightarrow> P" by (fastforce simp: isFinal_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> isFinal cap sl cps; isUntypedCap cap \<Longrightarrow> P; \<And>p c. \<lbrakk>cps p = Some c; p \<noteq> sl; \<not> isUntypedCap c; global.sameObjectAs cap c\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
theory Finalise_R

lemma not_Final_removeable:
  "\<not> isFinal cap sl (cteCaps_of s)
    \<Longrightarrow> removeable' sl s cap" apply (erule not_FinalE) apply (clarsimp simp: removeable'_def isCap_simps) apply (clarsimp simp: cteCaps_of_def sameObjectAs_def2 removeable'_def
                        cte_wp_at_ctes_of) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> isFinal cap sl (cteCaps_of s) \<Longrightarrow> removeable' sl s cap proof (prove)
goal (2 subgoals):
 1. isUntypedCap cap \<Longrightarrow> removeable' sl s cap
 2. \<And>p c. \<lbrakk>cteCaps_of s p = Some c; p \<noteq> sl; \<not> isUntypedCap c; global.sameObjectAs cap c\<rbrakk> \<Longrightarrow> removeable' sl s cap proof (prove)
goal (1 subgoal):
 1. \<And>p c. \<lbrakk>cteCaps_of s p = Some c; p \<noteq> sl; \<not> isUntypedCap c; global.sameObjectAs cap c\<rbrakk> \<Longrightarrow> removeable' sl s cap proof (prove)
goal (1 subgoal):
 1. \<And>p z. \<lbrakk>p \<noteq> sl; \<not> isUntypedCap (cteCap z); capMasterCap cap = capMasterCap (cteCap z); ctes_of s p = Some z; capMasterCap (cteCap z) \<noteq> capability.NullCap; \<not> isZombie (capMasterCap (cteCap z)); \<not> isUntypedCap (capMasterCap (cteCap z)); isArchPageCap (capMasterCap (cteCap z)) \<longrightarrow> capRange (capMasterCap (cteCap z)) \<noteq> {}; (\<exists>p\<in>cte_refs' cap (irq_node' s). p \<noteq> sl \<and> (\<forall>cte. ctes_of s p = Some cte \<longrightarrow> cteCap cte \<noteq> capability.NullCap)) \<or> (\<exists>p\<in>zobj_refs' cap. \<not> ko_wp_at' (Not \<circ> live') p s) \<or> (\<exists>t\<in>threadCapRefs cap. \<exists>a b. t \<in> set (ksReadyQueues s (a, b)))\<rbrakk> \<Longrightarrow> \<exists>p. p \<noteq> sl \<and> (\<exists>cte. ctes_of s p = Some cte \<and> capMasterCap (cteCap cte) = capMasterCap (cteCap z)) proof (prove)
goal:
No subgoals!
theory Finalise_R

lemma clearUntypedFreeIndex_cteCaps_of[wp]:
  "\<lbrace>\<lambda>s. P (cteCaps_of s)\<rbrace>
       clearUntypedFreeIndex sl \<lbrace>\<lambda>y s. P (cteCaps_of s)\<rbrace>" by (simp add: cteCaps_of_def, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cteCaps_of s)\<rbrace> clearUntypedFreeIndex sl \<lbrace>\<lambda>y s. P (cteCaps_of s)\<rbrace>
theory Finalise_R

lemma setIRQState_irq_node'[wp]:
  "\<lbrace>\<lambda>s. P (irq_node' s)\<rbrace> setIRQState state irq \<lbrace>\<lambda>_ s. P (irq_node' s)\<rbrace>" apply (simp add: setIRQState_def setInterruptState_def getInterruptState_def) apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (irq_node' s)\<rbrace> setIRQState state irq \<lbrace>\<lambda>_ s. P (irq_node' s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (irq_node' s)\<rbrace> do st <- gets ksInterruptState;
y <- modify (ksInterruptState_update (\<lambda>_. intStateIRQTable_update (\<lambda>_. (intStateIRQTable st)(irq := state)) st));
doMachineOp (maskInterrupt (state = irqstate.IRQInactive) irq)
od \<lbrace>\<lambda>_ s. P (irq_node' s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (irq_node' s) \<Longrightarrow> P (irq_node' (s\<lparr>ksInterruptState := intStateIRQTable_update (\<lambda>_. (intStateIRQTable (ksInterruptState s))(irq := state)) (ksInterruptState s)\<rparr>)) proof (prove)
goal:
No subgoals!
theory Finalise_R

lemma ctes_of_valid'[elim]:
  "\<lbrakk>ctes_of s p = Some cte; valid_objs' s\<rbrakk> \<Longrightarrow> s \<turnstile>' cteCap cte" by (cases cte, simp) (rule ctes_of_valid_cap')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s p = Some cte; valid_objs' s\<rbrakk> \<Longrightarrow> valid_cap' (cteCap cte) s
theory Finalise_R

lemma emptySlot_cteCaps_of:
  "\<lbrace>\<lambda>s. P ((cteCaps_of s)(p \<mapsto> NullCap))\<rbrace>
     emptySlot p opt
   \<lbrace>\<lambda>rv s. P (cteCaps_of s)\<rbrace>" apply (simp add: emptySlot_def case_Null_If) apply (wp opt_return_pres_lift getCTE_cteCap_wp
            clearUntypedFreeIndex_cteCaps_of) apply (clarsimp simp: cteCaps_of_def cte_wp_at_ctes_of) apply (auto elim!: rsubst[where P=P]
               simp: modify_map_def fun_upd_def[symmetric] o_def
                     fun_upd_idem cteCaps_of_def
              split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P ((cteCaps_of s)(p \<mapsto> capability.NullCap))\<rbrace> emptySlot p opt \<lbrace>\<lambda>rv s. P (cteCaps_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P ((cteCaps_of s)(p \<mapsto> capability.NullCap))\<rbrace> do y <- clearUntypedFreeIndex p;
newCTE <- getCTE p;
if cteCap newCTE = capability.NullCap then return () else do y <- updateMDB (mdbPrev (cteMDBNode newCTE)) (mdbNext_update (\<lambda>_. mdbNext (cteMDBNode newCTE)));
y <- updateMDB (mdbNext (cteMDBNode newCTE)) (\<lambda>mdb. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged mdb \<or> mdbFirstBadged (cteMDBNode newCTE)) (mdbPrev_update (\<lambda>_. mdbPrev (cteMDBNode newCTE)) mdb));
y <- updateCap p capability.NullCap;
y <- updateMDB p (const nullMDBNode);
global.postCapDeletion opt
od
od \<lbrace>\<lambda>rv s. P (cteCaps_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P ((cteCaps_of s)(p \<mapsto> capability.NullCap)) \<Longrightarrow> case cteCaps_of s p of None \<Rightarrow> True | Some cap \<Rightarrow> (cap = capability.NullCap \<longrightarrow> P (cteCaps_of s)) \<and> (cap \<noteq> capability.NullCap \<longrightarrow> P (modify_map (cteCaps_of s) p (K capability.NullCap))) proof (prove)
goal (1 subgoal):
 1. \<And>s. P ((map_option cteCap \<circ> ctes_of s)(p \<mapsto> capability.NullCap)) \<Longrightarrow> case ctes_of s p of None \<Rightarrow> True | Some x2 \<Rightarrow> (cteCap x2 = capability.NullCap \<longrightarrow> P (\<lambda>a. map_option cteCap (ctes_of s a))) \<and> (cteCap x2 \<noteq> capability.NullCap \<longrightarrow> P (modify_map (\<lambda>a. map_option cteCap (ctes_of s a)) p (\<lambda>a. capability.NullCap))) proof (prove)
goal:
No subgoals!
theory Finalise_R

lemma deletedIRQHandler_irq_handlers'[wp]:
  "\<lbrace>\<lambda>s. valid_irq_handlers' s \<and> (IRQHandlerCap irq \<notin> ran (cteCaps_of s))\<rbrace>
       deletedIRQHandler irq
   \<lbrace>\<lambda>rv. valid_irq_handlers'\<rbrace>" apply (simp add: deletedIRQHandler_def setIRQState_def setInterruptState_def getInterruptState_def) apply wp apply (clarsimp simp: valid_irq_handlers'_def irq_issued'_def ran_def cteCaps_of_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_irq_handlers' s \<and> capability.IRQHandlerCap irq \<notin> ran (cteCaps_of s)\<rbrace> deletedIRQHandler irq \<lbrace>\<lambda>rv. valid_irq_handlers'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_irq_handlers' s \<and> capability.IRQHandlerCap irq \<notin> ran (cteCaps_of s)\<rbrace> do st <- gets ksInterruptState;
y <- modify (ksInterruptState_update (\<lambda>_. intStateIRQTable_update (\<lambda>_. (intStateIRQTable st)(irq := irqstate.IRQInactive)) st));
doMachineOp (maskInterrupt True irq)
od \<lbrace>\<lambda>rv. valid_irq_handlers'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_irq_handlers' s \<and> capability.IRQHandlerCap irq \<notin> ran (cteCaps_of s) \<Longrightarrow> valid_irq_handlers' (s\<lparr>ksInterruptState := intStateIRQTable_update (\<lambda>_. (intStateIRQTable (ksInterruptState s))(irq := irqstate.IRQInactive)) (ksInterruptState s)\<rparr>) proof (prove)
goal:
No subgoals!
theory Finalise_R

lemma postCapDeletion_irq_handlers'[wp]:
  "\<lbrace>\<lambda>s. valid_irq_handlers' s \<and> (cap \<noteq> NullCap \<longrightarrow> cap \<notin> ran (cteCaps_of s))\<rbrace>
       postCapDeletion cap
   \<lbrace>\<lambda>rv. valid_irq_handlers'\<rbrace>" by (wpsimp simp: Retype_H.postCapDeletion_def ARM_H.postCapDeletion_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_irq_handlers' s \<and> (cap \<noteq> capability.NullCap \<longrightarrow> cap \<notin> ran (cteCaps_of s))\<rbrace> global.postCapDeletion cap \<lbrace>\<lambda>rv. valid_irq_handlers'\<rbrace>
theory Finalise_R

lemma deletedIRQHandler_irqs_masked'[wp]:
  "\<lbrace>irqs_masked'\<rbrace> deletedIRQHandler irq \<lbrace>\<lambda>_. irqs_masked'\<rbrace>" apply (simp add: deletedIRQHandler_def setIRQState_def getInterruptState_def setInterruptState_def) apply (wp dmo_maskInterrupt) apply (simp add: irqs_masked'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>irqs_masked'\<rbrace> deletedIRQHandler irq \<lbrace>\<lambda>_. irqs_masked'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>irqs_masked'\<rbrace> do st <- gets ksInterruptState;
y <- modify (ksInterruptState_update (\<lambda>_. intStateIRQTable_update (\<lambda>_. (intStateIRQTable st)(irq := irqstate.IRQInactive)) st));
doMachineOp (maskInterrupt True irq)
od \<lbrace>\<lambda>_. irqs_masked'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. irqs_masked' s \<Longrightarrow> irqs_masked' (ksMachineState_update (ARM.irq_masks_update (\<lambda>t. t(irq := True))) (s\<lparr>ksInterruptState := intStateIRQTable_update (\<lambda>_. (intStateIRQTable (ksInterruptState s))(irq := irqstate.IRQInactive)) (ksInterruptState s)\<rparr>)) proof (prove)
goal:
No subgoals!
theory Finalise_R

lemma setIRQState_umm:
 "\<lbrace>\<lambda>s. P (underlying_memory (ksMachineState s))\<rbrace>
   setIRQState irqState irq
  \<lbrace>\<lambda>_ s. P (underlying_memory (ksMachineState s))\<rbrace>" by (simp add: setIRQState_def maskInterrupt_def
                setInterruptState_def getInterruptState_def
      | wp dmo_lift')+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (underlying_memory (ksMachineState s))\<rbrace> setIRQState irqState irq \<lbrace>\<lambda>_ s. P (underlying_memory (ksMachineState s))\<rbrace>
theory Finalise_R

lemma deletedIRQHandler_ct_not_inQ[wp]:
  "\<lbrace>ct_not_inQ\<rbrace> deletedIRQHandler irq \<lbrace>\<lambda>_. ct_not_inQ\<rbrace>" apply (rule ct_not_inQ_lift [OF deletedIRQHandler_nosch]) apply (rule hoare_weaken_pre) apply (wps deletedIRQHandler_ct) apply (simp add: deletedIRQHandler_def setIRQState_def) apply (wp) apply (simp add: comp_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_not_inQ\<rbrace> deletedIRQHandler irq \<lbrace>\<lambda>_. ct_not_inQ\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> deletedIRQHandler irq \<lbrace>\<lambda>_ s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q7\<rbrace> deletedIRQHandler irq \<lbrace>\<lambda>_ s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace>
 2. \<And>s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<Longrightarrow> ?Q7 s proof (prove)
goal (2 subgoals):
 1. \<And>prev_s. \<lbrace>?P10 prev_s\<rbrace> deletedIRQHandler irq \<lbrace>\<lambda>rv. obj_at' (Not \<circ> tcbQueued) (ksCurThread prev_s)\<rbrace>
 2. \<And>s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<Longrightarrow> ?P10 s s proof (prove)
goal (2 subgoals):
 1. \<And>prev_s. \<lbrace>?P10 prev_s\<rbrace> do st <- getInterruptState;
y <- setInterruptState (intStateIRQTable_update (\<lambda>_. (intStateIRQTable st)(irq := irqstate.IRQInactive)) st);
doMachineOp (maskInterrupt True irq)
od \<lbrace>\<lambda>rv. obj_at' (Not \<circ> tcbQueued) (ksCurThread prev_s)\<rbrace>
 2. \<And>s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<Longrightarrow> ?P10 s s proof (prove)
goal (1 subgoal):
 1. \<And>s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<Longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s proof (prove)
goal:
No subgoals!
theory Finalise_R

lemma untypedZeroRange_modify_map_isUntypedCap:
  "m sl = Some v \<Longrightarrow> \<not> isUntypedCap v \<Longrightarrow> \<not> isUntypedCap (f v)
    \<Longrightarrow> (untypedZeroRange \<circ>\<^sub>m modify_map m sl f) = (untypedZeroRange \<circ>\<^sub>m m)" by (simp add: modify_map_def map_comp_def fun_eq_iff untypedZeroRange_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m sl = Some v; \<not> isUntypedCap v; \<not> isUntypedCap (f v)\<rbrakk> \<Longrightarrow> untypedZeroRange \<circ>\<^sub>m modify_map m sl f = untypedZeroRange \<circ>\<^sub>m m
theory Finalise_R

lemma deletedIRQHandler_corres:
  "corres dc \<top> \<top>
    (deleted_irq_handler irq)
    (deletedIRQHandler irq)" apply (simp add: deleted_irq_handler_def deletedIRQHandler_def) apply (rule setIRQState_corres) apply (simp add: irq_state_relation_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (\<lambda>_. True) (\<lambda>_. True) (deleted_irq_handler irq) (deletedIRQHandler irq) proof (prove)
goal (1 subgoal):
 1. corres dc (\<lambda>_. True) (\<lambda>_. True) (set_irq_state irq_state.IRQInactive irq) (setIRQState irqstate.IRQInactive irq) proof (prove)
goal (1 subgoal):
 1. irq_state_relation irq_state.IRQInactive irqstate.IRQInactive proof (prove)
goal:
No subgoals!
theory Finalise_R

lemma arch_postCapDeletion_corres:
  "acap_relation cap cap' \<Longrightarrow> corres dc \<top> \<top> (arch_post_cap_deletion cap) (ARM_H.postCapDeletion cap')" by (corresKsimp simp: arch_post_cap_deletion_def ARM_H.postCapDeletion_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. acap_relation cap cap' \<Longrightarrow> corres dc (\<lambda>_. True) (\<lambda>_. True) (arch_post_cap_deletion cap) (Arch.postCapDeletion cap')
theory Finalise_R

lemma postCapDeletion_corres:
  "cap_relation cap cap' \<Longrightarrow> corres dc \<top> \<top> (post_cap_deletion cap) (postCapDeletion cap')" apply (cases cap; clarsimp simp: post_cap_deletion_def Retype_H.postCapDeletion_def) apply (corresKsimp corres: deletedIRQHandler_corres) by (corresKsimp corres: arch_postCapDeletion_corres)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_relation cap cap' \<Longrightarrow> corres dc (\<lambda>_. True) (\<lambda>_. True) (post_cap_deletion cap) (global.postCapDeletion cap') proof (prove)
goal (2 subgoals):
 1. \<And>x10. \<lbrakk>cap' = capability.IRQHandlerCap x10; cap = cap.IRQHandlerCap x10\<rbrakk> \<Longrightarrow> corres dc (\<lambda>_. True) (\<lambda>_. True) (deleted_irq_handler x10) (deletedIRQHandler x10)
 2. \<And>x12 a'. \<lbrakk>cap = cap.ArchObjectCap x12; acap_relation x12 a'; cap' = capability.ArchObjectCap a'\<rbrakk> \<Longrightarrow> corres dc (\<lambda>_. True) (\<lambda>_. True) (arch_post_cap_deletion x12) (Arch.postCapDeletion a') proof (prove)
goal (1 subgoal):
 1. \<And>x12 a'. \<lbrakk>cap = cap.ArchObjectCap x12; acap_relation x12 a'; cap' = capability.ArchObjectCap a'\<rbrakk> \<Longrightarrow> corres dc (\<lambda>_. True) (\<lambda>_. True) (arch_post_cap_deletion x12) (Arch.postCapDeletion a')