kings-crown/FVELER_Isabelle huggingface dataset:
theory CNodeInv_R

lemma n_next:
  "n p = Some cte \<Longrightarrow> \<exists>z. m (s_d_swp p) = Some z \<and> s_d_swp (mdbNext (cteMDBNode cte)) = mdbNext (cteMDBNode z)" apply (drule conjI [THEN exI [THEN next_m_n2 [THEN iffD1, unfolded mdb_next_unfold]]]) apply (rule refl) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n p = Some cte \<Longrightarrow> \<exists>z. m (s_d_swp p) = Some z \<and> s_d_swp (mdbNext (cteMDBNode cte)) = mdbNext (cteMDBNode z) proof (prove)
goal (2 subgoals):
 1. ?p' = mdbNext (cteMDBNode cte)
 2. \<exists>z. m (s_d_swp p) = Some z \<and> s_d_swp ?p' = mdbNext (cteMDBNode z) \<Longrightarrow> \<exists>z. m (s_d_swp p) = Some z \<and> s_d_swp (mdbNext (cteMDBNode cte)) = mdbNext (cteMDBNode z) proof (prove)
goal (1 subgoal):
 1. \<exists>z. m (s_d_swp p) = Some z \<and> s_d_swp (mdbNext (cteMDBNode cte)) = mdbNext (cteMDBNode z) \<Longrightarrow> \<exists>z. m (s_d_swp p) = Some z \<and> s_d_swp (mdbNext (cteMDBNode cte)) = mdbNext (cteMDBNode z) proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma n_prev:
  "n p = Some cte \<Longrightarrow> \<exists>z. m (s_d_swp p) = Some z \<and> s_d_swp (mdbPrev (cteMDBNode cte)) = mdbPrev (cteMDBNode z)" apply (drule conjI [THEN exI [THEN n_prevD [unfolded mdb_prev_def]]]) apply (rule refl) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n p = Some cte \<Longrightarrow> \<exists>z. m (s_d_swp p) = Some z \<and> s_d_swp (mdbPrev (cteMDBNode cte)) = mdbPrev (cteMDBNode z) proof (prove)
goal (2 subgoals):
 1. ?p = mdbPrev (cteMDBNode cte)
 2. \<exists>z. m (s_d_swp p) = Some z \<and> s_d_swp ?p = mdbPrev (cteMDBNode z) \<Longrightarrow> \<exists>z. m (s_d_swp p) = Some z \<and> s_d_swp (mdbPrev (cteMDBNode cte)) = mdbPrev (cteMDBNode z) proof (prove)
goal (1 subgoal):
 1. \<exists>z. m (s_d_swp p) = Some z \<and> s_d_swp (mdbPrev (cteMDBNode cte)) = mdbPrev (cteMDBNode z) \<Longrightarrow> \<exists>z. m (s_d_swp p) = Some z \<and> s_d_swp (mdbPrev (cteMDBNode cte)) = mdbPrev (cteMDBNode z) proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma ut_rev_n: "ut_revocable' n" proof - from valid have "ut_revocable' m" .. thus ?thesis using dest_derived src_derived src dest apply (clarsimp simp: ut_revocable'_def) apply (frule n_cap) apply (frule revokable) by (auto simp: weak_derived'_def dest2_node_def
            split: if_split_asm) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ut_revocable' n proof (state)
goal (1 subgoal):
 1. ut_revocable' n proof (chain)
picking this:
valid_mdb_ctes m proof (prove)
using this:
valid_mdb_ctes m

goal (1 subgoal):
 1. ut_revocable' m proof (state)
this:
ut_revocable' m

goal (1 subgoal):
 1. ut_revocable' n proof (prove)
using this:
ut_revocable' m

goal (1 subgoal):
 1. ut_revocable' n proof (prove)
using this:
ut_revocable' m
weak_derived' dest_cap dcap
weak_derived' src_cap scap
m src = Some (CTE src_cap src_node)
m dest = Some (CTE dest_cap dest_node)

goal (1 subgoal):
 1. ut_revocable' n proof (prove)
goal (1 subgoal):
 1. \<And>p cap na. \<lbrakk>\<forall>p cap n. m p = Some (CTE cap n) \<longrightarrow> isUntypedCap cap \<longrightarrow> mdbRevocable n; weak_derived' dest_cap dcap; weak_derived' src_cap scap; m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); n p = Some (CTE cap na); isUntypedCap cap\<rbrakk> \<Longrightarrow> mdbRevocable na proof (prove)
goal (1 subgoal):
 1. \<And>p cap na. \<lbrakk>\<forall>p cap n. m p = Some (CTE cap n) \<longrightarrow> isUntypedCap cap \<longrightarrow> mdbRevocable n; weak_derived' dest_cap dcap; weak_derived' src_cap scap; m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); n p = Some (CTE cap na); isUntypedCap cap; if p = src then cap = dcap else if p = dest then cap = scap else \<exists>node'. m p = Some (CTE cap node')\<rbrakk> \<Longrightarrow> mdbRevocable na proof (prove)
goal (1 subgoal):
 1. \<And>p cap na. \<lbrakk>\<forall>p cap n. m p = Some (CTE cap n) \<longrightarrow> isUntypedCap cap \<longrightarrow> mdbRevocable n; weak_derived' dest_cap dcap; weak_derived' src_cap scap; m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); n p = Some (CTE cap na); isUntypedCap cap; if p = src then cap = dcap else if p = dest then cap = scap else \<exists>node'. m p = Some (CTE cap node'); if p = src then mdbRevocable na = mdbRevocable dest_node else if p = dest then mdbRevocable na = mdbRevocable src_node else \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbRevocable na = mdbRevocable node'\<rbrakk> \<Longrightarrow> mdbRevocable na proof (state)
this:
ut_revocable' n

goal:
No subgoals!
theory CNodeInv_R

lemma scap_class[simp]:
  "capClass scap = capClass src_cap" using src_derived apply (clarsimp simp: weak_derived'_def) apply (rule master_eqI, rule capClass_Master) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. capClass scap = capClass src_cap proof (prove)
using this:
weak_derived' src_cap scap

goal (1 subgoal):
 1. capClass scap = capClass src_cap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>capMasterCap src_cap = capMasterCap scap; capBadge src_cap = capBadge scap; capASID src_cap = capASID scap; cap_asid_base' src_cap = cap_asid_base' scap; cap_vptr' src_cap = cap_vptr' scap; isReplyCap src_cap \<longrightarrow> capTCBPtr src_cap = capTCBPtr scap \<and> capReplyMaster src_cap = capReplyMaster scap\<rbrakk> \<Longrightarrow> capClass scap = capClass src_cap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>capMasterCap src_cap = capMasterCap scap; capBadge src_cap = capBadge scap; capASID src_cap = capASID scap; cap_asid_base' src_cap = cap_asid_base' scap; cap_vptr' src_cap = cap_vptr' scap; isReplyCap src_cap \<longrightarrow> capTCBPtr src_cap = capTCBPtr scap \<and> capReplyMaster src_cap = capReplyMaster scap\<rbrakk> \<Longrightarrow> capClass (capMasterCap scap) = capClass (capMasterCap src_cap) proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma dcap_class[simp]:
  "capClass dcap = capClass dest_cap" using dest_derived apply (clarsimp simp: weak_derived'_def) apply (rule master_eqI, rule capClass_Master) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. capClass dcap = capClass dest_cap proof (prove)
using this:
weak_derived' dest_cap dcap

goal (1 subgoal):
 1. capClass dcap = capClass dest_cap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>capMasterCap dest_cap = capMasterCap dcap; capBadge dest_cap = capBadge dcap; capASID dest_cap = capASID dcap; cap_asid_base' dest_cap = cap_asid_base' dcap; cap_vptr' dest_cap = cap_vptr' dcap; isReplyCap dest_cap \<longrightarrow> capTCBPtr dest_cap = capTCBPtr dcap \<and> capReplyMaster dest_cap = capReplyMaster dcap\<rbrakk> \<Longrightarrow> capClass dcap = capClass dest_cap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>capMasterCap dest_cap = capMasterCap dcap; capBadge dest_cap = capBadge dcap; capASID dest_cap = capASID dcap; cap_asid_base' dest_cap = cap_asid_base' dcap; cap_vptr' dest_cap = cap_vptr' dcap; isReplyCap dest_cap \<longrightarrow> capTCBPtr dest_cap = capTCBPtr dcap \<and> capReplyMaster dest_cap = capReplyMaster dcap\<rbrakk> \<Longrightarrow> capClass (capMasterCap dcap) = capClass (capMasterCap dest_cap) proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma distinct_zombies_m:
  "distinct_zombies m" using valid by auto

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

lemma distinct_zombies_n:
  "distinct_zombies n" using distinct_zombies_m apply (simp add: n_def distinct_zombies_nonCTE_modify_map) apply (simp add: n'_def distinct_zombies_nonCTE_modify_map) apply (simp add: modify_map_apply src dest) apply (erule distinct_zombies_switchE, rule src, rule dest) apply (cut_tac weak_der_src) apply (clarsimp simp: weak_der'_def weak_derived'_def) apply (cut_tac weak_der_dest) apply (clarsimp simp: weak_der'_def weak_derived'_def) done

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

goal (1 subgoal):
 1. distinct_zombies n proof (prove)
goal (1 subgoal):
 1. distinct_zombies m \<Longrightarrow> distinct_zombies n' proof (prove)
goal (1 subgoal):
 1. distinct_zombies m \<Longrightarrow> distinct_zombies (modify_map (modify_map m src (cteCap_update (\<lambda>_. dcap))) dest (cteCap_update (\<lambda>_. scap))) proof (prove)
goal (1 subgoal):
 1. distinct_zombies m \<Longrightarrow> distinct_zombies (m(src \<mapsto> CTE dcap src_node, dest \<mapsto> CTE scap dest_node)) proof (prove)
goal (2 subgoals):
 1. capMasterCap (cteCap (CTE src_cap src_node)) = capMasterCap (cteCap (CTE scap dest_node))
 2. capMasterCap (cteCap (CTE dest_cap dest_node)) = capMasterCap (cteCap (CTE dcap src_node)) proof (prove)
goal (2 subgoals):
 1. weak_der' src_cap scap \<Longrightarrow> capMasterCap (cteCap (CTE src_cap src_node)) = capMasterCap (cteCap (CTE scap dest_node))
 2. capMasterCap (cteCap (CTE dest_cap dest_node)) = capMasterCap (cteCap (CTE dcap src_node)) proof (prove)
goal (1 subgoal):
 1. capMasterCap (cteCap (CTE dest_cap dest_node)) = capMasterCap (cteCap (CTE dcap src_node)) proof (prove)
goal (1 subgoal):
 1. weak_der' dest_cap dcap \<Longrightarrow> capMasterCap (cteCap (CTE dest_cap dest_node)) = capMasterCap (cteCap (CTE dcap src_node)) proof (prove)
goal:
No subgoals!
theory CNodeInv_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 CNodeInv_R

lemma cteSwap_valid_mdb_helper:
  assumes untyped_eq: "isUntypedCap src_cap \<Longrightarrow> scap = src_cap"
                      "isUntypedCap dest_cap \<Longrightarrow> dcap = dest_cap"
  shows "valid_mdb_ctes n" using cteSwap_chain cteSwap_dlist_helper cteSwap_valid_badges
        cteSwap_chunked caps_contained untyped_mdb_n untyped_inc_n
        nullcaps_n ut_rev_n class_links_n irq_control_n
        distinct_zombies_n reply_masters_rvk_fb_n by (auto simp:untyped_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_mdb_ctes n proof (prove)
using this:
mdb_chain_0 n
valid_dlist n
valid_badges n
mdb_chunked n
caps_contained' n
untyped_mdb' n
\<lbrakk>isUntypedCap src_cap \<Longrightarrow> scap = src_cap; isUntypedCap dest_cap \<Longrightarrow> dcap = dest_cap\<rbrakk> \<Longrightarrow> untyped_inc' n
valid_nullcaps n
ut_revocable' n
class_links n
irq_control n
distinct_zombies n
reply_masters_rvk_fb n

goal (1 subgoal):
 1. valid_mdb_ctes n
theory CNodeInv_R

lemma cteSwap_idle'[wp]:
  "\<lbrace>valid_idle'\<rbrace>
     cteSwap c c1 c' c2
   \<lbrace>\<lambda>rv s. valid_idle' s\<rbrace>" apply (simp add: cteSwap_def) apply (wp updateCap_idle' | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle'\<rbrace> cteSwap c c1 c' c2 \<lbrace>\<lambda>rv. valid_idle'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle'\<rbrace> do cte1 <- getCTE c1;
y <- updateCap c1 c';
y <- updateCap c2 c;
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. valid_idle'\<rbrace> proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma weak_derived_cte_refs:
  "weak_derived' c c' \<Longrightarrow> cte_refs' c' = cte_refs' c" apply (clarsimp simp: weak_derived'_def) apply (rule master_eqI, rule cte_refs_Master) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. weak_derived' c c' \<Longrightarrow> cte_refs' c' = cte_refs' c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>capMasterCap c = capMasterCap c'; capBadge c = capBadge c'; capASID c = capASID c'; cap_asid_base' c = cap_asid_base' c'; cap_vptr' c = cap_vptr' c'; isReplyCap c \<longrightarrow> capTCBPtr c = capTCBPtr c' \<and> capReplyMaster c = capReplyMaster c'\<rbrakk> \<Longrightarrow> cte_refs' c' = cte_refs' c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>capMasterCap c = capMasterCap c'; capBadge c = capBadge c'; capASID c = capASID c'; cap_asid_base' c = cap_asid_base' c'; cap_vptr' c = cap_vptr' c'; isReplyCap c \<longrightarrow> capTCBPtr c = capTCBPtr c' \<and> capReplyMaster c = capReplyMaster c'\<rbrakk> \<Longrightarrow> cte_refs' (capMasterCap c') = cte_refs' (capMasterCap c) proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma weak_derived_capRange_capBits:
  "weak_derived' c c' \<Longrightarrow> capRange c' = capRange c \<and> capBits c' = capBits c" apply (clarsimp simp: weak_derived'_def) apply (metis capRange_Master capBits_Master) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. weak_derived' c c' \<Longrightarrow> capRange c' = capRange c \<and> capBits c' = capBits c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>capMasterCap c = capMasterCap c'; capBadge c = capBadge c'; capASID c = capASID c'; cap_asid_base' c = cap_asid_base' c'; cap_vptr' c = cap_vptr' c'; isReplyCap c \<longrightarrow> capTCBPtr c = capTCBPtr c' \<and> capReplyMaster c = capReplyMaster c'\<rbrakk> \<Longrightarrow> capRange c' = capRange c \<and> capBits c' = capBits c proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma capSwap_invs'[wp]:
  "\<lbrace>invs' and ex_cte_cap_to' c1 and ex_cte_cap_to' c2\<rbrace>
  capSwapForDelete c1 c2
  \<lbrace>\<lambda>rv. invs'\<rbrace>" apply (simp add: capSwapForDelete_def) apply (wp getCTE_wp') apply (clarsimp simp: cte_wp_at_ctes_of) apply (auto dest!: ctes_of_valid') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and ex_cte_cap_wp_to' (\<lambda>_. True) c1 and ex_cte_cap_wp_to' (\<lambda>_. True) c2\<rbrace> capSwapForDelete c1 c2 \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and ex_cte_cap_wp_to' (\<lambda>_. True) c1 and ex_cte_cap_wp_to' (\<lambda>_. True) c2\<rbrace> when (c1 \<noteq> c2) (do cap1 <- liftM cteCap (getCTE c1);
cap2 <- liftM cteCap (getCTE c2);
cteSwap cap1 c1 cap2 c2
od) \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs' and ex_cte_cap_wp_to' (\<lambda>_. True) c1 and ex_cte_cap_wp_to' (\<lambda>_. True) c2) s \<Longrightarrow> (if c1 \<noteq> c2 then \<lambda>s. \<forall>cte. cte_wp_at' ((=) cte) c1 s \<longrightarrow> ((\<lambda>cap1 s. \<forall>cte. cte_wp_at' ((=) cte) c2 s \<longrightarrow> ((\<lambda>cap2 s. invs' s \<and> valid_cap' cap1 s \<and> valid_cap' cap2 s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) c1 s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) c2 s \<and> cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = cap1) c1 s \<and> cte_wp_at' (weak_derived' cap2 \<circ> cteCap) c2 s \<and> cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = cap2) c2 s \<and> cte_wp_at' (weak_derived' cap1 \<circ> cteCap) c1 s \<and> K (c1 \<noteq> c2) s) \<circ> cteCap) cte s) \<circ> cteCap) cte s else invs') s proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea. \<lbrakk>invs' s; ex_cte_cap_wp_to' (\<lambda>_. True) c1 s; ex_cte_cap_wp_to' (\<lambda>_. True) c2 s; c1 \<noteq> c2; ctes_of s c1 = Some cte; ctes_of s c2 = Some ctea\<rbrakk> \<Longrightarrow> valid_cap' (cteCap cte) s \<and> valid_cap' (cteCap ctea) s proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma Zombie_isZombie[simp]:
  "isZombie (Zombie x y z)" by (simp add: isZombie_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isZombie (capability.Zombie x y z)
theory CNodeInv_R

lemma mdb_next_cap_upd:
  "m sl = Some (CTE cap' mdbnode) \<Longrightarrow>
  m (sl \<mapsto> CTE cap mdbnode) \<turnstile> p \<leadsto> p' = m \<turnstile> p \<leadsto> p'" by (simp add: mdb_next_unfold)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m sl = Some (CTE cap' mdbnode) \<Longrightarrow> m(sl \<mapsto> CTE cap mdbnode) \<turnstile> p \<leadsto> p' = m \<turnstile> p \<leadsto> p'
theory CNodeInv_R

lemma rtrancl_cap_upd:
  "m sl = Some (CTE cap' mdbnode) \<Longrightarrow>
  m (sl \<mapsto> CTE cap mdbnode) \<turnstile> p \<leadsto>\<^sup>* p' = m \<turnstile> p \<leadsto>\<^sup>* p'" by (simp add: trancl_cap_upd rtrancl_eq_or_trancl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m sl = Some (CTE cap' mdbnode) \<Longrightarrow> m(sl \<mapsto> CTE cap mdbnode) \<turnstile> p \<leadsto>\<^sup>* p' = m \<turnstile> p \<leadsto>\<^sup>* p'
theory CNodeInv_R

lemma no_loops_tranclD:
  "\<lbrakk> m \<turnstile> p \<leadsto>\<^sup>+ p'; no_loops m \<rbrakk> \<Longrightarrow> \<not> m \<turnstile> p' \<leadsto>\<^sup>+ p" apply clarsimp apply (drule (1) trancl_trans) apply (simp add: no_loops_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> p \<leadsto>\<^sup>+ p'; no_loops m\<rbrakk> \<Longrightarrow> (p', p) \<notin> (mdb_next_rel m)\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> p \<leadsto>\<^sup>+ p'; no_loops m; m \<turnstile> p' \<leadsto>\<^sup>+ p\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_loops m; m \<turnstile> p' \<leadsto>\<^sup>+ p; m \<turnstile> p \<leadsto>\<^sup>+ p\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma ex_cte_cap_to'_cteCap:
  "ex_cte_cap_to' p = (\<lambda>s. \<exists>p' c. cteCaps_of s p' = Some c \<and> p \<in> cte_refs' c (irq_node' s))" apply (simp add: ex_cte_cap_to'_def cte_wp_at_ctes_of cteCaps_of_def) apply (fastforce intro!: ext) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ex_cte_cap_wp_to' (\<lambda>_. True) p = (\<lambda>s. \<exists>p' c. cteCaps_of s p' = Some c \<and> p \<in> cte_refs' c (irq_node' s)) proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. \<exists>cref cte. ctes_of s cref = Some cte \<and> p \<in> cte_refs' (cteCap cte) (irq_node' s)) = (\<lambda>s. \<exists>p' c. (\<exists>z. ctes_of s p' = Some z \<and> cteCap z = c) \<and> p \<in> cte_refs' c (irq_node' s)) proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma class_links_update:
  "\<lbrakk> class_links m; \<exists>cte. m x = Some cte
      \<and> mdbNext (cteMDBNode cte) = mdbNext (cteMDBNode cte')
      \<and> capClass (cteCap cte) = capClass (cteCap cte') \<rbrakk>
        \<Longrightarrow> class_links (m(x \<mapsto> cte'))" apply clarsimp apply (unfold class_links_def) apply (erule allEI, erule allEI) apply (clarsimp simp: mdb_next_unfold split del: if_split split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>class_links m; \<exists>cte. m x = Some cte \<and> mdbNext (cteMDBNode cte) = mdbNext (cteMDBNode cte') \<and> capClass (cteCap cte) = capClass (cteCap cte')\<rbrakk> \<Longrightarrow> class_links (m(x \<mapsto> cte')) proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrakk>class_links m; m x = Some cte; mdbNext (cteMDBNode cte) = mdbNext (cteMDBNode cte'); capClass (cteCap cte) = capClass (cteCap cte')\<rbrakk> \<Longrightarrow> class_links (m(x \<mapsto> cte')) proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrakk>\<forall>p p' cte cte'. m p = Some cte \<longrightarrow> m p' = Some cte' \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte'); m x = Some cte; mdbNext (cteMDBNode cte) = mdbNext (cteMDBNode cte'); capClass (cteCap cte) = capClass (cteCap cte')\<rbrakk> \<Longrightarrow> \<forall>p p' cte cte'a. (m(x \<mapsto> cte')) p = Some cte \<longrightarrow> (m(x \<mapsto> cte')) p' = Some cte'a \<longrightarrow> m(x \<mapsto> cte') \<turnstile> p \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte'a) proof (prove)
goal (1 subgoal):
 1. \<And>cte p p'. \<lbrakk>m x = Some cte; mdbNext (cteMDBNode cte) = mdbNext (cteMDBNode cte'); capClass (cteCap cte) = capClass (cteCap cte'); \<forall>cte cte'. m p = Some cte \<longrightarrow> m p' = Some cte' \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')\<rbrakk> \<Longrightarrow> \<forall>cte cte'a. (m(x \<mapsto> cte')) p = Some cte \<longrightarrow> (m(x \<mapsto> cte')) p' = Some cte'a \<longrightarrow> m(x \<mapsto> cte') \<turnstile> p \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte'a) proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma sameRegionAs_Zombie[simp]:
  "\<not> sameRegionAs (Zombie p zb n) cap" by (simp add: sameRegionAs_def3 isCap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> global.sameRegionAs (capability.Zombie p zb n) cap
theory CNodeInv_R

lemma invalid_Thread_CNode:
  "\<lbrakk> isThreadCap cap; isCNodeCap cap'; s \<turnstile>' cap; s \<turnstile>' cap' \<rbrakk>
        \<Longrightarrow> capUntypedPtr cap \<noteq> capUntypedPtr cap'" apply (clarsimp simp: valid_cap'_def isCap_simps) apply (drule_tac x=0 in spec) apply (clarsimp simp: obj_at'_def projectKOs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isThreadCap cap; isCNodeCap cap'; valid_cap' cap s; valid_cap' cap' s\<rbrakk> \<Longrightarrow> global.capUntypedPtr cap \<noteq> global.capUntypedPtr cap' proof (prove)
goal (1 subgoal):
 1. \<And>v0a v1 v2 v3. \<lbrakk>cap = capability.ThreadCap v0a; cap' = capability.CNodeCap v0a v1 v2 v3; capAligned (capability.ThreadCap v0a); tcb_at' v0a s; capAligned (capability.CNodeCap v0a v1 v2 v3); 0 < v1; v1 + v3 \<le> word_bits; v2 && mask v3 = v2; \<forall>addr. real_cte_at' (v0a + 2 ^ cteSizeBits * (addr && mask v1)) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>v0a v1 v2 v3. \<lbrakk>cap = capability.ThreadCap v0a; cap' = capability.CNodeCap v0a v1 v2 v3; capAligned (capability.ThreadCap v0a); tcb_at' v0a s; capAligned (capability.CNodeCap v0a v1 v2 v3); 0 < v1; v1 + v3 \<le> word_bits; v2 && mask v3 = v2; real_cte_at' (v0a + 2 ^ cteSizeBits * (0 && mask v1)) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma capBits_capUntyped_capRange:
  "\<lbrakk> capBits cap = capBits cap';
     capUntypedPtr cap = capUntypedPtr cap';
     capClass cap = capClass cap' \<rbrakk>
          \<Longrightarrow> capRange cap = capRange cap'" by (simp add: capRange_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>capBits cap = capBits cap'; global.capUntypedPtr cap = global.capUntypedPtr cap'; capClass cap = capClass cap'\<rbrakk> \<Longrightarrow> capRange cap = capRange cap'
theory CNodeInv_R

lemma ztc_phys:
  "\<lbrakk> isCNodeCap cap \<or> isThreadCap cap \<or> isZombie cap \<rbrakk>
       \<Longrightarrow> capClass cap = PhysicalClass" by (auto simp: isCap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isCNodeCap cap \<or> isThreadCap cap \<or> isZombie cap \<Longrightarrow> capClass cap = PhysicalClass