kings-crown/FVELER_Isabelle huggingface dataset:
theory CNodeInv_R

lemma ztc_sameRegion:
  "\<lbrakk> isCNodeCap cap \<or> isThreadCap cap \<or> isZombie cap \<rbrakk>
       \<Longrightarrow> sameRegionAs cap cap' = sameObjectAs cap cap'" apply (subgoal_tac "\<not> isUntypedCap cap \<and> \<not> isArchPageCap cap
                          \<and> \<not> isIRQControlCap cap") apply (simp add: sameRegionAs_def3 sameObjectAs_def3) apply (auto simp: isCap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isCNodeCap cap \<or> isThreadCap cap \<or> isZombie cap \<Longrightarrow> global.sameRegionAs cap cap' = global.sameObjectAs cap cap' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>isCNodeCap cap \<or> isThreadCap cap \<or> isZombie cap; \<not> isUntypedCap cap \<and> \<not> isArchPageCap cap \<and> \<not> isIRQControlCap cap\<rbrakk> \<Longrightarrow> global.sameRegionAs cap cap' = global.sameObjectAs cap cap'
 2. isCNodeCap cap \<or> isThreadCap cap \<or> isZombie cap \<Longrightarrow> \<not> isUntypedCap cap \<and> \<not> isArchPageCap cap \<and> \<not> isIRQControlCap cap proof (prove)
goal (2 subgoals):
 1. \<lbrakk>isCNodeCap cap \<or> isThreadCap cap \<or> isZombie cap; \<not> isUntypedCap cap \<and> \<not> isArchPageCap cap \<and> \<not> isIRQControlCap cap\<rbrakk> \<Longrightarrow> (capMasterCap cap = capMasterCap cap' \<and> cap \<noteq> capability.NullCap \<and> \<not> isZombie cap \<and> cap' \<noteq> capability.NullCap \<and> \<not> isZombie cap' \<and> \<not> isUntypedCap cap' \<and> \<not> isArchPageCap cap') = (capMasterCap cap = capMasterCap cap' \<and> cap \<noteq> capability.NullCap \<and> \<not> isZombie cap \<and> cap' \<noteq> capability.NullCap \<and> \<not> isZombie cap' \<and> \<not> isUntypedCap cap' \<and> (isArchPageCap cap' \<longrightarrow> capRange cap' \<noteq> {}))
 2. isCNodeCap cap \<or> isThreadCap cap \<or> isZombie cap \<Longrightarrow> \<not> isUntypedCap cap \<and> \<not> isArchPageCap cap \<and> \<not> isIRQControlCap cap proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma distinct_zombiesD:
  "\<lbrakk> m x = Some cte; distinct_zombies m; isZombie (cteCap cte);
       y \<noteq> x; m y = Some cte'; capBits (cteCap cte') = capBits (cteCap cte);
       capUntypedPtr (cteCap cte') = capUntypedPtr (cteCap cte);
       \<not> isUntypedCap (cteCap cte'); \<not> isArchPageCap (cteCap cte');
       capClass (cteCap cte') = PhysicalClass \<rbrakk>
       \<Longrightarrow> False" apply (simp add: distinct_zombies_def distinct_zombie_caps_def) apply (drule_tac x=x in spec, drule_tac x=y in spec) apply clarsimp apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m x = Some cte; distinct_zombies m; isZombie (cteCap cte); y \<noteq> x; m y = Some cte'; capBits (cteCap cte') = capBits (cteCap cte); global.capUntypedPtr (cteCap cte') = global.capUntypedPtr (cteCap cte); \<not> isUntypedCap (cteCap cte'); \<not> isArchPageCap (cteCap cte'); capClass (cteCap cte') = PhysicalClass\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m x = Some cte; \<forall>ptr ptr' cap cap'. (\<exists>z. m ptr = Some z \<and> cteCap z = cap) \<and> (\<exists>z. m ptr' = Some z \<and> cteCap z = cap') \<and> ptr \<noteq> ptr' \<and> isZombie cap \<and> capClass cap' = PhysicalClass \<and> \<not> isUntypedCap cap' \<and> \<not> isArchPageCap cap' \<and> capBits cap = capBits cap' \<longrightarrow> global.capUntypedPtr cap \<noteq> global.capUntypedPtr cap'; isZombie (cteCap cte); y \<noteq> x; m y = Some cte'; capBits (cteCap cte') = capBits (cteCap cte); global.capUntypedPtr (cteCap cte') = global.capUntypedPtr (cteCap cte); \<not> isUntypedCap (cteCap cte'); \<not> isArchPageCap (cteCap cte'); capClass (cteCap cte') = PhysicalClass\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m x = Some cte; isZombie (cteCap cte); y \<noteq> x; m y = Some cte'; capBits (cteCap cte') = capBits (cteCap cte); global.capUntypedPtr (cteCap cte') = global.capUntypedPtr (cteCap cte); \<not> isUntypedCap (cteCap cte'); \<not> isArchPageCap (cteCap cte'); capClass (cteCap cte') = PhysicalClass; \<forall>cap cap'. (\<exists>z. m x = Some z \<and> cteCap z = cap) \<and> (\<exists>z. m y = Some z \<and> cteCap z = cap') \<and> x \<noteq> y \<and> isZombie cap \<and> capClass cap' = PhysicalClass \<and> \<not> isUntypedCap cap' \<and> \<not> isArchPageCap cap' \<and> capBits cap = capBits cap' \<longrightarrow> global.capUntypedPtr cap \<noteq> global.capUntypedPtr cap'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m x = Some cte; isZombie (cteCap cte); y \<noteq> x; m y = Some cte'; capBits (cteCap cte') = capBits (cteCap cte); global.capUntypedPtr (cteCap cte') = global.capUntypedPtr (cteCap cte); \<not> isUntypedCap (cteCap cte'); \<not> isArchPageCap (cteCap cte'); capClass (cteCap cte') = PhysicalClass; \<forall>cap. isZombie cap \<longrightarrow> cteCap cte \<noteq> cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma updateCap_untyped_ranges_zero_simple:
  "\<lbrace>cte_wp_at' ((\<lambda>cp. untypedZeroRange cp = untypedZeroRange cap) o cteCap) sl and untyped_ranges_zero'\<rbrace>
    updateCap sl cap
  \<lbrace>\<lambda>_. untyped_ranges_zero'\<rbrace>" apply (rule hoare_pre, rule untyped_ranges_zero_lift, wp+) apply (clarsimp simp: modify_map_def cteCaps_of_def cte_wp_at_ctes_of) apply (simp add: untyped_ranges_zero_inv_def) apply (rule arg_cong[where f=ran]) apply (simp add: fun_eq_iff map_comp_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' ((\<lambda>cp. untypedZeroRange cp = untypedZeroRange cap) \<circ> cteCap) sl and untyped_ranges_zero'\<rbrace> updateCap sl cap \<lbrace>\<lambda>_. untyped_ranges_zero'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (cte_wp_at' ((\<lambda>cp. untypedZeroRange cp = untypedZeroRange cap) \<circ> cteCap) sl and untyped_ranges_zero') s \<Longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) sl (K cap)) (gsUntypedZeroRanges s) proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>untyped_ranges_zero_inv (map_option cteCap \<circ> ctes_of s) (gsUntypedZeroRanges s); ctes_of s sl = Some cte; untypedZeroRange (cteCap cte) = untypedZeroRange cap\<rbrakk> \<Longrightarrow> untyped_ranges_zero_inv (\<lambda>a. if a = sl then Some cap else map_option cteCap (ctes_of s a)) (gsUntypedZeroRanges s) proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>gsUntypedZeroRanges s = ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> ctes_of s)); ctes_of s sl = Some cte; untypedZeroRange (cteCap cte) = untypedZeroRange cap\<rbrakk> \<Longrightarrow> ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> ctes_of s)) = ran (untypedZeroRange \<circ>\<^sub>m (\<lambda>a. if a = sl then Some cap else map_option cteCap (ctes_of s a))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>gsUntypedZeroRanges s = ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> ctes_of s)); ctes_of s sl = Some cte; untypedZeroRange (cteCap cte) = untypedZeroRange cap\<rbrakk> \<Longrightarrow> untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> ctes_of s) = untypedZeroRange \<circ>\<^sub>m (\<lambda>a. if a = sl then Some cap else map_option cteCap (ctes_of s a)) proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma isFinal_Zombie:
  "isFinal (Zombie p' b n) p cs" by (simp add: isFinal_def sameObjectAs_def isCap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isFinal (capability.Zombie p' b n) p cs
theory CNodeInv_R

lemma cte_wp_at_cteCap_norm:
  "(cte_wp_at' (\<lambda>c. P (cteCap c)) p s) = (\<exists>cap. cte_wp_at' (\<lambda>c. cteCap c = cap) p s \<and> P cap)" by (auto simp add: cte_wp_at'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at' (\<lambda>c. P (cteCap c)) p s = (\<exists>cap. cte_wp_at' (\<lambda>c. cteCap c = cap) p s \<and> P cap)
theory CNodeInv_R

lemma cteSwap_cteCaps_of [wp]:
  "\<lbrace>\<lambda>s. P ((cteCaps_of s) ( a := Some cap2, b := Some cap1 ))\<rbrace>
     cteSwap cap1 a cap2 b
   \<lbrace>\<lambda>rv s. P (cteCaps_of s)\<rbrace>" apply (simp add: cteSwap_def) apply (wp getCTE_cteCap_wp | simp)+ apply (clarsimp split: option.split) apply (erule rsubst[where P=P], intro ext) apply (clarsimp simp: modify_map_def split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P ((cteCaps_of s)(a \<mapsto> cap2, b \<mapsto> cap1))\<rbrace> cteSwap cap1 a cap2 b \<lbrace>\<lambda>rv s. P (cteCaps_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P ((cteCaps_of s)(a \<mapsto> cap2, b \<mapsto> cap1))\<rbrace> do cte1 <- getCTE a;
y <- updateCap a cap2;
y <- updateCap b cap1;
y <- updateMDB (mdbPrev (cteMDBNode cte1)) (mdbNext_update (\<lambda>_. b));
y <- updateMDB (mdbNext (cteMDBNode cte1)) (mdbPrev_update (\<lambda>_. b));
cte2 <- getCTE b;
y <- updateMDB a (const (cteMDBNode cte2));
y <- updateMDB b (const (cteMDBNode cte1));
y <- updateMDB (mdbPrev (cteMDBNode cte2)) (mdbNext_update (\<lambda>_. a));
updateMDB (mdbNext (cteMDBNode cte2)) (mdbPrev_update (\<lambda>_. a))
od \<lbrace>\<lambda>rv s. P (cteCaps_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P ((cteCaps_of s)(a \<mapsto> cap2, b \<mapsto> cap1)) \<Longrightarrow> case cteCaps_of s a of None \<Rightarrow> True | Some cap \<Rightarrow> case modify_map (modify_map (cteCaps_of s) a (\<lambda>a. cap2)) b (\<lambda>a. cap1) b of None \<Rightarrow> True | Some cap \<Rightarrow> P (modify_map (modify_map (cteCaps_of s) a (\<lambda>a. cap2)) b (\<lambda>a. cap1)) proof (prove)
goal (1 subgoal):
 1. \<And>s x2 x2a. \<lbrakk>P ((cteCaps_of s)(a \<mapsto> cap2, b \<mapsto> cap1)); modify_map (modify_map (cteCaps_of s) a (\<lambda>a. cap2)) b (\<lambda>a. cap1) b = Some x2; cteCaps_of s a = Some x2a\<rbrakk> \<Longrightarrow> P (modify_map (modify_map (cteCaps_of s) a (\<lambda>a. cap2)) b (\<lambda>a. cap1)) proof (prove)
goal (1 subgoal):
 1. \<And>s x2 x2a x. \<lbrakk>modify_map (modify_map (cteCaps_of s) a (\<lambda>a. cap2)) b (\<lambda>a. cap1) b = Some x2; cteCaps_of s a = Some x2a\<rbrakk> \<Longrightarrow> ((cteCaps_of s)(a \<mapsto> cap2, b \<mapsto> cap1)) x = modify_map (modify_map (cteCaps_of s) a (\<lambda>a. cap2)) b (\<lambda>a. cap1) x proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma updateCap_cap_to':
  "\<lbrace>\<lambda>s. ex_cte_cap_to' p s \<and>
        cte_wp_at' (\<lambda>cte. p \<notin> cte_refs' (cteCap cte) (irq_node' s) - cte_refs' cap (irq_node' s)) sl s\<rbrace>
     updateCap sl cap
   \<lbrace>\<lambda>rv. ex_cte_cap_to' p\<rbrace>" apply (simp add: ex_cte_cap_to'_cteCap) apply wp apply clarsimp apply (rule_tac x=p' in exI) apply (clarsimp simp: modify_map_def cte_wp_at_ctes_of cteCaps_of_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. ex_cte_cap_wp_to' (\<lambda>_. True) p s \<and> cte_wp_at' (\<lambda>cte. p \<notin> cte_refs' (cteCap cte) (irq_node' s) - cte_refs' cap (irq_node' s)) sl s\<rbrace> updateCap sl cap \<lbrace>\<lambda>rv. ex_cte_cap_wp_to' (\<lambda>_. True) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<exists>p' c. cteCaps_of s p' = Some c \<and> p \<in> cte_refs' c (irq_node' s)) \<and> cte_wp_at' (\<lambda>cte. p \<in> cte_refs' (cteCap cte) (irq_node' s) \<longrightarrow> p \<in> cte_refs' cap (irq_node' s)) sl s\<rbrace> updateCap sl cap \<lbrace>\<lambda>rv s. \<exists>p' c. cteCaps_of s p' = Some c \<and> p \<in> cte_refs' c (irq_node' s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<exists>p' c. cteCaps_of s p' = Some c \<and> p \<in> cte_refs' c (irq_node' s)) \<and> cte_wp_at' (\<lambda>cte. p \<in> cte_refs' (cteCap cte) (irq_node' s) \<longrightarrow> p \<in> cte_refs' cap (irq_node' s)) sl s \<Longrightarrow> \<exists>p' c. modify_map (cteCaps_of s) sl (K cap) p' = Some c \<and> p \<in> cte_refs' c (irq_node' s) proof (prove)
goal (1 subgoal):
 1. \<And>s p' c. \<lbrakk>cte_wp_at' (\<lambda>cte. p \<in> cte_refs' (cteCap cte) (irq_node' s) \<longrightarrow> p \<in> cte_refs' cap (irq_node' s)) sl s; cteCaps_of s p' = Some c; p \<in> cte_refs' c (irq_node' s)\<rbrakk> \<Longrightarrow> \<exists>p' c. modify_map (cteCaps_of s) sl (\<lambda>y. cap) p' = Some c \<and> p \<in> cte_refs' c (irq_node' s) proof (prove)
goal (1 subgoal):
 1. \<And>s p' c. \<lbrakk>cte_wp_at' (\<lambda>cte. p \<in> cte_refs' (cteCap cte) (irq_node' s) \<longrightarrow> p \<in> cte_refs' cap (irq_node' s)) sl s; cteCaps_of s p' = Some c; p \<in> cte_refs' c (irq_node' s)\<rbrakk> \<Longrightarrow> \<exists>c. modify_map (cteCaps_of s) sl (\<lambda>y. cap) p' = Some c \<and> p \<in> cte_refs' c (irq_node' s) proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma emptySlot_deletes [wp]:
  "\<lbrace>\<top>\<rbrace> emptySlot p opt \<lbrace>\<lambda>rv s. cte_wp_at' (\<lambda>c. cteCap c = NullCap) p s\<rbrace>" apply (simp add: emptySlot_def case_Null_If) apply (subst tree_cte_cteCap_eq [unfolded o_def]) apply (wp getCTE_cteCap_wp opt_return_pres_lift) apply (clarsimp split: option.splits simp: modify_map_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> emptySlot p opt \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<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. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<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. 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> case cteCaps_of s p of None \<Rightarrow> True | Some cap \<Rightarrow> (cap = capability.NullCap \<longrightarrow> (case cteCaps_of s p of None \<Rightarrow> False | Some a \<Rightarrow> a = capability.NullCap)) \<and> (cap \<noteq> capability.NullCap \<longrightarrow> (case modify_map (cteCaps_of s) p (K capability.NullCap) p of None \<Rightarrow> False | Some a \<Rightarrow> a = capability.NullCap)) proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma capCylicZombieD[dest!]:
  "capCyclicZombie cap slot \<Longrightarrow> \<exists>zb n. cap = Zombie slot zb n" by (clarsimp simp: capCyclicZombie_def split: capability.split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. capCyclicZombie cap slot \<Longrightarrow> \<exists>zb n. cap = capability.Zombie slot zb n
theory CNodeInv_R

lemma cteSwap_cap_to'[wp]:
  "\<lbrace>ex_cte_cap_to' p\<rbrace> capSwapForDelete c1 c2 \<lbrace>\<lambda>rv. ex_cte_cap_to' p\<rbrace>" apply (simp add: cteSwap_def capSwapForDelete_def ex_cte_cap_to'_cteCap) apply (wp getCTE_cteCap_wp | simp add: o_def)+ apply (clarsimp split: option.splits) apply (rule_tac x="(id (c1 := c2, c2 := c1)) p'" in exI) apply (clarsimp simp: modify_map_def | rule conjI)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ex_cte_cap_wp_to' (\<lambda>_. True) p\<rbrace> capSwapForDelete c1 c2 \<lbrace>\<lambda>rv. ex_cte_cap_wp_to' (\<lambda>_. True) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<exists>p' c. cteCaps_of s p' = Some c \<and> p \<in> cte_refs' c (irq_node' s)\<rbrace> when (c1 \<noteq> c2) (do cap1 <- liftM cteCap (getCTE c1);
cap2 <- liftM cteCap (getCTE c2);
cte1 <- getCTE c1;
y <- updateCap c1 cap2;
y <- updateCap c2 cap1;
y <- updateMDB (mdbPrev (cteMDBNode cte1)) (mdbNext_update (\<lambda>_. c2));
y <- updateMDB (mdbNext (cteMDBNode cte1)) (mdbPrev_update (\<lambda>_. c2));
cte2 <- getCTE c2;
y <- updateMDB c1 (const (cteMDBNode cte2));
y <- updateMDB c2 (const (cteMDBNode cte1));
y <- updateMDB (mdbPrev (cteMDBNode cte2)) (mdbNext_update (\<lambda>_. c1));
updateMDB (mdbNext (cteMDBNode cte2)) (mdbPrev_update (\<lambda>_. c1))
od) \<lbrace>\<lambda>rv s. \<exists>p' c. cteCaps_of s p' = Some c \<and> p \<in> cte_refs' c (irq_node' s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<exists>p' c. cteCaps_of s p' = Some c \<and> p \<in> cte_refs' c (irq_node' s) \<Longrightarrow> c1 \<noteq> c2 \<longrightarrow> (case cteCaps_of s c1 of None \<Rightarrow> True | Some cap \<Rightarrow> case cteCaps_of s c2 of None \<Rightarrow> True | Some capa \<Rightarrow> case modify_map (modify_map (cteCaps_of s) c1 (\<lambda>a. capa)) c2 (\<lambda>a. cap) c2 of None \<Rightarrow> True | Some capb \<Rightarrow> \<exists>p' c. modify_map (modify_map (cteCaps_of s) c1 (\<lambda>a. capa)) c2 (\<lambda>a. cap) p' = Some c \<and> p \<in> cte_refs' c (irq_node' s)) proof (prove)
goal (1 subgoal):
 1. \<And>s p' c x2 x2a x2b. \<lbrakk>cteCaps_of s p' = Some c; p \<in> cte_refs' c (irq_node' s); modify_map (modify_map (cteCaps_of s) c1 (\<lambda>a. x2a)) c2 (\<lambda>a. x2) c2 = Some x2b; cteCaps_of s c2 = Some x2a; cteCaps_of s c1 = Some x2; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> \<exists>p' c. modify_map (modify_map (cteCaps_of s) c1 (\<lambda>a. x2a)) c2 (\<lambda>a. x2) p' = Some c \<and> p \<in> cte_refs' c (irq_node' s) proof (prove)
goal (1 subgoal):
 1. \<And>s p' c x2 x2a x2b. \<lbrakk>cteCaps_of s p' = Some c; p \<in> cte_refs' c (irq_node' s); modify_map (modify_map (cteCaps_of s) c1 (\<lambda>a. x2a)) c2 (\<lambda>a. x2) c2 = Some x2b; cteCaps_of s c2 = Some x2a; cteCaps_of s c1 = Some x2; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> \<exists>c. modify_map (modify_map (cteCaps_of s) c1 (\<lambda>a. x2a)) c2 (\<lambda>a. x2) ((id(c1 := c2, c2 := c1)) p') = Some c \<and> p \<in> cte_refs' c (irq_node' s) proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma zombieCTEs_le:
  "zombieCTEs zb \<le> 2 ^ zBits zb" by (cases zb, simp_all add: objBits_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. zombieCTEs zb \<le> 2 ^ zBits zb
theory CNodeInv_R

lemma cteSwap_sch_act_simple[wp]:
  "\<lbrace>sch_act_simple\<rbrace> cteSwap cap1 slot1 cap2 slot2 \<lbrace>\<lambda>_. sch_act_simple\<rbrace>" by (simp add: cteSwap_def sch_act_simple_def, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>sch_act_simple\<rbrace> cteSwap cap1 slot1 cap2 slot2 \<lbrace>\<lambda>_. sch_act_simple\<rbrace>
theory CNodeInv_R

lemma updateCap_sch_act_simple[wp]:
  "\<lbrace>sch_act_simple\<rbrace> updateCap slot newCap \<lbrace>\<lambda>_. sch_act_simple\<rbrace>" by (simp add: sch_act_simple_def, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>sch_act_simple\<rbrace> updateCap slot newCap \<lbrace>\<lambda>_. sch_act_simple\<rbrace>
theory CNodeInv_R

lemma no_cte_prop_top:
  "no_cte_prop \<top> = \<top>" by (simp add: no_cte_prop_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_cte_prop (\<lambda>_. True) = (\<lambda>_. True)
theory CNodeInv_R

lemma setCTE_no_cte_prop:
  "\<lbrace>no_cte_prop P\<rbrace> setCTE sl cte \<lbrace>\<lambda>_. no_cte_prop P\<rbrace>" by (simp add: no_cte_prop_def hoare_vcg_prop)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_cte_prop P\<rbrace> setCTE sl cte \<lbrace>\<lambda>_. no_cte_prop P\<rbrace>
theory CNodeInv_R

lemma setInterruptState_no_cte_prop:
  "\<lbrace>no_cte_prop P and K (finalise_prop_stuff P)\<rbrace> setInterruptState st \<lbrace>\<lambda>_. no_cte_prop P\<rbrace>" apply (simp add: setInterruptState_def, wp) apply (clarsimp simp: finalise_prop_stuff_def no_cte_prop_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_cte_prop P and K (finalise_prop_stuff P)\<rbrace> setInterruptState st \<lbrace>\<lambda>_. no_cte_prop P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (no_cte_prop P and (\<lambda>y. finalise_prop_stuff P)) s \<Longrightarrow> no_cte_prop P (s\<lparr>ksInterruptState := st\<rparr>) proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma dmo_maskInterrupt_no_cte_prop:
  "\<lbrace>no_cte_prop P and K (finalise_prop_stuff P)\<rbrace>
    doMachineOp (maskInterrupt m irq) \<lbrace>\<lambda>_. no_cte_prop P\<rbrace>" apply (wp dmo_maskInterrupt) apply (clarsimp simp: no_cte_prop_def finalise_prop_stuff_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_cte_prop P and K (finalise_prop_stuff P)\<rbrace> doMachineOp (maskInterrupt m irq) \<lbrace>\<lambda>_. no_cte_prop P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (no_cte_prop P and K (finalise_prop_stuff P)) s \<Longrightarrow> no_cte_prop P (ksMachineState_update (irq_masks_update (\<lambda>t. t(irq := m))) s) proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma updateTrackedFreeIndex_no_cte_prop[wp]:
  "\<lbrace>no_cte_prop P and K (finalise_prop_stuff P)\<rbrace>
    updateTrackedFreeIndex ptr idx \<lbrace>\<lambda>_. no_cte_prop P\<rbrace>" apply (simp add: updateTrackedFreeIndex_def getSlotCap_def) apply (wp getCTE_wp') apply (clarsimp simp: no_cte_prop_def finalise_prop_stuff_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_cte_prop P and K (finalise_prop_stuff P)\<rbrace> updateTrackedFreeIndex ptr idx \<lbrace>\<lambda>_. no_cte_prop P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_cte_prop P and (\<lambda>y. finalise_prop_stuff P)\<rbrace> do cte <- getCTE ptr;
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od \<lbrace>\<lambda>_. no_cte_prop P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (no_cte_prop P and (\<lambda>y. finalise_prop_stuff P)) s \<Longrightarrow> \<forall>cte. cte_wp_at' ((=) cte) ptr s \<longrightarrow> no_cte_prop P (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}, gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) of None \<Rightarrow> gsUntypedZeroRanges (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}\<rparr>) | Some r \<Rightarrow> insert r (gsUntypedZeroRanges (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}\<rparr>))\<rparr>) proof (prove)
goal:
No subgoals!