theory CSpace_R

lemma cteInsert_irq_control:
  "\<lbrace>valid_mdb' and pspace_distinct' and pspace_aligned' 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. irq_control (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 setUntypedCapAsFull_irq_control mdb_inv_preserve_fun_upd
    mdb_inv_preserve_modify_map,simp) 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 cteb) apply (rename_tac d_cap d_node) apply (simp add: nullPointer_def) apply (subgoal_tac "mdb_insert_der (ctes_of s) src s_cap s_node dest NullCap d_node cap") prefer 2 apply unfold_locales[1] apply (assumption|rule refl)+ apply (simp add: valid_mdb_ctes_def) apply (simp add: valid_mdb_ctes_def) apply assumption+ apply (drule mdb_insert_der.irq_control_n) apply (clarsimp simp: modify_map_apply irq_control_prev_update fun_upd_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_mdb' and pspace_distinct' and pspace_aligned' 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. irq_control (ctes_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_mdb' and pspace_distinct' and pspace_aligned' 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. irq_control (ctes_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. valid_mdb_ctes (ctes_of s)) and pspace_distinct' and pspace_aligned' 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. irq_control (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> irq_control (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_distinct' and pspace_aligned' 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> irq_control (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_distinct' and pspace_aligned' 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 (5 subgoals):
 1. \<And>srcCTE x. \<lbrace>?B3 srcCTE x ()\<rbrace> assert (mdbPrev (cteMDBNode x) = nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer) \<lbrace>\<lambda>a b. \<forall>x. src \<noteq> dest \<and> ctes_of b dest \<noteq> Some x \<or> src = dest \<and> CTE (maskedAsFull (cteCap srcCTE) cap) (cteMDBNode srcCTE) \<noteq> x \<and> cte_wp_at' ((=) srcCTE) src b \<or> no_0 (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of b a) \<and> cte_wp_at' ((=) srcCTE) src b \<and> irq_control (modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of b a) 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 b\<rbrace>
 2. \<And>srcCTE x. \<lbrace>?B2 srcCTE x\<rbrace> assert (cteCap x = capability.NullCap) \<lbrace>?B3 srcCTE x\<rbrace>
 3. \<And>srcCTE. \<lbrace>?B1 srcCTE\<rbrace> getCTE dest \<lbrace>?B2 srcCTE\<rbrace>
 4. \<lbrace>?Q\<rbrace> getCTE src \<lbrace>?B1\<rbrace>
 5. \<And>s. ((\<lambda>s. valid_mdb_ctes (ctes_of s)) and pspace_distinct' and pspace_aligned' 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_distinct' and pspace_aligned' 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> (cte_wp_at' (\<lambda>_. True) dest s \<longrightarrow> (\<exists>ctea. cte_wp_at' ((=) ctea) dest s \<and> (cteCap ctea = capability.NullCap \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> (\<forall>x. 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 (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of s a) \<and> cte_wp_at' ((=) cte) src s \<and> irq_control (modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) x) else ctes_of s a) 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 cteb. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; src \<noteq> dest; is_derived' (ctes_of s) src cap (cteCap cte); ctes_of s src = Some cte; ctes_of s dest = Some cteb; cteCap cteb = capability.NullCap; mdbPrev (cteMDBNode cteb) = nullPointer; mdbNext (cteMDBNode cteb) = nullPointer\<rbrakk> \<Longrightarrow> no_0 (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) cteb) else ctes_of s a) \<and> irq_control (modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) cteb) else ctes_of s a) 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 cteb. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; src \<noteq> dest; is_derived' (ctes_of s) src cap (cteCap cte); ctes_of s src = Some cte; ctes_of s dest = Some cteb; cteCap cteb = capability.NullCap; mdbPrev (cteMDBNode cteb) = nullPointer; mdbNext (cteMDBNode cteb) = nullPointer; src \<noteq> 0\<rbrakk> \<Longrightarrow> no_0 (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) cteb) else ctes_of s a) \<and> irq_control (modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) cteb) else ctes_of s a) 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 cteb. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; src \<noteq> dest; is_derived' (ctes_of s) src cap (cteCap cte); ctes_of s src = Some cte; ctes_of s dest = Some cteb; cteCap cteb = capability.NullCap; mdbPrev (cteMDBNode cteb) = nullPointer; mdbNext (cteMDBNode cteb) = nullPointer\<rbrakk> \<Longrightarrow> src \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. \<And>s cte cteb. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; src \<noteq> dest; is_derived' (ctes_of s) src cap (cteCap cte); ctes_of s src = Some cte; ctes_of s dest = Some cteb; cteCap cteb = capability.NullCap; mdbPrev (cteMDBNode cteb) = nullPointer; mdbNext (cteMDBNode cteb) = nullPointer\<rbrakk> \<Longrightarrow> src \<noteq> 0
 2. \<And>s cte cteb. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; src \<noteq> dest; is_derived' (ctes_of s) src cap (cteCap cte); ctes_of s src = Some cte; ctes_of s dest = Some cteb; cteCap cteb = capability.NullCap; mdbPrev (cteMDBNode cteb) = nullPointer; mdbNext (cteMDBNode cteb) = nullPointer; src \<noteq> 0\<rbrakk> \<Longrightarrow> no_0 (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) cteb) else ctes_of s a) \<and> irq_control (modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) cteb) else ctes_of s a) 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 cteb. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; src \<noteq> dest; is_derived' (ctes_of s) src cap (cteCap cte); ctes_of s src = Some cte; ctes_of s dest = Some cteb; cteCap cteb = capability.NullCap; mdbPrev (cteMDBNode cteb) = nullPointer; mdbNext (cteMDBNode cteb) = nullPointer; src \<noteq> 0\<rbrakk> \<Longrightarrow> no_0 (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) cteb) else ctes_of s a) \<and> irq_control (modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) cteb) else ctes_of s a) 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 cteb. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; src \<noteq> dest; is_derived' (ctes_of s) src cap (cteCap cte); ctes_of s src = Some cte; ctes_of s dest = Some cteb; cteCap cteb = capability.NullCap; mdbPrev (cteMDBNode cteb) = nullPointer; mdbNext (cteMDBNode cteb) = nullPointer; src \<noteq> 0; dest \<noteq> 0\<rbrakk> \<Longrightarrow> no_0 (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) cteb) else ctes_of s a) \<and> irq_control (modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) cteb) else ctes_of s a) 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 cteb. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; src \<noteq> dest; is_derived' (ctes_of s) src cap (cteCap cte); ctes_of s src = Some cte; ctes_of s dest = Some cteb; cteCap cteb = capability.NullCap; mdbPrev (cteMDBNode cteb) = nullPointer; mdbNext (cteMDBNode cteb) = nullPointer; src \<noteq> 0\<rbrakk> \<Longrightarrow> dest \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. \<And>s cte cteb. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; src \<noteq> dest; is_derived' (ctes_of s) src cap (cteCap cte); ctes_of s src = Some cte; ctes_of s dest = Some cteb; cteCap cteb = capability.NullCap; mdbPrev (cteMDBNode cteb) = nullPointer; mdbNext (cteMDBNode cteb) = nullPointer; src \<noteq> 0\<rbrakk> \<Longrightarrow> dest \<noteq> 0
 2. \<And>s cte cteb. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; src \<noteq> dest; is_derived' (ctes_of s) src cap (cteCap cte); ctes_of s src = Some cte; ctes_of s dest = Some cteb; cteCap cteb = capability.NullCap; mdbPrev (cteMDBNode cteb) = nullPointer; mdbNext (cteMDBNode cteb) = nullPointer; src \<noteq> 0; dest \<noteq> 0\<rbrakk> \<Longrightarrow> no_0 (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) cteb) else ctes_of s a) \<and> irq_control (modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) cteb) else ctes_of s a) 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 cteb. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; src \<noteq> dest; is_derived' (ctes_of s) src cap (cteCap cte); ctes_of s src = Some cte; ctes_of s dest = Some cteb; cteCap cteb = capability.NullCap; mdbPrev (cteMDBNode cteb) = nullPointer; mdbNext (cteMDBNode cteb) = nullPointer; src \<noteq> 0; dest \<noteq> 0\<rbrakk> \<Longrightarrow> no_0 (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) cteb) else ctes_of s a) \<and> irq_control (modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) cteb) else ctes_of s a) 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 cteb. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; src \<noteq> dest; is_derived' (ctes_of s) src cap (cteCap cte); ctes_of s src = Some cte; ctes_of s dest = Some cteb; cteCap cteb = capability.NullCap; mdbPrev (cteMDBNode cteb) = nullPointer; mdbNext (cteMDBNode cteb) = nullPointer; src \<noteq> 0; dest \<noteq> 0\<rbrakk> \<Longrightarrow> no_0 (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) cteb) else ctes_of s a)
 2. \<And>s cte cteb. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; src \<noteq> dest; is_derived' (ctes_of s) src cap (cteCap cte); ctes_of s src = Some cte; ctes_of s dest = Some cteb; cteCap cteb = capability.NullCap; mdbPrev (cteMDBNode cteb) = nullPointer; mdbNext (cteMDBNode cteb) = nullPointer; src \<noteq> 0; dest \<noteq> 0\<rbrakk> \<Longrightarrow> irq_control (modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) cteb) else ctes_of s a) 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 cteb. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; src \<noteq> dest; is_derived' (ctes_of s) src cap (cteCap cte); ctes_of s src = Some cte; ctes_of s dest = Some cteb; cteCap cteb = capability.NullCap; mdbPrev (cteMDBNode cteb) = nullPointer; mdbNext (cteMDBNode cteb) = nullPointer; src \<noteq> 0; dest \<noteq> 0\<rbrakk> \<Longrightarrow> irq_control (modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) cteb) else ctes_of s a) 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 cteb x1 x2. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; src \<noteq> dest; is_derived' (ctes_of s) src cap (cteCap cte); ctes_of s src = Some cte; ctes_of s dest = Some cteb; cteCap cteb = capability.NullCap; mdbPrev (cteMDBNode cteb) = nullPointer; mdbNext (cteMDBNode cteb) = nullPointer; src \<noteq> 0; dest \<noteq> 0; cte = CTE x1 x2\<rbrakk> \<Longrightarrow> irq_control (modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) cteb) else ctes_of s a) 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 cteb s_cap s_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; src \<noteq> dest; is_derived' (ctes_of s) src cap (cteCap cte); ctes_of s src = Some cte; ctes_of s dest = Some cteb; cteCap cteb = capability.NullCap; mdbPrev (cteMDBNode cteb) = nullPointer; mdbNext (cteMDBNode cteb) = nullPointer; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node\<rbrakk> \<Longrightarrow> irq_control (modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) cteb) else ctes_of s a) 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 cteb s_cap s_node x1 x2. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; src \<noteq> dest; is_derived' (ctes_of s) src cap (cteCap cte); ctes_of s src = Some cte; ctes_of s dest = Some cteb; cteCap cteb = capability.NullCap; mdbPrev (cteMDBNode cteb) = nullPointer; mdbNext (cteMDBNode cteb) = nullPointer; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE x1 x2\<rbrakk> \<Longrightarrow> irq_control (modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) cteb) else ctes_of s a) 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 cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' s; src \<noteq> dest; is_derived' (ctes_of s) src cap (cteCap cte); ctes_of s src = Some cte; ctes_of s dest = Some cteb; cteCap cteb = capability.NullCap; mdbPrev (cteMDBNode cteb) = nullPointer; mdbNext (cteMDBNode cteb) = nullPointer; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE d_cap d_node\<rbrakk> \<Longrightarrow> irq_control (modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (cteCap_update (\<lambda>_. cap) cteb) else ctes_of s a) 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 cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' 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 d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node\<rbrakk> \<Longrightarrow> irq_control (modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (CTE cap d_node) else ctes_of s a) 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 cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' 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 d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (ctes_of s) src s_cap s_node dest capability.NullCap d_node cap\<rbrakk> \<Longrightarrow> irq_control (modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (CTE cap d_node) else ctes_of s a) 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 cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' 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 d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node\<rbrakk> \<Longrightarrow> mdb_insert_der (ctes_of s) src s_cap s_node dest capability.NullCap d_node cap proof (prove)
goal (2 subgoals):
 1. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' 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 d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node\<rbrakk> \<Longrightarrow> mdb_insert_der (ctes_of s) src s_cap s_node dest capability.NullCap d_node cap
 2. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' 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 d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (ctes_of s) src s_cap s_node dest capability.NullCap d_node cap\<rbrakk> \<Longrightarrow> irq_control (modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (CTE cap d_node) else ctes_of s a) 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 (11 subgoals):
 1. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' 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 d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node\<rbrakk> \<Longrightarrow> valid_mdb_ctes (ctes_of s)
 2. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' 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 d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node\<rbrakk> \<Longrightarrow> ctes_of s src = Some (CTE s_cap s_node)
 3. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' 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 d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node\<rbrakk> \<Longrightarrow> ctes_of s dest = Some (CTE capability.NullCap d_node)
 4. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' 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 d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node\<rbrakk> \<Longrightarrow> capability.NullCap = capability.NullCap
 5. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' 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 d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node\<rbrakk> \<Longrightarrow> mdbPrev d_node = 0
 6. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' 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 d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node\<rbrakk> \<Longrightarrow> mdbNext d_node = 0
 7. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' 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 d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node\<rbrakk> \<Longrightarrow> valid_badges (ctes_of s)
 8. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' 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 d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node\<rbrakk> \<Longrightarrow> ut_revocable' (ctes_of s)
 9. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' 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 d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node\<rbrakk> \<Longrightarrow> src \<noteq> dest
 10. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' 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 d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node\<rbrakk> \<Longrightarrow> is_derived' (ctes_of s) src cap s_cap
A total of 11 subgoals... proof (prove)
goal (5 subgoals):
 1. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' 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 d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node\<rbrakk> \<Longrightarrow> valid_badges (ctes_of s)
 2. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' 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 d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node\<rbrakk> \<Longrightarrow> ut_revocable' (ctes_of s)
 3. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' 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 d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node\<rbrakk> \<Longrightarrow> src \<noteq> dest
 4. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' 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 d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node\<rbrakk> \<Longrightarrow> is_derived' (ctes_of s) src cap s_cap
 5. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' 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 d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (ctes_of s) src s_cap s_node dest capability.NullCap d_node cap\<rbrakk> \<Longrightarrow> irq_control (modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (CTE cap d_node) else ctes_of s a) 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 (4 subgoals):
 1. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' 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 d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node\<rbrakk> \<Longrightarrow> ut_revocable' (ctes_of s)
 2. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' 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 d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node\<rbrakk> \<Longrightarrow> src \<noteq> dest
 3. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' 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 d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node\<rbrakk> \<Longrightarrow> is_derived' (ctes_of s) src cap s_cap
 4. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' 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 d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (ctes_of s) src s_cap s_node dest capability.NullCap d_node cap\<rbrakk> \<Longrightarrow> irq_control (modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (CTE cap d_node) else ctes_of s a) 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 (3 subgoals):
 1. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' 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 d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node\<rbrakk> \<Longrightarrow> src \<noteq> dest
 2. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' 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 d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node\<rbrakk> \<Longrightarrow> is_derived' (ctes_of s) src cap s_cap
 3. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' 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 d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (ctes_of s) src s_cap s_node dest capability.NullCap d_node cap\<rbrakk> \<Longrightarrow> irq_control (modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (CTE cap d_node) else ctes_of s a) 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 (1 subgoal):
 1. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' 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 d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; mdb_insert_der (ctes_of s) src s_cap s_node dest capability.NullCap d_node cap\<rbrakk> \<Longrightarrow> irq_control (modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (CTE cap d_node) else ctes_of s a) 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 (1 subgoal):
 1. \<And>s cte cteb s_cap s_node d_cap d_node. \<lbrakk>valid_mdb_ctes (ctes_of s); pspace_distinct' s; pspace_aligned' 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 d_node); d_cap = capability.NullCap; mdbPrev d_node = 0; mdbNext d_node = 0; src \<noteq> 0; dest \<noteq> 0; cte = CTE s_cap s_node; cteb = CTE capability.NullCap d_node; irq_control (modify_map (modify_map (modify_map (ctes_of s) dest (cteCap_update (\<lambda>_. cap))) dest (cteMDBNode_update (\<lambda>m. mdbFirstBadged_update (\<lambda>a. revokable' s_cap cap) (mdbRevocable_update (\<lambda>a. revokable' s_cap cap) (mdbPrev_update (\<lambda>a. src) s_node))))) src (cteMDBNode_update (mdbNext_update (\<lambda>a. dest))))\<rbrakk> \<Longrightarrow> irq_control (modify_map (modify_map (modify_map (\<lambda>a. if a = dest then Some (CTE cap d_node) else ctes_of s a) 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:
No subgoals!