theory CSpace_C

lemma cteMove_ccorres:
  "ccorres dc xfdc
       (valid_mdb' and pspace_aligned' )
       (UNIV \<inter> {s. destSlot_' s = Ptr dest} \<inter>
               {s. srcSlot_' s = Ptr src} \<inter>
               {s. ccap_relation cap (newCap_' s)}) []
       (cteMove cap src dest)
       (Call cteMove_'proc)" apply (cinit (no_ignore_call) lift: destSlot_' srcSlot_' newCap_' simp del: return_bind) apply (ctac pre: ccorres_pre_getCTE ccorres_assert iffD2 [OF ccorres_seq_skip]) apply (ctac+, csymbr+)+ apply (erule_tac t = ret__unsigned in ssubst) apply (ctac add: updateMDB_mdbPrev_set_mdbNext) apply csymbr apply csymbr apply (erule_tac t = ret__unsigned in ssubst) apply (rule updateMDB_mdbNext_set_mdbPrev) apply simp apply simp apply (wp, vcg)+ apply (rule conjI) apply (clarsimp simp: cte_wp_at_ctes_of) apply (intro conjI, simp+) apply (erule (2) is_aligned_3_prev) apply (erule (2) is_aligned_3_next) apply (clarsimp split del: if_split) apply (simp add: ccap_relation_NullCap_iff) apply (clarsimp simp: cmdbnode_relation_def mdb_node_to_H_def nullMDBNode_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (valid_mdb' and pspace_aligned') (UNIV \<inter> \<lbrace>\<acute>destSlot = cte_Ptr dest\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = cte_Ptr src\<rbrace> \<inter> \<lbrace>ccap_relation cap \<acute>newCap\<rbrace>) [] (cteMove cap src dest) (Call cteMove_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>newCap srcSlot destSlot. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1686 newCap srcSlot destSlot) (?Q'1686 newCap srcSlot destSlot) [SKIP] (do oldCTE <- getCTE dest;
y <- assert (cteCap oldCTE = capability.NullCap);
y <- assert (mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer);
cte <- getCTE src;
mdb <- return (cteMDBNode cte);
y <- updateCap dest cap;
y <- updateCap src capability.NullCap;
y <- updateMDB dest (const mdb);
y <- updateMDB src (const nullMDBNode);
y <- updateMDB (mdbPrev mdb) (mdbNext_update (\<lambda>_. dest));
updateMDB (mdbNext mdb) (mdbPrev_update (\<lambda>_. dest))
od) (Guard C_Guard {s. s \<Turnstile>\<^sub>c srcSlot} (\<acute>mdb :== h_val (hrs_mem \<acute>t_hrs) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])));;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c destSlot} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(destSlot\<rightarrow>[''cap_C''])) newCap)));;
(\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c srcSlot} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(srcSlot\<rightarrow>[''cap_C''])) \<acute>ret__struct_cap_C)));;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c destSlot} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(destSlot\<rightarrow>[''cteMDBNode_C''])) \<acute>mdb)));;
(\<acute>ret__struct_mdb_node_C :== CALL mdb_node_new_'proc(0,SCAST(32 signed \<rightarrow> 32) false,SCAST(32 signed \<rightarrow> 32) false,0);;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c srcSlot} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])) \<acute>ret__struct_mdb_node_C)));;
(\<acute>ret__unsigned :== CALL mdb_node_get_mdbPrev_'proc(\<acute>mdb);;
(\<acute>prev_ptr :== \<acute>ret__unsigned;;
(IF \<acute>prev_ptr \<noteq> 0 THEN
  Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr (prev_ptr_' s)} (CALL mdb_node_ptr_set_mdbNext_'proc(mdb_Ptr &(cte_Ptr \<acute>prev_ptr\<rightarrow>[''cteMDBNode_C'']),ptr_val destSlot))
FI;;
(\<acute>ret__unsigned :== CALL mdb_node_get_mdbNext_'proc(\<acute>mdb);;
(\<acute>next_ptr :== \<acute>ret__unsigned;;
IF \<acute>next_ptr \<noteq> 0 THEN
  Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr (next_ptr_' s)} (CALL mdb_node_ptr_set_mdbPrev_'proc(mdb_Ptr &(cte_Ptr \<acute>next_ptr\<rightarrow>[''cteMDBNode_C'']),ptr_val destSlot))
FI))))))))))))
 2. \<And>newCap srcSlot destSlot s s'. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q1686 newCap srcSlot destSlot s \<and> s' \<in> ?Q'1686 newCap srcSlot destSlot proof (prove)
goal (4 subgoals):
 1. \<And>newCap srcSlot destSlot oldCTE cte rv mdb. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1699 newCap srcSlot destSlot oldCTE cte rv) (?Q'1699 newCap srcSlot destSlot oldCTE cte rv mdb) [SKIP] (do y <- updateCap dest cap;
y <- updateCap src capability.NullCap;
y <- updateMDB dest (const rv);
y <- updateMDB src (const nullMDBNode);
y <- updateMDB (mdbPrev rv) (mdbNext_update (\<lambda>_. dest));
updateMDB (mdbNext rv) (mdbPrev_update (\<lambda>_. dest))
od) (Guard C_Guard {s. s \<Turnstile>\<^sub>c destSlot} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(destSlot\<rightarrow>[''cap_C''])) newCap)));;
(\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c srcSlot} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(srcSlot\<rightarrow>[''cap_C''])) \<acute>ret__struct_cap_C)));;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c destSlot} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(destSlot\<rightarrow>[''cteMDBNode_C''])) mdb)));;
(\<acute>ret__struct_mdb_node_C :== CALL mdb_node_new_'proc(0,SCAST(32 signed \<rightarrow> 32) false,SCAST(32 signed \<rightarrow> 32) false,0);;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c srcSlot} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])) \<acute>ret__struct_mdb_node_C)));;
(\<acute>ret__unsigned :== CALL mdb_node_get_mdbPrev_'proc(mdb);;
(\<acute>prev_ptr :== \<acute>ret__unsigned;;
(IF \<acute>prev_ptr \<noteq> 0 THEN
  Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr (prev_ptr_' s)} (CALL mdb_node_ptr_set_mdbNext_'proc(mdb_Ptr &(cte_Ptr \<acute>prev_ptr\<rightarrow>[''cteMDBNode_C'']),ptr_val destSlot))
FI;;
(\<acute>ret__unsigned :== CALL mdb_node_get_mdbNext_'proc(mdb);;
(\<acute>next_ptr :== \<acute>ret__unsigned;;
IF \<acute>next_ptr \<noteq> 0 THEN
  Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr (next_ptr_' s)} (CALL mdb_node_ptr_set_mdbPrev_'proc(mdb_Ptr &(cte_Ptr \<acute>next_ptr\<rightarrow>[''cteMDBNode_C'']),ptr_val destSlot))
FI)))))))))))
 2. \<And>newCap srcSlot destSlot oldCTE cte. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer\<rbrakk> \<Longrightarrow> \<lbrace>?R1699 newCap srcSlot destSlot oldCTE cte\<rbrace> return (cteMDBNode cte) \<lbrace>?Q1699 newCap srcSlot destSlot oldCTE cte\<rbrace>
 3. \<And>newCap srcSlot destSlot oldCTE cte. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'1699 newCap srcSlot destSlot oldCTE cte) \<acute>mdb :== h_val (hrs_mem \<acute>t_hrs) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])) {s. \<forall>rv. cmdbnode_relation rv (mdb_' s) \<longrightarrow> s \<in> ?Q'1699 newCap srcSlot destSlot oldCTE cte rv (mdb_' s)}
 4. \<And>newCap srcSlot destSlot s s'. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s dest = Some cte \<longrightarrow> (\<forall>ctea. ctes_of s src = Some ctea \<longrightarrow> ((\<lambda>s. ctes_of s (?ptr1701 newCap srcSlot destSlot cte ctea) = Some ctea) and ?R1699 newCap srcSlot destSlot cte ctea and cte_wp_at' (\<lambda>_. True) (ptr_val srcSlot)) s)) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr dest) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. \<forall>cte'a. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr src) = Some cte'a \<and> cl_valid_cte cte'a \<longrightarrow> s \<in> \<lbrace>ptr_val srcSlot = ?ptr1701 newCap srcSlot destSlot (cte_to_H cte') (cte_to_H cte'a)\<rbrace> \<inter> ?R'1699 newCap srcSlot destSlot (cte_to_H cte') (cte_to_H cte'a) \<inter> \<lbrace>True\<rbrace>}} proof (prove)
goal (12 subgoals):
 1. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc xfdcd ret__unsigned. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdcb; dc yb xfdcc; mdb_node_lift ret__struct_mdb_node_C = \<lparr>mdbNext_CL = 0, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) false, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) false, mdbPrev_CL = 0\<rparr>; dc yc xfdcd; ret__unsigned = mdbPrev_CL (mdb_node_lift mdb)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q2660 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc) (?G'2828 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc xfdcd ret__unsigned) [SKIP] (do y <- updateMDB (mdbPrev rv) (mdbNext_update (\<lambda>_. dest));
updateMDB (mdbNext rv) (mdbPrev_update (\<lambda>_. dest))
od) (IF ret__unsigned \<noteq> 0 THEN
  Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr ret__unsigned} (CALL mdb_node_ptr_set_mdbNext_'proc(mdb_Ptr &(cte_Ptr ret__unsigned\<rightarrow>[''cteMDBNode_C'']),ptr_val destSlot))
FI;;
(\<acute>ret__unsigned :== CALL mdb_node_get_mdbNext_'proc(mdb);;
(\<acute>next_ptr :== \<acute>ret__unsigned;;
IF \<acute>next_ptr \<noteq> 0 THEN
  Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr (next_ptr_' s)} (CALL mdb_node_ptr_set_mdbPrev_'proc(mdb_Ptr &(cte_Ptr \<acute>next_ptr\<rightarrow>[''cteMDBNode_C'']),ptr_val destSlot))
FI)))
 2. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdc ret__struct_mdb_node_C. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdcb; dc yb xfdc; mdb_node_lift ret__struct_mdb_node_C = \<lparr>mdbNext_CL = 0, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) false, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) false, mdbPrev_CL = 0\<rparr>\<rbrakk> \<Longrightarrow> \<lbrace>?R2662 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb\<rbrace> updateMDB src (const nullMDBNode) \<lbrace>?Q2660 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdc ret__struct_mdb_node_C\<rbrace>
 3. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdcb; dc yb xfdcc; mdb_node_lift ret__struct_mdb_node_C = \<lparr>mdbNext_CL = 0, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) false, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) false, mdbPrev_CL = 0\<rparr>\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'2660 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C) \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])) ret__struct_mdb_node_C)) {s. \<forall>yc. dc yc (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>v. v = mdbPrev_CL (mdb_node_lift (mdb_node_' (mdb_node_'_update (\<lambda>_. mdb) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {sa. prev_ptr_'_update (\<lambda>_. v) sa \<in> ?G'2828 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc (xfdc s) v}}}
 4. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdc. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R2401 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya\<rbrace> updateMDB dest (const rv) \<lbrace>\<lambda>yb. (\<lambda>_. src \<noteq> 0) and ?R2662 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdc yb and cte_wp_at' (\<lambda>_. True) (ptr_val srcSlot)\<rbrace>
 5. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdcb\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'2399 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb) \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(destSlot\<rightarrow>[''cteMDBNode_C''])) mdb)) {s. \<forall>yb. dc yb (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>v. mdb_node_lift v = \<lparr>mdbNext_CL = mdbNext_' (mdbPrev_'_update (\<lambda>_. 0) (mdbFirstBadged_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbRevocable_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbNext_'_update (\<lambda>_. 0) sa)))) && ~~ mask 3, mdbRevocable_CL = mdbRevocable_' (mdbPrev_'_update (\<lambda>_. 0) (mdbFirstBadged_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbRevocable_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbNext_'_update (\<lambda>_. 0) sa)))) && mask 1, mdbFirstBadged_CL = mdbFirstBadged_' (mdbPrev_'_update (\<lambda>_. 0) (mdbFirstBadged_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbRevocable_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbNext_'_update (\<lambda>_. 0) sa)))) && mask 1, mdbPrev_CL = mdbPrev_' (mdbPrev_'_update (\<lambda>_. 0) (mdbFirstBadged_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbRevocable_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbNext_'_update (\<lambda>_. 0) sa)))) && ~~ mask 3\<rparr> \<longrightarrow> sa\<lparr>ret__struct_mdb_node_C_' := v\<rparr> \<in> \<lbrace>cmdbnode_relation nullMDBNode v\<rbrace> \<inter> \<lbrace>srcSlot = cte_Ptr src\<rbrace> \<inter> ?R'2660 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb (xfdc s) v \<inter> \<lbrace>True\<rbrace>}}
 6. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdc ret__struct_cap_C. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdc; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrakk> \<Longrightarrow> \<lbrace>?R2369 newCap srcSlot destSlot oldCTE cte rv mdb y\<rbrace> updateCap src capability.NullCap \<lbrace>\<lambda>ya. (\<lambda>_. dest \<noteq> 0) and ?R2401 newCap srcSlot destSlot oldCTE cte rv mdb y xfdc ret__struct_cap_C ya and cte_wp_at' (\<lambda>_. True) (ptr_val destSlot)\<rbrace>
 7. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'2367 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C) \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(srcSlot\<rightarrow>[''cap_C''])) ret__struct_cap_C)) {s. \<forall>ya. dc ya (xfdc s) \<longrightarrow> s \<in> \<lbrace>cmdbnode_relation rv mdb\<rbrace> \<inter> \<lbrace>destSlot = cte_Ptr dest\<rbrace> \<inter> ?R'2399 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya (xfdc s) \<inter> \<lbrace>True\<rbrace>}
 8. \<And>newCap srcSlot destSlot oldCTE cte rv mdb. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb\<rbrakk> \<Longrightarrow> \<lbrace>?R2045 newCap srcSlot destSlot oldCTE cte rv\<rbrace> updateCap dest cap \<lbrace>\<lambda>y. (\<lambda>_. True) and ?R2369 newCap srcSlot destSlot oldCTE cte rv mdb y and cte_wp_at' (\<lambda>_. True) (ptr_val srcSlot)\<rbrace>
 9. \<And>newCap srcSlot destSlot oldCTE cte rv mdb. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'2043 newCap srcSlot destSlot oldCTE cte rv mdb) \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(destSlot\<rightarrow>[''cap_C''])) newCap)) {s. \<forall>y. dc y (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>v. cap_get_tag v = SCAST(32 signed \<rightarrow> 32) cap_null_cap \<longrightarrow> sa\<lparr>ret__struct_cap_C_' := v\<rparr> \<in> \<lbrace>ccap_relation capability.NullCap v\<rbrace> \<inter> \<lbrace>srcSlot = cte_Ptr src\<rbrace> \<inter> ?R'2367 newCap srcSlot destSlot oldCTE cte rv mdb y (xfdc s) v \<inter> \<lbrace>True\<rbrace>}}
 10. \<And>newCap srcSlot destSlot oldCTE cte. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer\<rbrakk> \<Longrightarrow> \<lbrace>?R1699 newCap srcSlot destSlot oldCTE cte\<rbrace> return (cteMDBNode cte) \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?R2045 newCap srcSlot destSlot oldCTE cte rv and cte_wp_at' (\<lambda>_. True) (ptr_val destSlot)\<rbrace>
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc xfdcd ret__unsigned. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdcb; dc yb xfdcc; mdb_node_lift ret__struct_mdb_node_C = \<lparr>mdbNext_CL = 0, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) false, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) false, mdbPrev_CL = 0\<rparr>; dc yc xfdcd\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q2660 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc) (?G'2989 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc xfdcd ret__unsigned (mdbPrev_CL (mdb_node_lift mdb))) [SKIP] (do y <- updateMDB (mdbPrev rv) (mdbNext_update (\<lambda>_. dest));
updateMDB (mdbNext rv) (mdbPrev_update (\<lambda>_. dest))
od) (IF mdbPrev_CL (mdb_node_lift mdb) \<noteq> 0 THEN
  Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr (mdbPrev_CL (mdb_node_lift mdb))} (CALL mdb_node_ptr_set_mdbNext_'proc(mdb_Ptr &(cte_Ptr (mdbPrev_CL (mdb_node_lift mdb))\<rightarrow>[''cteMDBNode_C'']),ptr_val destSlot))
FI;;
(\<acute>ret__unsigned :== CALL mdb_node_get_mdbNext_'proc(mdb);;
(\<acute>next_ptr :== \<acute>ret__unsigned;;
IF \<acute>next_ptr \<noteq> 0 THEN
  Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr (next_ptr_' s)} (CALL mdb_node_ptr_set_mdbPrev_'proc(mdb_Ptr &(cte_Ptr \<acute>next_ptr\<rightarrow>[''cteMDBNode_C'']),ptr_val destSlot))
FI)))
 2. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdc ret__struct_mdb_node_C. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdcb; dc yb xfdc; mdb_node_lift ret__struct_mdb_node_C = \<lparr>mdbNext_CL = 0, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) false, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) false, mdbPrev_CL = 0\<rparr>\<rbrakk> \<Longrightarrow> \<lbrace>?R2662 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb\<rbrace> updateMDB src (const nullMDBNode) \<lbrace>?Q2660 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdc ret__struct_mdb_node_C\<rbrace>
 3. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdcb; dc yb xfdcc; mdb_node_lift ret__struct_mdb_node_C = \<lparr>mdbNext_CL = 0, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) false, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) false, mdbPrev_CL = 0\<rparr>\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'2660 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C) \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])) ret__struct_mdb_node_C)) {s. \<forall>yc. dc yc (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>v. v = mdbPrev_CL (mdb_node_lift (mdb_node_' (mdb_node_'_update (\<lambda>_. mdb) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {sa. prev_ptr_'_update (\<lambda>_. v) sa \<in> ?G'2989 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc (xfdc s) v v}}}
 4. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdc. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R2401 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya\<rbrace> updateMDB dest (const rv) \<lbrace>\<lambda>yb. (\<lambda>_. src \<noteq> 0) and ?R2662 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdc yb and cte_wp_at' (\<lambda>_. True) (ptr_val srcSlot)\<rbrace>
 5. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdcb\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'2399 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb) \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(destSlot\<rightarrow>[''cteMDBNode_C''])) mdb)) {s. \<forall>yb. dc yb (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>v. mdb_node_lift v = \<lparr>mdbNext_CL = mdbNext_' (mdbPrev_'_update (\<lambda>_. 0) (mdbFirstBadged_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbRevocable_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbNext_'_update (\<lambda>_. 0) sa)))) && ~~ mask 3, mdbRevocable_CL = mdbRevocable_' (mdbPrev_'_update (\<lambda>_. 0) (mdbFirstBadged_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbRevocable_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbNext_'_update (\<lambda>_. 0) sa)))) && mask 1, mdbFirstBadged_CL = mdbFirstBadged_' (mdbPrev_'_update (\<lambda>_. 0) (mdbFirstBadged_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbRevocable_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbNext_'_update (\<lambda>_. 0) sa)))) && mask 1, mdbPrev_CL = mdbPrev_' (mdbPrev_'_update (\<lambda>_. 0) (mdbFirstBadged_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbRevocable_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbNext_'_update (\<lambda>_. 0) sa)))) && ~~ mask 3\<rparr> \<longrightarrow> sa\<lparr>ret__struct_mdb_node_C_' := v\<rparr> \<in> \<lbrace>cmdbnode_relation nullMDBNode v\<rbrace> \<inter> \<lbrace>srcSlot = cte_Ptr src\<rbrace> \<inter> ?R'2660 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb (xfdc s) v \<inter> \<lbrace>True\<rbrace>}}
 6. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdc ret__struct_cap_C. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdc; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrakk> \<Longrightarrow> \<lbrace>?R2369 newCap srcSlot destSlot oldCTE cte rv mdb y\<rbrace> updateCap src capability.NullCap \<lbrace>\<lambda>ya. (\<lambda>_. dest \<noteq> 0) and ?R2401 newCap srcSlot destSlot oldCTE cte rv mdb y xfdc ret__struct_cap_C ya and cte_wp_at' (\<lambda>_. True) (ptr_val destSlot)\<rbrace>
 7. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'2367 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C) \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(srcSlot\<rightarrow>[''cap_C''])) ret__struct_cap_C)) {s. \<forall>ya. dc ya (xfdc s) \<longrightarrow> s \<in> \<lbrace>cmdbnode_relation rv mdb\<rbrace> \<inter> \<lbrace>destSlot = cte_Ptr dest\<rbrace> \<inter> ?R'2399 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya (xfdc s) \<inter> \<lbrace>True\<rbrace>}
 8. \<And>newCap srcSlot destSlot oldCTE cte rv mdb. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb\<rbrakk> \<Longrightarrow> \<lbrace>?R2045 newCap srcSlot destSlot oldCTE cte rv\<rbrace> updateCap dest cap \<lbrace>\<lambda>y. (\<lambda>_. True) and ?R2369 newCap srcSlot destSlot oldCTE cte rv mdb y and cte_wp_at' (\<lambda>_. True) (ptr_val srcSlot)\<rbrace>
 9. \<And>newCap srcSlot destSlot oldCTE cte rv mdb. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'2043 newCap srcSlot destSlot oldCTE cte rv mdb) \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(destSlot\<rightarrow>[''cap_C''])) newCap)) {s. \<forall>y. dc y (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>v. cap_get_tag v = SCAST(32 signed \<rightarrow> 32) cap_null_cap \<longrightarrow> sa\<lparr>ret__struct_cap_C_' := v\<rparr> \<in> \<lbrace>ccap_relation capability.NullCap v\<rbrace> \<inter> \<lbrace>srcSlot = cte_Ptr src\<rbrace> \<inter> ?R'2367 newCap srcSlot destSlot oldCTE cte rv mdb y (xfdc s) v \<inter> \<lbrace>True\<rbrace>}}
 10. \<And>newCap srcSlot destSlot oldCTE cte. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer\<rbrakk> \<Longrightarrow> \<lbrace>?R1699 newCap srcSlot destSlot oldCTE cte\<rbrace> return (cteMDBNode cte) \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?R2045 newCap srcSlot destSlot oldCTE cte rv and cte_wp_at' (\<lambda>_. True) (ptr_val destSlot)\<rbrace>
A total of 12 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc xfdcd ret__unsigned rva xfdce. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdcb; dc yb xfdcc; mdb_node_lift ret__struct_mdb_node_C = \<lparr>mdbNext_CL = 0, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) false, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) false, mdbPrev_CL = 0\<rparr>; dc yc xfdcd; dc rva xfdce\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q2995 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc xfdcd ret__unsigned rva) (?Q'2995 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc xfdcd ret__unsigned rva xfdce) [SKIP] (updateMDB (mdbNext rv) (mdbPrev_update (\<lambda>_. dest))) (\<acute>ret__unsigned :== CALL mdb_node_get_mdbNext_'proc(mdb);;
(\<acute>next_ptr :== \<acute>ret__unsigned;;
IF \<acute>next_ptr \<noteq> 0 THEN
  Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr (next_ptr_' s)} (CALL mdb_node_ptr_set_mdbPrev_'proc(mdb_Ptr &(cte_Ptr \<acute>next_ptr\<rightarrow>[''cteMDBNode_C'']),ptr_val destSlot))
FI))
 2. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc xfdc ret__unsigned. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdcb; dc yb xfdcc; mdb_node_lift ret__struct_mdb_node_C = \<lparr>mdbNext_CL = 0, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) false, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) false, mdbPrev_CL = 0\<rparr>; dc yc xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R3001 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc\<rbrace> updateMDB (mdbPrev rv) (mdbNext_update (\<lambda>_. dest)) \<lbrace>?Q2995 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc xfdc ret__unsigned\<rbrace>
 3. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc xfdcd ret__unsigned. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdcb; dc yb xfdcc; mdb_node_lift ret__struct_mdb_node_C = \<lparr>mdbNext_CL = 0, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) false, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) false, mdbPrev_CL = 0\<rparr>; dc yc xfdcd\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'2996 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc xfdcd ret__unsigned (mdbPrev_CL (mdb_node_lift mdb))) IF mdbPrev_CL (mdb_node_lift mdb) \<noteq> 0 THEN
  Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr (mdbPrev_CL (mdb_node_lift mdb))} (CALL mdb_node_ptr_set_mdbNext_'proc(mdb_Ptr &(cte_Ptr (mdbPrev_CL (mdb_node_lift mdb))\<rightarrow>[''cteMDBNode_C'']),ptr_val destSlot))
FI {s. \<forall>rva. dc rva (xfdc s) \<longrightarrow> s \<in> ?Q'2995 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc xfdcd ret__unsigned rva (xfdc s)}
 4. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdc ret__struct_mdb_node_C. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdcb; dc yb xfdc; mdb_node_lift ret__struct_mdb_node_C = \<lparr>mdbNext_CL = 0, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) false, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) false, mdbPrev_CL = 0\<rparr>\<rbrakk> \<Longrightarrow> \<lbrace>?R2662 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb\<rbrace> updateMDB src (const nullMDBNode) \<lbrace>\<lambda>a. (\<lambda>a. is_aligned (mdbPrev rv) 3 \<and> (dest \<noteq> 0 \<longrightarrow> is_aligned dest 3)) and ?R3001 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdc ret__struct_mdb_node_C a\<rbrace>
 5. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdcb; dc yb xfdcc; mdb_node_lift ret__struct_mdb_node_C = \<lparr>mdbNext_CL = 0, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) false, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) false, mdbPrev_CL = 0\<rparr>\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'2660 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C) \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])) ret__struct_mdb_node_C)) {s. \<forall>yc. dc yc (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>v. v = mdbPrev_CL (mdb_node_lift (mdb_node_' (mdb_node_'_update (\<lambda>_. mdb) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {sa. prev_ptr_'_update (\<lambda>_. v) sa \<in> UNIV \<inter> ?R'2996 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc (xfdc s) v v}}}
 6. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdc. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R2401 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya\<rbrace> updateMDB dest (const rv) \<lbrace>\<lambda>yb. (\<lambda>_. src \<noteq> 0) and ?R2662 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdc yb and cte_wp_at' (\<lambda>_. True) (ptr_val srcSlot)\<rbrace>
 7. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdcb\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'2399 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb) \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(destSlot\<rightarrow>[''cteMDBNode_C''])) mdb)) {s. \<forall>yb. dc yb (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>v. mdb_node_lift v = \<lparr>mdbNext_CL = mdbNext_' (mdbPrev_'_update (\<lambda>_. 0) (mdbFirstBadged_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbRevocable_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbNext_'_update (\<lambda>_. 0) sa)))) && ~~ mask 3, mdbRevocable_CL = mdbRevocable_' (mdbPrev_'_update (\<lambda>_. 0) (mdbFirstBadged_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbRevocable_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbNext_'_update (\<lambda>_. 0) sa)))) && mask 1, mdbFirstBadged_CL = mdbFirstBadged_' (mdbPrev_'_update (\<lambda>_. 0) (mdbFirstBadged_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbRevocable_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbNext_'_update (\<lambda>_. 0) sa)))) && mask 1, mdbPrev_CL = mdbPrev_' (mdbPrev_'_update (\<lambda>_. 0) (mdbFirstBadged_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbRevocable_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbNext_'_update (\<lambda>_. 0) sa)))) && ~~ mask 3\<rparr> \<longrightarrow> sa\<lparr>ret__struct_mdb_node_C_' := v\<rparr> \<in> \<lbrace>cmdbnode_relation nullMDBNode v\<rbrace> \<inter> \<lbrace>srcSlot = cte_Ptr src\<rbrace> \<inter> ?R'2660 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb (xfdc s) v \<inter> \<lbrace>True\<rbrace>}}
 8. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdc ret__struct_cap_C. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdc; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrakk> \<Longrightarrow> \<lbrace>?R2369 newCap srcSlot destSlot oldCTE cte rv mdb y\<rbrace> updateCap src capability.NullCap \<lbrace>\<lambda>ya. (\<lambda>_. dest \<noteq> 0) and ?R2401 newCap srcSlot destSlot oldCTE cte rv mdb y xfdc ret__struct_cap_C ya and cte_wp_at' (\<lambda>_. True) (ptr_val destSlot)\<rbrace>
 9. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'2367 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C) \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(srcSlot\<rightarrow>[''cap_C''])) ret__struct_cap_C)) {s. \<forall>ya. dc ya (xfdc s) \<longrightarrow> s \<in> \<lbrace>cmdbnode_relation rv mdb\<rbrace> \<inter> \<lbrace>destSlot = cte_Ptr dest\<rbrace> \<inter> ?R'2399 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya (xfdc s) \<inter> \<lbrace>True\<rbrace>}
 10. \<And>newCap srcSlot destSlot oldCTE cte rv mdb. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb\<rbrakk> \<Longrightarrow> \<lbrace>?R2045 newCap srcSlot destSlot oldCTE cte rv\<rbrace> updateCap dest cap \<lbrace>\<lambda>y. (\<lambda>_. True) and ?R2369 newCap srcSlot destSlot oldCTE cte rv mdb y and cte_wp_at' (\<lambda>_. True) (ptr_val srcSlot)\<rbrace>
A total of 14 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc xfdcd ret__unsigneda rva xfdce ret__unsigned. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdcb; dc yb xfdcc; mdb_node_lift ret__struct_mdb_node_C = \<lparr>mdbNext_CL = 0, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) false, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) false, mdbPrev_CL = 0\<rparr>; dc yc xfdcd; dc rva xfdce; ret__unsigned = mdbNext_CL (mdb_node_lift mdb)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q2995 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc xfdcd ret__unsigneda rva) (?G'3039 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc xfdcd ret__unsigneda rva xfdce ret__unsigned) [SKIP] (updateMDB (mdbNext rv) (mdbPrev_update (\<lambda>_. dest))) (\<acute>next_ptr :== ret__unsigned;;
IF \<acute>next_ptr \<noteq> 0 THEN
  Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr (next_ptr_' s)} (CALL mdb_node_ptr_set_mdbPrev_'proc(mdb_Ptr &(cte_Ptr \<acute>next_ptr\<rightarrow>[''cteMDBNode_C'']),ptr_val destSlot))
FI)
 2. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc xfdc ret__unsigned. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdcb; dc yb xfdcc; mdb_node_lift ret__struct_mdb_node_C = \<lparr>mdbNext_CL = 0, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) false, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) false, mdbPrev_CL = 0\<rparr>; dc yc xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R3001 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc\<rbrace> updateMDB (mdbPrev rv) (mdbNext_update (\<lambda>_. dest)) \<lbrace>?Q2995 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc xfdc ret__unsigned\<rbrace>
 3. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc xfdcd ret__unsigned. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdcb; dc yb xfdcc; mdb_node_lift ret__struct_mdb_node_C = \<lparr>mdbNext_CL = 0, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) false, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) false, mdbPrev_CL = 0\<rparr>; dc yc xfdcd\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'2996 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc xfdcd ret__unsigned (mdbPrev_CL (mdb_node_lift mdb))) IF mdbPrev_CL (mdb_node_lift mdb) \<noteq> 0 THEN
  Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr (mdbPrev_CL (mdb_node_lift mdb))} (CALL mdb_node_ptr_set_mdbNext_'proc(mdb_Ptr &(cte_Ptr (mdbPrev_CL (mdb_node_lift mdb))\<rightarrow>[''cteMDBNode_C'']),ptr_val destSlot))
FI {s. \<forall>rva. dc rva (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>v. v = mdbNext_CL (mdb_node_lift (mdb_node_' (mdb_node_'_update (\<lambda>_. mdb) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> ?G'3039 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc xfdcd ret__unsigned rva (xfdc s) v}}
 4. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdc ret__struct_mdb_node_C. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdcb; dc yb xfdc; mdb_node_lift ret__struct_mdb_node_C = \<lparr>mdbNext_CL = 0, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) false, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) false, mdbPrev_CL = 0\<rparr>\<rbrakk> \<Longrightarrow> \<lbrace>?R2662 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb\<rbrace> updateMDB src (const nullMDBNode) \<lbrace>\<lambda>a. (\<lambda>a. is_aligned (mdbPrev rv) 3 \<and> (dest \<noteq> 0 \<longrightarrow> is_aligned dest 3)) and ?R3001 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdc ret__struct_mdb_node_C a\<rbrace>
 5. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdcb; dc yb xfdcc; mdb_node_lift ret__struct_mdb_node_C = \<lparr>mdbNext_CL = 0, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) false, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) false, mdbPrev_CL = 0\<rparr>\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'2660 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C) \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])) ret__struct_mdb_node_C)) {s. \<forall>yc. dc yc (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>v. v = mdbPrev_CL (mdb_node_lift (mdb_node_' (mdb_node_'_update (\<lambda>_. mdb) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {sa. prev_ptr_'_update (\<lambda>_. v) sa \<in> UNIV \<inter> ?R'2996 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc (xfdc s) v v}}}
 6. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdc. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R2401 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya\<rbrace> updateMDB dest (const rv) \<lbrace>\<lambda>yb. (\<lambda>_. src \<noteq> 0) and ?R2662 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdc yb and cte_wp_at' (\<lambda>_. True) (ptr_val srcSlot)\<rbrace>
 7. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdcb\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'2399 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb) \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(destSlot\<rightarrow>[''cteMDBNode_C''])) mdb)) {s. \<forall>yb. dc yb (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>v. mdb_node_lift v = \<lparr>mdbNext_CL = mdbNext_' (mdbPrev_'_update (\<lambda>_. 0) (mdbFirstBadged_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbRevocable_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbNext_'_update (\<lambda>_. 0) sa)))) && ~~ mask 3, mdbRevocable_CL = mdbRevocable_' (mdbPrev_'_update (\<lambda>_. 0) (mdbFirstBadged_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbRevocable_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbNext_'_update (\<lambda>_. 0) sa)))) && mask 1, mdbFirstBadged_CL = mdbFirstBadged_' (mdbPrev_'_update (\<lambda>_. 0) (mdbFirstBadged_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbRevocable_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbNext_'_update (\<lambda>_. 0) sa)))) && mask 1, mdbPrev_CL = mdbPrev_' (mdbPrev_'_update (\<lambda>_. 0) (mdbFirstBadged_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbRevocable_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbNext_'_update (\<lambda>_. 0) sa)))) && ~~ mask 3\<rparr> \<longrightarrow> sa\<lparr>ret__struct_mdb_node_C_' := v\<rparr> \<in> \<lbrace>cmdbnode_relation nullMDBNode v\<rbrace> \<inter> \<lbrace>srcSlot = cte_Ptr src\<rbrace> \<inter> ?R'2660 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb (xfdc s) v \<inter> \<lbrace>True\<rbrace>}}
 8. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdc ret__struct_cap_C. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdc; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrakk> \<Longrightarrow> \<lbrace>?R2369 newCap srcSlot destSlot oldCTE cte rv mdb y\<rbrace> updateCap src capability.NullCap \<lbrace>\<lambda>ya. (\<lambda>_. dest \<noteq> 0) and ?R2401 newCap srcSlot destSlot oldCTE cte rv mdb y xfdc ret__struct_cap_C ya and cte_wp_at' (\<lambda>_. True) (ptr_val destSlot)\<rbrace>
 9. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'2367 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C) \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(srcSlot\<rightarrow>[''cap_C''])) ret__struct_cap_C)) {s. \<forall>ya. dc ya (xfdc s) \<longrightarrow> s \<in> \<lbrace>cmdbnode_relation rv mdb\<rbrace> \<inter> \<lbrace>destSlot = cte_Ptr dest\<rbrace> \<inter> ?R'2399 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya (xfdc s) \<inter> \<lbrace>True\<rbrace>}
 10. \<And>newCap srcSlot destSlot oldCTE cte rv mdb. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb\<rbrakk> \<Longrightarrow> \<lbrace>?R2045 newCap srcSlot destSlot oldCTE cte rv\<rbrace> updateCap dest cap \<lbrace>\<lambda>y. (\<lambda>_. True) and ?R2369 newCap srcSlot destSlot oldCTE cte rv mdb y and cte_wp_at' (\<lambda>_. True) (ptr_val srcSlot)\<rbrace>
A total of 14 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc xfdcd ret__unsigneda rva xfdce ret__unsigned. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdcb; dc yb xfdcc; mdb_node_lift ret__struct_mdb_node_C = \<lparr>mdbNext_CL = 0, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) false, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) false, mdbPrev_CL = 0\<rparr>; dc yc xfdcd; dc rva xfdce; ret__unsigned = mdbNext_CL (mdb_node_lift mdb)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q2995 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc xfdcd ret__unsigneda rva) (?G'3130 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc xfdcd ret__unsigneda rva xfdce ret__unsigned) [SKIP] (updateMDB (mdbNext rv) (mdbPrev_update (\<lambda>_. dest))) (IF ret__unsigned \<noteq> 0 THEN
  Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr ret__unsigned} (CALL mdb_node_ptr_set_mdbPrev_'proc(mdb_Ptr &(cte_Ptr ret__unsigned\<rightarrow>[''cteMDBNode_C'']),ptr_val destSlot))
FI)
 2. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc xfdc ret__unsigned. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdcb; dc yb xfdcc; mdb_node_lift ret__struct_mdb_node_C = \<lparr>mdbNext_CL = 0, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) false, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) false, mdbPrev_CL = 0\<rparr>; dc yc xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R3001 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc\<rbrace> updateMDB (mdbPrev rv) (mdbNext_update (\<lambda>_. dest)) \<lbrace>?Q2995 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc xfdc ret__unsigned\<rbrace>
 3. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc xfdcd ret__unsigned. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdcb; dc yb xfdcc; mdb_node_lift ret__struct_mdb_node_C = \<lparr>mdbNext_CL = 0, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) false, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) false, mdbPrev_CL = 0\<rparr>; dc yc xfdcd\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'2996 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc xfdcd ret__unsigned (mdbPrev_CL (mdb_node_lift mdb))) IF mdbPrev_CL (mdb_node_lift mdb) \<noteq> 0 THEN
  Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr (mdbPrev_CL (mdb_node_lift mdb))} (CALL mdb_node_ptr_set_mdbNext_'proc(mdb_Ptr &(cte_Ptr (mdbPrev_CL (mdb_node_lift mdb))\<rightarrow>[''cteMDBNode_C'']),ptr_val destSlot))
FI {s. \<forall>rva. dc rva (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>v. v = mdbNext_CL (mdb_node_lift (mdb_node_' (mdb_node_'_update (\<lambda>_. mdb) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {sa. next_ptr_'_update (\<lambda>_. v) sa \<in> ?G'3130 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc xfdcd ret__unsigned rva (xfdc s) v}}}
 4. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdc ret__struct_mdb_node_C. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdcb; dc yb xfdc; mdb_node_lift ret__struct_mdb_node_C = \<lparr>mdbNext_CL = 0, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) false, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) false, mdbPrev_CL = 0\<rparr>\<rbrakk> \<Longrightarrow> \<lbrace>?R2662 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb\<rbrace> updateMDB src (const nullMDBNode) \<lbrace>\<lambda>a. (\<lambda>a. is_aligned (mdbPrev rv) 3 \<and> (dest \<noteq> 0 \<longrightarrow> is_aligned dest 3)) and ?R3001 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdc ret__struct_mdb_node_C a\<rbrace>
 5. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdcb; dc yb xfdcc; mdb_node_lift ret__struct_mdb_node_C = \<lparr>mdbNext_CL = 0, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) false, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) false, mdbPrev_CL = 0\<rparr>\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'2660 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C) \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])) ret__struct_mdb_node_C)) {s. \<forall>yc. dc yc (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>v. v = mdbPrev_CL (mdb_node_lift (mdb_node_' (mdb_node_'_update (\<lambda>_. mdb) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {sa. prev_ptr_'_update (\<lambda>_. v) sa \<in> UNIV \<inter> ?R'2996 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc (xfdc s) v v}}}
 6. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdc. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R2401 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya\<rbrace> updateMDB dest (const rv) \<lbrace>\<lambda>yb. (\<lambda>_. src \<noteq> 0) and ?R2662 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdc yb and cte_wp_at' (\<lambda>_. True) (ptr_val srcSlot)\<rbrace>
 7. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdcb\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'2399 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb) \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(destSlot\<rightarrow>[''cteMDBNode_C''])) mdb)) {s. \<forall>yb. dc yb (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>v. mdb_node_lift v = \<lparr>mdbNext_CL = mdbNext_' (mdbPrev_'_update (\<lambda>_. 0) (mdbFirstBadged_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbRevocable_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbNext_'_update (\<lambda>_. 0) sa)))) && ~~ mask 3, mdbRevocable_CL = mdbRevocable_' (mdbPrev_'_update (\<lambda>_. 0) (mdbFirstBadged_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbRevocable_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbNext_'_update (\<lambda>_. 0) sa)))) && mask 1, mdbFirstBadged_CL = mdbFirstBadged_' (mdbPrev_'_update (\<lambda>_. 0) (mdbFirstBadged_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbRevocable_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbNext_'_update (\<lambda>_. 0) sa)))) && mask 1, mdbPrev_CL = mdbPrev_' (mdbPrev_'_update (\<lambda>_. 0) (mdbFirstBadged_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbRevocable_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbNext_'_update (\<lambda>_. 0) sa)))) && ~~ mask 3\<rparr> \<longrightarrow> sa\<lparr>ret__struct_mdb_node_C_' := v\<rparr> \<in> \<lbrace>cmdbnode_relation nullMDBNode v\<rbrace> \<inter> \<lbrace>srcSlot = cte_Ptr src\<rbrace> \<inter> ?R'2660 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb (xfdc s) v \<inter> \<lbrace>True\<rbrace>}}
 8. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdc ret__struct_cap_C. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdc; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrakk> \<Longrightarrow> \<lbrace>?R2369 newCap srcSlot destSlot oldCTE cte rv mdb y\<rbrace> updateCap src capability.NullCap \<lbrace>\<lambda>ya. (\<lambda>_. dest \<noteq> 0) and ?R2401 newCap srcSlot destSlot oldCTE cte rv mdb y xfdc ret__struct_cap_C ya and cte_wp_at' (\<lambda>_. True) (ptr_val destSlot)\<rbrace>
 9. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'2367 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C) \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(srcSlot\<rightarrow>[''cap_C''])) ret__struct_cap_C)) {s. \<forall>ya. dc ya (xfdc s) \<longrightarrow> s \<in> \<lbrace>cmdbnode_relation rv mdb\<rbrace> \<inter> \<lbrace>destSlot = cte_Ptr dest\<rbrace> \<inter> ?R'2399 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya (xfdc s) \<inter> \<lbrace>True\<rbrace>}
 10. \<And>newCap srcSlot destSlot oldCTE cte rv mdb. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb\<rbrakk> \<Longrightarrow> \<lbrace>?R2045 newCap srcSlot destSlot oldCTE cte rv\<rbrace> updateCap dest cap \<lbrace>\<lambda>y. (\<lambda>_. True) and ?R2369 newCap srcSlot destSlot oldCTE cte rv mdb y and cte_wp_at' (\<lambda>_. True) (ptr_val srcSlot)\<rbrace>
A total of 14 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc xfdcd ret__unsigneda rva xfdce ret__unsigned. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdcb; dc yb xfdcc; mdb_node_lift ret__struct_mdb_node_C = \<lparr>mdbNext_CL = 0, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) false, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) false, mdbPrev_CL = 0\<rparr>; dc yc xfdcd; dc rva xfdce\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q2995 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc xfdcd ret__unsigneda rva) (?G'3202 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc xfdcd ret__unsigneda rva xfdce ret__unsigned (mdbNext_CL (mdb_node_lift mdb))) [SKIP] (updateMDB (mdbNext rv) (mdbPrev_update (\<lambda>_. dest))) (IF mdbNext_CL (mdb_node_lift mdb) \<noteq> 0 THEN
  Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr (mdbNext_CL (mdb_node_lift mdb))} (CALL mdb_node_ptr_set_mdbPrev_'proc(mdb_Ptr &(cte_Ptr (mdbNext_CL (mdb_node_lift mdb))\<rightarrow>[''cteMDBNode_C'']),ptr_val destSlot))
FI)
 2. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc xfdc ret__unsigned. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdcb; dc yb xfdcc; mdb_node_lift ret__struct_mdb_node_C = \<lparr>mdbNext_CL = 0, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) false, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) false, mdbPrev_CL = 0\<rparr>; dc yc xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R3001 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc\<rbrace> updateMDB (mdbPrev rv) (mdbNext_update (\<lambda>_. dest)) \<lbrace>?Q2995 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc xfdc ret__unsigned\<rbrace>
 3. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc xfdcd ret__unsigned. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdcb; dc yb xfdcc; mdb_node_lift ret__struct_mdb_node_C = \<lparr>mdbNext_CL = 0, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) false, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) false, mdbPrev_CL = 0\<rparr>; dc yc xfdcd\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'2996 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc xfdcd ret__unsigned (mdbPrev_CL (mdb_node_lift mdb))) IF mdbPrev_CL (mdb_node_lift mdb) \<noteq> 0 THEN
  Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr (mdbPrev_CL (mdb_node_lift mdb))} (CALL mdb_node_ptr_set_mdbNext_'proc(mdb_Ptr &(cte_Ptr (mdbPrev_CL (mdb_node_lift mdb))\<rightarrow>[''cteMDBNode_C'']),ptr_val destSlot))
FI {s. \<forall>rva. dc rva (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>v. v = mdbNext_CL (mdb_node_lift (mdb_node_' (mdb_node_'_update (\<lambda>_. mdb) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {sa. next_ptr_'_update (\<lambda>_. v) sa \<in> ?G'3202 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc xfdcd ret__unsigned rva (xfdc s) v v}}}
 4. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdc ret__struct_mdb_node_C. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdcb; dc yb xfdc; mdb_node_lift ret__struct_mdb_node_C = \<lparr>mdbNext_CL = 0, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) false, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) false, mdbPrev_CL = 0\<rparr>\<rbrakk> \<Longrightarrow> \<lbrace>?R2662 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb\<rbrace> updateMDB src (const nullMDBNode) \<lbrace>\<lambda>a. (\<lambda>a. is_aligned (mdbPrev rv) 3 \<and> (dest \<noteq> 0 \<longrightarrow> is_aligned dest 3)) and ?R3001 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdc ret__struct_mdb_node_C a\<rbrace>
 5. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdcb; dc yb xfdcc; mdb_node_lift ret__struct_mdb_node_C = \<lparr>mdbNext_CL = 0, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) false, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) false, mdbPrev_CL = 0\<rparr>\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'2660 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C) \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])) ret__struct_mdb_node_C)) {s. \<forall>yc. dc yc (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>v. v = mdbPrev_CL (mdb_node_lift (mdb_node_' (mdb_node_'_update (\<lambda>_. mdb) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {sa. prev_ptr_'_update (\<lambda>_. v) sa \<in> UNIV \<inter> ?R'2996 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc (xfdc s) v v}}}
 6. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdc. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R2401 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya\<rbrace> updateMDB dest (const rv) \<lbrace>\<lambda>yb. (\<lambda>_. src \<noteq> 0) and ?R2662 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdc yb and cte_wp_at' (\<lambda>_. True) (ptr_val srcSlot)\<rbrace>
 7. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdcb\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'2399 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb) \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(destSlot\<rightarrow>[''cteMDBNode_C''])) mdb)) {s. \<forall>yb. dc yb (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>v. mdb_node_lift v = \<lparr>mdbNext_CL = mdbNext_' (mdbPrev_'_update (\<lambda>_. 0) (mdbFirstBadged_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbRevocable_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbNext_'_update (\<lambda>_. 0) sa)))) && ~~ mask 3, mdbRevocable_CL = mdbRevocable_' (mdbPrev_'_update (\<lambda>_. 0) (mdbFirstBadged_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbRevocable_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbNext_'_update (\<lambda>_. 0) sa)))) && mask 1, mdbFirstBadged_CL = mdbFirstBadged_' (mdbPrev_'_update (\<lambda>_. 0) (mdbFirstBadged_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbRevocable_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbNext_'_update (\<lambda>_. 0) sa)))) && mask 1, mdbPrev_CL = mdbPrev_' (mdbPrev_'_update (\<lambda>_. 0) (mdbFirstBadged_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbRevocable_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbNext_'_update (\<lambda>_. 0) sa)))) && ~~ mask 3\<rparr> \<longrightarrow> sa\<lparr>ret__struct_mdb_node_C_' := v\<rparr> \<in> \<lbrace>cmdbnode_relation nullMDBNode v\<rbrace> \<inter> \<lbrace>srcSlot = cte_Ptr src\<rbrace> \<inter> ?R'2660 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb (xfdc s) v \<inter> \<lbrace>True\<rbrace>}}
 8. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdc ret__struct_cap_C. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdc; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrakk> \<Longrightarrow> \<lbrace>?R2369 newCap srcSlot destSlot oldCTE cte rv mdb y\<rbrace> updateCap src capability.NullCap \<lbrace>\<lambda>ya. (\<lambda>_. dest \<noteq> 0) and ?R2401 newCap srcSlot destSlot oldCTE cte rv mdb y xfdc ret__struct_cap_C ya and cte_wp_at' (\<lambda>_. True) (ptr_val destSlot)\<rbrace>
 9. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'2367 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C) \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(srcSlot\<rightarrow>[''cap_C''])) ret__struct_cap_C)) {s. \<forall>ya. dc ya (xfdc s) \<longrightarrow> s \<in> \<lbrace>cmdbnode_relation rv mdb\<rbrace> \<inter> \<lbrace>destSlot = cte_Ptr dest\<rbrace> \<inter> ?R'2399 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya (xfdc s) \<inter> \<lbrace>True\<rbrace>}
 10. \<And>newCap srcSlot destSlot oldCTE cte rv mdb. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb\<rbrakk> \<Longrightarrow> \<lbrace>?R2045 newCap srcSlot destSlot oldCTE cte rv\<rbrace> updateCap dest cap \<lbrace>\<lambda>y. (\<lambda>_. True) and ?R2369 newCap srcSlot destSlot oldCTE cte rv mdb y and cte_wp_at' (\<lambda>_. True) (ptr_val srcSlot)\<rbrace>
A total of 14 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc xfdcd ret__unsigneda rva xfdc ret__unsigned. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdcb; dc yb xfdcc; mdb_node_lift ret__struct_mdb_node_C = \<lparr>mdbNext_CL = 0, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) false, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) false, mdbPrev_CL = 0\<rparr>; dc yc xfdcd; dc rva xfdc\<rbrakk> \<Longrightarrow> destSlot = cte_Ptr dest
 2. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc xfdcd ret__unsigneda rva xfdc ret__unsigned. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdcb; dc yb xfdcc; mdb_node_lift ret__struct_mdb_node_C = \<lparr>mdbNext_CL = 0, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) false, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) false, mdbPrev_CL = 0\<rparr>; dc yc xfdcd; dc rva xfdc\<rbrakk> \<Longrightarrow> cmdbnode_relation rv mdb
 3. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc xfdc ret__unsigned. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdcb; dc yb xfdcc; mdb_node_lift ret__struct_mdb_node_C = \<lparr>mdbNext_CL = 0, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) false, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) false, mdbPrev_CL = 0\<rparr>; dc yc xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R3001 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc\<rbrace> updateMDB (mdbPrev rv) (mdbNext_update (\<lambda>_. dest)) \<lbrace>\<lambda>a b. is_aligned (mdbNext rv) 3 \<and> (dest \<noteq> 0 \<longrightarrow> is_aligned dest 3)\<rbrace>
 4. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc xfdcd ret__unsigned. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdcb; dc yb xfdcc; mdb_node_lift ret__struct_mdb_node_C = \<lparr>mdbNext_CL = 0, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) false, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) false, mdbPrev_CL = 0\<rparr>; dc yc xfdcd\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'2996 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc xfdcd ret__unsigned (mdbPrev_CL (mdb_node_lift mdb))) IF mdbPrev_CL (mdb_node_lift mdb) \<noteq> 0 THEN
  Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr (mdbPrev_CL (mdb_node_lift mdb))} (CALL mdb_node_ptr_set_mdbNext_'proc(mdb_Ptr &(cte_Ptr (mdbPrev_CL (mdb_node_lift mdb))\<rightarrow>[''cteMDBNode_C'']),ptr_val destSlot))
FI {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {s. \<forall>v. v = mdbNext_CL (mdb_node_lift (mdb_node_' (mdb_node_'_update (\<lambda>_. mdb) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. next_ptr_'_update (\<lambda>_. v) s \<in> UNIV}}}
 5. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdc ret__struct_mdb_node_C. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdcb; dc yb xfdc; mdb_node_lift ret__struct_mdb_node_C = \<lparr>mdbNext_CL = 0, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) false, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) false, mdbPrev_CL = 0\<rparr>\<rbrakk> \<Longrightarrow> \<lbrace>?R2662 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb\<rbrace> updateMDB src (const nullMDBNode) \<lbrace>\<lambda>a. (\<lambda>a. is_aligned (mdbPrev rv) 3 \<and> (dest \<noteq> 0 \<longrightarrow> is_aligned dest 3)) and ?R3001 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdc ret__struct_mdb_node_C a\<rbrace>
 6. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdcb; dc yb xfdcc; mdb_node_lift ret__struct_mdb_node_C = \<lparr>mdbNext_CL = 0, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) false, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) false, mdbPrev_CL = 0\<rparr>\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'2660 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C) \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])) ret__struct_mdb_node_C)) {s. \<forall>yc. dc yc (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>v. v = mdbPrev_CL (mdb_node_lift (mdb_node_' (mdb_node_'_update (\<lambda>_. mdb) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {sa. prev_ptr_'_update (\<lambda>_. v) sa \<in> UNIV \<inter> ?R'2996 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc (xfdc s) v v}}}
 7. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdc. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R2401 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya\<rbrace> updateMDB dest (const rv) \<lbrace>\<lambda>yb. (\<lambda>_. src \<noteq> 0) and ?R2662 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdc yb and cte_wp_at' (\<lambda>_. True) (ptr_val srcSlot)\<rbrace>
 8. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdcb\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'2399 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb) \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(destSlot\<rightarrow>[''cteMDBNode_C''])) mdb)) {s. \<forall>yb. dc yb (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>v. mdb_node_lift v = \<lparr>mdbNext_CL = mdbNext_' (mdbPrev_'_update (\<lambda>_. 0) (mdbFirstBadged_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbRevocable_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbNext_'_update (\<lambda>_. 0) sa)))) && ~~ mask 3, mdbRevocable_CL = mdbRevocable_' (mdbPrev_'_update (\<lambda>_. 0) (mdbFirstBadged_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbRevocable_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbNext_'_update (\<lambda>_. 0) sa)))) && mask 1, mdbFirstBadged_CL = mdbFirstBadged_' (mdbPrev_'_update (\<lambda>_. 0) (mdbFirstBadged_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbRevocable_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbNext_'_update (\<lambda>_. 0) sa)))) && mask 1, mdbPrev_CL = mdbPrev_' (mdbPrev_'_update (\<lambda>_. 0) (mdbFirstBadged_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbRevocable_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbNext_'_update (\<lambda>_. 0) sa)))) && ~~ mask 3\<rparr> \<longrightarrow> sa\<lparr>ret__struct_mdb_node_C_' := v\<rparr> \<in> \<lbrace>cmdbnode_relation nullMDBNode v\<rbrace> \<inter> \<lbrace>srcSlot = cte_Ptr src\<rbrace> \<inter> ?R'2660 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb (xfdc s) v \<inter> \<lbrace>True\<rbrace>}}
 9. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdc ret__struct_cap_C. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdc; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrakk> \<Longrightarrow> \<lbrace>?R2369 newCap srcSlot destSlot oldCTE cte rv mdb y\<rbrace> updateCap src capability.NullCap \<lbrace>\<lambda>ya. (\<lambda>_. dest \<noteq> 0) and ?R2401 newCap srcSlot destSlot oldCTE cte rv mdb y xfdc ret__struct_cap_C ya and cte_wp_at' (\<lambda>_. True) (ptr_val destSlot)\<rbrace>
 10. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'2367 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C) \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(srcSlot\<rightarrow>[''cap_C''])) ret__struct_cap_C)) {s. \<forall>ya. dc ya (xfdc s) \<longrightarrow> s \<in> \<lbrace>cmdbnode_relation rv mdb\<rbrace> \<inter> \<lbrace>destSlot = cte_Ptr dest\<rbrace> \<inter> ?R'2399 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya (xfdc s) \<inter> \<lbrace>True\<rbrace>}
A total of 15 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc xfdcd ret__unsigneda rva xfdc ret__unsigned. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdcb; dc yb xfdcc; mdb_node_lift ret__struct_mdb_node_C = \<lparr>mdbNext_CL = 0, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) false, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) false, mdbPrev_CL = 0\<rparr>; dc yc xfdcd; dc rva xfdc\<rbrakk> \<Longrightarrow> cmdbnode_relation rv mdb
 2. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc xfdc ret__unsigned. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdcb; dc yb xfdcc; mdb_node_lift ret__struct_mdb_node_C = \<lparr>mdbNext_CL = 0, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) false, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) false, mdbPrev_CL = 0\<rparr>; dc yc xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R3001 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc\<rbrace> updateMDB (mdbPrev rv) (mdbNext_update (\<lambda>_. dest)) \<lbrace>\<lambda>a b. is_aligned (mdbNext rv) 3 \<and> (dest \<noteq> 0 \<longrightarrow> is_aligned dest 3)\<rbrace>
 3. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc xfdcd ret__unsigned. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdcb; dc yb xfdcc; mdb_node_lift ret__struct_mdb_node_C = \<lparr>mdbNext_CL = 0, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) false, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) false, mdbPrev_CL = 0\<rparr>; dc yc xfdcd\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'2996 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc xfdcd ret__unsigned (mdbPrev_CL (mdb_node_lift mdb))) IF mdbPrev_CL (mdb_node_lift mdb) \<noteq> 0 THEN
  Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr (mdbPrev_CL (mdb_node_lift mdb))} (CALL mdb_node_ptr_set_mdbNext_'proc(mdb_Ptr &(cte_Ptr (mdbPrev_CL (mdb_node_lift mdb))\<rightarrow>[''cteMDBNode_C'']),ptr_val destSlot))
FI {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {s. \<forall>v. v = mdbNext_CL (mdb_node_lift (mdb_node_' (mdb_node_'_update (\<lambda>_. mdb) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. next_ptr_'_update (\<lambda>_. v) s \<in> UNIV}}}
 4. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdc ret__struct_mdb_node_C. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdcb; dc yb xfdc; mdb_node_lift ret__struct_mdb_node_C = \<lparr>mdbNext_CL = 0, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) false, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) false, mdbPrev_CL = 0\<rparr>\<rbrakk> \<Longrightarrow> \<lbrace>?R2662 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb\<rbrace> updateMDB src (const nullMDBNode) \<lbrace>\<lambda>a. (\<lambda>a. is_aligned (mdbPrev rv) 3 \<and> (dest \<noteq> 0 \<longrightarrow> is_aligned dest 3)) and ?R3001 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdc ret__struct_mdb_node_C a\<rbrace>
 5. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdcb; dc yb xfdcc; mdb_node_lift ret__struct_mdb_node_C = \<lparr>mdbNext_CL = 0, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) false, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) false, mdbPrev_CL = 0\<rparr>\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'2660 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C) \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])) ret__struct_mdb_node_C)) {s. \<forall>yc. dc yc (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>v. v = mdbPrev_CL (mdb_node_lift (mdb_node_' (mdb_node_'_update (\<lambda>_. mdb) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {sa. prev_ptr_'_update (\<lambda>_. v) sa \<in> UNIV \<inter> ?R'2996 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc (xfdc s) v v}}}
 6. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdc. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R2401 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya\<rbrace> updateMDB dest (const rv) \<lbrace>\<lambda>yb. (\<lambda>_. src \<noteq> 0) and ?R2662 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdc yb and cte_wp_at' (\<lambda>_. True) (ptr_val srcSlot)\<rbrace>
 7. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdcb\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'2399 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb) \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(destSlot\<rightarrow>[''cteMDBNode_C''])) mdb)) {s. \<forall>yb. dc yb (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>v. mdb_node_lift v = \<lparr>mdbNext_CL = mdbNext_' (mdbPrev_'_update (\<lambda>_. 0) (mdbFirstBadged_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbRevocable_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbNext_'_update (\<lambda>_. 0) sa)))) && ~~ mask 3, mdbRevocable_CL = mdbRevocable_' (mdbPrev_'_update (\<lambda>_. 0) (mdbFirstBadged_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbRevocable_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbNext_'_update (\<lambda>_. 0) sa)))) && mask 1, mdbFirstBadged_CL = mdbFirstBadged_' (mdbPrev_'_update (\<lambda>_. 0) (mdbFirstBadged_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbRevocable_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbNext_'_update (\<lambda>_. 0) sa)))) && mask 1, mdbPrev_CL = mdbPrev_' (mdbPrev_'_update (\<lambda>_. 0) (mdbFirstBadged_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbRevocable_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbNext_'_update (\<lambda>_. 0) sa)))) && ~~ mask 3\<rparr> \<longrightarrow> sa\<lparr>ret__struct_mdb_node_C_' := v\<rparr> \<in> \<lbrace>cmdbnode_relation nullMDBNode v\<rbrace> \<inter> \<lbrace>srcSlot = cte_Ptr src\<rbrace> \<inter> ?R'2660 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb (xfdc s) v \<inter> \<lbrace>True\<rbrace>}}
 8. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdc ret__struct_cap_C. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdc; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrakk> \<Longrightarrow> \<lbrace>?R2369 newCap srcSlot destSlot oldCTE cte rv mdb y\<rbrace> updateCap src capability.NullCap \<lbrace>\<lambda>ya. (\<lambda>_. dest \<noteq> 0) and ?R2401 newCap srcSlot destSlot oldCTE cte rv mdb y xfdc ret__struct_cap_C ya and cte_wp_at' (\<lambda>_. True) (ptr_val destSlot)\<rbrace>
 9. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'2367 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C) \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(srcSlot\<rightarrow>[''cap_C''])) ret__struct_cap_C)) {s. \<forall>ya. dc ya (xfdc s) \<longrightarrow> s \<in> \<lbrace>cmdbnode_relation rv mdb\<rbrace> \<inter> \<lbrace>destSlot = cte_Ptr dest\<rbrace> \<inter> ?R'2399 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya (xfdc s) \<inter> \<lbrace>True\<rbrace>}
 10. \<And>newCap srcSlot destSlot oldCTE cte rv mdb. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb\<rbrakk> \<Longrightarrow> \<lbrace>?R2045 newCap srcSlot destSlot oldCTE cte rv\<rbrace> updateCap dest cap \<lbrace>\<lambda>y. (\<lambda>_. True) and ?R2369 newCap srcSlot destSlot oldCTE cte rv mdb y and cte_wp_at' (\<lambda>_. True) (ptr_val srcSlot)\<rbrace>
A total of 14 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc xfdc ret__unsigned. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdcb; dc yb xfdcc; mdb_node_lift ret__struct_mdb_node_C = \<lparr>mdbNext_CL = 0, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) false, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) false, mdbPrev_CL = 0\<rparr>; dc yc xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R3001 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc\<rbrace> updateMDB (mdbPrev rv) (mdbNext_update (\<lambda>_. dest)) \<lbrace>\<lambda>a b. is_aligned (mdbNext rv) 3 \<and> (dest \<noteq> 0 \<longrightarrow> is_aligned dest 3)\<rbrace>
 2. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc xfdcd ret__unsigned. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdcb; dc yb xfdcc; mdb_node_lift ret__struct_mdb_node_C = \<lparr>mdbNext_CL = 0, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) false, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) false, mdbPrev_CL = 0\<rparr>; dc yc xfdcd\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'2996 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc xfdcd ret__unsigned (mdbPrev_CL (mdb_node_lift mdb))) IF mdbPrev_CL (mdb_node_lift mdb) \<noteq> 0 THEN
  Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr (mdbPrev_CL (mdb_node_lift mdb))} (CALL mdb_node_ptr_set_mdbNext_'proc(mdb_Ptr &(cte_Ptr (mdbPrev_CL (mdb_node_lift mdb))\<rightarrow>[''cteMDBNode_C'']),ptr_val destSlot))
FI {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {s. \<forall>v. v = mdbNext_CL (mdb_node_lift (mdb_node_' (mdb_node_'_update (\<lambda>_. mdb) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. next_ptr_'_update (\<lambda>_. v) s \<in> UNIV}}}
 3. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdc ret__struct_mdb_node_C. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdcb; dc yb xfdc; mdb_node_lift ret__struct_mdb_node_C = \<lparr>mdbNext_CL = 0, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) false, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) false, mdbPrev_CL = 0\<rparr>\<rbrakk> \<Longrightarrow> \<lbrace>?R2662 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb\<rbrace> updateMDB src (const nullMDBNode) \<lbrace>\<lambda>a. (\<lambda>a. is_aligned (mdbPrev rv) 3 \<and> (dest \<noteq> 0 \<longrightarrow> is_aligned dest 3)) and ?R3001 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdc ret__struct_mdb_node_C a\<rbrace>
 4. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdcb; dc yb xfdcc; mdb_node_lift ret__struct_mdb_node_C = \<lparr>mdbNext_CL = 0, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) false, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) false, mdbPrev_CL = 0\<rparr>\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'2660 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C) \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])) ret__struct_mdb_node_C)) {s. \<forall>yc. dc yc (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>v. v = mdbPrev_CL (mdb_node_lift (mdb_node_' (mdb_node_'_update (\<lambda>_. mdb) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {sa. prev_ptr_'_update (\<lambda>_. v) sa \<in> UNIV \<inter> ?R'2996 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb xfdcc ret__struct_mdb_node_C yc (xfdc s) v v}}}
 5. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdc. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R2401 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya\<rbrace> updateMDB dest (const rv) \<lbrace>\<lambda>yb. (\<lambda>_. src \<noteq> 0) and ?R2662 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdc yb and cte_wp_at' (\<lambda>_. True) (ptr_val srcSlot)\<rbrace>
 6. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap; dc ya xfdcb\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'2399 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb) \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(destSlot\<rightarrow>[''cteMDBNode_C''])) mdb)) {s. \<forall>yb. dc yb (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>v. mdb_node_lift v = \<lparr>mdbNext_CL = mdbNext_' (mdbPrev_'_update (\<lambda>_. 0) (mdbFirstBadged_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbRevocable_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbNext_'_update (\<lambda>_. 0) sa)))) && ~~ mask 3, mdbRevocable_CL = mdbRevocable_' (mdbPrev_'_update (\<lambda>_. 0) (mdbFirstBadged_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbRevocable_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbNext_'_update (\<lambda>_. 0) sa)))) && mask 1, mdbFirstBadged_CL = mdbFirstBadged_' (mdbPrev_'_update (\<lambda>_. 0) (mdbFirstBadged_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbRevocable_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbNext_'_update (\<lambda>_. 0) sa)))) && mask 1, mdbPrev_CL = mdbPrev_' (mdbPrev_'_update (\<lambda>_. 0) (mdbFirstBadged_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbRevocable_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (mdbNext_'_update (\<lambda>_. 0) sa)))) && ~~ mask 3\<rparr> \<longrightarrow> sa\<lparr>ret__struct_mdb_node_C_' := v\<rparr> \<in> \<lbrace>cmdbnode_relation nullMDBNode v\<rbrace> \<inter> \<lbrace>srcSlot = cte_Ptr src\<rbrace> \<inter> ?R'2660 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya xfdcb yb (xfdc s) v \<inter> \<lbrace>True\<rbrace>}}
 7. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdc ret__struct_cap_C. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdc; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrakk> \<Longrightarrow> \<lbrace>?R2369 newCap srcSlot destSlot oldCTE cte rv mdb y\<rbrace> updateCap src capability.NullCap \<lbrace>\<lambda>ya. (\<lambda>_. dest \<noteq> 0) and ?R2401 newCap srcSlot destSlot oldCTE cte rv mdb y xfdc ret__struct_cap_C ya and cte_wp_at' (\<lambda>_. True) (ptr_val destSlot)\<rbrace>
 8. \<And>newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb; dc y xfdca; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'2367 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C) \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(srcSlot\<rightarrow>[''cap_C''])) ret__struct_cap_C)) {s. \<forall>ya. dc ya (xfdc s) \<longrightarrow> s \<in> \<lbrace>cmdbnode_relation rv mdb\<rbrace> \<inter> \<lbrace>destSlot = cte_Ptr dest\<rbrace> \<inter> ?R'2399 newCap srcSlot destSlot oldCTE cte rv mdb y xfdca ret__struct_cap_C ya (xfdc s) \<inter> \<lbrace>True\<rbrace>}
 9. \<And>newCap srcSlot destSlot oldCTE cte rv mdb. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb\<rbrakk> \<Longrightarrow> \<lbrace>?R2045 newCap srcSlot destSlot oldCTE cte rv\<rbrace> updateCap dest cap \<lbrace>\<lambda>y. (\<lambda>_. True) and ?R2369 newCap srcSlot destSlot oldCTE cte rv mdb y and cte_wp_at' (\<lambda>_. True) (ptr_val srcSlot)\<rbrace>
 10. \<And>newCap srcSlot destSlot oldCTE cte rv mdb. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; cteCap oldCTE = capability.NullCap; mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer; cmdbnode_relation rv mdb\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'2043 newCap srcSlot destSlot oldCTE cte rv mdb) \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(destSlot\<rightarrow>[''cap_C''])) newCap)) {s. \<forall>y. dc y (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>v. cap_get_tag v = SCAST(32 signed \<rightarrow> 32) cap_null_cap \<longrightarrow> sa\<lparr>ret__struct_cap_C_' := v\<rparr> \<in> \<lbrace>ccap_relation capability.NullCap v\<rbrace> \<inter> \<lbrace>srcSlot = cte_Ptr src\<rbrace> \<inter> ?R'2367 newCap srcSlot destSlot oldCTE cte rv mdb y (xfdc s) v \<inter> \<lbrace>True\<rbrace>}}
A total of 13 subgoals... proof (prove)
goal (1 subgoal):
 1. \<And>newCap srcSlot destSlot s s'. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s dest = Some cte \<longrightarrow> (\<forall>ctea. ctes_of s src = Some ctea \<longrightarrow> ((\<lambda>s. ctes_of s (?ptr1701 newCap srcSlot destSlot cte ctea) = Some ctea) and ((\<lambda>_. True) and (\<lambda>s. True \<and> dest \<noteq> 0 \<and> src \<noteq> 0 \<and> ((is_aligned (mdbPrev (cteMDBNode ctea)) 3 \<and> (dest \<noteq> 0 \<longrightarrow> is_aligned dest 3)) \<and> is_aligned (mdbNext (cteMDBNode ctea)) 3 \<and> (dest \<noteq> 0 \<longrightarrow> is_aligned dest 3)) \<and> cte_wp_at' (\<lambda>_. True) (ptr_val srcSlot) s \<and> cte_wp_at' (\<lambda>_. True) (ptr_val destSlot) s \<and> cte_wp_at' (\<lambda>_. True) (ptr_val srcSlot) s) and cte_wp_at' (\<lambda>_. True) (ptr_val destSlot)) and cte_wp_at' (\<lambda>_. True) (ptr_val srcSlot)) s)) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr dest) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. \<forall>cte'a. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr src) = Some cte'a \<and> cl_valid_cte cte'a \<longrightarrow> s \<in> \<lbrace>ptr_val srcSlot = ?ptr1701 newCap srcSlot destSlot (cte_to_H cte') (cte_to_H cte'a)\<rbrace> \<inter> {s. \<forall>rv. cmdbnode_relation rv (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C'']))) \<longrightarrow> ccap_relation cap newCap \<and> destSlot = cte_Ptr dest \<and> (\<forall>y. dc y (xfdc (globals_update (t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(destSlot\<rightarrow>[''cap_C''])) newCap))) (mdb_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C'']))) s))) \<longrightarrow> (\<forall>v. cap_get_tag v = SCAST(32 signed \<rightarrow> 32) cap_null_cap \<longrightarrow> ccap_relation capability.NullCap v \<and> srcSlot = cte_Ptr src \<and> (\<forall>y. dc y (xfdc (globals_update (t_hrs_'_update (\<lambda>x. hrs_mem_update (heap_update (cap_Ptr &(srcSlot\<rightarrow>[''cap_C''])) v) (hrs_mem_update (heap_update (cap_Ptr &(destSlot\<rightarrow>[''cap_C''])) newCap) x))) (s\<lparr>mdb_' := h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])), ret__struct_cap_C_' := v\<rparr>))) \<longrightarrow> cmdbnode_relation rv (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C'']))) \<and> destSlot = cte_Ptr dest \<and> (\<forall>y. dc y (xfdc (globals_update (t_hrs_'_update (\<lambda>x. hrs_mem_update (heap_update (mdb_Ptr &(destSlot\<rightarrow>[''cteMDBNode_C''])) (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])))) (hrs_mem_update (heap_update (cap_Ptr &(srcSlot\<rightarrow>[''cap_C''])) v) (hrs_mem_update (heap_update (cap_Ptr &(destSlot\<rightarrow>[''cap_C''])) newCap) x)))) (s\<lparr>mdb_' := h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])), ret__struct_cap_C_' := v\<rparr>))) \<longrightarrow> (\<forall>va. mdb_node_lift va = \<lparr>mdbNext_CL = 0 && ~~ mask 3, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) false && mask 1, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) false && mask 1, mdbPrev_CL = 0 && ~~ mask 3\<rparr> \<longrightarrow> cmdbnode_relation nullMDBNode va \<and> srcSlot = cte_Ptr src \<and> (\<forall>y. dc y (xfdc (globals_update (t_hrs_'_update (\<lambda>x. hrs_mem_update (heap_update (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])) va) (hrs_mem_update (heap_update (mdb_Ptr &(destSlot\<rightarrow>[''cteMDBNode_C''])) (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])))) (hrs_mem_update (heap_update (cap_Ptr &(srcSlot\<rightarrow>[''cap_C''])) v) (hrs_mem_update (heap_update (cap_Ptr &(destSlot\<rightarrow>[''cap_C''])) newCap) x))))) (s\<lparr>mdb_' := h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])), ret__struct_cap_C_' := v, ret__struct_mdb_node_C_' := va\<rparr>))) \<longrightarrow> (\<forall>vb. vb = mdbPrev_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])))) \<longrightarrow> True \<and> (vb \<noteq> 0 \<longrightarrow> hrs_htd (hrs_mem_update (heap_update (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])) va) (hrs_mem_update (heap_update (mdb_Ptr &(destSlot\<rightarrow>[''cteMDBNode_C''])) (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])))) (hrs_mem_update (heap_update (cap_Ptr &(srcSlot\<rightarrow>[''cap_C''])) v) (hrs_mem_update (heap_update (cap_Ptr &(destSlot\<rightarrow>[''cap_C''])) newCap) (t_hrs_' (globals s)))))) \<Turnstile>\<^sub>t cte_Ptr vb \<longrightarrow> hrs_htd (hrs_mem_update (heap_update (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])) va) (hrs_mem_update (heap_update (mdb_Ptr &(destSlot\<rightarrow>[''cteMDBNode_C''])) (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])))) (hrs_mem_update (heap_update (cap_Ptr &(srcSlot\<rightarrow>[''cap_C''])) v) (hrs_mem_update (heap_update (cap_Ptr &(destSlot\<rightarrow>[''cap_C''])) newCap) (t_hrs_' (globals s)))))) \<Turnstile>\<^sub>t cparent (mdb_Ptr &(cte_Ptr vb\<rightarrow>[''cteMDBNode_C''])) [''cteMDBNode_C'']) \<and> (\<not> vb \<noteq> 0 \<longrightarrow> (\<forall>rv. dc rv (xfdc (prev_ptr_'_update (\<lambda>_. vb) (globals_update (t_hrs_'_update (\<lambda>x. hrs_mem_update (heap_update (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])) va) (hrs_mem_update (heap_update (mdb_Ptr &(destSlot\<rightarrow>[''cteMDBNode_C''])) (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])))) (hrs_mem_update (heap_update (cap_Ptr &(srcSlot\<rightarrow>[''cap_C''])) v) (hrs_mem_update (heap_update (cap_Ptr &(destSlot\<rightarrow>[''cap_C''])) newCap) x))))) (s\<lparr>mdb_' := h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])), ret__struct_cap_C_' := v, ret__struct_mdb_node_C_' := va\<rparr>)\<lparr>ret__unsigned_' := vb\<rparr>))) \<longrightarrow> (\<forall>v. v = mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])))) \<longrightarrow> True))))) \<and> True)) \<and> True) \<and> True)) \<and> True} \<inter> \<lbrace>True\<rbrace>}} proof (prove)
goal (2 subgoals):
 1. \<And>newCap srcSlot destSlot s s'. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> \<forall>cte. ctes_of s dest = Some cte \<longrightarrow> (\<forall>ctea. ctes_of s src = Some ctea \<longrightarrow> ((\<lambda>s. ctes_of s (?ptr1701 newCap srcSlot destSlot cte ctea) = Some ctea) and ((\<lambda>_. True) and (\<lambda>s. True \<and> dest \<noteq> 0 \<and> src \<noteq> 0 \<and> ((is_aligned (mdbPrev (cteMDBNode ctea)) 3 \<and> (dest \<noteq> 0 \<longrightarrow> is_aligned dest 3)) \<and> is_aligned (mdbNext (cteMDBNode ctea)) 3 \<and> (dest \<noteq> 0 \<longrightarrow> is_aligned dest 3)) \<and> cte_wp_at' (\<lambda>_. True) (ptr_val srcSlot) s \<and> cte_wp_at' (\<lambda>_. True) (ptr_val destSlot) s \<and> cte_wp_at' (\<lambda>_. True) (ptr_val srcSlot) s) and cte_wp_at' (\<lambda>_. True) (ptr_val destSlot)) and cte_wp_at' (\<lambda>_. True) (ptr_val srcSlot)) s)
 2. \<And>newCap srcSlot destSlot s s'. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr dest) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. \<forall>cte'a. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr src) = Some cte'a \<and> cl_valid_cte cte'a \<longrightarrow> s \<in> \<lbrace>ptr_val srcSlot = ?ptr1701 newCap srcSlot destSlot (cte_to_H cte') (cte_to_H cte'a)\<rbrace> \<inter> {s. \<forall>rv. cmdbnode_relation rv (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C'']))) \<longrightarrow> ccap_relation cap newCap \<and> destSlot = cte_Ptr dest \<and> (\<forall>y. dc y (xfdc (globals_update (t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(destSlot\<rightarrow>[''cap_C''])) newCap))) (mdb_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C'']))) s))) \<longrightarrow> (\<forall>v. cap_get_tag v = SCAST(32 signed \<rightarrow> 32) cap_null_cap \<longrightarrow> ccap_relation capability.NullCap v \<and> srcSlot = cte_Ptr src \<and> (\<forall>y. dc y (xfdc (globals_update (t_hrs_'_update (\<lambda>x. hrs_mem_update (heap_update (cap_Ptr &(srcSlot\<rightarrow>[''cap_C''])) v) (hrs_mem_update (heap_update (cap_Ptr &(destSlot\<rightarrow>[''cap_C''])) newCap) x))) (s\<lparr>mdb_' := h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])), ret__struct_cap_C_' := v\<rparr>))) \<longrightarrow> cmdbnode_relation rv (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C'']))) \<and> destSlot = cte_Ptr dest \<and> (\<forall>y. dc y (xfdc (globals_update (t_hrs_'_update (\<lambda>x. hrs_mem_update (heap_update (mdb_Ptr &(destSlot\<rightarrow>[''cteMDBNode_C''])) (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])))) (hrs_mem_update (heap_update (cap_Ptr &(srcSlot\<rightarrow>[''cap_C''])) v) (hrs_mem_update (heap_update (cap_Ptr &(destSlot\<rightarrow>[''cap_C''])) newCap) x)))) (s\<lparr>mdb_' := h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])), ret__struct_cap_C_' := v\<rparr>))) \<longrightarrow> (\<forall>va. mdb_node_lift va = \<lparr>mdbNext_CL = 0 && ~~ mask 3, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) false && mask 1, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) false && mask 1, mdbPrev_CL = 0 && ~~ mask 3\<rparr> \<longrightarrow> cmdbnode_relation nullMDBNode va \<and> srcSlot = cte_Ptr src \<and> (\<forall>y. dc y (xfdc (globals_update (t_hrs_'_update (\<lambda>x. hrs_mem_update (heap_update (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])) va) (hrs_mem_update (heap_update (mdb_Ptr &(destSlot\<rightarrow>[''cteMDBNode_C''])) (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])))) (hrs_mem_update (heap_update (cap_Ptr &(srcSlot\<rightarrow>[''cap_C''])) v) (hrs_mem_update (heap_update (cap_Ptr &(destSlot\<rightarrow>[''cap_C''])) newCap) x))))) (s\<lparr>mdb_' := h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])), ret__struct_cap_C_' := v, ret__struct_mdb_node_C_' := va\<rparr>))) \<longrightarrow> (\<forall>vb. vb = mdbPrev_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])))) \<longrightarrow> True \<and> (vb \<noteq> 0 \<longrightarrow> hrs_htd (hrs_mem_update (heap_update (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])) va) (hrs_mem_update (heap_update (mdb_Ptr &(destSlot\<rightarrow>[''cteMDBNode_C''])) (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])))) (hrs_mem_update (heap_update (cap_Ptr &(srcSlot\<rightarrow>[''cap_C''])) v) (hrs_mem_update (heap_update (cap_Ptr &(destSlot\<rightarrow>[''cap_C''])) newCap) (t_hrs_' (globals s)))))) \<Turnstile>\<^sub>t cte_Ptr vb \<longrightarrow> hrs_htd (hrs_mem_update (heap_update (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])) va) (hrs_mem_update (heap_update (mdb_Ptr &(destSlot\<rightarrow>[''cteMDBNode_C''])) (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])))) (hrs_mem_update (heap_update (cap_Ptr &(srcSlot\<rightarrow>[''cap_C''])) v) (hrs_mem_update (heap_update (cap_Ptr &(destSlot\<rightarrow>[''cap_C''])) newCap) (t_hrs_' (globals s)))))) \<Turnstile>\<^sub>t cparent (mdb_Ptr &(cte_Ptr vb\<rightarrow>[''cteMDBNode_C''])) [''cteMDBNode_C'']) \<and> (\<not> vb \<noteq> 0 \<longrightarrow> (\<forall>rv. dc rv (xfdc (prev_ptr_'_update (\<lambda>_. vb) (globals_update (t_hrs_'_update (\<lambda>x. hrs_mem_update (heap_update (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])) va) (hrs_mem_update (heap_update (mdb_Ptr &(destSlot\<rightarrow>[''cteMDBNode_C''])) (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])))) (hrs_mem_update (heap_update (cap_Ptr &(srcSlot\<rightarrow>[''cap_C''])) v) (hrs_mem_update (heap_update (cap_Ptr &(destSlot\<rightarrow>[''cap_C''])) newCap) x))))) (s\<lparr>mdb_' := h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])), ret__struct_cap_C_' := v, ret__struct_mdb_node_C_' := va\<rparr>)\<lparr>ret__unsigned_' := vb\<rparr>))) \<longrightarrow> (\<forall>v. v = mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])))) \<longrightarrow> True))))) \<and> True)) \<and> True) \<and> True)) \<and> True} \<inter> \<lbrace>True\<rbrace>}} proof (prove)
goal (2 subgoals):
 1. \<And>newCap s s' cte ctea. \<lbrakk>ccap_relation cap newCap; (s, s') \<in> rf_sr; valid_mdb' s; pspace_aligned' s; ctes_of s dest = Some cte; ctes_of s src = Some ctea\<rbrakk> \<Longrightarrow> ctes_of s (?ptr1701 newCap (cte_Ptr src) (cte_Ptr dest) cte ctea) = Some ctea \<and> is_aligned (mdbPrev (cteMDBNode ctea)) 3 \<and> is_aligned (mdbNext (cteMDBNode ctea)) 3
 2. \<And>newCap srcSlot destSlot s s'. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr dest) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. \<forall>cte'a. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr src) = Some cte'a \<and> cl_valid_cte cte'a \<longrightarrow> s \<in> \<lbrace>ptr_val srcSlot = ?ptr1701 newCap srcSlot destSlot (cte_to_H cte') (cte_to_H cte'a)\<rbrace> \<inter> {s. \<forall>rv. cmdbnode_relation rv (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C'']))) \<longrightarrow> ccap_relation cap newCap \<and> destSlot = cte_Ptr dest \<and> (\<forall>y. dc y (xfdc (globals_update (t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(destSlot\<rightarrow>[''cap_C''])) newCap))) (mdb_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C'']))) s))) \<longrightarrow> (\<forall>v. cap_get_tag v = SCAST(32 signed \<rightarrow> 32) cap_null_cap \<longrightarrow> ccap_relation capability.NullCap v \<and> srcSlot = cte_Ptr src \<and> (\<forall>y. dc y (xfdc (globals_update (t_hrs_'_update (\<lambda>x. hrs_mem_update (heap_update (cap_Ptr &(srcSlot\<rightarrow>[''cap_C''])) v) (hrs_mem_update (heap_update (cap_Ptr &(destSlot\<rightarrow>[''cap_C''])) newCap) x))) (s\<lparr>mdb_' := h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])), ret__struct_cap_C_' := v\<rparr>))) \<longrightarrow> cmdbnode_relation rv (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C'']))) \<and> destSlot = cte_Ptr dest \<and> (\<forall>y. dc y (xfdc (globals_update (t_hrs_'_update (\<lambda>x. hrs_mem_update (heap_update (mdb_Ptr &(destSlot\<rightarrow>[''cteMDBNode_C''])) (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])))) (hrs_mem_update (heap_update (cap_Ptr &(srcSlot\<rightarrow>[''cap_C''])) v) (hrs_mem_update (heap_update (cap_Ptr &(destSlot\<rightarrow>[''cap_C''])) newCap) x)))) (s\<lparr>mdb_' := h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])), ret__struct_cap_C_' := v\<rparr>))) \<longrightarrow> (\<forall>va. mdb_node_lift va = \<lparr>mdbNext_CL = 0 && ~~ mask 3, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) false && mask 1, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) false && mask 1, mdbPrev_CL = 0 && ~~ mask 3\<rparr> \<longrightarrow> cmdbnode_relation nullMDBNode va \<and> srcSlot = cte_Ptr src \<and> (\<forall>y. dc y (xfdc (globals_update (t_hrs_'_update (\<lambda>x. hrs_mem_update (heap_update (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])) va) (hrs_mem_update (heap_update (mdb_Ptr &(destSlot\<rightarrow>[''cteMDBNode_C''])) (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])))) (hrs_mem_update (heap_update (cap_Ptr &(srcSlot\<rightarrow>[''cap_C''])) v) (hrs_mem_update (heap_update (cap_Ptr &(destSlot\<rightarrow>[''cap_C''])) newCap) x))))) (s\<lparr>mdb_' := h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])), ret__struct_cap_C_' := v, ret__struct_mdb_node_C_' := va\<rparr>))) \<longrightarrow> (\<forall>vb. vb = mdbPrev_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])))) \<longrightarrow> True \<and> (vb \<noteq> 0 \<longrightarrow> hrs_htd (hrs_mem_update (heap_update (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])) va) (hrs_mem_update (heap_update (mdb_Ptr &(destSlot\<rightarrow>[''cteMDBNode_C''])) (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])))) (hrs_mem_update (heap_update (cap_Ptr &(srcSlot\<rightarrow>[''cap_C''])) v) (hrs_mem_update (heap_update (cap_Ptr &(destSlot\<rightarrow>[''cap_C''])) newCap) (t_hrs_' (globals s)))))) \<Turnstile>\<^sub>t cte_Ptr vb \<longrightarrow> hrs_htd (hrs_mem_update (heap_update (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])) va) (hrs_mem_update (heap_update (mdb_Ptr &(destSlot\<rightarrow>[''cteMDBNode_C''])) (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])))) (hrs_mem_update (heap_update (cap_Ptr &(srcSlot\<rightarrow>[''cap_C''])) v) (hrs_mem_update (heap_update (cap_Ptr &(destSlot\<rightarrow>[''cap_C''])) newCap) (t_hrs_' (globals s)))))) \<Turnstile>\<^sub>t cparent (mdb_Ptr &(cte_Ptr vb\<rightarrow>[''cteMDBNode_C''])) [''cteMDBNode_C'']) \<and> (\<not> vb \<noteq> 0 \<longrightarrow> (\<forall>rv. dc rv (xfdc (prev_ptr_'_update (\<lambda>_. vb) (globals_update (t_hrs_'_update (\<lambda>x. hrs_mem_update (heap_update (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])) va) (hrs_mem_update (heap_update (mdb_Ptr &(destSlot\<rightarrow>[''cteMDBNode_C''])) (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])))) (hrs_mem_update (heap_update (cap_Ptr &(srcSlot\<rightarrow>[''cap_C''])) v) (hrs_mem_update (heap_update (cap_Ptr &(destSlot\<rightarrow>[''cap_C''])) newCap) x))))) (s\<lparr>mdb_' := h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])), ret__struct_cap_C_' := v, ret__struct_mdb_node_C_' := va\<rparr>)\<lparr>ret__unsigned_' := vb\<rparr>))) \<longrightarrow> (\<forall>v. v = mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])))) \<longrightarrow> True))))) \<and> True)) \<and> True) \<and> True)) \<and> True} \<inter> \<lbrace>True\<rbrace>}} proof (prove)
goal (3 subgoals):
 1. \<And>newCap s s' cte ctea. \<lbrakk>ccap_relation cap newCap; (s, s') \<in> rf_sr; valid_mdb' s; pspace_aligned' s; ctes_of s dest = Some cte; ctes_of s src = Some ctea\<rbrakk> \<Longrightarrow> is_aligned (mdbPrev (cteMDBNode ctea)) 3
 2. \<And>newCap s s' cte ctea. \<lbrakk>ccap_relation cap newCap; (s, s') \<in> rf_sr; valid_mdb' s; pspace_aligned' s; ctes_of s dest = Some cte; ctes_of s src = Some ctea\<rbrakk> \<Longrightarrow> is_aligned (mdbNext (cteMDBNode ctea)) 3
 3. \<And>newCap srcSlot destSlot s s'. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr dest) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr src) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> \<lbrace>ptr_val srcSlot = src\<rbrace> \<inter> {s. \<forall>rv. cmdbnode_relation rv (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C'']))) \<longrightarrow> ccap_relation cap newCap \<and> destSlot = cte_Ptr dest \<and> (\<forall>y. dc y (xfdc (globals_update (t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(destSlot\<rightarrow>[''cap_C''])) newCap))) (mdb_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C'']))) s))) \<longrightarrow> (\<forall>v. cap_get_tag v = SCAST(32 signed \<rightarrow> 32) cap_null_cap \<longrightarrow> ccap_relation capability.NullCap v \<and> srcSlot = cte_Ptr src \<and> (\<forall>y. dc y (xfdc (globals_update (t_hrs_'_update (\<lambda>x. hrs_mem_update (heap_update (cap_Ptr &(srcSlot\<rightarrow>[''cap_C''])) v) (hrs_mem_update (heap_update (cap_Ptr &(destSlot\<rightarrow>[''cap_C''])) newCap) x))) (s\<lparr>mdb_' := h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])), ret__struct_cap_C_' := v\<rparr>))) \<longrightarrow> cmdbnode_relation rv (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C'']))) \<and> destSlot = cte_Ptr dest \<and> (\<forall>y. dc y (xfdc (globals_update (t_hrs_'_update (\<lambda>x. hrs_mem_update (heap_update (mdb_Ptr &(destSlot\<rightarrow>[''cteMDBNode_C''])) (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])))) (hrs_mem_update (heap_update (cap_Ptr &(srcSlot\<rightarrow>[''cap_C''])) v) (hrs_mem_update (heap_update (cap_Ptr &(destSlot\<rightarrow>[''cap_C''])) newCap) x)))) (s\<lparr>mdb_' := h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])), ret__struct_cap_C_' := v\<rparr>))) \<longrightarrow> (\<forall>va. mdb_node_lift va = \<lparr>mdbNext_CL = 0 && ~~ mask 3, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) false && mask 1, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) false && mask 1, mdbPrev_CL = 0 && ~~ mask 3\<rparr> \<longrightarrow> cmdbnode_relation nullMDBNode va \<and> srcSlot = cte_Ptr src \<and> (\<forall>y. dc y (xfdc (globals_update (t_hrs_'_update (\<lambda>x. hrs_mem_update (heap_update (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])) va) (hrs_mem_update (heap_update (mdb_Ptr &(destSlot\<rightarrow>[''cteMDBNode_C''])) (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])))) (hrs_mem_update (heap_update (cap_Ptr &(srcSlot\<rightarrow>[''cap_C''])) v) (hrs_mem_update (heap_update (cap_Ptr &(destSlot\<rightarrow>[''cap_C''])) newCap) x))))) (s\<lparr>mdb_' := h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])), ret__struct_cap_C_' := v, ret__struct_mdb_node_C_' := va\<rparr>))) \<longrightarrow> (\<forall>vb. vb = mdbPrev_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])))) \<longrightarrow> True \<and> (vb \<noteq> 0 \<longrightarrow> hrs_htd (hrs_mem_update (heap_update (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])) va) (hrs_mem_update (heap_update (mdb_Ptr &(destSlot\<rightarrow>[''cteMDBNode_C''])) (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])))) (hrs_mem_update (heap_update (cap_Ptr &(srcSlot\<rightarrow>[''cap_C''])) v) (hrs_mem_update (heap_update (cap_Ptr &(destSlot\<rightarrow>[''cap_C''])) newCap) (t_hrs_' (globals s)))))) \<Turnstile>\<^sub>t cte_Ptr vb \<longrightarrow> hrs_htd (hrs_mem_update (heap_update (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])) va) (hrs_mem_update (heap_update (mdb_Ptr &(destSlot\<rightarrow>[''cteMDBNode_C''])) (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])))) (hrs_mem_update (heap_update (cap_Ptr &(srcSlot\<rightarrow>[''cap_C''])) v) (hrs_mem_update (heap_update (cap_Ptr &(destSlot\<rightarrow>[''cap_C''])) newCap) (t_hrs_' (globals s)))))) \<Turnstile>\<^sub>t cparent (mdb_Ptr &(cte_Ptr vb\<rightarrow>[''cteMDBNode_C''])) [''cteMDBNode_C'']) \<and> (\<not> vb \<noteq> 0 \<longrightarrow> (\<forall>rv. dc rv (xfdc (prev_ptr_'_update (\<lambda>_. vb) (globals_update (t_hrs_'_update (\<lambda>x. hrs_mem_update (heap_update (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])) va) (hrs_mem_update (heap_update (mdb_Ptr &(destSlot\<rightarrow>[''cteMDBNode_C''])) (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])))) (hrs_mem_update (heap_update (cap_Ptr &(srcSlot\<rightarrow>[''cap_C''])) v) (hrs_mem_update (heap_update (cap_Ptr &(destSlot\<rightarrow>[''cap_C''])) newCap) x))))) (s\<lparr>mdb_' := h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])), ret__struct_cap_C_' := v, ret__struct_mdb_node_C_' := va\<rparr>)\<lparr>ret__unsigned_' := vb\<rparr>))) \<longrightarrow> (\<forall>v. v = mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])))) \<longrightarrow> True))))) \<and> True)) \<and> True) \<and> True)) \<and> True} \<inter> \<lbrace>True\<rbrace>}} proof (prove)
goal (2 subgoals):
 1. \<And>newCap s s' cte ctea. \<lbrakk>ccap_relation cap newCap; (s, s') \<in> rf_sr; valid_mdb' s; pspace_aligned' s; ctes_of s dest = Some cte; ctes_of s src = Some ctea\<rbrakk> \<Longrightarrow> is_aligned (mdbNext (cteMDBNode ctea)) 3
 2. \<And>newCap srcSlot destSlot s s'. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr dest) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr src) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> \<lbrace>ptr_val srcSlot = src\<rbrace> \<inter> {s. \<forall>rv. cmdbnode_relation rv (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C'']))) \<longrightarrow> ccap_relation cap newCap \<and> destSlot = cte_Ptr dest \<and> (\<forall>y. dc y (xfdc (globals_update (t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(destSlot\<rightarrow>[''cap_C''])) newCap))) (mdb_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C'']))) s))) \<longrightarrow> (\<forall>v. cap_get_tag v = SCAST(32 signed \<rightarrow> 32) cap_null_cap \<longrightarrow> ccap_relation capability.NullCap v \<and> srcSlot = cte_Ptr src \<and> (\<forall>y. dc y (xfdc (globals_update (t_hrs_'_update (\<lambda>x. hrs_mem_update (heap_update (cap_Ptr &(srcSlot\<rightarrow>[''cap_C''])) v) (hrs_mem_update (heap_update (cap_Ptr &(destSlot\<rightarrow>[''cap_C''])) newCap) x))) (s\<lparr>mdb_' := h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])), ret__struct_cap_C_' := v\<rparr>))) \<longrightarrow> cmdbnode_relation rv (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C'']))) \<and> destSlot = cte_Ptr dest \<and> (\<forall>y. dc y (xfdc (globals_update (t_hrs_'_update (\<lambda>x. hrs_mem_update (heap_update (mdb_Ptr &(destSlot\<rightarrow>[''cteMDBNode_C''])) (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])))) (hrs_mem_update (heap_update (cap_Ptr &(srcSlot\<rightarrow>[''cap_C''])) v) (hrs_mem_update (heap_update (cap_Ptr &(destSlot\<rightarrow>[''cap_C''])) newCap) x)))) (s\<lparr>mdb_' := h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])), ret__struct_cap_C_' := v\<rparr>))) \<longrightarrow> (\<forall>va. mdb_node_lift va = \<lparr>mdbNext_CL = 0 && ~~ mask 3, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) false && mask 1, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) false && mask 1, mdbPrev_CL = 0 && ~~ mask 3\<rparr> \<longrightarrow> cmdbnode_relation nullMDBNode va \<and> srcSlot = cte_Ptr src \<and> (\<forall>y. dc y (xfdc (globals_update (t_hrs_'_update (\<lambda>x. hrs_mem_update (heap_update (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])) va) (hrs_mem_update (heap_update (mdb_Ptr &(destSlot\<rightarrow>[''cteMDBNode_C''])) (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])))) (hrs_mem_update (heap_update (cap_Ptr &(srcSlot\<rightarrow>[''cap_C''])) v) (hrs_mem_update (heap_update (cap_Ptr &(destSlot\<rightarrow>[''cap_C''])) newCap) x))))) (s\<lparr>mdb_' := h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])), ret__struct_cap_C_' := v, ret__struct_mdb_node_C_' := va\<rparr>))) \<longrightarrow> (\<forall>vb. vb = mdbPrev_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])))) \<longrightarrow> True \<and> (vb \<noteq> 0 \<longrightarrow> hrs_htd (hrs_mem_update (heap_update (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])) va) (hrs_mem_update (heap_update (mdb_Ptr &(destSlot\<rightarrow>[''cteMDBNode_C''])) (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])))) (hrs_mem_update (heap_update (cap_Ptr &(srcSlot\<rightarrow>[''cap_C''])) v) (hrs_mem_update (heap_update (cap_Ptr &(destSlot\<rightarrow>[''cap_C''])) newCap) (t_hrs_' (globals s)))))) \<Turnstile>\<^sub>t cte_Ptr vb \<longrightarrow> hrs_htd (hrs_mem_update (heap_update (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])) va) (hrs_mem_update (heap_update (mdb_Ptr &(destSlot\<rightarrow>[''cteMDBNode_C''])) (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])))) (hrs_mem_update (heap_update (cap_Ptr &(srcSlot\<rightarrow>[''cap_C''])) v) (hrs_mem_update (heap_update (cap_Ptr &(destSlot\<rightarrow>[''cap_C''])) newCap) (t_hrs_' (globals s)))))) \<Turnstile>\<^sub>t cparent (mdb_Ptr &(cte_Ptr vb\<rightarrow>[''cteMDBNode_C''])) [''cteMDBNode_C'']) \<and> (\<not> vb \<noteq> 0 \<longrightarrow> (\<forall>rv. dc rv (xfdc (prev_ptr_'_update (\<lambda>_. vb) (globals_update (t_hrs_'_update (\<lambda>x. hrs_mem_update (heap_update (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])) va) (hrs_mem_update (heap_update (mdb_Ptr &(destSlot\<rightarrow>[''cteMDBNode_C''])) (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])))) (hrs_mem_update (heap_update (cap_Ptr &(srcSlot\<rightarrow>[''cap_C''])) v) (hrs_mem_update (heap_update (cap_Ptr &(destSlot\<rightarrow>[''cap_C''])) newCap) x))))) (s\<lparr>mdb_' := h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])), ret__struct_cap_C_' := v, ret__struct_mdb_node_C_' := va\<rparr>)\<lparr>ret__unsigned_' := vb\<rparr>))) \<longrightarrow> (\<forall>v. v = mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])))) \<longrightarrow> True))))) \<and> True)) \<and> True) \<and> True)) \<and> True} \<inter> \<lbrace>True\<rbrace>}} proof (prove)
goal (1 subgoal):
 1. \<And>newCap srcSlot destSlot s s'. \<lbrakk>ccap_relation cap newCap; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr dest) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr src) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> \<lbrace>ptr_val srcSlot = src\<rbrace> \<inter> {s. \<forall>rv. cmdbnode_relation rv (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C'']))) \<longrightarrow> ccap_relation cap newCap \<and> destSlot = cte_Ptr dest \<and> (\<forall>y. dc y (xfdc (globals_update (t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(destSlot\<rightarrow>[''cap_C''])) newCap))) (mdb_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C'']))) s))) \<longrightarrow> (\<forall>v. cap_get_tag v = SCAST(32 signed \<rightarrow> 32) cap_null_cap \<longrightarrow> ccap_relation capability.NullCap v \<and> srcSlot = cte_Ptr src \<and> (\<forall>y. dc y (xfdc (globals_update (t_hrs_'_update (\<lambda>x. hrs_mem_update (heap_update (cap_Ptr &(srcSlot\<rightarrow>[''cap_C''])) v) (hrs_mem_update (heap_update (cap_Ptr &(destSlot\<rightarrow>[''cap_C''])) newCap) x))) (s\<lparr>mdb_' := h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])), ret__struct_cap_C_' := v\<rparr>))) \<longrightarrow> cmdbnode_relation rv (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C'']))) \<and> destSlot = cte_Ptr dest \<and> (\<forall>y. dc y (xfdc (globals_update (t_hrs_'_update (\<lambda>x. hrs_mem_update (heap_update (mdb_Ptr &(destSlot\<rightarrow>[''cteMDBNode_C''])) (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])))) (hrs_mem_update (heap_update (cap_Ptr &(srcSlot\<rightarrow>[''cap_C''])) v) (hrs_mem_update (heap_update (cap_Ptr &(destSlot\<rightarrow>[''cap_C''])) newCap) x)))) (s\<lparr>mdb_' := h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])), ret__struct_cap_C_' := v\<rparr>))) \<longrightarrow> (\<forall>va. mdb_node_lift va = \<lparr>mdbNext_CL = 0 && ~~ mask 3, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) false && mask 1, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) false && mask 1, mdbPrev_CL = 0 && ~~ mask 3\<rparr> \<longrightarrow> cmdbnode_relation nullMDBNode va \<and> srcSlot = cte_Ptr src \<and> (\<forall>y. dc y (xfdc (globals_update (t_hrs_'_update (\<lambda>x. hrs_mem_update (heap_update (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])) va) (hrs_mem_update (heap_update (mdb_Ptr &(destSlot\<rightarrow>[''cteMDBNode_C''])) (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])))) (hrs_mem_update (heap_update (cap_Ptr &(srcSlot\<rightarrow>[''cap_C''])) v) (hrs_mem_update (heap_update (cap_Ptr &(destSlot\<rightarrow>[''cap_C''])) newCap) x))))) (s\<lparr>mdb_' := h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])), ret__struct_cap_C_' := v, ret__struct_mdb_node_C_' := va\<rparr>))) \<longrightarrow> (\<forall>vb. vb = mdbPrev_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])))) \<longrightarrow> True \<and> (vb \<noteq> 0 \<longrightarrow> hrs_htd (hrs_mem_update (heap_update (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])) va) (hrs_mem_update (heap_update (mdb_Ptr &(destSlot\<rightarrow>[''cteMDBNode_C''])) (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])))) (hrs_mem_update (heap_update (cap_Ptr &(srcSlot\<rightarrow>[''cap_C''])) v) (hrs_mem_update (heap_update (cap_Ptr &(destSlot\<rightarrow>[''cap_C''])) newCap) (t_hrs_' (globals s)))))) \<Turnstile>\<^sub>t cte_Ptr vb \<longrightarrow> hrs_htd (hrs_mem_update (heap_update (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])) va) (hrs_mem_update (heap_update (mdb_Ptr &(destSlot\<rightarrow>[''cteMDBNode_C''])) (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])))) (hrs_mem_update (heap_update (cap_Ptr &(srcSlot\<rightarrow>[''cap_C''])) v) (hrs_mem_update (heap_update (cap_Ptr &(destSlot\<rightarrow>[''cap_C''])) newCap) (t_hrs_' (globals s)))))) \<Turnstile>\<^sub>t cparent (mdb_Ptr &(cte_Ptr vb\<rightarrow>[''cteMDBNode_C''])) [''cteMDBNode_C'']) \<and> (\<not> vb \<noteq> 0 \<longrightarrow> (\<forall>rv. dc rv (xfdc (prev_ptr_'_update (\<lambda>_. vb) (globals_update (t_hrs_'_update (\<lambda>x. hrs_mem_update (heap_update (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])) va) (hrs_mem_update (heap_update (mdb_Ptr &(destSlot\<rightarrow>[''cteMDBNode_C''])) (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])))) (hrs_mem_update (heap_update (cap_Ptr &(srcSlot\<rightarrow>[''cap_C''])) v) (hrs_mem_update (heap_update (cap_Ptr &(destSlot\<rightarrow>[''cap_C''])) newCap) x))))) (s\<lparr>mdb_' := h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])), ret__struct_cap_C_' := v, ret__struct_mdb_node_C_' := va\<rparr>)\<lparr>ret__unsigned_' := vb\<rparr>))) \<longrightarrow> (\<forall>v. v = mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(srcSlot\<rightarrow>[''cteMDBNode_C''])))) \<longrightarrow> True))))) \<and> True)) \<and> True) \<and> True)) \<and> True} \<inter> \<lbrace>True\<rbrace>}} proof (prove)
goal (1 subgoal):
 1. \<And>newCap s s' cte' cte'a rv v. \<lbrakk>ccap_relation cap newCap; (s, s') \<in> rf_sr; valid_mdb' s; pspace_aligned' s; (cte_lift \<circ>\<^sub>m cslift s') (cte_Ptr dest) = Some cte'; cl_valid_cte cte'; (cte_lift \<circ>\<^sub>m cslift s') (cte_Ptr src) = Some cte'a; cl_valid_cte cte'a; cmdbnode_relation rv (h_val (hrs_mem (t_hrs_' (globals s'))) (mdb_Ptr &(cte_Ptr src\<rightarrow>[''cteMDBNode_C'']))); cap_get_tag v = SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrakk> \<Longrightarrow> ccap_relation capability.NullCap v \<and> (\<forall>v. mdb_node_lift v = \<lparr>mdbNext_CL = 0, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) false, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) false, mdbPrev_CL = 0\<rparr> \<longrightarrow> cmdbnode_relation nullMDBNode v) proof (prove)
goal (1 subgoal):
 1. \<And>newCap s s' cte' cte'a rv v. \<lbrakk>ccap_relation cap newCap; (s, s') \<in> rf_sr; valid_mdb' s; pspace_aligned' s; (cte_lift \<circ>\<^sub>m cslift s') (cte_Ptr dest) = Some cte'; cl_valid_cte cte'; (cte_lift \<circ>\<^sub>m cslift s') (cte_Ptr src) = Some cte'a; cl_valid_cte cte'a; cmdbnode_relation rv (h_val (hrs_mem (t_hrs_' (globals s'))) (mdb_Ptr &(cte_Ptr src\<rightarrow>[''cteMDBNode_C'']))); cap_get_tag v = SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrakk> \<Longrightarrow> \<forall>v. mdb_node_lift v = \<lparr>mdbNext_CL = 0, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) false, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) false, mdbPrev_CL = 0\<rparr> \<longrightarrow> cmdbnode_relation nullMDBNode v proof (prove)
goal:
No subgoals!