theory CSpace_R

lemma cteInsert_mdb_chain_0:
  "\<lbrace>valid_mdb' and pspace_aligned' and pspace_distinct' and (\<lambda>s. src \<noteq> dest) and
    (\<lambda>s. cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s)\<rbrace>
  cteInsert cap src dest
  \<lbrace>\<lambda>_ s. mdb_chain_0 (ctes_of s)\<rbrace>" apply (unfold cteInsert_def updateCap_def) apply (simp add: valid_mdb'_def split del: if_split) apply (wp updateMDB_ctes_of_no_0 getCTE_wp') apply (clarsimp simp: cte_wp_at_ctes_of simp del: fun_upd_apply) apply (wp hoare_vcg_imp_lift hoare_vcg_all_lift setUntypedCapAsFull_ctes_of
    setUntypedCapAsFull_ctes_of_no_0  mdb_inv_preserve_modify_map
    setUntypedCapAsFull_mdb_chain_0 mdb_inv_preserve_fun_upd | simp del:fun_upd_apply)+ apply (wp getCTE_wp)+ apply (clarsimp simp:cte_wp_at_ctes_of simp del:fun_upd_apply) apply (subgoal_tac "src \<noteq> 0") prefer 2 apply (fastforce simp: valid_mdb_ctes_def no_0_def) apply (subgoal_tac "dest \<noteq> 0") prefer 2 apply (fastforce simp: valid_mdb_ctes_def no_0_def) apply (rule conjI) apply (fastforce simp: valid_mdb_ctes_def no_0_def) apply (case_tac cte) apply (rename_tac s_cap s_node) apply (case_tac x) apply (simp add: nullPointer_def) apply (subgoal_tac "mdb_insert (ctes_of s) src s_cap s_node dest NullCap node" for node) apply (drule mdb_insert.chain_n) apply (rule mdb_chain_0_modify_map_prev) apply (simp add:modify_map_apply) apply (clarsimp simp: valid_badges_def) apply unfold_locales apply (assumption|rule refl)+ apply (simp add: valid_mdb_ctes_def) apply (simp add: valid_mdb_ctes_def) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_mdb' and pspace_aligned' and pspace_distinct' and (\<lambda>s. src \<noteq> dest) and (\<lambda>s. cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s)\<rbrace> cteInsert cap src dest \<lbrace>\<lambda>_ s. mdb_chain_0 (ctes_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_mdb' and pspace_aligned' and pspace_distinct' and (\<lambda>s. src \<noteq> dest) and (\<lambda>s. cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s)\<rbrace> do srcCTE <- getCTE src;
srcMDB <- return (cteMDBNode srcCTE);
srcCap <- return (cteCap srcCTE);
newCapIsRevocable <- return (revokable' srcCap cap);
newMDB <- return (mdbFirstBadged_update (\<lambda>_. newCapIsRevocable) (mdbRevocable_update (\<lambda>_. newCapIsRevocable) (mdbPrev_update (\<lambda>_. src) srcMDB)));
oldCTE <- getCTE dest;
haskell_assert (isNullCap $ cteCap oldCTE) [];
haskell_assert (mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer) [];
setUntypedCapAsFull srcCap cap src;
do cte <- getCTE dest;
setCTE dest (cteCap_update (\<lambda>_. cap) cte)
od;
updateMDB dest (const newMDB);
updateMDB src (mdbNext_update (\<lambda>_. dest));
updateMDB (mdbNext newMDB) (mdbPrev_update (\<lambda>_. dest))
od \<lbrace>\<lambda>_ s. mdb_chain_0 (ctes_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. valid_mdb_ctes (ctes_of s)) and pspace_aligned' and pspace_distinct' and (\<lambda>s. src \<noteq> dest) and (\<lambda>s. cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s)\<rbrace> do srcCTE <- getCTE src;
oldCTE <- getCTE dest;
y <- assert (cteCap oldCTE = capability.NullCap);
y <- assert (mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer);
y <- setUntypedCapAsFull (cteCap srcCTE) cap src;
y <- do cte <- getCTE dest;
setCTE dest (cteCap_update (\<lambda>_. cap) cte)
od;
y <- updateMDB dest (const (mdbFirstBadged_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode srcCTE)))));
y <- updateMDB src (mdbNext_update (\<lambda>_. dest));
updateMDB (mdbNext (cteMDBNode srcCTE)) (mdbPrev_update (\<lambda>_. dest))
od \<lbrace>\<lambda>_ s. mdb_chain_0 (ctes_of s)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>srcCTE x y ya. \<lbrace>?B4 srcCTE x y ya\<rbrace> setUntypedCapAsFull (cteCap srcCTE) cap src \<lbrace>\<lambda>yb s. \<forall>cte. cte_wp_at' ((=) cte) dest s \<longrightarrow> no_0 ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) cte)) \<and> no_0 (modify_map ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) cte)) dest (cteMDBNode_update (const (mdbFirstBadged_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode srcCTE))))))) \<and> no_0 (modify_map (modify_map ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) cte)) dest (cteMDBNode_update (const (mdbFirstBadged_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode srcCTE))))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) \<and> mdb_chain_0 (modify_map (modify_map (modify_map ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) cte)) dest (cteMDBNode_update (const (mdbFirstBadged_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode srcCTE))))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode srcCTE)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))))\<rbrace>
 2. \<And>srcCTE x y. \<lbrace>?B3 srcCTE x y\<rbrace> assert (mdbPrev (cteMDBNode x) = nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer) \<lbrace>?B4 srcCTE x y\<rbrace>
 3. \<And>srcCTE x. \<lbrace>?B2 srcCTE x\<rbrace> assert (cteCap x = capability.NullCap) \<lbrace>?B3 srcCTE x\<rbrace>
 4. \<And>srcCTE. \<lbrace>?B1 srcCTE\<rbrace> getCTE dest \<lbrace>?B2 srcCTE\<rbrace>
 5. \<lbrace>?Q\<rbrace> getCTE src \<lbrace>?B1\<rbrace>
 6. \<And>s. ((\<lambda>s. valid_mdb_ctes (ctes_of s)) and pspace_aligned' and pspace_distinct' and (\<lambda>s. src \<noteq> dest) and (\<lambda>s. cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s)) s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>srcCTE x. \<lbrace>?B4 srcCTE x () ()\<rbrace> setUntypedCapAsFull (cteCap srcCTE) cap src \<lbrace>\<lambda>yb s. \<forall>cte. ctes_of s dest = Some cte \<longrightarrow> no_0 ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) cte)) \<and> mdb_chain_0 (modify_map (modify_map (modify_map ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) cte)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode srcCTE)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode srcCTE)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))))\<rbrace>
 2. \<And>srcCTE x y. \<lbrace>?B3 srcCTE x y\<rbrace> assert (mdbPrev (cteMDBNode x) = nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer) \<lbrace>?B4 srcCTE x y\<rbrace>
 3. \<And>srcCTE x. \<lbrace>?B2 srcCTE x\<rbrace> assert (cteCap x = capability.NullCap) \<lbrace>?B3 srcCTE x\<rbrace>
 4. \<And>srcCTE. \<lbrace>?B1 srcCTE\<rbrace> getCTE dest \<lbrace>?B2 srcCTE\<rbrace>
 5. \<lbrace>?Q\<rbrace> getCTE src \<lbrace>?B1\<rbrace>
 6. \<And>s. ((\<lambda>s. valid_mdb_ctes (ctes_of s)) and pspace_aligned' and pspace_distinct' and (\<lambda>s. src \<noteq> dest) and (\<lambda>s. cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s)) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>srcCTE x. \<lbrace>?P'68 srcCTE x\<rbrace> getCTE dest \<lbrace>\<lambda>rv s. cteCap rv \<noteq> capability.NullCap\<rbrace>
 2. \<And>srcCTE x. \<lbrace>?Q'68 srcCTE x\<rbrace> getCTE dest \<lbrace>\<lambda>rv s. mdbPrev (cteMDBNode rv) = nullPointer \<longrightarrow> mdbNext (cteMDBNode rv) = nullPointer \<longrightarrow> src \<noteq> dest \<and> ctes_of s dest \<noteq> Some x \<or> src = dest \<and> CTE (maskedAsFull (cteCap srcCTE) cap) (cteMDBNode srcCTE) \<noteq> x \<and> cte_wp_at' ((=) srcCTE) src s \<or> no_0 ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) x)) \<and> cte_wp_at' ((=) srcCTE) src s \<and> mdb_chain_0 (modify_map (modify_map (modify_map ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) x)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode srcCTE)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode srcCTE)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) \<and> cte_wp_at' (\<lambda>c. c = srcCTE) src s\<rbrace>
 3. \<lbrace>?Q\<rbrace> getCTE src \<lbrace>\<lambda>srcCTE s. \<forall>x. ?P'68 srcCTE x s \<or> ?Q'68 srcCTE x s\<rbrace>
 4. \<And>s. ((\<lambda>s. valid_mdb_ctes (ctes_of s)) and pspace_aligned' and pspace_distinct' and (\<lambda>s. src \<noteq> dest) and (\<lambda>s. cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s)) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. valid_mdb_ctes (ctes_of s)) and pspace_aligned' and pspace_distinct' and (\<lambda>s. src \<noteq> dest) and (\<lambda>s. cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s)) s \<Longrightarrow> cte_wp_at' (\<lambda>_. True) src s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) src s \<and> (\<forall>x. (cte_wp_at' (\<lambda>_. True) dest s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) dest s \<and> cteCap cte \<noteq> capability.NullCap)) \<or> (cte_wp_at' (\<lambda>_. True) dest s \<longrightarrow> (\<exists>ctea. cte_wp_at' ((=) ctea) dest s \<and> (mdbPrev (cteMDBNode ctea) = nullPointer \<longrightarrow> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> src \<noteq> dest \<and> ctes_of s dest \<noteq> Some x \<or> src = dest \<and> CTE (maskedAsFull (cteCap cte) cap) (cteMDBNode cte) \<noteq> x \<and> cte_wp_at' ((=) cte) src s \<or> no_0 ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) x)) \<and> cte_wp_at' ((=) cte) src s \<and> mdb_chain_0 (modify_map (modify_map (modify_map ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) x)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode cte)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) \<and> cte_wp_at' (\<lambda>c. c = cte) src s))))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte x. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; is_derived' (ctes_of s) src cap (cteCap cte); ctes_of s src = Some cte; ctes_of s dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = nullPointer; mdbNext (cteMDBNode x) = nullPointer\<rbrakk> \<Longrightarrow> no_0 ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) x)) \<and> mdb_chain_0 (modify_map (modify_map (modify_map ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) x)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode cte)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (2 subgoals):
 1. \<And>s cte x. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; is_derived' (ctes_of s) src cap (cteCap cte); ctes_of s src = Some cte; ctes_of s dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = nullPointer; mdbNext (cteMDBNode x) = nullPointer; src \<noteq> 0\<rbrakk> \<Longrightarrow> no_0 ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) x)) \<and> mdb_chain_0 (modify_map (modify_map (modify_map ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) x)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode cte)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))))
 2. \<And>s cte x. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; is_derived' (ctes_of s) src cap (cteCap cte); ctes_of s src = Some cte; ctes_of s dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = nullPointer; mdbNext (cteMDBNode x) = nullPointer\<rbrakk> \<Longrightarrow> src \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. \<And>s cte x. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; is_derived' (ctes_of s) src cap (cteCap cte); ctes_of s src = Some cte; ctes_of s dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = nullPointer; mdbNext (cteMDBNode x) = nullPointer\<rbrakk> \<Longrightarrow> src \<noteq> 0
 2. \<And>s cte x. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; is_derived' (ctes_of s) src cap (cteCap cte); ctes_of s src = Some cte; ctes_of s dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = nullPointer; mdbNext (cteMDBNode x) = nullPointer; src \<noteq> 0\<rbrakk> \<Longrightarrow> no_0 ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) x)) \<and> mdb_chain_0 (modify_map (modify_map (modify_map ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) x)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode cte)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte x. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; is_derived' (ctes_of s) src cap (cteCap cte); ctes_of s src = Some cte; ctes_of s dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = nullPointer; mdbNext (cteMDBNode x) = nullPointer; src \<noteq> 0\<rbrakk> \<Longrightarrow> no_0 ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) x)) \<and> mdb_chain_0 (modify_map (modify_map (modify_map ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) x)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode cte)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (2 subgoals):
 1. \<And>s cte x. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; is_derived' (ctes_of s) src cap (cteCap cte); ctes_of s src = Some cte; ctes_of s dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = nullPointer; mdbNext (cteMDBNode x) = nullPointer; src \<noteq> 0; dest \<noteq> 0\<rbrakk> \<Longrightarrow> no_0 ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) x)) \<and> mdb_chain_0 (modify_map (modify_map (modify_map ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) x)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode cte)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))))
 2. \<And>s cte x. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; is_derived' (ctes_of s) src cap (cteCap cte); ctes_of s src = Some cte; ctes_of s dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = nullPointer; mdbNext (cteMDBNode x) = nullPointer; src \<noteq> 0\<rbrakk> \<Longrightarrow> dest \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. \<And>s cte x. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; is_derived' (ctes_of s) src cap (cteCap cte); ctes_of s src = Some cte; ctes_of s dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = nullPointer; mdbNext (cteMDBNode x) = nullPointer; src \<noteq> 0\<rbrakk> \<Longrightarrow> dest \<noteq> 0
 2. \<And>s cte x. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; is_derived' (ctes_of s) src cap (cteCap cte); ctes_of s src = Some cte; ctes_of s dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = nullPointer; mdbNext (cteMDBNode x) = nullPointer; src \<noteq> 0; dest \<noteq> 0\<rbrakk> \<Longrightarrow> no_0 ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) x)) \<and> mdb_chain_0 (modify_map (modify_map (modify_map ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) x)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode cte)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte x. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; is_derived' (ctes_of s) src cap (cteCap cte); ctes_of s src = Some cte; ctes_of s dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = nullPointer; mdbNext (cteMDBNode x) = nullPointer; src \<noteq> 0; dest \<noteq> 0\<rbrakk> \<Longrightarrow> no_0 ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) x)) \<and> mdb_chain_0 (modify_map (modify_map (modify_map ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) x)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode cte)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (2 subgoals):
 1. \<And>s cte x. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; is_derived' (ctes_of s) src cap (cteCap cte); ctes_of s src = Some cte; ctes_of s dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = nullPointer; mdbNext (cteMDBNode x) = nullPointer; src \<noteq> 0; dest \<noteq> 0\<rbrakk> \<Longrightarrow> no_0 ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) x))
 2. \<And>s cte x. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; is_derived' (ctes_of s) src cap (cteCap cte); ctes_of s src = Some cte; ctes_of s dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = nullPointer; mdbNext (cteMDBNode x) = nullPointer; src \<noteq> 0; dest \<noteq> 0\<rbrakk> \<Longrightarrow> mdb_chain_0 (modify_map (modify_map (modify_map ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) x)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode cte)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte x. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; is_derived' (ctes_of s) src cap (cteCap cte); ctes_of s src = Some cte; ctes_of s dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = nullPointer; mdbNext (cteMDBNode x) = nullPointer; src \<noteq> 0; dest \<noteq> 0\<rbrakk> \<Longrightarrow> mdb_chain_0 (modify_map (modify_map (modify_map ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) x)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode cte)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte x x1 x2. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; is_derived' (ctes_of s) src cap (cteCap cte); ctes_of s src = Some cte; ctes_of s dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = nullPointer; mdbNext (cteMDBNode x) = nullPointer; src \<noteq> 0; dest \<noteq> 0; cte = CTE x1 x2\<rbrakk> \<Longrightarrow> mdb_chain_0 (modify_map (modify_map (modify_map ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) x)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode cte)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte x s_cap s_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; is_derived' (ctes_of s) src cap (cteCap cte); ctes_of s src = Some cte; ctes_of s dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = nullPointer; mdbNext (cteMDBNode x) = nullPointer; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node\<rbrakk> \<Longrightarrow> mdb_chain_0 (modify_map (modify_map (modify_map ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) x)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode cte)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte x s_cap s_node x1 x2. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; is_derived' (ctes_of s) src cap (cteCap cte); ctes_of s src = Some cte; ctes_of s dest = Some x; cteCap x = capability.NullCap; mdbPrev (cteMDBNode x) = nullPointer; mdbNext (cteMDBNode x) = nullPointer; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; x = CTE x1 x2\<rbrakk> \<Longrightarrow> mdb_chain_0 (modify_map (modify_map (modify_map ((ctes_of s)(dest \<mapsto> cteCap_update (\<lambda>_. cap) x)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap cte) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode cte)))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext (cteMDBNode cte)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte x s_cap s_node x1 x2. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap x2); x1 = capability.NullCap; mdbPrev x2 = 0; mdbNext x2 = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; x = CTE capability.NullCap x2\<rbrakk> \<Longrightarrow> mdb_chain_0 (modify_map (modify_map (modify_map ((ctes_of s)(dest \<mapsto> CTE cap x2)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' s_cap cap) (mdbRevocable_update (\<lambda>_. revokable' s_cap cap) (mdbPrev_update (\<lambda>_. src) s_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext s_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (2 subgoals):
 1. \<And>s cte x s_cap s_node x1 x2. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap x2); x1 = capability.NullCap; mdbPrev x2 = 0; mdbNext x2 = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; x = CTE capability.NullCap x2; mdb_insert (ctes_of s) src s_cap s_node dest capability.NullCap (?node119 s cte x s_cap s_node x1 x2)\<rbrakk> \<Longrightarrow> mdb_chain_0 (modify_map (modify_map (modify_map ((ctes_of s)(dest \<mapsto> CTE cap x2)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' s_cap cap) (mdbRevocable_update (\<lambda>_. revokable' s_cap cap) (mdbPrev_update (\<lambda>_. src) s_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext s_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))))
 2. \<And>s cte x s_cap s_node x1 x2. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap x2); x1 = capability.NullCap; mdbPrev x2 = 0; mdbNext x2 = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; x = CTE capability.NullCap x2\<rbrakk> \<Longrightarrow> mdb_insert (ctes_of s) src s_cap s_node dest capability.NullCap (?node119 s cte x s_cap s_node x1 x2) proof (prove)
goal (2 subgoals):
 1. \<And>s cte x s_cap s_node x1 x2. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap x2); x1 = capability.NullCap; mdbPrev x2 = 0; mdbNext x2 = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; x = CTE capability.NullCap x2; mdb_chain_0 (modify_map (modify_map (modify_map (ctes_of s) dest (cteCap_update (\<lambda>_. ?c'120 s cte x s_cap s_node x1 x2))) dest (cteMDBNode_update (\<lambda>m. mdbFirstBadged_update (\<lambda>a. revokable' s_cap (?c'120 s cte x s_cap s_node x1 x2)) (mdbRevocable_update (\<lambda>a. revokable' s_cap (?c'120 s cte x s_cap s_node x1 x2)) (mdbPrev_update (\<lambda>a. src) s_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>a. dest))))\<rbrakk> \<Longrightarrow> mdb_chain_0 (modify_map (modify_map (modify_map ((ctes_of s)(dest \<mapsto> CTE cap x2)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' s_cap cap) (mdbRevocable_update (\<lambda>_. revokable' s_cap cap) (mdbPrev_update (\<lambda>_. src) s_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext s_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))))
 2. \<And>s cte x s_cap s_node x1 x2. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap x2); x1 = capability.NullCap; mdbPrev x2 = 0; mdbNext x2 = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; x = CTE capability.NullCap x2\<rbrakk> \<Longrightarrow> mdb_insert (ctes_of s) src s_cap s_node dest capability.NullCap (?node119 s cte x s_cap s_node x1 x2) proof (prove)
goal (2 subgoals):
 1. \<And>s cte x s_cap s_node x1 x2. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap x2); x1 = capability.NullCap; mdbPrev x2 = 0; mdbNext x2 = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; x = CTE capability.NullCap x2; mdb_chain_0 (modify_map (modify_map (modify_map (ctes_of s) dest (cteCap_update (\<lambda>_. ?c'120 s cte x s_cap s_node x1 x2))) dest (cteMDBNode_update (\<lambda>m. mdbFirstBadged_update (\<lambda>a. revokable' s_cap (?c'120 s cte x s_cap s_node x1 x2)) (mdbRevocable_update (\<lambda>a. revokable' s_cap (?c'120 s cte x s_cap s_node x1 x2)) (mdbPrev_update (\<lambda>a. src) s_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>a. dest))))\<rbrakk> \<Longrightarrow> mdb_chain_0 (modify_map (modify_map ((ctes_of s)(dest \<mapsto> CTE cap x2)) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' s_cap cap) (mdbRevocable_update (\<lambda>_. revokable' s_cap cap) (mdbPrev_update (\<lambda>_. src) s_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest))))
 2. \<And>s cte x s_cap s_node x1 x2. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap x2); x1 = capability.NullCap; mdbPrev x2 = 0; mdbNext x2 = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; x = CTE capability.NullCap x2\<rbrakk> \<Longrightarrow> mdb_insert (ctes_of s) src s_cap s_node dest capability.NullCap (?node119 s cte x s_cap s_node x1 x2) proof (prove)
goal (1 subgoal):
 1. \<And>s cte x s_cap s_node x1 x2. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap x2); x1 = capability.NullCap; mdbPrev x2 = 0; mdbNext x2 = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; x = CTE capability.NullCap x2\<rbrakk> \<Longrightarrow> mdb_insert (ctes_of s) src s_cap s_node dest capability.NullCap (?node119 s cte x s_cap s_node x1 x2) proof (prove)
goal (1 subgoal):
 1. \<And>s s_cap s_node x2. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap x2); mdbPrev x2 = 0; mdbNext x2 = 0; src \<noteq> 0; dest \<noteq> 0\<rbrakk> \<Longrightarrow> mdb_insert (ctes_of s) src s_cap s_node dest capability.NullCap (?node119 s (CTE s_cap s_node) (CTE capability.NullCap x2) s_cap s_node capability.NullCap x2) proof (prove)
goal (9 subgoals):
 1. \<And>s s_cap s_node x2. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap x2); mdbPrev x2 = 0; mdbNext x2 = 0; src \<noteq> 0; dest \<noteq> 0\<rbrakk> \<Longrightarrow> valid_mdb_ctes (ctes_of s)
 2. \<And>s s_cap s_node x2. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap x2); mdbPrev x2 = 0; mdbNext x2 = 0; src \<noteq> 0; dest \<noteq> 0\<rbrakk> \<Longrightarrow> ctes_of s src = Some (CTE s_cap s_node)
 3. \<And>s s_cap s_node x2. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap x2); mdbPrev x2 = 0; mdbNext x2 = 0; src \<noteq> 0; dest \<noteq> 0\<rbrakk> \<Longrightarrow> ctes_of s dest = Some (CTE capability.NullCap (?node119 s (CTE s_cap s_node) (CTE capability.NullCap x2) s_cap s_node capability.NullCap x2))
 4. \<And>s s_cap s_node x2. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap x2); mdbPrev x2 = 0; mdbNext x2 = 0; src \<noteq> 0; dest \<noteq> 0\<rbrakk> \<Longrightarrow> capability.NullCap = capability.NullCap
 5. \<And>s s_cap s_node x2. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap x2); mdbPrev x2 = 0; mdbNext x2 = 0; src \<noteq> 0; dest \<noteq> 0\<rbrakk> \<Longrightarrow> mdbPrev (?node119 s (CTE s_cap s_node) (CTE capability.NullCap x2) s_cap s_node capability.NullCap x2) = 0
 6. \<And>s s_cap s_node x2. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap x2); mdbPrev x2 = 0; mdbNext x2 = 0; src \<noteq> 0; dest \<noteq> 0\<rbrakk> \<Longrightarrow> mdbNext (?node119 s (CTE s_cap s_node) (CTE capability.NullCap x2) s_cap s_node capability.NullCap x2) = 0
 7. \<And>s s_cap s_node x2. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap x2); mdbPrev x2 = 0; mdbNext x2 = 0; src \<noteq> 0; dest \<noteq> 0\<rbrakk> \<Longrightarrow> valid_badges (ctes_of s)
 8. \<And>s s_cap s_node x2. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap x2); mdbPrev x2 = 0; mdbNext x2 = 0; src \<noteq> 0; dest \<noteq> 0\<rbrakk> \<Longrightarrow> ut_revocable' (ctes_of s)
 9. \<And>s s_cap s_node x2. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap x2); mdbPrev x2 = 0; mdbNext x2 = 0; src \<noteq> 0; dest \<noteq> 0\<rbrakk> \<Longrightarrow> src \<noteq> dest proof (prove)
goal (3 subgoals):
 1. \<And>s s_cap s_node x2. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap x2); mdbPrev x2 = 0; mdbNext x2 = 0; src \<noteq> 0; dest \<noteq> 0\<rbrakk> \<Longrightarrow> valid_badges (ctes_of s)
 2. \<And>s s_cap s_node x2. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap x2); mdbPrev x2 = 0; mdbNext x2 = 0; src \<noteq> 0; dest \<noteq> 0\<rbrakk> \<Longrightarrow> ut_revocable' (ctes_of s)
 3. \<And>s s_cap s_node x2. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap x2); mdbPrev x2 = 0; mdbNext x2 = 0; src \<noteq> 0; dest \<noteq> 0\<rbrakk> \<Longrightarrow> src \<noteq> dest proof (prove)
goal (2 subgoals):
 1. \<And>s s_cap s_node x2. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap x2); mdbPrev x2 = 0; mdbNext x2 = 0; src \<noteq> 0; dest \<noteq> 0\<rbrakk> \<Longrightarrow> ut_revocable' (ctes_of s)
 2. \<And>s s_cap s_node x2. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap x2); mdbPrev x2 = 0; mdbNext x2 = 0; src \<noteq> 0; dest \<noteq> 0\<rbrakk> \<Longrightarrow> src \<noteq> dest proof (prove)
goal (1 subgoal):
 1. \<And>s s_cap s_node x2. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_aligned' s; pspace_distinct' s; src \<noteq> dest; is_derived' (ctes_of s) src cap s_cap; ctes_of s src = Some (CTE s_cap s_node); ctes_of s dest = Some (CTE capability.NullCap x2); mdbPrev x2 = 0; mdbNext x2 = 0; src \<noteq> 0; dest \<noteq> 0\<rbrakk> \<Longrightarrow> src \<noteq> dest proof (prove)
goal:
No subgoals!