kings-crown/FVELER_Isabelle huggingface dataset:
theory CNodeInv_R

lemma capBadge_updateCapData_True:
  "updateCapData True x c \<noteq> NullCap \<Longrightarrow> capBadge (updateCapData True x c) = capBadge c" apply (simp add: updateCapData_def isCap_simps Let_def
            split: if_split_asm split del: if_split) apply (simp add: ARM_H.updateCapData_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. global.updateCapData True x c \<noteq> capability.NullCap \<Longrightarrow> capBadge (global.updateCapData True x c) = capBadge c proof (prove)
goal (1 subgoal):
 1. \<And>v0. \<lbrakk>c = capability.ArchObjectCap v0; Arch.updateCapData True x v0 \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> capBadge (Arch.updateCapData True x v0) = None proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma badge_derived_updateCapData:
  "\<lbrakk> updateCapData False x cap \<noteq> NullCap; badge_derived' cap cap' \<rbrakk>
         \<Longrightarrow> badge_derived' (updateCapData False x cap) cap'" by (simp add: badge_derived'_def updateCapData_Master
                updateCapData_ordering)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>global.updateCapData False x cap \<noteq> capability.NullCap; badge_derived' cap cap'\<rbrakk> \<Longrightarrow> badge_derived' (global.updateCapData False x cap) cap'
theory CNodeInv_R

lemma deriveCap_Null_helper:
  assumes "\<lbrace>P\<rbrace> deriveCap x cap \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> Q rv s\<rbrace>,-"
  shows   "\<lbrace>\<lambda>s. cap \<noteq> NullCap \<longrightarrow> P s\<rbrace> deriveCap x cap \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> Q rv s\<rbrace>,-" apply (cases "cap = NullCap") apply (simp add: deriveCap_def isCap_simps) apply (wp | simp)+ apply (rule hoare_post_imp_R, rule assms) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cap \<noteq> capability.NullCap \<longrightarrow> P s\<rbrace> global.deriveCap x cap \<lbrace>\<lambda>rv s. rv \<noteq> capability.NullCap \<longrightarrow> Q rv s\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. cap = capability.NullCap \<Longrightarrow> \<lbrace>\<lambda>s. cap \<noteq> capability.NullCap \<longrightarrow> P s\<rbrace> global.deriveCap x cap \<lbrace>\<lambda>rv s. rv \<noteq> capability.NullCap \<longrightarrow> Q rv s\<rbrace>, -
 2. cap \<noteq> capability.NullCap \<Longrightarrow> \<lbrace>\<lambda>s. cap \<noteq> capability.NullCap \<longrightarrow> P s\<rbrace> global.deriveCap x cap \<lbrace>\<lambda>rv s. rv \<noteq> capability.NullCap \<longrightarrow> Q rv s\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. cap = capability.NullCap \<Longrightarrow> \<lbrace>\<lambda>s. True\<rbrace> returnOk capability.NullCap \<lbrace>\<lambda>rv s. rv \<noteq> capability.NullCap \<longrightarrow> Q rv s\<rbrace>, -
 2. cap \<noteq> capability.NullCap \<Longrightarrow> \<lbrace>\<lambda>s. cap \<noteq> capability.NullCap \<longrightarrow> P s\<rbrace> global.deriveCap x cap \<lbrace>\<lambda>rv s. rv \<noteq> capability.NullCap \<longrightarrow> Q rv s\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. cap \<noteq> capability.NullCap \<Longrightarrow> \<lbrace>P\<rbrace> global.deriveCap x cap \<lbrace>\<lambda>rv s. rv \<noteq> capability.NullCap \<longrightarrow> Q rv s\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<lbrakk>cap \<noteq> capability.NullCap; rv \<noteq> capability.NullCap \<longrightarrow> Q rv s\<rbrakk> \<Longrightarrow> rv \<noteq> capability.NullCap \<longrightarrow> Q rv s proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma hasCancelSendRights_not_Null:
  "hasCancelSendRights cap \<Longrightarrow> isEndpointCap cap" by (clarsimp simp: hasCancelSendRights_def isCap_simps split: capability.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. hasCancelSendRights cap \<Longrightarrow> isEndpointCap cap
theory CNodeInv_R

lemma untyped_derived_eq_updateCapData:
  "RetypeDecls_H.updateCapData x y cap \<noteq> NullCap
    \<Longrightarrow> untyped_derived_eq (RetypeDecls_H.updateCapData x y cap) cap'
        = untyped_derived_eq cap cap'" apply (simp add: untyped_derived_eq_def) apply (rule imp_cong) apply (rule capMaster_isUntyped) apply (erule updateCapData_Master) apply (clarsimp simp: isCap_simps) apply (clarsimp simp: updateCapData_def isCap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. global.updateCapData x y cap \<noteq> capability.NullCap \<Longrightarrow> untyped_derived_eq (global.updateCapData x y cap) cap' = untyped_derived_eq cap cap' proof (prove)
goal (1 subgoal):
 1. global.updateCapData x y cap \<noteq> capability.NullCap \<Longrightarrow> (isUntypedCap (global.updateCapData x y cap) \<longrightarrow> global.updateCapData x y cap = cap') = (isUntypedCap cap \<longrightarrow> cap = cap') proof (prove)
goal (2 subgoals):
 1. global.updateCapData x y cap \<noteq> capability.NullCap \<Longrightarrow> isUntypedCap (global.updateCapData x y cap) = isUntypedCap cap
 2. \<lbrakk>global.updateCapData x y cap \<noteq> capability.NullCap; isUntypedCap cap\<rbrakk> \<Longrightarrow> (global.updateCapData x y cap = cap') = (cap = cap') proof (prove)
goal (2 subgoals):
 1. global.updateCapData x y cap \<noteq> capability.NullCap \<Longrightarrow> capMasterCap (global.updateCapData x y cap) = capMasterCap cap
 2. \<lbrakk>global.updateCapData x y cap \<noteq> capability.NullCap; isUntypedCap cap\<rbrakk> \<Longrightarrow> (global.updateCapData x y cap = cap') = (cap = cap') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>global.updateCapData x y cap \<noteq> capability.NullCap; isUntypedCap cap\<rbrakk> \<Longrightarrow> (global.updateCapData x y cap = cap') = (cap = cap') proof (prove)
goal (1 subgoal):
 1. \<And>d v0 v1 f. \<lbrakk>global.updateCapData x y (capability.UntypedCap d v0 v1 f) \<noteq> capability.NullCap; cap = capability.UntypedCap d v0 v1 f\<rbrakk> \<Longrightarrow> (global.updateCapData x y (capability.UntypedCap d v0 v1 f) = cap') = (capability.UntypedCap d v0 v1 f = cap') proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma untyped_derived_eq_refl:
  "untyped_derived_eq c c" by (simp add: untyped_derived_eq_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. untyped_derived_eq c c
theory CNodeInv_R

lemma not_recursive_ctes_wu [simp]:
  "not_recursive_ctes (ksWorkUnitsCompleted_update f s) = not_recursive_ctes s" by (simp add: not_recursive_ctes_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. not_recursive_ctes (ksWorkUnitsCompleted_update f s) = not_recursive_ctes s
theory CNodeInv_R

lemma not_recursive_ctes_irq_state_independent[simp, intro!]:
  "not_recursive_ctes (s \<lparr> ksMachineState := ksMachineState s \<lparr> irq_state := x \<rparr>\<rparr>) = not_recursive_ctes s" by (simp add: not_recursive_ctes_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. not_recursive_ctes (s\<lparr>ksMachineState := ksMachineState s\<lparr>irq_state := x\<rparr>\<rparr>) = not_recursive_ctes s
theory CNodeInv_R

lemma suspend_ctes_of_thread:
  "\<lbrace>\<lambda>s. \<exists>node. ctes_of s x = Some (CTE (ThreadCap t) node)\<rbrace>
     suspend t
   \<lbrace>\<lambda>rv s. \<exists>node. ctes_of s x = Some (CTE (ThreadCap t) node)\<rbrace>" apply (rule hoare_chain) apply (rule suspend_cte_wp_at'[where P="(=) (ThreadCap t)" and p=x]) apply (clarsimp simp add: finaliseCap_def Let_def isCap_simps) apply (clarsimp simp: cte_wp_at_ctes_of) apply (clarsimp simp: cte_wp_at_ctes_of) apply (case_tac cte, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<exists>node. ctes_of s x = Some (CTE (capability.ThreadCap t) node)\<rbrace> ThreadDecls_H.suspend t \<lbrace>\<lambda>rv s. \<exists>node. ctes_of s x = Some (CTE (capability.ThreadCap t) node)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P\<rbrace> ThreadDecls_H.suspend t \<lbrace>?Q\<rbrace>
 2. \<And>s. \<exists>node. ctes_of s x = Some (CTE (capability.ThreadCap t) node) \<Longrightarrow> ?P s
 3. \<And>rv s. ?Q rv s \<Longrightarrow> \<exists>node. ctes_of s x = Some (CTE (capability.ThreadCap t) node) proof (prove)
goal (3 subgoals):
 1. \<And>cap final. capability.ThreadCap t = cap \<Longrightarrow> global.finaliseCap cap final True = fail
 2. \<And>s. \<exists>node. ctes_of s x = Some (CTE (capability.ThreadCap t) node) \<Longrightarrow> cte_wp_at' (\<lambda>cte. capability.ThreadCap t = cteCap cte) x s
 3. \<And>rv s. cte_wp_at' (\<lambda>cte. capability.ThreadCap t = cteCap cte) x s \<Longrightarrow> \<exists>node. ctes_of s x = Some (CTE (capability.ThreadCap t) node) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<exists>node. ctes_of s x = Some (CTE (capability.ThreadCap t) node) \<Longrightarrow> cte_wp_at' (\<lambda>cte. capability.ThreadCap t = cteCap cte) x s
 2. \<And>rv s. cte_wp_at' (\<lambda>cte. capability.ThreadCap t = cteCap cte) x s \<Longrightarrow> \<exists>node. ctes_of s x = Some (CTE (capability.ThreadCap t) node) proof (prove)
goal (1 subgoal):
 1. \<And>rv s. cte_wp_at' (\<lambda>cte. capability.ThreadCap t = cteCap cte) x s \<Longrightarrow> \<exists>node. ctes_of s x = Some (CTE (capability.ThreadCap t) node) proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>ctes_of s x = Some cte; capability.ThreadCap t = cteCap cte\<rbrakk> \<Longrightarrow> \<exists>node. cte = CTE (cteCap cte) node proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma unbindNotification_ctes_of_thread:
  "\<lbrace>\<lambda>s. \<exists>node. ctes_of s x = Some (CTE (ThreadCap t) node)\<rbrace>
     unbindNotification t
   \<lbrace>\<lambda>rv s. \<exists>node. ctes_of s x = Some (CTE (ThreadCap t) node)\<rbrace>" by wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<exists>node. ctes_of s x = Some (CTE (capability.ThreadCap t) node)\<rbrace> unbindNotification t \<lbrace>\<lambda>rv s. \<exists>node. ctes_of s x = Some (CTE (capability.ThreadCap t) node)\<rbrace>
theory CNodeInv_R

lemma prepareThreadDelete_ctes_of_thread:
  "\<lbrace>\<lambda>s. \<exists>node. ctes_of s x = Some (CTE (ThreadCap t) node)\<rbrace>
     prepareThreadDelete t
   \<lbrace>\<lambda>rv s. \<exists>node. ctes_of s x = Some (CTE (ThreadCap t) node)\<rbrace>" by (wpsimp simp: prepareThreadDelete_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<exists>node. ctes_of s x = Some (CTE (capability.ThreadCap t) node)\<rbrace> prepareThreadDelete t \<lbrace>\<lambda>rv s. \<exists>node. ctes_of s x = Some (CTE (capability.ThreadCap t) node)\<rbrace>
theory CNodeInv_R

lemma unbindNotification_not_recursive_ctes:
  "\<lbrace>\<lambda>s. P (not_recursive_ctes s)\<rbrace>
     unbindNotification t
   \<lbrace>\<lambda>rv s. P (not_recursive_ctes s)\<rbrace>" apply (simp only: not_recursive_ctes_def cteCaps_of_def) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (not_recursive_ctes s)\<rbrace> unbindNotification t \<lbrace>\<lambda>rv s. P (not_recursive_ctes s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P {ptr. \<exists>cap. (map_option cteCap \<circ> ctes_of s) ptr = Some cap \<and> \<not> (isZombie cap \<and> capZombiePtr cap = ptr)}\<rbrace> unbindNotification t \<lbrace>\<lambda>rv s. P {ptr. \<exists>cap. (map_option cteCap \<circ> ctes_of s) ptr = Some cap \<and> \<not> (isZombie cap \<and> capZombiePtr cap = ptr)}\<rbrace> proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma prepareThreadDelete_not_recursive_ctes:
  "\<lbrace>\<lambda>s. P (not_recursive_ctes s)\<rbrace>
     prepareThreadDelete t
   \<lbrace>\<lambda>rv s. P (not_recursive_ctes s)\<rbrace>" apply (simp only: prepareThreadDelete_def cteCaps_of_def) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (not_recursive_ctes s)\<rbrace> prepareThreadDelete t \<lbrace>\<lambda>rv s. P (not_recursive_ctes s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (not_recursive_ctes s)\<rbrace> return () \<lbrace>\<lambda>rv s. P (not_recursive_ctes s)\<rbrace> proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma finaliseSlot_recset_wf: "wf finaliseSlot_recset" unfolding finaliseSlot_recset_def by (intro wf_sum_wf wf_rdcall_finalise_ord_lift wf_measure
            wf_inv_image wf_lex_prod wf_less_than)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. wf finaliseSlot_recset proof (prove)
goal (1 subgoal):
 1. wf (wf_sum (\<lambda>(slot, exposed, state). exposed) (inv_image (less_than <*lex*> less_than) (\<lambda>(x, exp, s). case ctes_of s x of None \<Rightarrow> (3, 0) | Some (CTE capability.NullCap node) \<Rightarrow> (0, 0) | Some (CTE (capability.Zombie p zb n) node) \<Rightarrow> (if p = x then 1 else 2, n) | Some (CTE _ node) \<Rightarrow> (3, 0))) (measure (\<lambda>(x, exp, s). card (not_recursive_ctes s))))
theory CNodeInv_R

lemma updateCap_implies_cte_at:
  "(rv, s') \<in> fst (updateCap ptr cap s)
      \<Longrightarrow> cte_at' ptr s" apply (clarsimp simp: updateCap_def in_monad) apply (frule in_inv_by_hoareD [OF getCTE_inv]) apply (drule use_valid [OF _ getCTE_cte_wp_at], simp) apply (clarsimp simp: cte_wp_at_ctes_of) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (rv, s') \<in> fst (updateCap ptr cap s) \<Longrightarrow> cte_wp_at' (\<lambda>_. True) ptr s proof (prove)
goal (1 subgoal):
 1. \<And>s'' cte. \<lbrakk>(cte, s'') \<in> fst (getCTE ptr s); ((), s') \<in> fst (setCTE ptr (cteCap_update (\<lambda>_. cap) cte) s'')\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) ptr s proof (prove)
goal (1 subgoal):
 1. \<And>s'' cte. \<lbrakk>(cte, s'') \<in> fst (getCTE ptr s); ((), s') \<in> fst (setCTE ptr (cteCap_update (\<lambda>_. cap) cte) s''); s'' = s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) ptr s proof (prove)
goal (1 subgoal):
 1. \<And>s'' cte. \<lbrakk>((), s') \<in> fst (setCTE ptr (cteCap_update (\<lambda>_. cap) cte) s''); s'' = s; cte_wp_at' (\<lambda>c. c = cte) ptr s''\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) ptr s proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma case_Zombie_assert_fold:
  "(case cap of Zombie ptr zb n \<Rightarrow> haskell_assertE (P ptr) str | _ \<Rightarrow> returnOk ())
       = assertE (isZombie cap \<longrightarrow> P (capZombiePtr cap))" by (cases cap, simp_all add: isCap_simps assertE_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (case cap of capability.Zombie ptr zb n \<Rightarrow> haskell_assertE (P ptr) str | _ \<Rightarrow> returnOk ()) = assertE (isZombie cap \<longrightarrow> P (capZombiePtr cap))
theory CNodeInv_R

lemma cteDelete_preservation:
  assumes wp:
    "\<And>cap final. \<lbrace>P\<rbrace> finaliseCap cap final False \<lbrace>\<lambda>rv. P\<rbrace>"
    "\<And>sl opt. \<lbrace>P\<rbrace> emptySlot sl opt \<lbrace>\<lambda>rv. P\<rbrace>"
    "\<And>sl1 sl2. \<lbrace>P\<rbrace> capSwapForDelete sl1 sl2 \<lbrace>\<lambda>rv. P\<rbrace>"
    "\<And>sl cap. \<lbrace>P\<rbrace> updateCap sl cap \<lbrace>\<lambda>rv. P\<rbrace>"
    "\<And>f s. P (ksWorkUnitsCompleted_update f s) = P s"
  assumes irq: "irq_state_independent_H P"
  shows
    "\<lbrace>P\<rbrace> cteDelete p e \<lbrace>\<lambda>rv. P\<rbrace>" apply (simp add: cteDelete_def whenE_def split_def) apply (wp wp) apply (simp only: simp_thms cases_simp) apply (wp finaliseSlot_preservation wp irq) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> cteDelete p e \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> doE pa <- finaliseSlot p e;
if e \<or> fst pa then liftE (emptySlot p (snd pa)) else returnOk ()
odE \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> finaliseSlot p e \<lbrace>\<lambda>p s. (e \<or> fst p \<longrightarrow> P s) \<and> (\<not> (e \<or> fst p) \<longrightarrow> P s)\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 2. \<And>s. P s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> finaliseSlot p e \<lbrace>\<lambda>p. P\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 2. \<And>s. P s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> P s \<and> P s proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma modify_map_next_trancl_iff:
  assumes inv: "\<And>cte. mdbNext (cteMDBNode (f cte)) = mdbNext (cteMDBNode cte)"
  shows  "(modify_map m ptr f) \<turnstile> x \<leadsto>\<^sup>+ y = m \<turnstile> x \<leadsto>\<^sup>+ y" using inv by (auto intro: modify_map_next_trancl  modify_map_next_trancl2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. modify_map m ptr f \<turnstile> x \<leadsto>\<^sup>+ y = m \<turnstile> x \<leadsto>\<^sup>+ y proof (prove)
using this:
mdbNext (cteMDBNode (f ?cte)) = mdbNext (cteMDBNode ?cte)

goal (1 subgoal):
 1. modify_map m ptr f \<turnstile> x \<leadsto>\<^sup>+ y = m \<turnstile> x \<leadsto>\<^sup>+ y
theory CNodeInv_R

lemma modify_map_dlist_iff:
  assumes inv: "\<And>cte. cteMDBNode (f cte) = cteMDBNode cte"
  shows  "valid_dlist (modify_map m ptr f) = valid_dlist m" using inv by (auto intro: modify_map_dlist modify_map_dlist2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_dlist (modify_map m ptr f) = valid_dlist m proof (prove)
using this:
cteMDBNode (f ?cte) = cteMDBNode ?cte

goal (1 subgoal):
 1. valid_dlist (modify_map m ptr f) = valid_dlist m
theory CNodeInv_R

lemma mdb_chain_0_modify_map_inv:
  "\<lbrakk> mdb_chain_0 m; \<And>cte. mdbNext (cteMDBNode (f cte)) = mdbNext (cteMDBNode cte) \<rbrakk> \<Longrightarrow> mdb_chain_0 (modify_map m ptr f)" unfolding mdb_chain_0_def by (auto simp: modify_map_next_trancl_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdb_chain_0 m; \<And>cte. mdbNext (cteMDBNode (f cte)) = mdbNext (cteMDBNode cte)\<rbrakk> \<Longrightarrow> mdb_chain_0 (modify_map m ptr f) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>dom m. m \<turnstile> x \<leadsto>\<^sup>+ 0; \<And>cte. mdbNext (cteMDBNode (f cte)) = mdbNext (cteMDBNode cte)\<rbrakk> \<Longrightarrow> \<forall>x\<in>dom (modify_map m ptr f). modify_map m ptr f \<turnstile> x \<leadsto>\<^sup>+ 0
theory CNodeInv_R

lemma setCTE_cte_wp_at_other:
 "\<lbrace>cte_wp_at' P p and (\<lambda>s. ptr \<noteq> p)\<rbrace>
  setCTE ptr cte
  \<lbrace>\<lambda>uu s. cte_wp_at' P p s\<rbrace>" apply (simp add: cte_wp_at_ctes_of) apply wp apply (clarsimp simp: cte_wp_at_ctes_of) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' P p and (\<lambda>s. ptr \<noteq> p)\<rbrace> setCTE ptr cte \<lbrace>\<lambda>uu. cte_wp_at' P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' P p and (\<lambda>s. ptr \<noteq> p)\<rbrace> setCTE ptr cte \<lbrace>\<lambda>uu s. \<exists>cte. ctes_of s p = Some cte \<and> P cte\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (cte_wp_at' P p and (\<lambda>s. ptr \<noteq> p)) s \<Longrightarrow> \<exists>ctea. ((ctes_of s)(ptr \<mapsto> cte)) p = Some ctea \<and> P ctea proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma updateMDB_cte_wp_at_other:
 "\<lbrace>cte_wp_at' P p and (\<lambda>s. m \<noteq> p)\<rbrace>
  updateMDB m f
  \<lbrace>\<lambda>uu. cte_wp_at' P p\<rbrace>" unfolding updateMDB_def apply simp apply safe apply wp apply simp apply (wp setCTE_cte_wp_at_other) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' P p and (\<lambda>s. m \<noteq> p)\<rbrace> updateMDB m f \<lbrace>\<lambda>uu. cte_wp_at' P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' P p and (\<lambda>s. m \<noteq> p)\<rbrace> let slot = m in if slot = 0 then return () else do cte <- getCTE slot;
mdb <- return (cteMDBNode cte);
mdb' <- return (f mdb);
return (cteMDBNode_update (\<lambda>_. mdb') cte) >>= setCTE slot
od \<lbrace>\<lambda>uu. cte_wp_at' P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. (m = 0 \<longrightarrow> \<lbrace>cte_wp_at' P p and (\<lambda>s. p \<noteq> 0)\<rbrace> return () \<lbrace>\<lambda>uu. cte_wp_at' P p\<rbrace>) \<and> (m \<noteq> 0 \<longrightarrow> \<lbrace>cte_wp_at' P p and (\<lambda>s. m \<noteq> p)\<rbrace> do cte <- getCTE m;
setCTE m (cteMDBNode_update (\<lambda>_. f (cteMDBNode cte)) cte)
od \<lbrace>\<lambda>uu. cte_wp_at' P p\<rbrace>) proof (prove)
goal (2 subgoals):
 1. m = 0 \<Longrightarrow> \<lbrace>cte_wp_at' P p and (\<lambda>s. p \<noteq> 0)\<rbrace> return () \<lbrace>\<lambda>uu. cte_wp_at' P p\<rbrace>
 2. m \<noteq> 0 \<Longrightarrow> \<lbrace>cte_wp_at' P p and (\<lambda>s. m \<noteq> p)\<rbrace> do cte <- getCTE m;
setCTE m (cteMDBNode_update (\<lambda>_. f (cteMDBNode cte)) cte)
od \<lbrace>\<lambda>uu. cte_wp_at' P p\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>m = 0; (cte_wp_at' P p and (\<lambda>s. p \<noteq> 0)) s\<rbrakk> \<Longrightarrow> cte_wp_at' P p s
 2. m \<noteq> 0 \<Longrightarrow> \<lbrace>cte_wp_at' P p and (\<lambda>s. m \<noteq> p)\<rbrace> do cte <- getCTE m;
setCTE m (cteMDBNode_update (\<lambda>_. f (cteMDBNode cte)) cte)
od \<lbrace>\<lambda>uu. cte_wp_at' P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. m \<noteq> 0 \<Longrightarrow> \<lbrace>cte_wp_at' P p and (\<lambda>s. m \<noteq> p)\<rbrace> do cte <- getCTE m;
setCTE m (cteMDBNode_update (\<lambda>_. f (cteMDBNode cte)) cte)
od \<lbrace>\<lambda>uu. cte_wp_at' P p\<rbrace> proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma ctes_of_strng:
  "(\<exists>cte. ctes_of s ptr = Some cte \<and> P cte)
  \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) ptr s \<and> P cte)" by (clarsimp simp: cte_wp_at_ctes_of)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<exists>cte. ctes_of s ptr = Some cte \<and> P cte) \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) ptr s \<and> P cte)
theory CNodeInv_R

lemma updateCap_valid_cap [wp]:
  "\<lbrace>valid_cap' cap\<rbrace> updateCap ptr cap' \<lbrace>\<lambda>r. valid_cap' cap\<rbrace>" unfolding updateCap_def by (wp setCTE_valid_cap getCTE_wp) (clarsimp dest!: cte_at_cte_wp_atD)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_cap' cap\<rbrace> updateCap ptr cap' \<lbrace>\<lambda>r. valid_cap' cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_cap' cap\<rbrace> do cte <- getCTE ptr;
setCTE ptr (cteCap_update (\<lambda>_. cap') cte)
od \<lbrace>\<lambda>r. valid_cap' cap\<rbrace>
theory CNodeInv_R

lemma next_fold:
  "\<lbrakk> m a = Some cte; mdbNext (cteMDBNode cte) = b\<rbrakk> \<Longrightarrow> m \<turnstile> a \<leadsto> b" by (clarsimp simp: next_unfold')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m a = Some cte; mdbNext (cteMDBNode cte) = b\<rbrakk> \<Longrightarrow> m \<turnstile> a \<leadsto> b
theory CNodeInv_R

lemma cteMDBNode_update_comp [simp]:
  "(cteMDBNode_update f \<circ> cteMDBNode_update g) = cteMDBNode_update (f \<circ> g)" by rule (case_tac x, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cteMDBNode_update f \<circ> cteMDBNode_update g = cteMDBNode_update (f \<circ> g)
theory CNodeInv_R

lemma modify_map_lhs_trancl:
  "\<lbrakk> m p = Some cte; \<not> m \<turnstile> mdbNext (cteMDBNode (f cte)) \<leadsto>\<^sup>* p \<rbrakk> \<Longrightarrow>
  modify_map m p f \<turnstile> p \<leadsto>\<^sup>+ x = m \<turnstile> mdbNext (cteMDBNode (f cte)) \<leadsto>\<^sup>* x" by (clarsimp simp: next_update_is_modify [symmetric] intro!: next_update_lhs_trancl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some cte; (mdbNext (cteMDBNode (f cte)), p) \<notin> (mdb_next_rel m)\<^sup>*\<rbrakk> \<Longrightarrow> modify_map m p f \<turnstile> p \<leadsto>\<^sup>+ x = m \<turnstile> mdbNext (cteMDBNode (f cte)) \<leadsto>\<^sup>* x