theory CSpace_R

lemma cteInsert_simple_mdb':
  "\<lbrace>valid_mdb' and pspace_aligned' and pspace_distinct' and (\<lambda>s. src \<noteq> dest) and K (capAligned cap) and
    (\<lambda>s. safe_parent_for' (ctes_of s) src cap) and K (is_simple_cap' cap) \<rbrace>
  cteInsert cap src dest
  \<lbrace>\<lambda>_. valid_mdb'\<rbrace>" unfolding cteInsert_def valid_mdb'_def apply simp apply (rule hoare_name_pre_state) apply (rule hoare_pre) apply (wp updateCap_ctes_of_wp getCTE_wp' setUntypedCapAsFull_ctes
     mdb_inv_preserve_updateCap mdb_inv_preserve_modify_map | clarsimp)+ apply (clarsimp simp: cte_wp_at_ctes_of) apply (rule conjI) apply (clarsimp simp: valid_mdb_ctes_def) apply (case_tac cte) apply (rename_tac src_cap src_node) apply (case_tac ctea) apply (rename_tac dest_cap dest_node) apply clarsimp apply (subst modify_map_eq) apply simp+ apply (clarsimp simp:maskedAsFull_def is_simple_cap'_def) apply (subgoal_tac "mdb_insert_simple'
    (ctes_of sa) src src_cap src_node dest NullCap dest_node cap") prefer 2 apply (intro mdb_insert_simple'.intro
                mdb_insert_simple.intro mdb_insert_simple_axioms.intro
                mdb_ptr.intro mdb_insert.intro vmdb.intro
                mdb_ptr_axioms.intro mdb_insert_axioms.intro) apply (simp add:modify_map_def valid_mdb_ctes_maskedAsFull)+ apply (clarsimp simp:nullPointer_def)+ apply ((clarsimp simp:valid_mdb_ctes_def)+) apply (drule mdb_insert_simple'.mdb) apply (clarsimp simp:valid_mdb_ctes_def) 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 K (capAligned cap) and (\<lambda>s. safe_parent_for' (ctes_of s) src cap) and K (is_simple_cap' cap)\<rbrace> cteInsert cap src dest \<lbrace>\<lambda>_. valid_mdb'\<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 K (capAligned cap) and (\<lambda>s. safe_parent_for' (ctes_of s) src cap) and K (is_simple_cap' cap)\<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;
updateCap dest cap;
updateMDB dest (const newMDB);
updateMDB src (mdbNext_update (\<lambda>_. dest));
updateMDB (mdbNext newMDB) (mdbPrev_update (\<lambda>_. dest))
od \<lbrace>\<lambda>_ s. valid_mdb_ctes (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>y. capAligned cap) and (\<lambda>s. safe_parent_for' (ctes_of s) src cap) and (\<lambda>y. is_simple_cap' cap)\<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 <- updateCap dest cap;
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. valid_mdb_ctes (ctes_of s)\<rbrace> 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>y. capAligned cap) and (\<lambda>s. safe_parent_for' (ctes_of s) src cap) and (\<lambda>y. is_simple_cap' cap)) s \<Longrightarrow> \<lbrace>(=) 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 <- updateCap dest cap;
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. valid_mdb_ctes (ctes_of s)\<rbrace> proof (prove)
goal (2 subgoals):
 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>y. capAligned cap) and (\<lambda>s. safe_parent_for' (ctes_of s) src cap) and (\<lambda>y. is_simple_cap' cap)) s \<Longrightarrow> \<lbrace>?Q2 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 <- updateCap dest cap;
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. valid_mdb_ctes (ctes_of s)\<rbrace>
 2. \<And>s sa. \<lbrakk>((\<lambda>s. valid_mdb_ctes (ctes_of s)) and pspace_aligned' and pspace_distinct' and (\<lambda>s. src \<noteq> dest) and (\<lambda>y. capAligned cap) and (\<lambda>s. safe_parent_for' (ctes_of s) src cap) and (\<lambda>y. is_simple_cap' cap)) s; s = sa\<rbrakk> \<Longrightarrow> ?Q2 s sa proof (prove)
goal (1 subgoal):
 1. \<And>sa cte ctea. \<lbrakk>valid_mdb_ctes (ctes_of sa); pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; safe_parent_for' (ctes_of sa) src cap; is_simple_cap' cap; cte_wp_at' ((=) cte) src sa; cte_wp_at' ((=) ctea) dest sa; cteCap ctea = capability.NullCap; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>c. c = cte) src sa \<and> no_0 (ctes_of sa) \<and> valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (modify_map (ctes_of sa) src (cteCap_update (\<lambda>_. maskedAsFull (cteCap cte) cap))) dest (cteCap_update (\<lambda>_. cap))) 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>sa cte ctea. \<lbrakk>valid_mdb_ctes (ctes_of sa); pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; safe_parent_for' (ctes_of sa) src cap; is_simple_cap' cap; ctes_of sa src = Some cte; ctes_of sa dest = Some ctea; cteCap ctea = capability.NullCap; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer\<rbrakk> \<Longrightarrow> no_0 (ctes_of sa) \<and> valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (modify_map (ctes_of sa) src (cteCap_update (\<lambda>_. maskedAsFull (cteCap cte) cap))) dest (cteCap_update (\<lambda>_. cap))) 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>sa cte ctea. \<lbrakk>valid_mdb_ctes (ctes_of sa); pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; safe_parent_for' (ctes_of sa) src cap; is_simple_cap' cap; ctes_of sa src = Some cte; ctes_of sa dest = Some ctea; cteCap ctea = capability.NullCap; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer\<rbrakk> \<Longrightarrow> no_0 (ctes_of sa)
 2. \<And>sa cte ctea. \<lbrakk>valid_mdb_ctes (ctes_of sa); pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; safe_parent_for' (ctes_of sa) src cap; is_simple_cap' cap; ctes_of sa src = Some cte; ctes_of sa dest = Some ctea; cteCap ctea = capability.NullCap; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer\<rbrakk> \<Longrightarrow> valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (modify_map (ctes_of sa) src (cteCap_update (\<lambda>_. maskedAsFull (cteCap cte) cap))) dest (cteCap_update (\<lambda>_. cap))) 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>sa cte ctea. \<lbrakk>valid_mdb_ctes (ctes_of sa); pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; safe_parent_for' (ctes_of sa) src cap; is_simple_cap' cap; ctes_of sa src = Some cte; ctes_of sa dest = Some ctea; cteCap ctea = capability.NullCap; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer\<rbrakk> \<Longrightarrow> valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (modify_map (ctes_of sa) src (cteCap_update (\<lambda>_. maskedAsFull (cteCap cte) cap))) dest (cteCap_update (\<lambda>_. cap))) 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>sa cte ctea x1 x2. \<lbrakk>valid_mdb_ctes (ctes_of sa); pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; safe_parent_for' (ctes_of sa) src cap; is_simple_cap' cap; ctes_of sa src = Some cte; ctes_of sa dest = Some ctea; cteCap ctea = capability.NullCap; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer; cte = CTE x1 x2\<rbrakk> \<Longrightarrow> valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (modify_map (ctes_of sa) src (cteCap_update (\<lambda>_. maskedAsFull (cteCap cte) cap))) dest (cteCap_update (\<lambda>_. cap))) 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>sa cte ctea src_cap src_node. \<lbrakk>valid_mdb_ctes (ctes_of sa); pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; safe_parent_for' (ctes_of sa) src cap; is_simple_cap' cap; ctes_of sa src = Some cte; ctes_of sa dest = Some ctea; cteCap ctea = capability.NullCap; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer; cte = CTE src_cap src_node\<rbrakk> \<Longrightarrow> valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (modify_map (ctes_of sa) src (cteCap_update (\<lambda>_. maskedAsFull (cteCap cte) cap))) dest (cteCap_update (\<lambda>_. cap))) 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>sa cte ctea src_cap src_node x1 x2. \<lbrakk>valid_mdb_ctes (ctes_of sa); pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; safe_parent_for' (ctes_of sa) src cap; is_simple_cap' cap; ctes_of sa src = Some cte; ctes_of sa dest = Some ctea; cteCap ctea = capability.NullCap; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer; cte = CTE src_cap src_node; ctea = CTE x1 x2\<rbrakk> \<Longrightarrow> valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (modify_map (ctes_of sa) src (cteCap_update (\<lambda>_. maskedAsFull (cteCap cte) cap))) dest (cteCap_update (\<lambda>_. cap))) 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>sa cte ctea src_cap src_node dest_cap dest_node. \<lbrakk>valid_mdb_ctes (ctes_of sa); pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; safe_parent_for' (ctes_of sa) src cap; is_simple_cap' cap; ctes_of sa src = Some cte; ctes_of sa dest = Some ctea; cteCap ctea = capability.NullCap; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer; cte = CTE src_cap src_node; ctea = CTE dest_cap dest_node\<rbrakk> \<Longrightarrow> valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (modify_map (ctes_of sa) src (cteCap_update (\<lambda>_. maskedAsFull (cteCap cte) cap))) dest (cteCap_update (\<lambda>_. cap))) 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>sa src_cap src_node dest_node. \<lbrakk>valid_mdb_ctes (ctes_of sa); pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; safe_parent_for' (ctes_of sa) src cap; is_simple_cap' cap; ctes_of sa src = Some (CTE src_cap src_node); ctes_of sa dest = Some (CTE capability.NullCap dest_node); mdbPrev dest_node = nullPointer; mdbNext dest_node = nullPointer\<rbrakk> \<Longrightarrow> valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (modify_map (ctes_of sa) src (cteCap_update (\<lambda>_. maskedAsFull src_cap cap))) dest (cteCap_update (\<lambda>_. cap))) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' src_cap cap) (mdbRevocable_update (\<lambda>_. revokable' src_cap cap) (mdbPrev_update (\<lambda>_. src) src_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (3 subgoals):
 1. \<And>sa src_cap src_node dest_node. \<lbrakk>valid_mdb_ctes (ctes_of sa); pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; safe_parent_for' (ctes_of sa) src cap; is_simple_cap' cap; ctes_of sa src = Some (CTE src_cap src_node); ctes_of sa dest = Some (CTE capability.NullCap dest_node); mdbPrev dest_node = nullPointer; mdbNext dest_node = nullPointer\<rbrakk> \<Longrightarrow> ctes_of sa src = Some (?srcCTE63 sa src_cap src_node dest_node)
 2. \<And>sa src_cap src_node dest_node. \<lbrakk>valid_mdb_ctes (ctes_of sa); pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; safe_parent_for' (ctes_of sa) src cap; is_simple_cap' cap; ctes_of sa src = Some (CTE src_cap src_node); ctes_of sa dest = Some (CTE capability.NullCap dest_node); mdbPrev dest_node = nullPointer; mdbNext dest_node = nullPointer\<rbrakk> \<Longrightarrow> maskedAsFull src_cap cap = cteCap (?srcCTE63 sa src_cap src_node dest_node)
 3. \<And>sa src_cap src_node dest_node. \<lbrakk>valid_mdb_ctes (ctes_of sa); pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; safe_parent_for' (ctes_of sa) src cap; is_simple_cap' cap; ctes_of sa src = Some (CTE src_cap src_node); ctes_of sa dest = Some (CTE capability.NullCap dest_node); mdbPrev dest_node = nullPointer; mdbNext dest_node = nullPointer\<rbrakk> \<Longrightarrow> valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (ctes_of sa) dest (cteCap_update (\<lambda>_. cap))) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' src_cap cap) (mdbRevocable_update (\<lambda>_. revokable' src_cap cap) (mdbPrev_update (\<lambda>_. src) src_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (2 subgoals):
 1. \<And>sa src_cap src_node dest_node. \<lbrakk>valid_mdb_ctes (ctes_of sa); pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; safe_parent_for' (ctes_of sa) src cap; is_simple_cap' cap; ctes_of sa src = Some (CTE src_cap src_node); ctes_of sa dest = Some (CTE capability.NullCap dest_node); mdbPrev dest_node = nullPointer; mdbNext dest_node = nullPointer\<rbrakk> \<Longrightarrow> maskedAsFull src_cap cap = src_cap
 2. \<And>sa src_cap src_node dest_node. \<lbrakk>valid_mdb_ctes (ctes_of sa); pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; safe_parent_for' (ctes_of sa) src cap; is_simple_cap' cap; ctes_of sa src = Some (CTE src_cap src_node); ctes_of sa dest = Some (CTE capability.NullCap dest_node); mdbPrev dest_node = nullPointer; mdbNext dest_node = nullPointer\<rbrakk> \<Longrightarrow> valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (ctes_of sa) dest (cteCap_update (\<lambda>_. cap))) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' src_cap cap) (mdbRevocable_update (\<lambda>_. revokable' src_cap cap) (mdbPrev_update (\<lambda>_. src) src_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (1 subgoal):
 1. \<And>sa src_cap src_node dest_node. \<lbrakk>valid_mdb_ctes (ctes_of sa); pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; safe_parent_for' (ctes_of sa) src cap; is_simple_cap' cap; ctes_of sa src = Some (CTE src_cap src_node); ctes_of sa dest = Some (CTE capability.NullCap dest_node); mdbPrev dest_node = nullPointer; mdbNext dest_node = nullPointer\<rbrakk> \<Longrightarrow> valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (ctes_of sa) dest (cteCap_update (\<lambda>_. cap))) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' src_cap cap) (mdbRevocable_update (\<lambda>_. revokable' src_cap cap) (mdbPrev_update (\<lambda>_. src) src_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (2 subgoals):
 1. \<And>sa src_cap src_node dest_node. \<lbrakk>valid_mdb_ctes (ctes_of sa); pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; safe_parent_for' (ctes_of sa) src cap; is_simple_cap' cap; ctes_of sa src = Some (CTE src_cap src_node); ctes_of sa dest = Some (CTE capability.NullCap dest_node); mdbPrev dest_node = nullPointer; mdbNext dest_node = nullPointer; mdb_insert_simple' (ctes_of sa) src src_cap src_node dest capability.NullCap dest_node cap\<rbrakk> \<Longrightarrow> valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (ctes_of sa) dest (cteCap_update (\<lambda>_. cap))) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' src_cap cap) (mdbRevocable_update (\<lambda>_. revokable' src_cap cap) (mdbPrev_update (\<lambda>_. src) src_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))))
 2. \<And>sa src_cap src_node dest_node. \<lbrakk>valid_mdb_ctes (ctes_of sa); pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; safe_parent_for' (ctes_of sa) src cap; is_simple_cap' cap; ctes_of sa src = Some (CTE src_cap src_node); ctes_of sa dest = Some (CTE capability.NullCap dest_node); mdbPrev dest_node = nullPointer; mdbNext dest_node = nullPointer\<rbrakk> \<Longrightarrow> mdb_insert_simple' (ctes_of sa) src src_cap src_node dest capability.NullCap dest_node cap proof (prove)
goal (2 subgoals):
 1. \<And>sa src_cap src_node dest_node. \<lbrakk>valid_mdb_ctes (ctes_of sa); pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; safe_parent_for' (ctes_of sa) src cap; is_simple_cap' cap; ctes_of sa src = Some (CTE src_cap src_node); ctes_of sa dest = Some (CTE capability.NullCap dest_node); mdbPrev dest_node = nullPointer; mdbNext dest_node = nullPointer\<rbrakk> \<Longrightarrow> mdb_insert_simple' (ctes_of sa) src src_cap src_node dest capability.NullCap dest_node cap
 2. \<And>sa src_cap src_node dest_node. \<lbrakk>valid_mdb_ctes (ctes_of sa); pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; safe_parent_for' (ctes_of sa) src cap; is_simple_cap' cap; ctes_of sa src = Some (CTE src_cap src_node); ctes_of sa dest = Some (CTE capability.NullCap dest_node); mdbPrev dest_node = nullPointer; mdbNext dest_node = nullPointer; mdb_insert_simple' (ctes_of sa) src src_cap src_node dest capability.NullCap dest_node cap\<rbrakk> \<Longrightarrow> valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (ctes_of sa) dest (cteCap_update (\<lambda>_. cap))) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' src_cap cap) (mdbRevocable_update (\<lambda>_. revokable' src_cap cap) (mdbPrev_update (\<lambda>_. src) src_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (13 subgoals):
 1. \<And>sa src_cap src_node dest_node. \<lbrakk>valid_mdb_ctes (ctes_of sa); pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; safe_parent_for' (ctes_of sa) src cap; is_simple_cap' cap; ctes_of sa src = Some (CTE src_cap src_node); ctes_of sa dest = Some (CTE capability.NullCap dest_node); mdbPrev dest_node = nullPointer; mdbNext dest_node = nullPointer\<rbrakk> \<Longrightarrow> valid_mdb_ctes (ctes_of sa)
 2. \<And>sa src_cap src_node dest_node. \<lbrakk>valid_mdb_ctes (ctes_of sa); pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; safe_parent_for' (ctes_of sa) src cap; is_simple_cap' cap; ctes_of sa src = Some (CTE src_cap src_node); ctes_of sa dest = Some (CTE capability.NullCap dest_node); mdbPrev dest_node = nullPointer; mdbNext dest_node = nullPointer\<rbrakk> \<Longrightarrow> ctes_of sa src = Some (CTE src_cap src_node)
 3. \<And>sa src_cap src_node dest_node. \<lbrakk>valid_mdb_ctes (ctes_of sa); pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; safe_parent_for' (ctes_of sa) src cap; is_simple_cap' cap; ctes_of sa src = Some (CTE src_cap src_node); ctes_of sa dest = Some (CTE capability.NullCap dest_node); mdbPrev dest_node = nullPointer; mdbNext dest_node = nullPointer\<rbrakk> \<Longrightarrow> valid_mdb_ctes (ctes_of sa)
 4. \<And>sa src_cap src_node dest_node. \<lbrakk>valid_mdb_ctes (ctes_of sa); pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; safe_parent_for' (ctes_of sa) src cap; is_simple_cap' cap; ctes_of sa src = Some (CTE src_cap src_node); ctes_of sa dest = Some (CTE capability.NullCap dest_node); mdbPrev dest_node = nullPointer; mdbNext dest_node = nullPointer\<rbrakk> \<Longrightarrow> ctes_of sa dest = Some (CTE capability.NullCap dest_node)
 5. \<And>sa src_cap src_node dest_node. \<lbrakk>valid_mdb_ctes (ctes_of sa); pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; safe_parent_for' (ctes_of sa) src cap; is_simple_cap' cap; ctes_of sa src = Some (CTE src_cap src_node); ctes_of sa dest = Some (CTE capability.NullCap dest_node); mdbPrev dest_node = nullPointer; mdbNext dest_node = nullPointer\<rbrakk> \<Longrightarrow> capability.NullCap = capability.NullCap
 6. \<And>sa src_cap src_node dest_node. \<lbrakk>valid_mdb_ctes (ctes_of sa); pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; safe_parent_for' (ctes_of sa) src cap; is_simple_cap' cap; ctes_of sa src = Some (CTE src_cap src_node); ctes_of sa dest = Some (CTE capability.NullCap dest_node); mdbPrev dest_node = nullPointer; mdbNext dest_node = nullPointer\<rbrakk> \<Longrightarrow> mdbPrev dest_node = 0
 7. \<And>sa src_cap src_node dest_node. \<lbrakk>valid_mdb_ctes (ctes_of sa); pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; safe_parent_for' (ctes_of sa) src cap; is_simple_cap' cap; ctes_of sa src = Some (CTE src_cap src_node); ctes_of sa dest = Some (CTE capability.NullCap dest_node); mdbPrev dest_node = nullPointer; mdbNext dest_node = nullPointer\<rbrakk> \<Longrightarrow> mdbNext dest_node = 0
 8. \<And>sa src_cap src_node dest_node. \<lbrakk>valid_mdb_ctes (ctes_of sa); pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; safe_parent_for' (ctes_of sa) src cap; is_simple_cap' cap; ctes_of sa src = Some (CTE src_cap src_node); ctes_of sa dest = Some (CTE capability.NullCap dest_node); mdbPrev dest_node = nullPointer; mdbNext dest_node = nullPointer\<rbrakk> \<Longrightarrow> valid_badges (ctes_of sa)
 9. \<And>sa src_cap src_node dest_node. \<lbrakk>valid_mdb_ctes (ctes_of sa); pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; safe_parent_for' (ctes_of sa) src cap; is_simple_cap' cap; ctes_of sa src = Some (CTE src_cap src_node); ctes_of sa dest = Some (CTE capability.NullCap dest_node); mdbPrev dest_node = nullPointer; mdbNext dest_node = nullPointer\<rbrakk> \<Longrightarrow> ut_revocable' (ctes_of sa)
 10. \<And>sa src_cap src_node dest_node. \<lbrakk>valid_mdb_ctes (ctes_of sa); pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; safe_parent_for' (ctes_of sa) src cap; is_simple_cap' cap; ctes_of sa src = Some (CTE src_cap src_node); ctes_of sa dest = Some (CTE capability.NullCap dest_node); mdbPrev dest_node = nullPointer; mdbNext dest_node = nullPointer\<rbrakk> \<Longrightarrow> src \<noteq> dest
A total of 13 subgoals... proof (prove)
goal (8 subgoals):
 1. \<And>sa src_cap src_node dest_node. \<lbrakk>valid_mdb_ctes (ctes_of sa); pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; safe_parent_for' (ctes_of sa) src cap; is_simple_cap' cap; ctes_of sa src = Some (CTE src_cap src_node); ctes_of sa dest = Some (CTE capability.NullCap dest_node); mdbPrev dest_node = nullPointer; mdbNext dest_node = nullPointer\<rbrakk> \<Longrightarrow> nullPointer = 0
 2. \<And>sa src_cap src_node dest_node. \<lbrakk>valid_mdb_ctes (ctes_of sa); pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; safe_parent_for' (ctes_of sa) src cap; is_simple_cap' cap; ctes_of sa src = Some (CTE src_cap src_node); ctes_of sa dest = Some (CTE capability.NullCap dest_node); mdbPrev dest_node = nullPointer; mdbNext dest_node = nullPointer\<rbrakk> \<Longrightarrow> mdbNext dest_node = 0
 3. \<And>sa src_cap src_node dest_node. \<lbrakk>valid_mdb_ctes (ctes_of sa); pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; safe_parent_for' (ctes_of sa) src cap; is_simple_cap' cap; ctes_of sa src = Some (CTE src_cap src_node); ctes_of sa dest = Some (CTE capability.NullCap dest_node); mdbPrev dest_node = nullPointer; mdbNext dest_node = nullPointer\<rbrakk> \<Longrightarrow> valid_badges (ctes_of sa)
 4. \<And>sa src_cap src_node dest_node. \<lbrakk>valid_mdb_ctes (ctes_of sa); pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; safe_parent_for' (ctes_of sa) src cap; is_simple_cap' cap; ctes_of sa src = Some (CTE src_cap src_node); ctes_of sa dest = Some (CTE capability.NullCap dest_node); mdbPrev dest_node = nullPointer; mdbNext dest_node = nullPointer\<rbrakk> \<Longrightarrow> ut_revocable' (ctes_of sa)
 5. \<And>sa src_cap src_node dest_node. \<lbrakk>valid_mdb_ctes (ctes_of sa); pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; safe_parent_for' (ctes_of sa) src cap; is_simple_cap' cap; ctes_of sa src = Some (CTE src_cap src_node); ctes_of sa dest = Some (CTE capability.NullCap dest_node); mdbPrev dest_node = nullPointer; mdbNext dest_node = nullPointer\<rbrakk> \<Longrightarrow> src \<noteq> dest
 6. \<And>sa src_cap src_node dest_node. \<lbrakk>valid_mdb_ctes (ctes_of sa); pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; safe_parent_for' (ctes_of sa) src cap; is_simple_cap' cap; ctes_of sa src = Some (CTE src_cap src_node); ctes_of sa dest = Some (CTE capability.NullCap dest_node); mdbPrev dest_node = nullPointer; mdbNext dest_node = nullPointer\<rbrakk> \<Longrightarrow> safe_parent_for' (ctes_of sa) src cap
 7. \<And>sa src_cap src_node dest_node. \<lbrakk>valid_mdb_ctes (ctes_of sa); pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; safe_parent_for' (ctes_of sa) src cap; is_simple_cap' cap; ctes_of sa src = Some (CTE src_cap src_node); ctes_of sa dest = Some (CTE capability.NullCap dest_node); mdbPrev dest_node = nullPointer; mdbNext dest_node = nullPointer\<rbrakk> \<Longrightarrow> is_simple_cap' cap
 8. \<And>sa src_cap src_node dest_node. \<lbrakk>valid_mdb_ctes (ctes_of sa); pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; safe_parent_for' (ctes_of sa) src cap; is_simple_cap' cap; ctes_of sa src = Some (CTE src_cap src_node); ctes_of sa dest = Some (CTE capability.NullCap dest_node); mdbPrev dest_node = nullPointer; mdbNext dest_node = nullPointer; mdb_insert_simple' (ctes_of sa) src src_cap src_node dest capability.NullCap dest_node cap\<rbrakk> \<Longrightarrow> valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (ctes_of sa) dest (cteCap_update (\<lambda>_. cap))) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' src_cap cap) (mdbRevocable_update (\<lambda>_. revokable' src_cap cap) (mdbPrev_update (\<lambda>_. src) src_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (6 subgoals):
 1. \<And>sa src_cap src_node dest_node. \<lbrakk>valid_mdb_ctes (ctes_of sa); pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; safe_parent_for' (ctes_of sa) src cap; is_simple_cap' cap; ctes_of sa src = Some (CTE src_cap src_node); ctes_of sa dest = Some (CTE capability.NullCap dest_node); mdbPrev dest_node = 0; mdbNext dest_node = 0\<rbrakk> \<Longrightarrow> valid_badges (ctes_of sa)
 2. \<And>sa src_cap src_node dest_node. \<lbrakk>valid_mdb_ctes (ctes_of sa); pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; safe_parent_for' (ctes_of sa) src cap; is_simple_cap' cap; ctes_of sa src = Some (CTE src_cap src_node); ctes_of sa dest = Some (CTE capability.NullCap dest_node); mdbPrev dest_node = nullPointer; mdbNext dest_node = nullPointer\<rbrakk> \<Longrightarrow> ut_revocable' (ctes_of sa)
 3. \<And>sa src_cap src_node dest_node. \<lbrakk>valid_mdb_ctes (ctes_of sa); pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; safe_parent_for' (ctes_of sa) src cap; is_simple_cap' cap; ctes_of sa src = Some (CTE src_cap src_node); ctes_of sa dest = Some (CTE capability.NullCap dest_node); mdbPrev dest_node = nullPointer; mdbNext dest_node = nullPointer\<rbrakk> \<Longrightarrow> src \<noteq> dest
 4. \<And>sa src_cap src_node dest_node. \<lbrakk>valid_mdb_ctes (ctes_of sa); pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; safe_parent_for' (ctes_of sa) src cap; is_simple_cap' cap; ctes_of sa src = Some (CTE src_cap src_node); ctes_of sa dest = Some (CTE capability.NullCap dest_node); mdbPrev dest_node = nullPointer; mdbNext dest_node = nullPointer\<rbrakk> \<Longrightarrow> safe_parent_for' (ctes_of sa) src cap
 5. \<And>sa src_cap src_node dest_node. \<lbrakk>valid_mdb_ctes (ctes_of sa); pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; safe_parent_for' (ctes_of sa) src cap; is_simple_cap' cap; ctes_of sa src = Some (CTE src_cap src_node); ctes_of sa dest = Some (CTE capability.NullCap dest_node); mdbPrev dest_node = nullPointer; mdbNext dest_node = nullPointer\<rbrakk> \<Longrightarrow> is_simple_cap' cap
 6. \<And>sa src_cap src_node dest_node. \<lbrakk>valid_mdb_ctes (ctes_of sa); pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; safe_parent_for' (ctes_of sa) src cap; is_simple_cap' cap; ctes_of sa src = Some (CTE src_cap src_node); ctes_of sa dest = Some (CTE capability.NullCap dest_node); mdbPrev dest_node = nullPointer; mdbNext dest_node = nullPointer; mdb_insert_simple' (ctes_of sa) src src_cap src_node dest capability.NullCap dest_node cap\<rbrakk> \<Longrightarrow> valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (ctes_of sa) dest (cteCap_update (\<lambda>_. cap))) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' src_cap cap) (mdbRevocable_update (\<lambda>_. revokable' src_cap cap) (mdbPrev_update (\<lambda>_. src) src_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (1 subgoal):
 1. \<And>sa src_cap src_node dest_node. \<lbrakk>pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; safe_parent_for' (ctes_of sa) src cap; is_simple_cap' cap; ctes_of sa src = Some (CTE src_cap src_node); ctes_of sa dest = Some (CTE capability.NullCap dest_node); mdbPrev dest_node = nullPointer; mdbNext dest_node = nullPointer; mdb_insert_simple' (ctes_of sa) src src_cap src_node dest capability.NullCap dest_node cap; valid_dlist (ctes_of sa); no_0 (ctes_of sa); mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa)\<rbrakk> \<Longrightarrow> valid_dlist (modify_map (modify_map (modify_map (modify_map (ctes_of sa) dest (cteCap_update (\<lambda>_. cap))) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' src_cap cap) (mdbRevocable_update (\<lambda>_. revokable' src_cap cap) (mdbPrev_update (\<lambda>_. src) src_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) \<and> mdb_chain_0 (modify_map (modify_map (modify_map (modify_map (ctes_of sa) dest (cteCap_update (\<lambda>_. cap))) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' src_cap cap) (mdbRevocable_update (\<lambda>_. revokable' src_cap cap) (mdbPrev_update (\<lambda>_. src) src_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) \<and> valid_badges (modify_map (modify_map (modify_map (modify_map (ctes_of sa) dest (cteCap_update (\<lambda>_. cap))) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' src_cap cap) (mdbRevocable_update (\<lambda>_. revokable' src_cap cap) (mdbPrev_update (\<lambda>_. src) src_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) \<and> caps_contained' (modify_map (modify_map (modify_map (modify_map (ctes_of sa) dest (cteCap_update (\<lambda>_. cap))) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' src_cap cap) (mdbRevocable_update (\<lambda>_. revokable' src_cap cap) (mdbPrev_update (\<lambda>_. src) src_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) \<and> mdb_chunked (modify_map (modify_map (modify_map (modify_map (ctes_of sa) dest (cteCap_update (\<lambda>_. cap))) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' src_cap cap) (mdbRevocable_update (\<lambda>_. revokable' src_cap cap) (mdbPrev_update (\<lambda>_. src) src_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) \<and> untyped_mdb' (modify_map (modify_map (modify_map (modify_map (ctes_of sa) dest (cteCap_update (\<lambda>_. cap))) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' src_cap cap) (mdbRevocable_update (\<lambda>_. revokable' src_cap cap) (mdbPrev_update (\<lambda>_. src) src_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) \<and> untyped_inc' (modify_map (modify_map (modify_map (modify_map (ctes_of sa) dest (cteCap_update (\<lambda>_. cap))) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' src_cap cap) (mdbRevocable_update (\<lambda>_. revokable' src_cap cap) (mdbPrev_update (\<lambda>_. src) src_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) \<and> valid_nullcaps (modify_map (modify_map (modify_map (modify_map (ctes_of sa) dest (cteCap_update (\<lambda>_. cap))) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' src_cap cap) (mdbRevocable_update (\<lambda>_. revokable' src_cap cap) (mdbPrev_update (\<lambda>_. src) src_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) \<and> ut_revocable' (modify_map (modify_map (modify_map (modify_map (ctes_of sa) dest (cteCap_update (\<lambda>_. cap))) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' src_cap cap) (mdbRevocable_update (\<lambda>_. revokable' src_cap cap) (mdbPrev_update (\<lambda>_. src) src_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) \<and> class_links (modify_map (modify_map (modify_map (modify_map (ctes_of sa) dest (cteCap_update (\<lambda>_. cap))) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' src_cap cap) (mdbRevocable_update (\<lambda>_. revokable' src_cap cap) (mdbPrev_update (\<lambda>_. src) src_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) \<and> distinct_zombies (modify_map (modify_map (modify_map (modify_map (ctes_of sa) dest (cteCap_update (\<lambda>_. cap))) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' src_cap cap) (mdbRevocable_update (\<lambda>_. revokable' src_cap cap) (mdbPrev_update (\<lambda>_. src) src_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) \<and> irq_control (modify_map (modify_map (modify_map (modify_map (ctes_of sa) dest (cteCap_update (\<lambda>_. cap))) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' src_cap cap) (mdbRevocable_update (\<lambda>_. revokable' src_cap cap) (mdbPrev_update (\<lambda>_. src) src_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) \<and> reply_masters_rvk_fb (modify_map (modify_map (modify_map (modify_map (ctes_of sa) dest (cteCap_update (\<lambda>_. cap))) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' src_cap cap) (mdbRevocable_update (\<lambda>_. revokable' src_cap cap) (mdbPrev_update (\<lambda>_. src) src_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal (1 subgoal):
 1. \<And>sa src_cap src_node dest_node. \<lbrakk>pspace_aligned' sa; pspace_distinct' sa; src \<noteq> dest; capAligned cap; safe_parent_for' (ctes_of sa) src cap; is_simple_cap' cap; ctes_of sa src = Some (CTE src_cap src_node); ctes_of sa dest = Some (CTE capability.NullCap dest_node); mdbPrev dest_node = nullPointer; mdbNext dest_node = nullPointer; valid_dlist (ctes_of sa); no_0 (ctes_of sa); mdb_chain_0 (ctes_of sa); valid_badges (ctes_of sa); caps_contained' (ctes_of sa); mdb_chunked (ctes_of sa); untyped_mdb' (ctes_of sa); untyped_inc' (ctes_of sa); valid_nullcaps (ctes_of sa); ut_revocable' (ctes_of sa); class_links (ctes_of sa); distinct_zombies (ctes_of sa); irq_control (ctes_of sa); reply_masters_rvk_fb (ctes_of sa); valid_mdb_ctes (modify_map (modify_map (modify_map (modify_map (ctes_of sa) dest (cteCap_update (\<lambda>_. cap))) dest (cteMDBNode_update (\<lambda>m. mdbFirstBadged_update (\<lambda>a. revokable' src_cap cap) (mdbRevocable_update (\<lambda>a. revokable' src_cap cap) (mdbPrev_update (\<lambda>a. src) src_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>a. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))))\<rbrakk> \<Longrightarrow> valid_dlist (modify_map (modify_map (modify_map (modify_map (ctes_of sa) dest (cteCap_update (\<lambda>_. cap))) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' src_cap cap) (mdbRevocable_update (\<lambda>_. revokable' src_cap cap) (mdbPrev_update (\<lambda>_. src) src_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) \<and> mdb_chain_0 (modify_map (modify_map (modify_map (modify_map (ctes_of sa) dest (cteCap_update (\<lambda>_. cap))) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' src_cap cap) (mdbRevocable_update (\<lambda>_. revokable' src_cap cap) (mdbPrev_update (\<lambda>_. src) src_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) \<and> valid_badges (modify_map (modify_map (modify_map (modify_map (ctes_of sa) dest (cteCap_update (\<lambda>_. cap))) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' src_cap cap) (mdbRevocable_update (\<lambda>_. revokable' src_cap cap) (mdbPrev_update (\<lambda>_. src) src_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) \<and> caps_contained' (modify_map (modify_map (modify_map (modify_map (ctes_of sa) dest (cteCap_update (\<lambda>_. cap))) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' src_cap cap) (mdbRevocable_update (\<lambda>_. revokable' src_cap cap) (mdbPrev_update (\<lambda>_. src) src_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) \<and> mdb_chunked (modify_map (modify_map (modify_map (modify_map (ctes_of sa) dest (cteCap_update (\<lambda>_. cap))) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' src_cap cap) (mdbRevocable_update (\<lambda>_. revokable' src_cap cap) (mdbPrev_update (\<lambda>_. src) src_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) \<and> untyped_mdb' (modify_map (modify_map (modify_map (modify_map (ctes_of sa) dest (cteCap_update (\<lambda>_. cap))) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' src_cap cap) (mdbRevocable_update (\<lambda>_. revokable' src_cap cap) (mdbPrev_update (\<lambda>_. src) src_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) \<and> untyped_inc' (modify_map (modify_map (modify_map (modify_map (ctes_of sa) dest (cteCap_update (\<lambda>_. cap))) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' src_cap cap) (mdbRevocable_update (\<lambda>_. revokable' src_cap cap) (mdbPrev_update (\<lambda>_. src) src_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) \<and> valid_nullcaps (modify_map (modify_map (modify_map (modify_map (ctes_of sa) dest (cteCap_update (\<lambda>_. cap))) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' src_cap cap) (mdbRevocable_update (\<lambda>_. revokable' src_cap cap) (mdbPrev_update (\<lambda>_. src) src_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) \<and> ut_revocable' (modify_map (modify_map (modify_map (modify_map (ctes_of sa) dest (cteCap_update (\<lambda>_. cap))) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' src_cap cap) (mdbRevocable_update (\<lambda>_. revokable' src_cap cap) (mdbPrev_update (\<lambda>_. src) src_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) \<and> class_links (modify_map (modify_map (modify_map (modify_map (ctes_of sa) dest (cteCap_update (\<lambda>_. cap))) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' src_cap cap) (mdbRevocable_update (\<lambda>_. revokable' src_cap cap) (mdbPrev_update (\<lambda>_. src) src_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) \<and> distinct_zombies (modify_map (modify_map (modify_map (modify_map (ctes_of sa) dest (cteCap_update (\<lambda>_. cap))) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' src_cap cap) (mdbRevocable_update (\<lambda>_. revokable' src_cap cap) (mdbPrev_update (\<lambda>_. src) src_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) \<and> irq_control (modify_map (modify_map (modify_map (modify_map (ctes_of sa) dest (cteCap_update (\<lambda>_. cap))) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' src_cap cap) (mdbRevocable_update (\<lambda>_. revokable' src_cap cap) (mdbPrev_update (\<lambda>_. src) src_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) \<and> reply_masters_rvk_fb (modify_map (modify_map (modify_map (modify_map (ctes_of sa) dest (cteCap_update (\<lambda>_. cap))) dest (cteMDBNode_update (\<lambda>a. mdbFirstBadged_update (\<lambda>_. revokable' src_cap cap) (mdbRevocable_update (\<lambda>_. revokable' src_cap cap) (mdbPrev_update (\<lambda>_. src) src_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) proof (prove)
goal:
No subgoals!