theory Retype_C

lemma insertNewCap_ccorres1:
  "ccorres dc xfdc (pspace_aligned' and valid_mdb' and valid_objs' and valid_cap' cap)
     ({s. (case untypedZeroRange cap of None \<Rightarrow> True
          | Some (a, b) \<Rightarrow> region_actually_is_zero_bytes a (unat ((b + 1) - a)) s)}
       \<inter> {s. ccap_relation cap (cap_' s)} \<inter> {s. parent_' s = Ptr parent}
       \<inter> {s. slot_' s = Ptr slot}) []
     (insertNewCap parent slot cap)
     (Call insertNewCap_'proc)" supply if_cong[cong] option.case_cong[cong] apply (cinit (no_ignore_call) lift: cap_' parent_' slot_') apply (rule ccorres_liftM_getCTE_cte_at) apply (rule ccorres_move_c_guard_cte) apply (simp only: ) apply (rule ccorres_split_nothrow [OF mdb_node_get_mdbNext_heap_ccorres]) apply ceqv apply (erule_tac s = "next" in subst) apply csymbr apply (ctac (c_lines 3) pre: ccorres_pre_getCTE ccorres_assert add: insertNewCap_ccorres_helper) apply (simp only: Ptr_not_null_pointer_not_zero) apply (ctac add: updateMDB_set_mdbPrev) apply (rule ccorres_seq_skip'[THEN iffD1]) apply ctac apply (rule updateNewFreeIndex_noop_ccorres[where cap=cap]) apply (wp updateMDB_weak_cte_wp_at) apply simp apply (vcg exspec=mdb_node_ptr_set_mdbNext_preserves_bytes) apply (wp updateMDB_weak_cte_wp_at) apply clarsimp apply (vcg exspec=mdb_node_ptr_set_mdbPrev_preserves_bytes) apply (wp setCTE_weak_cte_wp_at) apply (clarsimp simp: hrs_mem_update Collect_const_mem
                 simp del: imp_disjL) apply vcg apply simp apply (wp getCTE_wp') apply (clarsimp simp: hrs_mem_update) apply vcg apply (rule conjI) apply (clarsimp simp: cte_wp_at_ctes_of is_aligned_3_next) apply (clarsimp split: option.split) apply (intro allI conjI impI; simp; clarsimp simp: region_actually_is_bytes) apply (erule trans[OF heap_list_h_eq2, rotated]) apply (rule byte_regions_unmodified_region_is_bytes) apply (erule byte_regions_unmodified_trans[rotated]
         | simp
         | rule byte_regions_unmodified_hrs_mem_update
         | simp add: typ_heap_simps')+ apply (erule trans[OF heap_list_h_eq2, rotated]) apply (rule byte_regions_unmodified_region_is_bytes) apply (erule byte_regions_unmodified_trans[rotated]
        | simp
        | rule byte_regions_unmodified_hrs_mem_update
        | simp add: typ_heap_simps')+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (pspace_aligned' and valid_mdb' and valid_objs' and valid_cap' cap) ({s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0} \<inter> \<lbrace>ccap_relation cap \<acute>cap\<rbrace> \<inter> \<lbrace>\<acute>parent = cte_Ptr parent\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr slot\<rbrace>) [] (insertNewCap parent slot cap) (Call insertNewCap_'proc) proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (pspace_aligned' and valid_mdb' and valid_objs' and valid_cap' cap) ({s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0} \<inter> \<lbrace>ccap_relation cap \<acute>cap\<rbrace> \<inter> \<lbrace>\<acute>parent = cte_Ptr parent\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr slot\<rbrace>) [] (insertNewCap parent slot cap) (Call insertNewCap_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>slota parenta capa. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q670 slota parenta capa) (?Q'670 slota parenta capa) [SKIP] (do next <- liftM (mdbNext \<circ> cteMDBNode) (getCTE parent);
oldCTE <- getCTE slot;
y <- assert (nullCapPointers oldCTE);
y <- setCTE slot (CTE cap (MDB next parent True True));
y <- updateMDB next (mdbPrev_update (\<lambda>_. slot));
y <- updateMDB parent (mdbNext_update (\<lambda>_. slot));
updateNewFreeIndex slot
od) (Guard C_Guard {s. s \<Turnstile>\<^sub>c parenta} (\<acute>ret__unsigned :== CALL mdb_node_get_mdbNext_'proc(h_val (hrs_mem \<acute>t_hrs) (mdb_Ptr &(parenta\<rightarrow>[''cteMDBNode_C'']))));;
(\<acute>next :== cte_Ptr \<acute>ret__unsigned;;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c slota} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(slota\<rightarrow>[''cap_C''])) capa)));;
(\<acute>ret__struct_mdb_node_C :== CALL mdb_node_new_'proc(ptr_val \<acute>next,SCAST(32 signed \<rightarrow> 32) true,SCAST(32 signed \<rightarrow> 32) true,ptr_val parenta);;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c slota} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C''])) \<acute>ret__struct_mdb_node_C)));;
(IF \<acute>next \<noteq> NULL THEN
  Guard C_Guard {s. s \<Turnstile>\<^sub>c next_' s} (CALL mdb_node_ptr_set_mdbPrev_'proc(mdb_Ptr &(\<acute>next\<rightarrow>[''cteMDBNode_C'']),ptr_val slota))
FI;;
Guard C_Guard {s. s \<Turnstile>\<^sub>c parenta} (CALL mdb_node_ptr_set_mdbNext_'proc(mdb_Ptr &(parenta\<rightarrow>[''cteMDBNode_C'']),ptr_val slota))))))))
 2. \<And>slota parenta capa s s'. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; (s, s') \<in> rf_sr; (pspace_aligned' and valid_mdb' and valid_objs' and valid_cap' cap) s; s' \<in> {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0}\<rbrakk> \<Longrightarrow> ?Q670 slota parenta capa s \<and> s' \<in> ?Q'670 slota parenta capa proof (prove)
goal (2 subgoals):
 1. \<And>slota parenta capa. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?G676 slota parenta capa) (?Q'670 slota parenta capa) [SKIP] (do next <- liftM (mdbNext \<circ> cteMDBNode) (getCTE parent);
oldCTE <- getCTE slot;
y <- assert (nullCapPointers oldCTE);
y <- setCTE slot (CTE cap (MDB next parent True True));
y <- updateMDB next (mdbPrev_update (\<lambda>_. slot));
y <- updateMDB parent (mdbNext_update (\<lambda>_. slot));
updateNewFreeIndex slot
od) (Guard C_Guard {s. s \<Turnstile>\<^sub>c parenta} (\<acute>ret__unsigned :== CALL mdb_node_get_mdbNext_'proc(h_val (hrs_mem \<acute>t_hrs) (mdb_Ptr &(parenta\<rightarrow>[''cteMDBNode_C'']))));;
(\<acute>next :== cte_Ptr \<acute>ret__unsigned;;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c slota} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(slota\<rightarrow>[''cap_C''])) capa)));;
(\<acute>ret__struct_mdb_node_C :== CALL mdb_node_new_'proc(ptr_val \<acute>next,SCAST(32 signed \<rightarrow> 32) true,SCAST(32 signed \<rightarrow> 32) true,ptr_val parenta);;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c slota} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C''])) \<acute>ret__struct_mdb_node_C)));;
(IF \<acute>next \<noteq> NULL THEN
  Guard C_Guard {s. s \<Turnstile>\<^sub>c next_' s} (CALL mdb_node_ptr_set_mdbPrev_'proc(mdb_Ptr &(\<acute>next\<rightarrow>[''cteMDBNode_C'']),ptr_val slota))
FI;;
Guard C_Guard {s. s \<Turnstile>\<^sub>c parenta} (CALL mdb_node_ptr_set_mdbNext_'proc(mdb_Ptr &(parenta\<rightarrow>[''cteMDBNode_C'']),ptr_val slota))))))))
 2. \<And>slota parenta capa s s'. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; (s, s') \<in> rf_sr; (pspace_aligned' and valid_mdb' and valid_objs' and valid_cap' cap) s; s' \<in> {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0}\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) parent s \<longrightarrow> ?G676 slota parenta capa s) \<and> s' \<in> ?Q'670 slota parenta capa proof (prove)
goal (2 subgoals):
 1. \<And>slota parenta capa. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?A678 slota parenta capa) (?C'678 slota parenta capa) [SKIP] (do next <- liftM (mdbNext \<circ> cteMDBNode) (getCTE parent);
oldCTE <- getCTE slot;
y <- assert (nullCapPointers oldCTE);
y <- setCTE slot (CTE cap (MDB next parent True True));
y <- updateMDB next (mdbPrev_update (\<lambda>_. slot));
y <- updateMDB parent (mdbNext_update (\<lambda>_. slot));
updateNewFreeIndex slot
od) (\<acute>ret__unsigned :== CALL mdb_node_get_mdbNext_'proc(h_val (hrs_mem \<acute>t_hrs) (mdb_Ptr &(parenta\<rightarrow>[''cteMDBNode_C''])));;
(\<acute>next :== cte_Ptr \<acute>ret__unsigned;;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c slota} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(slota\<rightarrow>[''cap_C''])) capa)));;
(\<acute>ret__struct_mdb_node_C :== CALL mdb_node_new_'proc(ptr_val \<acute>next,SCAST(32 signed \<rightarrow> 32) true,SCAST(32 signed \<rightarrow> 32) true,ptr_val parenta);;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c slota} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C''])) \<acute>ret__struct_mdb_node_C)));;
(IF \<acute>next \<noteq> NULL THEN
  Guard C_Guard {s. s \<Turnstile>\<^sub>c next_' s} (CALL mdb_node_ptr_set_mdbPrev_'proc(mdb_Ptr &(\<acute>next\<rightarrow>[''cteMDBNode_C'']),ptr_val slota))
FI;;
Guard C_Guard {s. s \<Turnstile>\<^sub>c parenta} (CALL mdb_node_ptr_set_mdbNext_'proc(mdb_Ptr &(parenta\<rightarrow>[''cteMDBNode_C'']),ptr_val slota))))))))
 2. \<And>slota parenta capa s s'. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; (s, s') \<in> rf_sr; (pspace_aligned' and valid_mdb' and valid_objs' and valid_cap' cap) s; s' \<in> {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0}\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) parent s \<longrightarrow> (?A678 slota parenta capa and cte_wp_at' (\<lambda>_. True) (ptr_val parenta)) s) \<and> s' \<in> ?C'678 slota parenta capa \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>slota parenta capa. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?A678 (cte_Ptr slot) (cte_Ptr parent) capa) (?C'678 (cte_Ptr slot) (cte_Ptr parent) capa) [SKIP] (do next <- liftM (mdbNext \<circ> cteMDBNode) (getCTE parent);
oldCTE <- getCTE slot;
y <- assert (nullCapPointers oldCTE);
y <- setCTE slot (CTE cap (MDB next parent True True));
y <- updateMDB next (mdbPrev_update (\<lambda>_. slot));
y <- updateMDB parent (mdbNext_update (\<lambda>_. slot));
updateNewFreeIndex slot
od) (\<acute>ret__unsigned :== CALL mdb_node_get_mdbNext_'proc(h_val (hrs_mem \<acute>t_hrs) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C''])));;
(\<acute>next :== cte_Ptr \<acute>ret__unsigned;;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr slot} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C''])) capa)));;
(\<acute>ret__struct_mdb_node_C :== CALL mdb_node_new_'proc(ptr_val \<acute>next,SCAST(32 signed \<rightarrow> 32) true,SCAST(32 signed \<rightarrow> 32) true,ptr_val (cte_Ptr parent));;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr slot} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(cte_Ptr slot\<rightarrow>[''cteMDBNode_C''])) \<acute>ret__struct_mdb_node_C)));;
(IF \<acute>next \<noteq> NULL THEN
  Guard C_Guard {s. s \<Turnstile>\<^sub>c next_' s} (CALL mdb_node_ptr_set_mdbPrev_'proc(mdb_Ptr &(\<acute>next\<rightarrow>[''cteMDBNode_C'']),ptr_val (cte_Ptr slot)))
FI;;
Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr parent} (CALL mdb_node_ptr_set_mdbNext_'proc(mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C'']),ptr_val (cte_Ptr slot)))))))))
 2. \<And>slota parenta capa s s'. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; (s, s') \<in> rf_sr; (pspace_aligned' and valid_mdb' and valid_objs' and valid_cap' cap) s; s' \<in> {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0}\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) parent s \<longrightarrow> (?A678 slota parenta capa and cte_wp_at' (\<lambda>_. True) (ptr_val parenta)) s) \<and> s' \<in> ?C'678 slota parenta capa \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>slota parenta capa rv' t t'. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa\<rbrakk> \<Longrightarrow> ceqv \<Gamma> ret__unsigned_' rv' t t' (\<acute>next :== cte_Ptr \<acute>ret__unsigned;;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr slot} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C''])) capa)));;
(\<acute>ret__struct_mdb_node_C :== CALL mdb_node_new_'proc(ptr_val \<acute>next,SCAST(32 signed \<rightarrow> 32) true,SCAST(32 signed \<rightarrow> 32) true,ptr_val (cte_Ptr parent));;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr slot} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(cte_Ptr slot\<rightarrow>[''cteMDBNode_C''])) \<acute>ret__struct_mdb_node_C)));;
(IF \<acute>next \<noteq> NULL THEN
  Guard C_Guard {s. s \<Turnstile>\<^sub>c next_' s} (CALL mdb_node_ptr_set_mdbPrev_'proc(mdb_Ptr &(\<acute>next\<rightarrow>[''cteMDBNode_C'']),ptr_val (cte_Ptr slot)))
FI;;
Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr parent} (CALL mdb_node_ptr_set_mdbNext_'proc(mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C'']),ptr_val (cte_Ptr slot)))))))) (?d'680 slota parenta capa rv')
 2. \<And>slota parenta capa next rv'. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; next = rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q680 slota parenta capa next) (?Q'680 slota parenta capa next rv') [SKIP] (do oldCTE <- getCTE slot;
y <- assert (nullCapPointers oldCTE);
y <- setCTE slot (CTE cap (MDB next parent True True));
y <- updateMDB next (mdbPrev_update (\<lambda>_. slot));
y <- updateMDB parent (mdbNext_update (\<lambda>_. slot));
updateNewFreeIndex slot
od) (?d'680 slota parenta capa rv')
 3. \<And>slota parenta capa. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<lbrace>?R685 (cte_Ptr slot) (cte_Ptr parent) capa\<rbrace> liftM (mdbNext \<circ> cteMDBNode) (getCTE parent) \<lbrace>?Q680 slota parenta capa\<rbrace>
 4. \<And>slota parenta capa. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F680 slota parenta capa\<^esub> (?R'682 (cte_Ptr slot) (cte_Ptr parent) capa) \<acute>ret__unsigned :== CALL mdb_node_get_mdbNext_'proc(h_val (hrs_mem \<acute>t_hrs) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C'']))) {s. \<forall>next. next = ret__unsigned_' s \<longrightarrow> s \<in> ?Q'680 slota parenta capa next (ret__unsigned_' s)}
 5. \<And>slota parenta capa s s'. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; (s, s') \<in> rf_sr; (pspace_aligned' and valid_mdb' and valid_objs' and valid_cap' cap) s; s' \<in> {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0}\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) parent s \<longrightarrow> ((\<lambda>_. True) and ?R685 slota parenta capa and cte_wp_at' (\<lambda>_. True) (ptr_val parenta)) s) \<and> s' \<in> UNIV \<inter> ?R'682 slota parenta capa \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>slota parenta capa next rv'. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; next = rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q680 slota parenta capa next) (?Q'680 slota parenta capa next rv') [SKIP] (do oldCTE <- getCTE slot;
y <- assert (nullCapPointers oldCTE);
y <- setCTE slot (CTE cap (MDB next parent True True));
y <- updateMDB next (mdbPrev_update (\<lambda>_. slot));
y <- updateMDB parent (mdbNext_update (\<lambda>_. slot));
updateNewFreeIndex slot
od) (\<acute>next :== cte_Ptr rv';;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr slot} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C''])) capa)));;
(\<acute>ret__struct_mdb_node_C :== CALL mdb_node_new_'proc(ptr_val \<acute>next,SCAST(32 signed \<rightarrow> 32) true,SCAST(32 signed \<rightarrow> 32) true,ptr_val (cte_Ptr parent));;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr slot} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(cte_Ptr slot\<rightarrow>[''cteMDBNode_C''])) \<acute>ret__struct_mdb_node_C)));;
(IF \<acute>next \<noteq> NULL THEN
  Guard C_Guard {s. s \<Turnstile>\<^sub>c next_' s} (CALL mdb_node_ptr_set_mdbPrev_'proc(mdb_Ptr &(\<acute>next\<rightarrow>[''cteMDBNode_C'']),ptr_val (cte_Ptr slot)))
FI;;
Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr parent} (CALL mdb_node_ptr_set_mdbNext_'proc(mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C'']),ptr_val (cte_Ptr slot))))))))
 2. \<And>slota parenta capa. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<lbrace>?R685 (cte_Ptr slot) (cte_Ptr parent) capa\<rbrace> liftM (mdbNext \<circ> cteMDBNode) (getCTE parent) \<lbrace>?Q680 slota parenta capa\<rbrace>
 3. \<And>slota parenta capa. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F680 slota parenta capa\<^esub> (?R'682 (cte_Ptr slot) (cte_Ptr parent) capa) \<acute>ret__unsigned :== CALL mdb_node_get_mdbNext_'proc(h_val (hrs_mem \<acute>t_hrs) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C'']))) {s. \<forall>next. next = ret__unsigned_' s \<longrightarrow> s \<in> ?Q'680 slota parenta capa next (ret__unsigned_' s)}
 4. \<And>slota parenta capa s s'. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; (s, s') \<in> rf_sr; (pspace_aligned' and valid_mdb' and valid_objs' and valid_cap' cap) s; s' \<in> {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0}\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) parent s \<longrightarrow> ((\<lambda>_. True) and ?R685 slota parenta capa and cte_wp_at' (\<lambda>_. True) (ptr_val parenta)) s) \<and> s' \<in> UNIV \<inter> ?R'682 slota parenta capa \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>slota parenta capa next rv'. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q680 slota parenta capa next) (?Q'858 slota parenta capa next rv' next) [SKIP] (do oldCTE <- getCTE slot;
y <- assert (nullCapPointers oldCTE);
y <- setCTE slot (CTE cap (MDB next parent True True));
y <- updateMDB next (mdbPrev_update (\<lambda>_. slot));
y <- updateMDB parent (mdbNext_update (\<lambda>_. slot));
updateNewFreeIndex slot
od) (\<acute>next :== cte_Ptr next;;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr slot} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C''])) capa)));;
(\<acute>ret__struct_mdb_node_C :== CALL mdb_node_new_'proc(ptr_val \<acute>next,SCAST(32 signed \<rightarrow> 32) true,SCAST(32 signed \<rightarrow> 32) true,ptr_val (cte_Ptr parent));;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr slot} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(cte_Ptr slot\<rightarrow>[''cteMDBNode_C''])) \<acute>ret__struct_mdb_node_C)));;
(IF \<acute>next \<noteq> NULL THEN
  Guard C_Guard {s. s \<Turnstile>\<^sub>c next_' s} (CALL mdb_node_ptr_set_mdbPrev_'proc(mdb_Ptr &(\<acute>next\<rightarrow>[''cteMDBNode_C'']),ptr_val (cte_Ptr slot)))
FI;;
Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr parent} (CALL mdb_node_ptr_set_mdbNext_'proc(mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C'']),ptr_val (cte_Ptr slot))))))))
 2. \<And>slota parenta capa. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<lbrace>?R685 (cte_Ptr slot) (cte_Ptr parent) capa\<rbrace> liftM (mdbNext \<circ> cteMDBNode) (getCTE parent) \<lbrace>?Q680 slota parenta capa\<rbrace>
 3. \<And>slota parenta capa. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F680 slota parenta capa\<^esub> (?R'682 (cte_Ptr slot) (cte_Ptr parent) capa) \<acute>ret__unsigned :== CALL mdb_node_get_mdbNext_'proc(h_val (hrs_mem \<acute>t_hrs) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C'']))) {s. \<forall>next. next = ret__unsigned_' s \<longrightarrow> s \<in> ?Q'858 slota parenta capa next (ret__unsigned_' s) (ret__unsigned_' s)}
 4. \<And>slota parenta capa s s'. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; (s, s') \<in> rf_sr; (pspace_aligned' and valid_mdb' and valid_objs' and valid_cap' cap) s; s' \<in> {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0}\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) parent s \<longrightarrow> ((\<lambda>_. True) and ?R685 slota parenta capa and cte_wp_at' (\<lambda>_. True) (ptr_val parenta)) s) \<and> s' \<in> UNIV \<inter> ?R'682 slota parenta capa \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>slota parenta capa next rv'. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q680 slota parenta capa next) (?G'869 slota parenta capa next next rv') [SKIP] (do oldCTE <- getCTE slot;
y <- assert (nullCapPointers oldCTE);
y <- setCTE slot (CTE cap (MDB next parent True True));
y <- updateMDB next (mdbPrev_update (\<lambda>_. slot));
y <- updateMDB parent (mdbNext_update (\<lambda>_. slot));
updateNewFreeIndex slot
od) (Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr slot} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C''])) capa)));;
(\<acute>ret__struct_mdb_node_C :== CALL mdb_node_new_'proc(ptr_val (cte_Ptr next),SCAST(32 signed \<rightarrow> 32) true,SCAST(32 signed \<rightarrow> 32) true,ptr_val (cte_Ptr parent));;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr slot} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(cte_Ptr slot\<rightarrow>[''cteMDBNode_C''])) \<acute>ret__struct_mdb_node_C)));;
(IF cte_Ptr next \<noteq> NULL THEN
  Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr next} (CALL mdb_node_ptr_set_mdbPrev_'proc(mdb_Ptr &(cte_Ptr next\<rightarrow>[''cteMDBNode_C'']),ptr_val (cte_Ptr slot)))
FI;;
Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr parent} (CALL mdb_node_ptr_set_mdbNext_'proc(mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C'']),ptr_val (cte_Ptr slot)))))))
 2. \<And>slota parenta capa. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<lbrace>?R685 (cte_Ptr slot) (cte_Ptr parent) capa\<rbrace> liftM (mdbNext \<circ> cteMDBNode) (getCTE parent) \<lbrace>?Q680 slota parenta capa\<rbrace>
 3. \<And>slota parenta capa. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F680 slota parenta capa\<^esub> (?R'682 (cte_Ptr slot) (cte_Ptr parent) capa) \<acute>ret__unsigned :== CALL mdb_node_get_mdbNext_'proc(h_val (hrs_mem \<acute>t_hrs) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C'']))) {s. \<forall>next. next = ret__unsigned_' s \<longrightarrow> s \<in> {sa. next_'_update (\<lambda>_. cte_Ptr (ret__unsigned_' s)) sa \<in> ?G'869 slota parenta capa next (ret__unsigned_' s) (ret__unsigned_' s)}}
 4. \<And>slota parenta capa s s'. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; (s, s') \<in> rf_sr; (pspace_aligned' and valid_mdb' and valid_objs' and valid_cap' cap) s; s' \<in> {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0}\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) parent s \<longrightarrow> ((\<lambda>_. True) and ?R685 slota parenta capa and cte_wp_at' (\<lambda>_. True) (ptr_val parenta)) s) \<and> s' \<in> UNIV \<inter> ?R'682 slota parenta capa \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>slota parenta capa next rv' oldCTE rv xfdca. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; nullCapPointers oldCTE; dc rv xfdca\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1050 slota parenta capa next rv' oldCTE rv) (?Q'1050 slota parenta capa next rv' oldCTE rv xfdca) [SKIP] (do y <- updateMDB next (mdbPrev_update (\<lambda>_. slot));
y <- updateMDB parent (mdbNext_update (\<lambda>_. slot));
updateNewFreeIndex slot
od) (IF cte_Ptr next \<noteq> NULL THEN
  Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr next} (CALL mdb_node_ptr_set_mdbPrev_'proc(mdb_Ptr &(cte_Ptr next\<rightarrow>[''cteMDBNode_C'']),ptr_val (cte_Ptr slot)))
FI;;
Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr parent} (CALL mdb_node_ptr_set_mdbNext_'proc(mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C'']),ptr_val (cte_Ptr slot))))
 2. \<And>slota parenta capa next rv' oldCTE. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; nullCapPointers oldCTE\<rbrakk> \<Longrightarrow> \<lbrace>?R1056 slota parenta capa next oldCTE\<rbrace> setCTE slot (CTE cap (MDB next parent True True)) \<lbrace>?Q1050 slota parenta capa next rv' oldCTE\<rbrace>
 3. \<And>slota parenta capa next rv' oldCTE. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; nullCapPointers oldCTE\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'1050 slota parenta capa next rv' oldCTE) \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C''])) capa));;
\<acute>ret__struct_mdb_node_C :== CALL mdb_node_new_'proc(ptr_val (cte_Ptr next),SCAST(32 signed \<rightarrow> 32) true,SCAST(32 signed \<rightarrow> 32) true,ptr_val (cte_Ptr parent));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr slot} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(cte_Ptr slot\<rightarrow>[''cteMDBNode_C''])) \<acute>ret__struct_mdb_node_C))) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> ?Q'1050 slota parenta capa next rv' oldCTE rv (xfdc s)}
 4. \<And>slota parenta capa. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<lbrace>?R685 (cte_Ptr slot) (cte_Ptr parent) capa\<rbrace> liftM (mdbNext \<circ> cteMDBNode) (getCTE parent) \<lbrace>\<lambda>a b. \<forall>cte. ctes_of b slot = Some cte \<longrightarrow> (cte_wp_at' (\<lambda>_. True) slot and K (is_aligned a 3 \<and> is_aligned parent 3) and ?R1056 slota parenta capa a cte and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr slot))) b\<rbrace>
 5. \<And>slota parenta capa. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F680 slota parenta capa\<^esub> (?R'682 (cte_Ptr slot) (cte_Ptr parent) capa) \<acute>ret__unsigned :== CALL mdb_node_get_mdbNext_'proc(h_val (hrs_mem \<acute>t_hrs) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C'']))) {s. \<forall>next. next = ret__unsigned_' s \<longrightarrow> s \<in> {sa. next_'_update (\<lambda>_. cte_Ptr (ret__unsigned_' s)) sa \<in> {sa. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift sa) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> sa \<in> UNIV \<inter> ?R'1053 slota parenta capa next (ret__unsigned_' s) (ret__unsigned_' s) cte' \<inter> \<lbrace>True\<rbrace>}}}
 6. \<And>slota parenta capa s s'. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; (s, s') \<in> rf_sr; (pspace_aligned' and valid_mdb' and valid_objs' and valid_cap' cap) s; s' \<in> {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0}\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) parent s \<longrightarrow> ((\<lambda>_. True) and ?R685 slota parenta capa and cte_wp_at' (\<lambda>_. True) (ptr_val parenta)) s) \<and> s' \<in> UNIV \<inter> ?R'682 slota parenta capa \<inter> \<lbrace>True\<rbrace>
flex-flex pairs:
\<lambda>slota parenta capa next. ?R'1053 slota parenta capa next next \<equiv>\<^sup>? \<lambda>slota parenta capa next rv' cte'. ?R'1050 slota parenta capa next rv' (cte_to_H cte') proof (prove)
goal (6 subgoals):
 1. \<And>slota parenta capa next rv' oldCTE rv xfdca. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; nullCapPointers oldCTE; dc rv xfdca\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1050 (cte_Ptr slot) (cte_Ptr parent) capa next rv' oldCTE rv) (?Q'1050 (cte_Ptr slot) (cte_Ptr parent) capa next rv' oldCTE rv xfdca) [SKIP] (do y <- updateMDB next (mdbPrev_update (\<lambda>_. slot));
y <- updateMDB parent (mdbNext_update (\<lambda>_. slot));
updateNewFreeIndex slot
od) (IF next \<noteq> 0 THEN
  Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr next} (CALL mdb_node_ptr_set_mdbPrev_'proc(mdb_Ptr &(cte_Ptr next\<rightarrow>[''cteMDBNode_C'']),ptr_val (cte_Ptr slot)))
FI;;
Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr parent} (CALL mdb_node_ptr_set_mdbNext_'proc(mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C'']),ptr_val (cte_Ptr slot))))
 2. \<And>slota parenta capa next rv' oldCTE. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; nullCapPointers oldCTE\<rbrakk> \<Longrightarrow> \<lbrace>?R1056 slota parenta capa next oldCTE\<rbrace> setCTE slot (CTE cap (MDB next parent True True)) \<lbrace>?Q1050 slota parenta capa next rv' oldCTE\<rbrace>
 3. \<And>slota parenta capa next rv' oldCTE. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; nullCapPointers oldCTE\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'1050 slota parenta capa next rv' oldCTE) \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C''])) capa));;
\<acute>ret__struct_mdb_node_C :== CALL mdb_node_new_'proc(ptr_val (cte_Ptr next),SCAST(32 signed \<rightarrow> 32) true,SCAST(32 signed \<rightarrow> 32) true,ptr_val (cte_Ptr parent));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr slot} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(cte_Ptr slot\<rightarrow>[''cteMDBNode_C''])) \<acute>ret__struct_mdb_node_C))) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> ?Q'1050 slota parenta capa next rv' oldCTE rv (xfdc s)}
 4. \<And>slota parenta capa. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<lbrace>?R685 (cte_Ptr slot) (cte_Ptr parent) capa\<rbrace> liftM (mdbNext \<circ> cteMDBNode) (getCTE parent) \<lbrace>\<lambda>a b. \<forall>cte. ctes_of b slot = Some cte \<longrightarrow> (cte_wp_at' (\<lambda>_. True) slot and K (is_aligned a 3 \<and> is_aligned parent 3) and ?R1056 slota parenta capa a cte and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr slot))) b\<rbrace>
 5. \<And>slota parenta capa. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F680 slota parenta capa\<^esub> (?R'682 (cte_Ptr slot) (cte_Ptr parent) capa) \<acute>ret__unsigned :== CALL mdb_node_get_mdbNext_'proc(h_val (hrs_mem \<acute>t_hrs) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C'']))) {s. \<forall>next. next = ret__unsigned_' s \<longrightarrow> s \<in> {sa. next_'_update (\<lambda>_. cte_Ptr (ret__unsigned_' s)) sa \<in> {sa. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift sa) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> sa \<in> UNIV \<inter> ?R'1053 slota parenta capa next (ret__unsigned_' s) (ret__unsigned_' s) cte' \<inter> \<lbrace>True\<rbrace>}}}
 6. \<And>slota parenta capa s s'. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; (s, s') \<in> rf_sr; (pspace_aligned' and valid_mdb' and valid_objs' and valid_cap' cap) s; s' \<in> {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0}\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) parent s \<longrightarrow> ((\<lambda>_. True) and ?R685 slota parenta capa and cte_wp_at' (\<lambda>_. True) (ptr_val parenta)) s) \<and> s' \<in> UNIV \<inter> ?R'682 slota parenta capa \<inter> \<lbrace>True\<rbrace>
flex-flex pairs:
\<lambda>slota parenta capa next. ?R'1053 slota parenta capa next next \<equiv>\<^sup>? \<lambda>slota parenta capa next rv' cte'. ?R'1050 slota parenta capa next rv' (cte_to_H cte') proof (prove)
goal (8 subgoals):
 1. \<And>slota parenta capa next rv' oldCTE rv xfdca rva xfdcb. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; nullCapPointers oldCTE; dc rv xfdca; dc rva xfdcb\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1090 slota parenta capa next rv' oldCTE rv xfdca rva) (?Q'1090 slota parenta capa next rv' oldCTE rv xfdca rva xfdcb) [SKIP] (do y <- updateMDB parent (mdbNext_update (\<lambda>_. slot));
updateNewFreeIndex slot
od) (Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr parent} (CALL mdb_node_ptr_set_mdbNext_'proc(mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C'']),ptr_val (cte_Ptr slot))))
 2. \<And>slota parenta capa next rv' oldCTE rv xfdc. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; nullCapPointers oldCTE; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1097 (cte_Ptr slot) (cte_Ptr parent) capa next rv' oldCTE rv\<rbrace> updateMDB next (mdbPrev_update (\<lambda>_. slot)) \<lbrace>?Q1090 slota parenta capa next rv' oldCTE rv xfdc\<rbrace>
 3. \<And>slota parenta capa next rv' oldCTE rv xfdca. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; nullCapPointers oldCTE; dc rv xfdca\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'1091 (cte_Ptr slot) (cte_Ptr parent) capa next rv' oldCTE rv xfdca) IF next \<noteq> 0 THEN
  Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr next} (CALL mdb_node_ptr_set_mdbPrev_'proc(mdb_Ptr &(cte_Ptr next\<rightarrow>[''cteMDBNode_C'']),ptr_val (cte_Ptr slot)))
FI {s. \<forall>rva. dc rva (xfdc s) \<longrightarrow> s \<in> ?Q'1090 slota parenta capa next rv' oldCTE rv xfdca rva (xfdc s)}
 4. \<And>slota parenta capa next rv' oldCTE. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; nullCapPointers oldCTE\<rbrakk> \<Longrightarrow> \<lbrace>?R1056 slota parenta capa next oldCTE\<rbrace> setCTE slot (CTE cap (MDB next parent True True)) \<lbrace>\<lambda>a. (\<lambda>a. is_aligned next 3 \<and> (slot \<noteq> 0 \<longrightarrow> is_aligned slot 3)) and ?R1097 slota parenta capa next rv' oldCTE a\<rbrace>
 5. \<And>slota parenta capa next rv' oldCTE. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; nullCapPointers oldCTE\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'1050 slota parenta capa next rv' oldCTE) \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C''])) capa));;
\<acute>ret__struct_mdb_node_C :== CALL mdb_node_new_'proc(ptr_val (cte_Ptr next),SCAST(32 signed \<rightarrow> 32) true,SCAST(32 signed \<rightarrow> 32) true,ptr_val (cte_Ptr parent));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr slot} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(cte_Ptr slot\<rightarrow>[''cteMDBNode_C''])) \<acute>ret__struct_mdb_node_C))) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> \<lbrace>ptr_val slota = slot\<rbrace> \<inter> ?R'1091 slota parenta capa next rv' oldCTE rv (xfdc s)}
 6. \<And>slota parenta capa. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<lbrace>?R685 (cte_Ptr slot) (cte_Ptr parent) capa\<rbrace> liftM (mdbNext \<circ> cteMDBNode) (getCTE parent) \<lbrace>\<lambda>a b. \<forall>cte. ctes_of b slot = Some cte \<longrightarrow> (cte_wp_at' (\<lambda>_. True) slot and K (is_aligned a 3 \<and> is_aligned parent 3) and ?R1056 slota parenta capa a cte and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr slot))) b\<rbrace>
 7. \<And>slota parenta capa. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F680 slota parenta capa\<^esub> (?R'682 (cte_Ptr slot) (cte_Ptr parent) capa) \<acute>ret__unsigned :== CALL mdb_node_get_mdbNext_'proc(h_val (hrs_mem \<acute>t_hrs) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C'']))) {s. \<forall>next. next = ret__unsigned_' s \<longrightarrow> s \<in> {sa. next_'_update (\<lambda>_. cte_Ptr (ret__unsigned_' s)) sa \<in> {sa. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift sa) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> sa \<in> UNIV \<inter> ?R'1053 slota parenta capa next (ret__unsigned_' s) (ret__unsigned_' s) cte' \<inter> \<lbrace>True\<rbrace>}}}
 8. \<And>slota parenta capa s s'. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; (s, s') \<in> rf_sr; (pspace_aligned' and valid_mdb' and valid_objs' and valid_cap' cap) s; s' \<in> {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0}\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) parent s \<longrightarrow> ((\<lambda>_. True) and ?R685 slota parenta capa and cte_wp_at' (\<lambda>_. True) (ptr_val parenta)) s) \<and> s' \<in> UNIV \<inter> ?R'682 slota parenta capa \<inter> \<lbrace>True\<rbrace>
flex-flex pairs:
\<lambda>slota parenta capa next. ?R'1053 slota parenta capa next next \<equiv>\<^sup>? \<lambda>slota parenta capa next rv' cte'. ?R'1050 slota parenta capa next rv' (cte_to_H cte') proof (prove)
goal (8 subgoals):
 1. \<And>slota parenta capa next rv' oldCTE rv xfdca rva xfdcb. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; nullCapPointers oldCTE; dc rv xfdca; dc rva xfdcb\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1090 slota parenta capa next rv' oldCTE rv xfdca rva) (?Q'1090 slota parenta capa next rv' oldCTE rv xfdca rva xfdcb) [SKIP] (do y <- updateMDB parent (mdbNext_update (\<lambda>_. slot));
updateNewFreeIndex slot
od) (Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr parent} (CALL mdb_node_ptr_set_mdbNext_'proc(mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C'']),ptr_val (cte_Ptr slot)));;
SKIP)
 2. \<And>slota parenta capa next rv' oldCTE rv xfdc. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; nullCapPointers oldCTE; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1097 (cte_Ptr slot) (cte_Ptr parent) capa next rv' oldCTE rv\<rbrace> updateMDB next (mdbPrev_update (\<lambda>_. slot)) \<lbrace>?Q1090 slota parenta capa next rv' oldCTE rv xfdc\<rbrace>
 3. \<And>slota parenta capa next rv' oldCTE rv xfdca. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; nullCapPointers oldCTE; dc rv xfdca\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'1091 (cte_Ptr slot) (cte_Ptr parent) capa next rv' oldCTE rv xfdca) IF next \<noteq> 0 THEN
  Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr next} (CALL mdb_node_ptr_set_mdbPrev_'proc(mdb_Ptr &(cte_Ptr next\<rightarrow>[''cteMDBNode_C'']),ptr_val (cte_Ptr slot)))
FI {s. \<forall>rva. dc rva (xfdc s) \<longrightarrow> s \<in> ?Q'1090 slota parenta capa next rv' oldCTE rv xfdca rva (xfdc s)}
 4. \<And>slota parenta capa next rv' oldCTE. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; nullCapPointers oldCTE\<rbrakk> \<Longrightarrow> \<lbrace>?R1056 slota parenta capa next oldCTE\<rbrace> setCTE slot (CTE cap (MDB next parent True True)) \<lbrace>\<lambda>a. (\<lambda>a. is_aligned next 3 \<and> (slot \<noteq> 0 \<longrightarrow> is_aligned slot 3)) and ?R1097 slota parenta capa next rv' oldCTE a\<rbrace>
 5. \<And>slota parenta capa next rv' oldCTE. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; nullCapPointers oldCTE\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'1050 slota parenta capa next rv' oldCTE) \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C''])) capa));;
\<acute>ret__struct_mdb_node_C :== CALL mdb_node_new_'proc(ptr_val (cte_Ptr next),SCAST(32 signed \<rightarrow> 32) true,SCAST(32 signed \<rightarrow> 32) true,ptr_val (cte_Ptr parent));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr slot} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(cte_Ptr slot\<rightarrow>[''cteMDBNode_C''])) \<acute>ret__struct_mdb_node_C))) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> \<lbrace>ptr_val slota = slot\<rbrace> \<inter> ?R'1091 slota parenta capa next rv' oldCTE rv (xfdc s)}
 6. \<And>slota parenta capa. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<lbrace>?R685 (cte_Ptr slot) (cte_Ptr parent) capa\<rbrace> liftM (mdbNext \<circ> cteMDBNode) (getCTE parent) \<lbrace>\<lambda>a b. \<forall>cte. ctes_of b slot = Some cte \<longrightarrow> (cte_wp_at' (\<lambda>_. True) slot and K (is_aligned a 3 \<and> is_aligned parent 3) and ?R1056 slota parenta capa a cte and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr slot))) b\<rbrace>
 7. \<And>slota parenta capa. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F680 slota parenta capa\<^esub> (?R'682 (cte_Ptr slot) (cte_Ptr parent) capa) \<acute>ret__unsigned :== CALL mdb_node_get_mdbNext_'proc(h_val (hrs_mem \<acute>t_hrs) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C'']))) {s. \<forall>next. next = ret__unsigned_' s \<longrightarrow> s \<in> {sa. next_'_update (\<lambda>_. cte_Ptr (ret__unsigned_' s)) sa \<in> {sa. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift sa) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> sa \<in> UNIV \<inter> ?R'1053 slota parenta capa next (ret__unsigned_' s) (ret__unsigned_' s) cte' \<inter> \<lbrace>True\<rbrace>}}}
 8. \<And>slota parenta capa s s'. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; (s, s') \<in> rf_sr; (pspace_aligned' and valid_mdb' and valid_objs' and valid_cap' cap) s; s' \<in> {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0}\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) parent s \<longrightarrow> ((\<lambda>_. True) and ?R685 slota parenta capa and cte_wp_at' (\<lambda>_. True) (ptr_val parenta)) s) \<and> s' \<in> UNIV \<inter> ?R'682 slota parenta capa \<inter> \<lbrace>True\<rbrace>
flex-flex pairs:
\<lambda>slota parenta capa next. ?R'1053 slota parenta capa next next \<equiv>\<^sup>? \<lambda>slota parenta capa next rv' cte'. ?R'1050 slota parenta capa next rv' (cte_to_H cte') proof (prove)
goal (10 subgoals):
 1. \<And>slota parenta capa next rv' oldCTE rv xfdca rva xfdcb rvb xfdcc. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; nullCapPointers oldCTE; dc rv xfdca; dc rva xfdcb; dc rvb xfdcc\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1139 slota parenta capa next rv' oldCTE rv xfdca rva xfdcb rvb) (?Q'1139 slota parenta capa next rv' oldCTE rv xfdca rva xfdcb rvb xfdcc) [SKIP] (updateNewFreeIndex slot) SKIP
 2. \<And>slota parenta capa next rv' oldCTE rv xfdca rva xfdc. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; nullCapPointers oldCTE; dc rv xfdca; dc rva xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1143 slota parenta capa next rv' oldCTE rv xfdca rva\<rbrace> updateMDB parent (mdbNext_update (\<lambda>_. slot)) \<lbrace>?Q1139 slota parenta capa next rv' oldCTE rv xfdca rva xfdc\<rbrace>
 3. \<And>slota parenta capa next rv' oldCTE rv xfdca rva xfdcb. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; nullCapPointers oldCTE; dc rv xfdca; dc rva xfdcb\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'1139 slota parenta capa next rv' oldCTE rv xfdca rva xfdcb) CALL mdb_node_ptr_set_mdbNext_'proc(mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C'']),ptr_val (cte_Ptr slot)) {s. \<forall>rvb. dc rvb (xfdc s) \<longrightarrow> s \<in> ?Q'1139 slota parenta capa next rv' oldCTE rv xfdca rva xfdcb rvb (xfdc s)}
 4. \<And>slota parenta capa next rv' oldCTE rv xfdc. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; nullCapPointers oldCTE; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1097 (cte_Ptr slot) (cte_Ptr parent) capa next rv' oldCTE rv\<rbrace> updateMDB next (mdbPrev_update (\<lambda>_. slot)) \<lbrace>\<lambda>a. (\<lambda>a. parent \<noteq> 0 \<and> (slot \<noteq> 0 \<longrightarrow> is_aligned slot 3)) and ?R1143 slota parenta capa next rv' oldCTE rv xfdc a and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr parent))\<rbrace>
 5. \<And>slota parenta capa next rv' oldCTE rv xfdca. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; nullCapPointers oldCTE; dc rv xfdca\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'1091 (cte_Ptr slot) (cte_Ptr parent) capa next rv' oldCTE rv xfdca) IF next \<noteq> 0 THEN
  Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr next} (CALL mdb_node_ptr_set_mdbPrev_'proc(mdb_Ptr &(cte_Ptr next\<rightarrow>[''cteMDBNode_C'']),ptr_val (cte_Ptr slot)))
FI {s. \<forall>rva. dc rva (xfdc s) \<longrightarrow> s \<in> {s. v32_'_update (\<lambda>_. ptr_val (cte_Ptr slot)) (mdb_node_ptr_'_update (\<lambda>_. mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C''])) s) \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = slot\<rbrace>} \<inter> ?R'1139 slota parenta capa next rv' oldCTE rv xfdca rva (xfdc s) \<inter> \<lbrace>True\<rbrace>}
 6. \<And>slota parenta capa next rv' oldCTE. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; nullCapPointers oldCTE\<rbrakk> \<Longrightarrow> \<lbrace>?R1056 slota parenta capa next oldCTE\<rbrace> setCTE slot (CTE cap (MDB next parent True True)) \<lbrace>\<lambda>a. (\<lambda>a. is_aligned next 3 \<and> (slot \<noteq> 0 \<longrightarrow> is_aligned slot 3)) and ?R1097 slota parenta capa next rv' oldCTE a\<rbrace>
 7. \<And>slota parenta capa next rv' oldCTE. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; nullCapPointers oldCTE\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'1050 slota parenta capa next rv' oldCTE) \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C''])) capa));;
\<acute>ret__struct_mdb_node_C :== CALL mdb_node_new_'proc(ptr_val (cte_Ptr next),SCAST(32 signed \<rightarrow> 32) true,SCAST(32 signed \<rightarrow> 32) true,ptr_val (cte_Ptr parent));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr slot} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(cte_Ptr slot\<rightarrow>[''cteMDBNode_C''])) \<acute>ret__struct_mdb_node_C))) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> \<lbrace>ptr_val slota = slot\<rbrace> \<inter> ?R'1091 slota parenta capa next rv' oldCTE rv (xfdc s)}
 8. \<And>slota parenta capa. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<lbrace>?R685 (cte_Ptr slot) (cte_Ptr parent) capa\<rbrace> liftM (mdbNext \<circ> cteMDBNode) (getCTE parent) \<lbrace>\<lambda>a b. \<forall>cte. ctes_of b slot = Some cte \<longrightarrow> (cte_wp_at' (\<lambda>_. True) slot and K (is_aligned a 3 \<and> is_aligned parent 3) and ?R1056 slota parenta capa a cte and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr slot))) b\<rbrace>
 9. \<And>slota parenta capa. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F680 slota parenta capa\<^esub> (?R'682 (cte_Ptr slot) (cte_Ptr parent) capa) \<acute>ret__unsigned :== CALL mdb_node_get_mdbNext_'proc(h_val (hrs_mem \<acute>t_hrs) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C'']))) {s. \<forall>next. next = ret__unsigned_' s \<longrightarrow> s \<in> {sa. next_'_update (\<lambda>_. cte_Ptr (ret__unsigned_' s)) sa \<in> {sa. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift sa) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> sa \<in> UNIV \<inter> ?R'1053 slota parenta capa next (ret__unsigned_' s) (ret__unsigned_' s) cte' \<inter> \<lbrace>True\<rbrace>}}}
 10. \<And>slota parenta capa s s'. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; (s, s') \<in> rf_sr; (pspace_aligned' and valid_mdb' and valid_objs' and valid_cap' cap) s; s' \<in> {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0}\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) parent s \<longrightarrow> ((\<lambda>_. True) and ?R685 slota parenta capa and cte_wp_at' (\<lambda>_. True) (ptr_val parenta)) s) \<and> s' \<in> UNIV \<inter> ?R'682 slota parenta capa \<inter> \<lbrace>True\<rbrace>
flex-flex pairs:
\<lambda>slota parenta capa next. ?R'1053 slota parenta capa next next \<equiv>\<^sup>? \<lambda>slota parenta capa next rv' cte'. ?R'1050 slota parenta capa next rv' (cte_to_H cte') proof (prove)
goal (9 subgoals):
 1. \<And>slota parenta capa next rv' oldCTE rv xfdca rva xfdc. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; nullCapPointers oldCTE; dc rv xfdca; dc rva xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1143 slota parenta capa next rv' oldCTE rv xfdca rva\<rbrace> updateMDB parent (mdbNext_update (\<lambda>_. slot)) \<lbrace>\<lambda>a. valid_objs' and cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot\<rbrace>
 2. \<And>slota parenta capa next rv' oldCTE rv xfdca rva xfdcb. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; nullCapPointers oldCTE; dc rv xfdca; dc rva xfdcb\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'1139 slota parenta capa next rv' oldCTE rv xfdca rva xfdcb) CALL mdb_node_ptr_set_mdbNext_'proc(mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C'']),ptr_val (cte_Ptr slot)) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0}}
 3. \<And>slota parenta capa next rv' oldCTE rv xfdc. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; nullCapPointers oldCTE; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1097 (cte_Ptr slot) (cte_Ptr parent) capa next rv' oldCTE rv\<rbrace> updateMDB next (mdbPrev_update (\<lambda>_. slot)) \<lbrace>\<lambda>a. (\<lambda>a. parent \<noteq> 0 \<and> (slot \<noteq> 0 \<longrightarrow> is_aligned slot 3)) and ?R1143 slota parenta capa next rv' oldCTE rv xfdc a and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr parent))\<rbrace>
 4. \<And>slota parenta capa next rv' oldCTE rv xfdca. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; nullCapPointers oldCTE; dc rv xfdca\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'1091 (cte_Ptr slot) (cte_Ptr parent) capa next rv' oldCTE rv xfdca) IF next \<noteq> 0 THEN
  Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr next} (CALL mdb_node_ptr_set_mdbPrev_'proc(mdb_Ptr &(cte_Ptr next\<rightarrow>[''cteMDBNode_C'']),ptr_val (cte_Ptr slot)))
FI {s. \<forall>rva. dc rva (xfdc s) \<longrightarrow> s \<in> {s. v32_'_update (\<lambda>_. ptr_val (cte_Ptr slot)) (mdb_node_ptr_'_update (\<lambda>_. mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C''])) s) \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = slot\<rbrace>} \<inter> ?R'1139 slota parenta capa next rv' oldCTE rv xfdca rva (xfdc s) \<inter> \<lbrace>True\<rbrace>}
 5. \<And>slota parenta capa next rv' oldCTE. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; nullCapPointers oldCTE\<rbrakk> \<Longrightarrow> \<lbrace>?R1056 slota parenta capa next oldCTE\<rbrace> setCTE slot (CTE cap (MDB next parent True True)) \<lbrace>\<lambda>a. (\<lambda>a. is_aligned next 3 \<and> (slot \<noteq> 0 \<longrightarrow> is_aligned slot 3)) and ?R1097 slota parenta capa next rv' oldCTE a\<rbrace>
 6. \<And>slota parenta capa next rv' oldCTE. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; nullCapPointers oldCTE\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'1050 slota parenta capa next rv' oldCTE) \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C''])) capa));;
\<acute>ret__struct_mdb_node_C :== CALL mdb_node_new_'proc(ptr_val (cte_Ptr next),SCAST(32 signed \<rightarrow> 32) true,SCAST(32 signed \<rightarrow> 32) true,ptr_val (cte_Ptr parent));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr slot} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(cte_Ptr slot\<rightarrow>[''cteMDBNode_C''])) \<acute>ret__struct_mdb_node_C))) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> \<lbrace>ptr_val slota = slot\<rbrace> \<inter> ?R'1091 slota parenta capa next rv' oldCTE rv (xfdc s)}
 7. \<And>slota parenta capa. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<lbrace>?R685 (cte_Ptr slot) (cte_Ptr parent) capa\<rbrace> liftM (mdbNext \<circ> cteMDBNode) (getCTE parent) \<lbrace>\<lambda>a b. \<forall>cte. ctes_of b slot = Some cte \<longrightarrow> (cte_wp_at' (\<lambda>_. True) slot and K (is_aligned a 3 \<and> is_aligned parent 3) and ?R1056 slota parenta capa a cte and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr slot))) b\<rbrace>
 8. \<And>slota parenta capa. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F680 slota parenta capa\<^esub> (?R'682 (cte_Ptr slot) (cte_Ptr parent) capa) \<acute>ret__unsigned :== CALL mdb_node_get_mdbNext_'proc(h_val (hrs_mem \<acute>t_hrs) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C'']))) {s. \<forall>next. next = ret__unsigned_' s \<longrightarrow> s \<in> {sa. next_'_update (\<lambda>_. cte_Ptr (ret__unsigned_' s)) sa \<in> {sa. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift sa) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> sa \<in> UNIV \<inter> ?R'1053 slota parenta capa next (ret__unsigned_' s) (ret__unsigned_' s) cte' \<inter> \<lbrace>True\<rbrace>}}}
 9. \<And>slota parenta capa s s'. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; (s, s') \<in> rf_sr; (pspace_aligned' and valid_mdb' and valid_objs' and valid_cap' cap) s; s' \<in> {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0}\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) parent s \<longrightarrow> ((\<lambda>_. True) and ?R685 slota parenta capa and cte_wp_at' (\<lambda>_. True) (ptr_val parenta)) s) \<and> s' \<in> UNIV \<inter> ?R'682 slota parenta capa \<inter> \<lbrace>True\<rbrace>
flex-flex pairs:
\<lambda>slota parenta capa next. ?R'1053 slota parenta capa next next \<equiv>\<^sup>? \<lambda>slota parenta capa next rv' cte'. ?R'1050 slota parenta capa next rv' (cte_to_H cte') proof (prove)
goal (8 subgoals):
 1. \<And>slota parenta capa next rv' oldCTE rv xfdca rva xfdcb. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; nullCapPointers oldCTE; dc rv xfdca; dc rva xfdcb\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'1139 slota parenta capa next rv' oldCTE rv xfdca rva xfdcb) CALL mdb_node_ptr_set_mdbNext_'proc(mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C'']),ptr_val (cte_Ptr slot)) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0}}
 2. \<And>slota parenta capa next rv' oldCTE rv xfdc. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; nullCapPointers oldCTE; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1097 (cte_Ptr slot) (cte_Ptr parent) capa next rv' oldCTE rv\<rbrace> updateMDB next (mdbPrev_update (\<lambda>_. slot)) \<lbrace>\<lambda>a. (\<lambda>a. parent \<noteq> 0 \<and> (slot \<noteq> 0 \<longrightarrow> is_aligned slot 3)) and (\<lambda>a. valid_objs' a \<and> cte_wp_at' (\<lambda>c. cteCap c = cap) slot a) and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr parent))\<rbrace>
 3. \<And>slota parenta capa next rv' oldCTE rv xfdca. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; nullCapPointers oldCTE; dc rv xfdca\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'1091 (cte_Ptr slot) (cte_Ptr parent) capa next rv' oldCTE rv xfdca) IF next \<noteq> 0 THEN
  Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr next} (CALL mdb_node_ptr_set_mdbPrev_'proc(mdb_Ptr &(cte_Ptr next\<rightarrow>[''cteMDBNode_C'']),ptr_val (cte_Ptr slot)))
FI {s. \<forall>rva. dc rva (xfdc s) \<longrightarrow> s \<in> {s. v32_'_update (\<lambda>_. ptr_val (cte_Ptr slot)) (mdb_node_ptr_'_update (\<lambda>_. mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C''])) s) \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = slot\<rbrace>} \<inter> ?R'1139 slota parenta capa next rv' oldCTE rv xfdca rva (xfdc s) \<inter> \<lbrace>True\<rbrace>}
 4. \<And>slota parenta capa next rv' oldCTE. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; nullCapPointers oldCTE\<rbrakk> \<Longrightarrow> \<lbrace>?R1056 slota parenta capa next oldCTE\<rbrace> setCTE slot (CTE cap (MDB next parent True True)) \<lbrace>\<lambda>a. (\<lambda>a. is_aligned next 3 \<and> (slot \<noteq> 0 \<longrightarrow> is_aligned slot 3)) and ?R1097 slota parenta capa next rv' oldCTE a\<rbrace>
 5. \<And>slota parenta capa next rv' oldCTE. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; nullCapPointers oldCTE\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'1050 slota parenta capa next rv' oldCTE) \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C''])) capa));;
\<acute>ret__struct_mdb_node_C :== CALL mdb_node_new_'proc(ptr_val (cte_Ptr next),SCAST(32 signed \<rightarrow> 32) true,SCAST(32 signed \<rightarrow> 32) true,ptr_val (cte_Ptr parent));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr slot} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(cte_Ptr slot\<rightarrow>[''cteMDBNode_C''])) \<acute>ret__struct_mdb_node_C))) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> \<lbrace>ptr_val slota = slot\<rbrace> \<inter> ?R'1091 slota parenta capa next rv' oldCTE rv (xfdc s)}
 6. \<And>slota parenta capa. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<lbrace>?R685 (cte_Ptr slot) (cte_Ptr parent) capa\<rbrace> liftM (mdbNext \<circ> cteMDBNode) (getCTE parent) \<lbrace>\<lambda>a b. \<forall>cte. ctes_of b slot = Some cte \<longrightarrow> (cte_wp_at' (\<lambda>_. True) slot and K (is_aligned a 3 \<and> is_aligned parent 3) and ?R1056 slota parenta capa a cte and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr slot))) b\<rbrace>
 7. \<And>slota parenta capa. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F680 slota parenta capa\<^esub> (?R'682 (cte_Ptr slot) (cte_Ptr parent) capa) \<acute>ret__unsigned :== CALL mdb_node_get_mdbNext_'proc(h_val (hrs_mem \<acute>t_hrs) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C'']))) {s. \<forall>next. next = ret__unsigned_' s \<longrightarrow> s \<in> {sa. next_'_update (\<lambda>_. cte_Ptr (ret__unsigned_' s)) sa \<in> {sa. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift sa) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> sa \<in> UNIV \<inter> ?R'1053 slota parenta capa next (ret__unsigned_' s) (ret__unsigned_' s) cte' \<inter> \<lbrace>True\<rbrace>}}}
 8. \<And>slota parenta capa s s'. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; (s, s') \<in> rf_sr; (pspace_aligned' and valid_mdb' and valid_objs' and valid_cap' cap) s; s' \<in> {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0}\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) parent s \<longrightarrow> ((\<lambda>_. True) and ?R685 slota parenta capa and cte_wp_at' (\<lambda>_. True) (ptr_val parenta)) s) \<and> s' \<in> UNIV \<inter> ?R'682 slota parenta capa \<inter> \<lbrace>True\<rbrace>
flex-flex pairs:
\<lambda>slota parenta capa next. ?R'1053 slota parenta capa next next \<equiv>\<^sup>? \<lambda>slota parenta capa next rv' cte'. ?R'1050 slota parenta capa next rv' (cte_to_H cte') proof (prove)
goal (8 subgoals):
 1. \<And>slota parenta capa next rv' oldCTE xfdca xfdc. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; nullCapPointers oldCTE\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'1139 (cte_Ptr slot) (cte_Ptr parent) capa next rv' oldCTE () xfdca () xfdc) CALL mdb_node_ptr_set_mdbNext_'proc(mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C'']),slot) {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0}
 2. \<And>slota parenta capa next rv' oldCTE rv xfdc. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; nullCapPointers oldCTE; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1097 (cte_Ptr slot) (cte_Ptr parent) capa next rv' oldCTE rv\<rbrace> updateMDB next (mdbPrev_update (\<lambda>_. slot)) \<lbrace>\<lambda>a. (\<lambda>a. parent \<noteq> 0 \<and> (slot \<noteq> 0 \<longrightarrow> is_aligned slot 3)) and (\<lambda>a. valid_objs' a \<and> cte_wp_at' (\<lambda>c. cteCap c = cap) slot a) and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr parent))\<rbrace>
 3. \<And>slota parenta capa next rv' oldCTE rv xfdca. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; nullCapPointers oldCTE; dc rv xfdca\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'1091 (cte_Ptr slot) (cte_Ptr parent) capa next rv' oldCTE rv xfdca) IF next \<noteq> 0 THEN
  Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr next} (CALL mdb_node_ptr_set_mdbPrev_'proc(mdb_Ptr &(cte_Ptr next\<rightarrow>[''cteMDBNode_C'']),ptr_val (cte_Ptr slot)))
FI {s. \<forall>rva. dc rva (xfdc s) \<longrightarrow> s \<in> {s. v32_'_update (\<lambda>_. ptr_val (cte_Ptr slot)) (mdb_node_ptr_'_update (\<lambda>_. mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C''])) s) \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = slot\<rbrace>} \<inter> ?R'1139 slota parenta capa next rv' oldCTE rv xfdca rva (xfdc s) \<inter> \<lbrace>True\<rbrace>}
 4. \<And>slota parenta capa next rv' oldCTE. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; nullCapPointers oldCTE\<rbrakk> \<Longrightarrow> \<lbrace>?R1056 slota parenta capa next oldCTE\<rbrace> setCTE slot (CTE cap (MDB next parent True True)) \<lbrace>\<lambda>a. (\<lambda>a. is_aligned next 3 \<and> (slot \<noteq> 0 \<longrightarrow> is_aligned slot 3)) and ?R1097 slota parenta capa next rv' oldCTE a\<rbrace>
 5. \<And>slota parenta capa next rv' oldCTE. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; nullCapPointers oldCTE\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'1050 slota parenta capa next rv' oldCTE) \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C''])) capa));;
\<acute>ret__struct_mdb_node_C :== CALL mdb_node_new_'proc(ptr_val (cte_Ptr next),SCAST(32 signed \<rightarrow> 32) true,SCAST(32 signed \<rightarrow> 32) true,ptr_val (cte_Ptr parent));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr slot} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(cte_Ptr slot\<rightarrow>[''cteMDBNode_C''])) \<acute>ret__struct_mdb_node_C))) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> \<lbrace>ptr_val slota = slot\<rbrace> \<inter> ?R'1091 slota parenta capa next rv' oldCTE rv (xfdc s)}
 6. \<And>slota parenta capa. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<lbrace>?R685 (cte_Ptr slot) (cte_Ptr parent) capa\<rbrace> liftM (mdbNext \<circ> cteMDBNode) (getCTE parent) \<lbrace>\<lambda>a b. \<forall>cte. ctes_of b slot = Some cte \<longrightarrow> (cte_wp_at' (\<lambda>_. True) slot and K (is_aligned a 3 \<and> is_aligned parent 3) and ?R1056 slota parenta capa a cte and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr slot))) b\<rbrace>
 7. \<And>slota parenta capa. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F680 slota parenta capa\<^esub> (?R'682 (cte_Ptr slot) (cte_Ptr parent) capa) \<acute>ret__unsigned :== CALL mdb_node_get_mdbNext_'proc(h_val (hrs_mem \<acute>t_hrs) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C'']))) {s. \<forall>next. next = ret__unsigned_' s \<longrightarrow> s \<in> {sa. next_'_update (\<lambda>_. cte_Ptr (ret__unsigned_' s)) sa \<in> {sa. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift sa) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> sa \<in> UNIV \<inter> ?R'1053 slota parenta capa next (ret__unsigned_' s) (ret__unsigned_' s) cte' \<inter> \<lbrace>True\<rbrace>}}}
 8. \<And>slota parenta capa s s'. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; (s, s') \<in> rf_sr; (pspace_aligned' and valid_mdb' and valid_objs' and valid_cap' cap) s; s' \<in> {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0}\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) parent s \<longrightarrow> ((\<lambda>_. True) and ?R685 slota parenta capa and cte_wp_at' (\<lambda>_. True) (ptr_val parenta)) s) \<and> s' \<in> UNIV \<inter> ?R'682 slota parenta capa \<inter> \<lbrace>True\<rbrace>
flex-flex pairs:
\<lambda>slota parenta capa next. ?R'1053 slota parenta capa next next \<equiv>\<^sup>? \<lambda>slota parenta capa next rv' cte'. ?R'1050 slota parenta capa next rv' (cte_to_H cte') proof (prove)
goal (7 subgoals):
 1. \<And>slota parenta capa next rv' oldCTE rv xfdc. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; nullCapPointers oldCTE; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R1097 (cte_Ptr slot) (cte_Ptr parent) capa next rv' oldCTE rv\<rbrace> updateMDB next (mdbPrev_update (\<lambda>_. slot)) \<lbrace>\<lambda>a. (\<lambda>a. parent \<noteq> 0 \<and> (slot \<noteq> 0 \<longrightarrow> is_aligned slot 3)) and (\<lambda>a. valid_objs' a \<and> cte_wp_at' (\<lambda>c. cteCap c = cap) slot a) and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr parent))\<rbrace>
 2. \<And>slota parenta capa next rv' oldCTE rv xfdca. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; nullCapPointers oldCTE; dc rv xfdca\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'1091 (cte_Ptr slot) (cte_Ptr parent) capa next rv' oldCTE rv xfdca) IF next \<noteq> 0 THEN
  Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr next} (CALL mdb_node_ptr_set_mdbPrev_'proc(mdb_Ptr &(cte_Ptr next\<rightarrow>[''cteMDBNode_C'']),ptr_val (cte_Ptr slot)))
FI {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {s. v32_'_update (\<lambda>_. ptr_val (cte_Ptr slot)) (mdb_node_ptr_'_update (\<lambda>_. mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C''])) s) \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = slot\<rbrace>} \<inter> {s. \<forall>t. hrs_htd (t_hrs_' (globals t)) = hrs_htd (t_hrs_' (globals s)) \<and> byte_regions_unmodified (t_hrs_' (globals s)) (t_hrs_' (globals t)) \<longrightarrow> (case untypedZeroRange cap of None \<Rightarrow> True | Some (aa, b) \<Rightarrow> region_actually_is_bytes aa (unat (b + 1 - aa)) s \<and> heap_list (hrs_mem (t_hrs_' (globals t))) (unat (b + 1 - aa)) aa = replicate (unat (b + 1 - aa)) 0)} \<inter> \<lbrace>True\<rbrace>}
 3. \<And>slota parenta capa next rv' oldCTE. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; nullCapPointers oldCTE\<rbrakk> \<Longrightarrow> \<lbrace>?R1056 slota parenta capa next oldCTE\<rbrace> setCTE slot (CTE cap (MDB next parent True True)) \<lbrace>\<lambda>a. (\<lambda>a. is_aligned next 3 \<and> (slot \<noteq> 0 \<longrightarrow> is_aligned slot 3)) and ?R1097 slota parenta capa next rv' oldCTE a\<rbrace>
 4. \<And>slota parenta capa next rv' oldCTE. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; nullCapPointers oldCTE\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'1050 slota parenta capa next rv' oldCTE) \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C''])) capa));;
\<acute>ret__struct_mdb_node_C :== CALL mdb_node_new_'proc(ptr_val (cte_Ptr next),SCAST(32 signed \<rightarrow> 32) true,SCAST(32 signed \<rightarrow> 32) true,ptr_val (cte_Ptr parent));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr slot} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(cte_Ptr slot\<rightarrow>[''cteMDBNode_C''])) \<acute>ret__struct_mdb_node_C))) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> \<lbrace>ptr_val slota = slot\<rbrace> \<inter> ?R'1091 slota parenta capa next rv' oldCTE rv (xfdc s)}
 5. \<And>slota parenta capa. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<lbrace>?R685 (cte_Ptr slot) (cte_Ptr parent) capa\<rbrace> liftM (mdbNext \<circ> cteMDBNode) (getCTE parent) \<lbrace>\<lambda>a b. \<forall>cte. ctes_of b slot = Some cte \<longrightarrow> (cte_wp_at' (\<lambda>_. True) slot and K (is_aligned a 3 \<and> is_aligned parent 3) and ?R1056 slota parenta capa a cte and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr slot))) b\<rbrace>
 6. \<And>slota parenta capa. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F680 slota parenta capa\<^esub> (?R'682 (cte_Ptr slot) (cte_Ptr parent) capa) \<acute>ret__unsigned :== CALL mdb_node_get_mdbNext_'proc(h_val (hrs_mem \<acute>t_hrs) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C'']))) {s. \<forall>next. next = ret__unsigned_' s \<longrightarrow> s \<in> {sa. next_'_update (\<lambda>_. cte_Ptr (ret__unsigned_' s)) sa \<in> {sa. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift sa) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> sa \<in> UNIV \<inter> ?R'1053 slota parenta capa next (ret__unsigned_' s) (ret__unsigned_' s) cte' \<inter> \<lbrace>True\<rbrace>}}}
 7. \<And>slota parenta capa s s'. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; (s, s') \<in> rf_sr; (pspace_aligned' and valid_mdb' and valid_objs' and valid_cap' cap) s; s' \<in> {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0}\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) parent s \<longrightarrow> ((\<lambda>_. True) and ?R685 slota parenta capa and cte_wp_at' (\<lambda>_. True) (ptr_val parenta)) s) \<and> s' \<in> UNIV \<inter> ?R'682 slota parenta capa \<inter> \<lbrace>True\<rbrace>
flex-flex pairs:
\<lambda>slota parenta capa next. ?R'1053 slota parenta capa next next \<equiv>\<^sup>? \<lambda>slota parenta capa next rv' cte'. ?R'1050 slota parenta capa next rv' (cte_to_H cte') proof (prove)
goal (6 subgoals):
 1. \<And>slota parenta capa next rv' oldCTE rv xfdca. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; nullCapPointers oldCTE; dc rv xfdca\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'1091 (cte_Ptr slot) (cte_Ptr parent) capa next rv' oldCTE rv xfdca) IF next \<noteq> 0 THEN
  Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr next} (CALL mdb_node_ptr_set_mdbPrev_'proc(mdb_Ptr &(cte_Ptr next\<rightarrow>[''cteMDBNode_C'']),ptr_val (cte_Ptr slot)))
FI {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {s. v32_'_update (\<lambda>_. ptr_val (cte_Ptr slot)) (mdb_node_ptr_'_update (\<lambda>_. mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C''])) s) \<in> \<lbrace>\<acute>mdb_node_ptr = mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = slot\<rbrace>} \<inter> {s. \<forall>t. hrs_htd (t_hrs_' (globals t)) = hrs_htd (t_hrs_' (globals s)) \<and> byte_regions_unmodified (t_hrs_' (globals s)) (t_hrs_' (globals t)) \<longrightarrow> (case untypedZeroRange cap of None \<Rightarrow> True | Some (aa, b) \<Rightarrow> region_actually_is_bytes aa (unat (b + 1 - aa)) s \<and> heap_list (hrs_mem (t_hrs_' (globals t))) (unat (b + 1 - aa)) aa = replicate (unat (b + 1 - aa)) 0)} \<inter> \<lbrace>True\<rbrace>}
 2. \<And>slota parenta capa next rv' oldCTE. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; nullCapPointers oldCTE\<rbrakk> \<Longrightarrow> \<lbrace>?R1056 slota parenta capa next oldCTE\<rbrace> setCTE slot (CTE cap (MDB next parent True True)) \<lbrace>\<lambda>a. (\<lambda>a. is_aligned next 3 \<and> (slot \<noteq> 0 \<longrightarrow> is_aligned slot 3)) and (\<lambda>a. (parent \<noteq> 0 \<and> (slot \<noteq> 0 \<longrightarrow> is_aligned slot 3)) \<and> valid_objs' a \<and> cte_wp_at' (\<lambda>c. cteCap c = cap) slot a \<and> cte_wp_at' (\<lambda>c. True) (ptr_val parenta) a)\<rbrace>
 3. \<And>slota parenta capa next rv' oldCTE. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; nullCapPointers oldCTE\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'1050 slota parenta capa next rv' oldCTE) \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C''])) capa));;
\<acute>ret__struct_mdb_node_C :== CALL mdb_node_new_'proc(ptr_val (cte_Ptr next),SCAST(32 signed \<rightarrow> 32) true,SCAST(32 signed \<rightarrow> 32) true,ptr_val (cte_Ptr parent));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr slot} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(cte_Ptr slot\<rightarrow>[''cteMDBNode_C''])) \<acute>ret__struct_mdb_node_C))) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> \<lbrace>ptr_val slota = slot\<rbrace> \<inter> ?R'1091 slota parenta capa next rv' oldCTE rv (xfdc s)}
 4. \<And>slota parenta capa. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<lbrace>?R685 (cte_Ptr slot) (cte_Ptr parent) capa\<rbrace> liftM (mdbNext \<circ> cteMDBNode) (getCTE parent) \<lbrace>\<lambda>a b. \<forall>cte. ctes_of b slot = Some cte \<longrightarrow> (cte_wp_at' (\<lambda>_. True) slot and K (is_aligned a 3 \<and> is_aligned parent 3) and ?R1056 slota parenta capa a cte and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr slot))) b\<rbrace>
 5. \<And>slota parenta capa. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F680 slota parenta capa\<^esub> (?R'682 (cte_Ptr slot) (cte_Ptr parent) capa) \<acute>ret__unsigned :== CALL mdb_node_get_mdbNext_'proc(h_val (hrs_mem \<acute>t_hrs) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C'']))) {s. \<forall>next. next = ret__unsigned_' s \<longrightarrow> s \<in> {sa. next_'_update (\<lambda>_. cte_Ptr (ret__unsigned_' s)) sa \<in> {sa. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift sa) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> sa \<in> UNIV \<inter> ?R'1053 slota parenta capa next (ret__unsigned_' s) (ret__unsigned_' s) cte' \<inter> \<lbrace>True\<rbrace>}}}
 6. \<And>slota parenta capa s s'. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; (s, s') \<in> rf_sr; (pspace_aligned' and valid_mdb' and valid_objs' and valid_cap' cap) s; s' \<in> {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0}\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) parent s \<longrightarrow> ((\<lambda>_. True) and ?R685 slota parenta capa and cte_wp_at' (\<lambda>_. True) (ptr_val parenta)) s) \<and> s' \<in> UNIV \<inter> ?R'682 slota parenta capa \<inter> \<lbrace>True\<rbrace>
flex-flex pairs:
\<lambda>slota parenta capa next. ?R'1053 slota parenta capa next next \<equiv>\<^sup>? \<lambda>slota parenta capa next rv' cte'. ?R'1050 slota parenta capa next rv' (cte_to_H cte') proof (prove)
goal (6 subgoals):
 1. \<And>capa next rv' oldCTE xfdc. \<lbrakk>ccap_relation cap capa; cteCap oldCTE = capability.NullCap; mdbNext (cteMDBNode oldCTE) = nullPointer; mdbPrev (cteMDBNode oldCTE) = nullPointer\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'1091 (cte_Ptr slot) (cte_Ptr parent) capa next rv' oldCTE () xfdc) Cond (if next \<noteq> 0 then UNIV else {}) (Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr next} (CALL mdb_node_ptr_set_mdbPrev_'proc(mdb_Ptr &(cte_Ptr next\<rightarrow>[''cteMDBNode_C'']),slot))) SKIP {s. \<forall>t. hrs_htd (t_hrs_' (globals t)) = hrs_htd (t_hrs_' (globals s)) \<and> byte_regions_unmodified (t_hrs_' (globals s)) (t_hrs_' (globals t)) \<longrightarrow> (case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals t))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0)}
 2. \<And>slota parenta capa next rv' oldCTE. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; nullCapPointers oldCTE\<rbrakk> \<Longrightarrow> \<lbrace>?R1056 slota parenta capa next oldCTE\<rbrace> setCTE slot (CTE cap (MDB next parent True True)) \<lbrace>\<lambda>a. (\<lambda>a. is_aligned next 3 \<and> (slot \<noteq> 0 \<longrightarrow> is_aligned slot 3)) and (\<lambda>a. (parent \<noteq> 0 \<and> (slot \<noteq> 0 \<longrightarrow> is_aligned slot 3)) \<and> valid_objs' a \<and> cte_wp_at' (\<lambda>c. cteCap c = cap) slot a \<and> cte_wp_at' (\<lambda>c. True) (ptr_val parenta) a)\<rbrace>
 3. \<And>slota parenta capa next rv' oldCTE. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; nullCapPointers oldCTE\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'1050 slota parenta capa next rv' oldCTE) \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C''])) capa));;
\<acute>ret__struct_mdb_node_C :== CALL mdb_node_new_'proc(ptr_val (cte_Ptr next),SCAST(32 signed \<rightarrow> 32) true,SCAST(32 signed \<rightarrow> 32) true,ptr_val (cte_Ptr parent));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr slot} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(cte_Ptr slot\<rightarrow>[''cteMDBNode_C''])) \<acute>ret__struct_mdb_node_C))) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> \<lbrace>ptr_val slota = slot\<rbrace> \<inter> ?R'1091 slota parenta capa next rv' oldCTE rv (xfdc s)}
 4. \<And>slota parenta capa. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<lbrace>?R685 (cte_Ptr slot) (cte_Ptr parent) capa\<rbrace> liftM (mdbNext \<circ> cteMDBNode) (getCTE parent) \<lbrace>\<lambda>a b. \<forall>cte. ctes_of b slot = Some cte \<longrightarrow> (cte_wp_at' (\<lambda>_. True) slot and K (is_aligned a 3 \<and> is_aligned parent 3) and ?R1056 slota parenta capa a cte and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr slot))) b\<rbrace>
 5. \<And>slota parenta capa. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F680 slota parenta capa\<^esub> (?R'682 (cte_Ptr slot) (cte_Ptr parent) capa) \<acute>ret__unsigned :== CALL mdb_node_get_mdbNext_'proc(h_val (hrs_mem \<acute>t_hrs) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C'']))) {s. \<forall>next. next = ret__unsigned_' s \<longrightarrow> s \<in> {sa. next_'_update (\<lambda>_. cte_Ptr (ret__unsigned_' s)) sa \<in> {sa. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift sa) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> sa \<in> UNIV \<inter> ?R'1053 slota parenta capa next (ret__unsigned_' s) (ret__unsigned_' s) cte' \<inter> \<lbrace>True\<rbrace>}}}
 6. \<And>slota parenta capa s s'. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; (s, s') \<in> rf_sr; (pspace_aligned' and valid_mdb' and valid_objs' and valid_cap' cap) s; s' \<in> {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0}\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) parent s \<longrightarrow> ((\<lambda>_. True) and ?R685 slota parenta capa and cte_wp_at' (\<lambda>_. True) (ptr_val parenta)) s) \<and> s' \<in> UNIV \<inter> ?R'682 slota parenta capa \<inter> \<lbrace>True\<rbrace>
flex-flex pairs:
\<lambda>slota parenta capa next. ?R'1053 slota parenta capa next next \<equiv>\<^sup>? \<lambda>slota parenta capa next rv' cte'. ?R'1050 slota parenta capa next rv' (cte_to_H cte') proof (prove)
goal (5 subgoals):
 1. \<And>slota parenta capa next rv' oldCTE. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; nullCapPointers oldCTE\<rbrakk> \<Longrightarrow> \<lbrace>?R1056 slota parenta capa next oldCTE\<rbrace> setCTE slot (CTE cap (MDB next parent True True)) \<lbrace>\<lambda>a. (\<lambda>a. is_aligned next 3 \<and> (slot \<noteq> 0 \<longrightarrow> is_aligned slot 3)) and (\<lambda>a. (parent \<noteq> 0 \<and> (slot \<noteq> 0 \<longrightarrow> is_aligned slot 3)) \<and> valid_objs' a \<and> cte_wp_at' (\<lambda>c. cteCap c = cap) slot a \<and> cte_wp_at' (\<lambda>c. True) (ptr_val parenta) a)\<rbrace>
 2. \<And>slota parenta capa next rv' oldCTE. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; nullCapPointers oldCTE\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'1050 slota parenta capa next rv' oldCTE) \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C''])) capa));;
\<acute>ret__struct_mdb_node_C :== CALL mdb_node_new_'proc(ptr_val (cte_Ptr next),SCAST(32 signed \<rightarrow> 32) true,SCAST(32 signed \<rightarrow> 32) true,ptr_val (cte_Ptr parent));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr slot} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(cte_Ptr slot\<rightarrow>[''cteMDBNode_C''])) \<acute>ret__struct_mdb_node_C))) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> \<lbrace>ptr_val slota = slot\<rbrace> \<inter> {s. (s \<in> (if next \<noteq> 0 then UNIV else {}) \<longrightarrow> s \<Turnstile>\<^sub>c cte_Ptr next \<longrightarrow> (\<forall>t. hrs_htd (t_hrs_' (globals t)) = hrs_htd (t_hrs_' (globals s)) \<and> byte_regions_unmodified (t_hrs_' (globals s)) (t_hrs_' (globals t)) \<longrightarrow> (\<forall>ta. hrs_htd (t_hrs_' (globals ta)) = hrs_htd (t_hrs_' (globals s)) \<and> byte_regions_unmodified (t_hrs_' (globals t)) (t_hrs_' (globals ta)) \<longrightarrow> (case untypedZeroRange cap of None \<Rightarrow> True | Some (aa, b) \<Rightarrow> region_actually_is_bytes aa (unat (b + 1 - aa)) s \<and> heap_list (hrs_mem (t_hrs_' (globals ta))) (unat (b + 1 - aa)) aa = replicate (unat (b + 1 - aa)) 0)))) \<and> (s \<notin> (if next \<noteq> 0 then UNIV else {}) \<longrightarrow> (\<forall>t. hrs_htd (t_hrs_' (globals t)) = hrs_htd (t_hrs_' (globals s)) \<and> byte_regions_unmodified (t_hrs_' (globals s)) (t_hrs_' (globals t)) \<longrightarrow> (case untypedZeroRange cap of None \<Rightarrow> True | Some (aa, b) \<Rightarrow> region_actually_is_bytes aa (unat (b + 1 - aa)) s \<and> heap_list (hrs_mem (t_hrs_' (globals t))) (unat (b + 1 - aa)) aa = replicate (unat (b + 1 - aa)) 0)))}}
 3. \<And>slota parenta capa. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<lbrace>?R685 (cte_Ptr slot) (cte_Ptr parent) capa\<rbrace> liftM (mdbNext \<circ> cteMDBNode) (getCTE parent) \<lbrace>\<lambda>a b. \<forall>cte. ctes_of b slot = Some cte \<longrightarrow> (cte_wp_at' (\<lambda>_. True) slot and K (is_aligned a 3 \<and> is_aligned parent 3) and ?R1056 slota parenta capa a cte and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr slot))) b\<rbrace>
 4. \<And>slota parenta capa. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F680 slota parenta capa\<^esub> (?R'682 (cte_Ptr slot) (cte_Ptr parent) capa) \<acute>ret__unsigned :== CALL mdb_node_get_mdbNext_'proc(h_val (hrs_mem \<acute>t_hrs) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C'']))) {s. \<forall>next. next = ret__unsigned_' s \<longrightarrow> s \<in> {sa. next_'_update (\<lambda>_. cte_Ptr (ret__unsigned_' s)) sa \<in> {sa. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift sa) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> sa \<in> UNIV \<inter> ?R'1053 slota parenta capa next (ret__unsigned_' s) (ret__unsigned_' s) cte' \<inter> \<lbrace>True\<rbrace>}}}
 5. \<And>slota parenta capa s s'. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; (s, s') \<in> rf_sr; (pspace_aligned' and valid_mdb' and valid_objs' and valid_cap' cap) s; s' \<in> {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0}\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) parent s \<longrightarrow> ((\<lambda>_. True) and ?R685 slota parenta capa and cte_wp_at' (\<lambda>_. True) (ptr_val parenta)) s) \<and> s' \<in> UNIV \<inter> ?R'682 slota parenta capa \<inter> \<lbrace>True\<rbrace>
flex-flex pairs:
\<lambda>slota parenta capa next. ?R'1053 slota parenta capa next next \<equiv>\<^sup>? \<lambda>slota parenta capa next rv' cte'. ?R'1050 slota parenta capa next rv' (cte_to_H cte') proof (prove)
goal (4 subgoals):
 1. \<And>slota parenta capa next rv' oldCTE. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; nullCapPointers oldCTE\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'1050 slota parenta capa next rv' oldCTE) \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C''])) capa));;
\<acute>ret__struct_mdb_node_C :== CALL mdb_node_new_'proc(ptr_val (cte_Ptr next),SCAST(32 signed \<rightarrow> 32) true,SCAST(32 signed \<rightarrow> 32) true,ptr_val (cte_Ptr parent));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr slot} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(cte_Ptr slot\<rightarrow>[''cteMDBNode_C''])) \<acute>ret__struct_mdb_node_C))) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> \<lbrace>ptr_val slota = slot\<rbrace> \<inter> {s. (s \<in> (if next \<noteq> 0 then UNIV else {}) \<longrightarrow> s \<Turnstile>\<^sub>c cte_Ptr next \<longrightarrow> (\<forall>t. hrs_htd (t_hrs_' (globals t)) = hrs_htd (t_hrs_' (globals s)) \<and> byte_regions_unmodified (t_hrs_' (globals s)) (t_hrs_' (globals t)) \<longrightarrow> (\<forall>ta. hrs_htd (t_hrs_' (globals ta)) = hrs_htd (t_hrs_' (globals s)) \<and> byte_regions_unmodified (t_hrs_' (globals t)) (t_hrs_' (globals ta)) \<longrightarrow> (case untypedZeroRange cap of None \<Rightarrow> True | Some (aa, b) \<Rightarrow> region_actually_is_bytes aa (unat (b + 1 - aa)) s \<and> heap_list (hrs_mem (t_hrs_' (globals ta))) (unat (b + 1 - aa)) aa = replicate (unat (b + 1 - aa)) 0)))) \<and> (s \<notin> (if next \<noteq> 0 then UNIV else {}) \<longrightarrow> (\<forall>t. hrs_htd (t_hrs_' (globals t)) = hrs_htd (t_hrs_' (globals s)) \<and> byte_regions_unmodified (t_hrs_' (globals s)) (t_hrs_' (globals t)) \<longrightarrow> (case untypedZeroRange cap of None \<Rightarrow> True | Some (aa, b) \<Rightarrow> region_actually_is_bytes aa (unat (b + 1 - aa)) s \<and> heap_list (hrs_mem (t_hrs_' (globals t))) (unat (b + 1 - aa)) aa = replicate (unat (b + 1 - aa)) 0)))}}
 2. \<And>slota parenta capa. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<lbrace>?R685 (cte_Ptr slot) (cte_Ptr parent) capa\<rbrace> liftM (mdbNext \<circ> cteMDBNode) (getCTE parent) \<lbrace>\<lambda>a b. \<forall>cte. ctes_of b slot = Some cte \<longrightarrow> (cte_wp_at' (\<lambda>_. True) slot and K (is_aligned a 3 \<and> is_aligned parent 3) and (\<lambda>b. (is_aligned a 3 \<and> (slot \<noteq> 0 \<longrightarrow> is_aligned slot 3)) \<and> (parent \<noteq> 0 \<and> (slot \<noteq> 0 \<longrightarrow> is_aligned slot 3)) \<and> (valid_objs' and valid_cap' (cteCap (CTE cap (MDB a parent True True)))) b \<and> (if slot = slot then cteCap (CTE cap (MDB a parent True True)) = cap else cte_wp_at' (\<lambda>c. cteCap c = cap) slot b) \<and> (if ptr_val parenta = slot then True else cte_wp_at' (\<lambda>c. True) (ptr_val parenta) b)) and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr slot))) b\<rbrace>
 3. \<And>slota parenta capa. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F680 slota parenta capa\<^esub> (?R'682 (cte_Ptr slot) (cte_Ptr parent) capa) \<acute>ret__unsigned :== CALL mdb_node_get_mdbNext_'proc(h_val (hrs_mem \<acute>t_hrs) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C'']))) {s. \<forall>next. next = ret__unsigned_' s \<longrightarrow> s \<in> {sa. next_'_update (\<lambda>_. cte_Ptr (ret__unsigned_' s)) sa \<in> {sa. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift sa) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> sa \<in> UNIV \<inter> ?R'1053 slota parenta capa next (ret__unsigned_' s) (ret__unsigned_' s) cte' \<inter> \<lbrace>True\<rbrace>}}}
 4. \<And>slota parenta capa s s'. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; (s, s') \<in> rf_sr; (pspace_aligned' and valid_mdb' and valid_objs' and valid_cap' cap) s; s' \<in> {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0}\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) parent s \<longrightarrow> ((\<lambda>_. True) and ?R685 slota parenta capa and cte_wp_at' (\<lambda>_. True) (ptr_val parenta)) s) \<and> s' \<in> UNIV \<inter> ?R'682 slota parenta capa \<inter> \<lbrace>True\<rbrace>
flex-flex pairs:
\<lambda>slota parenta capa next. ?R'1053 slota parenta capa next next \<equiv>\<^sup>? \<lambda>slota parenta capa next rv' cte'. ?R'1050 slota parenta capa next rv' (cte_to_H cte') proof (prove)
goal (4 subgoals):
 1. \<And>capa next rv' oldCTE. \<lbrakk>ccap_relation cap capa; cteCap oldCTE = capability.NullCap; mdbNext (cteMDBNode oldCTE) = nullPointer; mdbPrev (cteMDBNode oldCTE) = nullPointer\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'1050 (cte_Ptr slot) (cte_Ptr parent) capa next rv' oldCTE) \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C''])) capa));;
\<acute>ret__struct_mdb_node_C :== CALL mdb_node_new_'proc(next,SCAST(32 signed \<rightarrow> 32) true,SCAST(32 signed \<rightarrow> 32) true,parent);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr slot} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(cte_Ptr slot\<rightarrow>[''cteMDBNode_C''])) \<acute>ret__struct_mdb_node_C))) {s. (next \<noteq> 0 \<longrightarrow> s \<Turnstile>\<^sub>c cte_Ptr next \<longrightarrow> (\<forall>t. hrs_htd (t_hrs_' (globals t)) = hrs_htd (t_hrs_' (globals s)) \<and> byte_regions_unmodified (t_hrs_' (globals s)) (t_hrs_' (globals t)) \<longrightarrow> (\<forall>ta. hrs_htd (t_hrs_' (globals ta)) = hrs_htd (t_hrs_' (globals s)) \<and> byte_regions_unmodified (t_hrs_' (globals t)) (t_hrs_' (globals ta)) \<longrightarrow> (case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals ta))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0)))) \<and> (next = 0 \<longrightarrow> (\<forall>t. hrs_htd (t_hrs_' (globals t)) = hrs_htd (t_hrs_' (globals s)) \<and> byte_regions_unmodified (t_hrs_' (globals s)) (t_hrs_' (globals t)) \<longrightarrow> (case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals t))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0)))}
 2. \<And>slota parenta capa. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<lbrace>?R685 (cte_Ptr slot) (cte_Ptr parent) capa\<rbrace> liftM (mdbNext \<circ> cteMDBNode) (getCTE parent) \<lbrace>\<lambda>a b. \<forall>cte. ctes_of b slot = Some cte \<longrightarrow> (cte_wp_at' (\<lambda>_. True) slot and K (is_aligned a 3 \<and> is_aligned parent 3) and (\<lambda>b. (is_aligned a 3 \<and> (slot \<noteq> 0 \<longrightarrow> is_aligned slot 3)) \<and> (parent \<noteq> 0 \<and> (slot \<noteq> 0 \<longrightarrow> is_aligned slot 3)) \<and> (valid_objs' and valid_cap' (cteCap (CTE cap (MDB a parent True True)))) b \<and> (if slot = slot then cteCap (CTE cap (MDB a parent True True)) = cap else cte_wp_at' (\<lambda>c. cteCap c = cap) slot b) \<and> (if ptr_val parenta = slot then True else cte_wp_at' (\<lambda>c. True) (ptr_val parenta) b)) and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr slot))) b\<rbrace>
 3. \<And>slota parenta capa. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F680 slota parenta capa\<^esub> (?R'682 (cte_Ptr slot) (cte_Ptr parent) capa) \<acute>ret__unsigned :== CALL mdb_node_get_mdbNext_'proc(h_val (hrs_mem \<acute>t_hrs) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C'']))) {s. \<forall>next. next = ret__unsigned_' s \<longrightarrow> s \<in> {sa. next_'_update (\<lambda>_. cte_Ptr (ret__unsigned_' s)) sa \<in> {sa. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift sa) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> sa \<in> UNIV \<inter> ?R'1053 slota parenta capa next (ret__unsigned_' s) (ret__unsigned_' s) cte' \<inter> \<lbrace>True\<rbrace>}}}
 4. \<And>slota parenta capa s s'. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; (s, s') \<in> rf_sr; (pspace_aligned' and valid_mdb' and valid_objs' and valid_cap' cap) s; s' \<in> {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0}\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) parent s \<longrightarrow> ((\<lambda>_. True) and ?R685 slota parenta capa and cte_wp_at' (\<lambda>_. True) (ptr_val parenta)) s) \<and> s' \<in> UNIV \<inter> ?R'682 slota parenta capa \<inter> \<lbrace>True\<rbrace>
flex-flex pairs:
\<lambda>slota parenta capa next. ?R'1053 slota parenta capa next next \<equiv>\<^sup>? \<lambda>slota parenta capa next rv' cte'. ?R'1050 slota parenta capa next rv' (cte_to_H cte') proof (prove)
goal (3 subgoals):
 1. \<And>slota parenta capa. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<lbrace>?R685 (cte_Ptr slot) (cte_Ptr parent) capa\<rbrace> liftM (mdbNext \<circ> cteMDBNode) (getCTE parent) \<lbrace>\<lambda>a b. \<forall>cte. ctes_of b slot = Some cte \<longrightarrow> (cte_wp_at' (\<lambda>_. True) slot and K (is_aligned a 3 \<and> is_aligned parent 3) and (\<lambda>b. (is_aligned a 3 \<and> (slot \<noteq> 0 \<longrightarrow> is_aligned slot 3)) \<and> (parent \<noteq> 0 \<and> (slot \<noteq> 0 \<longrightarrow> is_aligned slot 3)) \<and> (valid_objs' and valid_cap' (cteCap (CTE cap (MDB a parent True True)))) b \<and> (if slot = slot then cteCap (CTE cap (MDB a parent True True)) = cap else cte_wp_at' (\<lambda>c. cteCap c = cap) slot b) \<and> (if ptr_val parenta = slot then True else cte_wp_at' (\<lambda>c. True) (ptr_val parenta) b)) and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr slot))) b\<rbrace>
 2. \<And>slota parenta capa. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F680 slota parenta capa\<^esub> (?R'682 (cte_Ptr slot) (cte_Ptr parent) capa) \<acute>ret__unsigned :== CALL mdb_node_get_mdbNext_'proc(h_val (hrs_mem \<acute>t_hrs) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C'']))) {s. \<forall>next. next = ret__unsigned_' s \<longrightarrow> s \<in> {sa. next_'_update (\<lambda>_. cte_Ptr (ret__unsigned_' s)) sa \<in> {sa. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift sa) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> sa \<in> UNIV \<inter> \<lbrace>\<forall>t. mdb_node_lift \<^bsup>t\<^esup>ret__struct_mdb_node_C = \<lparr>mdbNext_CL = \<^bsup>s\<^esup>ret__unsigned && ~~ mask 3, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) true && mask 1, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) true && mask 1, mdbPrev_CL = parent && ~~ mask 3\<rparr> \<longrightarrow> hrs_htd (hrs_mem_update (heap_update (cap_Ptr &(slota\<rightarrow>[''cap_C''])) capa) \<acute>t_hrs) \<Turnstile>\<^sub>t slota \<longrightarrow> (\<^bsup>s\<^esup>ret__unsigned \<noteq> 0 \<longrightarrow> hrs_htd (hrs_mem_update (heap_update (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C''])) \<^bsup>t\<^esup>ret__struct_mdb_node_C) (hrs_mem_update (heap_update (cap_Ptr &(slota\<rightarrow>[''cap_C''])) capa) \<acute>t_hrs)) \<Turnstile>\<^sub>t cte_Ptr \<^bsup>s\<^esup>ret__unsigned \<longrightarrow> (\<forall>ta. hrs_htd \<^bsup>ta\<^esup>t_hrs = hrs_htd (hrs_mem_update (heap_update (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C''])) \<^bsup>t\<^esup>ret__struct_mdb_node_C) (hrs_mem_update (heap_update (cap_Ptr &(slota\<rightarrow>[''cap_C''])) capa) \<acute>t_hrs)) \<and> byte_regions_unmodified (hrs_mem_update (heap_update (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C''])) \<^bsup>t\<^esup>ret__struct_mdb_node_C) (hrs_mem_update (heap_update (cap_Ptr &(slota\<rightarrow>[''cap_C''])) capa) \<acute>t_hrs)) \<^bsup>ta\<^esup>t_hrs \<longrightarrow> (\<forall>tb. hrs_htd \<^bsup>tb\<^esup>t_hrs = hrs_htd (hrs_mem_update (heap_update (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C''])) \<^bsup>t\<^esup>ret__struct_mdb_node_C) (hrs_mem_update (heap_update (cap_Ptr &(slota\<rightarrow>[''cap_C''])) capa) \<acute>t_hrs)) \<and> byte_regions_unmodified \<^bsup>ta\<^esup>t_hrs \<^bsup>tb\<^esup>t_hrs \<longrightarrow> (case untypedZeroRange cap of None \<Rightarrow> True | Some (aa, b) \<Rightarrow> region_actually_is_bytes' aa (unat (b + 1 - aa)) (hrs_htd (hrs_mem_update (heap_update (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C''])) \<^bsup>t\<^esup>ret__struct_mdb_node_C) (hrs_mem_update (heap_update (cap_Ptr &(slota\<rightarrow>[''cap_C''])) capa) \<acute>t_hrs))) \<and> heap_list (hrs_mem \<^bsup>tb\<^esup>t_hrs) (unat (b + 1 - aa)) aa = replicate (unat (b + 1 - aa)) 0)))) \<and> (\<^bsup>s\<^esup>ret__unsigned = 0 \<longrightarrow> (\<forall>ta. hrs_htd \<^bsup>ta\<^esup>t_hrs = hrs_htd (hrs_mem_update (heap_update (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C''])) \<^bsup>t\<^esup>ret__struct_mdb_node_C) (hrs_mem_update (heap_update (cap_Ptr &(slota\<rightarrow>[''cap_C''])) capa) \<acute>t_hrs)) \<and> byte_regions_unmodified (hrs_mem_update (heap_update (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C''])) \<^bsup>t\<^esup>ret__struct_mdb_node_C) (hrs_mem_update (heap_update (cap_Ptr &(slota\<rightarrow>[''cap_C''])) capa) \<acute>t_hrs)) \<^bsup>ta\<^esup>t_hrs \<longrightarrow> (case untypedZeroRange cap of None \<Rightarrow> True | Some (aa, b) \<Rightarrow> region_actually_is_bytes' aa (unat (b + 1 - aa)) (hrs_htd (hrs_mem_update (heap_update (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C''])) \<^bsup>t\<^esup>ret__struct_mdb_node_C) (hrs_mem_update (heap_update (cap_Ptr &(slota\<rightarrow>[''cap_C''])) capa) \<acute>t_hrs))) \<and> heap_list (hrs_mem \<^bsup>ta\<^esup>t_hrs) (unat (b + 1 - aa)) aa = replicate (unat (b + 1 - aa)) 0)))\<rbrace> \<inter> \<lbrace>True\<rbrace>}}}
 3. \<And>slota parenta capa s s'. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; (s, s') \<in> rf_sr; (pspace_aligned' and valid_mdb' and valid_objs' and valid_cap' cap) s; s' \<in> {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0}\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) parent s \<longrightarrow> ((\<lambda>_. True) and ?R685 slota parenta capa and cte_wp_at' (\<lambda>_. True) (ptr_val parenta)) s) \<and> s' \<in> UNIV \<inter> ?R'682 slota parenta capa \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>slota parenta capa. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<lbrace>?R685 (cte_Ptr slot) (cte_Ptr parent) capa\<rbrace> liftM (mdbNext \<circ> cteMDBNode) (getCTE parent) \<lbrace>\<lambda>a b. (\<exists>cte. ctes_of b slot = Some cte) \<longrightarrow> cte_wp_at' (\<lambda>_. True) slot b \<and> is_aligned a 3 \<and> is_aligned parent 3 \<and> is_aligned a 3 \<and> (slot \<noteq> 0 \<longrightarrow> is_aligned slot 3) \<and> parent \<noteq> 0 \<and> (slot \<noteq> 0 \<longrightarrow> is_aligned slot 3) \<and> valid_objs' b \<and> valid_cap' cap b \<and> (if parent = slot then True else cte_wp_at' (\<lambda>c. True) parent b) \<and> cte_wp_at' (\<lambda>_. True) slot b\<rbrace>
 2. \<And>slota parenta capa. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F680 slota parenta capa\<^esub> (?R'682 (cte_Ptr slot) (cte_Ptr parent) capa) \<acute>ret__unsigned :== CALL mdb_node_get_mdbNext_'proc(h_val (hrs_mem \<acute>t_hrs) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C'']))) {s. \<forall>next. next = ret__unsigned_' s \<longrightarrow> s \<in> {sa. next_'_update (\<lambda>_. cte_Ptr (ret__unsigned_' s)) sa \<in> {sa. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift sa) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> sa \<in> UNIV \<inter> \<lbrace>\<forall>t. mdb_node_lift \<^bsup>t\<^esup>ret__struct_mdb_node_C = \<lparr>mdbNext_CL = \<^bsup>s\<^esup>ret__unsigned && ~~ mask 3, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) true && mask 1, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) true && mask 1, mdbPrev_CL = parent && ~~ mask 3\<rparr> \<longrightarrow> hrs_htd (hrs_mem_update (heap_update (cap_Ptr &(slota\<rightarrow>[''cap_C''])) capa) \<acute>t_hrs) \<Turnstile>\<^sub>t slota \<longrightarrow> (\<^bsup>s\<^esup>ret__unsigned \<noteq> 0 \<longrightarrow> hrs_htd (hrs_mem_update (heap_update (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C''])) \<^bsup>t\<^esup>ret__struct_mdb_node_C) (hrs_mem_update (heap_update (cap_Ptr &(slota\<rightarrow>[''cap_C''])) capa) \<acute>t_hrs)) \<Turnstile>\<^sub>t cte_Ptr \<^bsup>s\<^esup>ret__unsigned \<longrightarrow> (\<forall>ta. hrs_htd \<^bsup>ta\<^esup>t_hrs = hrs_htd (hrs_mem_update (heap_update (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C''])) \<^bsup>t\<^esup>ret__struct_mdb_node_C) (hrs_mem_update (heap_update (cap_Ptr &(slota\<rightarrow>[''cap_C''])) capa) \<acute>t_hrs)) \<and> byte_regions_unmodified (hrs_mem_update (heap_update (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C''])) \<^bsup>t\<^esup>ret__struct_mdb_node_C) (hrs_mem_update (heap_update (cap_Ptr &(slota\<rightarrow>[''cap_C''])) capa) \<acute>t_hrs)) \<^bsup>ta\<^esup>t_hrs \<longrightarrow> (\<forall>tb. hrs_htd \<^bsup>tb\<^esup>t_hrs = hrs_htd (hrs_mem_update (heap_update (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C''])) \<^bsup>t\<^esup>ret__struct_mdb_node_C) (hrs_mem_update (heap_update (cap_Ptr &(slota\<rightarrow>[''cap_C''])) capa) \<acute>t_hrs)) \<and> byte_regions_unmodified \<^bsup>ta\<^esup>t_hrs \<^bsup>tb\<^esup>t_hrs \<longrightarrow> (case untypedZeroRange cap of None \<Rightarrow> True | Some (aa, b) \<Rightarrow> region_actually_is_bytes' aa (unat (b + 1 - aa)) (hrs_htd (hrs_mem_update (heap_update (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C''])) \<^bsup>t\<^esup>ret__struct_mdb_node_C) (hrs_mem_update (heap_update (cap_Ptr &(slota\<rightarrow>[''cap_C''])) capa) \<acute>t_hrs))) \<and> heap_list (hrs_mem \<^bsup>tb\<^esup>t_hrs) (unat (b + 1 - aa)) aa = replicate (unat (b + 1 - aa)) 0)))) \<and> (\<^bsup>s\<^esup>ret__unsigned = 0 \<longrightarrow> (\<forall>ta. hrs_htd \<^bsup>ta\<^esup>t_hrs = hrs_htd (hrs_mem_update (heap_update (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C''])) \<^bsup>t\<^esup>ret__struct_mdb_node_C) (hrs_mem_update (heap_update (cap_Ptr &(slota\<rightarrow>[''cap_C''])) capa) \<acute>t_hrs)) \<and> byte_regions_unmodified (hrs_mem_update (heap_update (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C''])) \<^bsup>t\<^esup>ret__struct_mdb_node_C) (hrs_mem_update (heap_update (cap_Ptr &(slota\<rightarrow>[''cap_C''])) capa) \<acute>t_hrs)) \<^bsup>ta\<^esup>t_hrs \<longrightarrow> (case untypedZeroRange cap of None \<Rightarrow> True | Some (aa, b) \<Rightarrow> region_actually_is_bytes' aa (unat (b + 1 - aa)) (hrs_htd (hrs_mem_update (heap_update (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C''])) \<^bsup>t\<^esup>ret__struct_mdb_node_C) (hrs_mem_update (heap_update (cap_Ptr &(slota\<rightarrow>[''cap_C''])) capa) \<acute>t_hrs))) \<and> heap_list (hrs_mem \<^bsup>ta\<^esup>t_hrs) (unat (b + 1 - aa)) aa = replicate (unat (b + 1 - aa)) 0)))\<rbrace> \<inter> \<lbrace>True\<rbrace>}}}
 3. \<And>slota parenta capa s s'. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; (s, s') \<in> rf_sr; (pspace_aligned' and valid_mdb' and valid_objs' and valid_cap' cap) s; s' \<in> {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0}\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) parent s \<longrightarrow> ((\<lambda>_. True) and ?R685 slota parenta capa and cte_wp_at' (\<lambda>_. True) (ptr_val parenta)) s) \<and> s' \<in> UNIV \<inter> ?R'682 slota parenta capa \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>slota parenta capa. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F680 slota parenta capa\<^esub> (?R'682 (cte_Ptr slot) (cte_Ptr parent) capa) \<acute>ret__unsigned :== CALL mdb_node_get_mdbNext_'proc(h_val (hrs_mem \<acute>t_hrs) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C'']))) {s. \<forall>next. next = ret__unsigned_' s \<longrightarrow> s \<in> {sa. next_'_update (\<lambda>_. cte_Ptr (ret__unsigned_' s)) sa \<in> {sa. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift sa) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> sa \<in> UNIV \<inter> \<lbrace>\<forall>t. mdb_node_lift \<^bsup>t\<^esup>ret__struct_mdb_node_C = \<lparr>mdbNext_CL = \<^bsup>s\<^esup>ret__unsigned && ~~ mask 3, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) true && mask 1, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) true && mask 1, mdbPrev_CL = parent && ~~ mask 3\<rparr> \<longrightarrow> hrs_htd (hrs_mem_update (heap_update (cap_Ptr &(slota\<rightarrow>[''cap_C''])) capa) \<acute>t_hrs) \<Turnstile>\<^sub>t slota \<longrightarrow> (\<^bsup>s\<^esup>ret__unsigned \<noteq> 0 \<longrightarrow> hrs_htd (hrs_mem_update (heap_update (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C''])) \<^bsup>t\<^esup>ret__struct_mdb_node_C) (hrs_mem_update (heap_update (cap_Ptr &(slota\<rightarrow>[''cap_C''])) capa) \<acute>t_hrs)) \<Turnstile>\<^sub>t cte_Ptr \<^bsup>s\<^esup>ret__unsigned \<longrightarrow> (\<forall>ta. hrs_htd \<^bsup>ta\<^esup>t_hrs = hrs_htd (hrs_mem_update (heap_update (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C''])) \<^bsup>t\<^esup>ret__struct_mdb_node_C) (hrs_mem_update (heap_update (cap_Ptr &(slota\<rightarrow>[''cap_C''])) capa) \<acute>t_hrs)) \<and> byte_regions_unmodified (hrs_mem_update (heap_update (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C''])) \<^bsup>t\<^esup>ret__struct_mdb_node_C) (hrs_mem_update (heap_update (cap_Ptr &(slota\<rightarrow>[''cap_C''])) capa) \<acute>t_hrs)) \<^bsup>ta\<^esup>t_hrs \<longrightarrow> (\<forall>tb. hrs_htd \<^bsup>tb\<^esup>t_hrs = hrs_htd (hrs_mem_update (heap_update (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C''])) \<^bsup>t\<^esup>ret__struct_mdb_node_C) (hrs_mem_update (heap_update (cap_Ptr &(slota\<rightarrow>[''cap_C''])) capa) \<acute>t_hrs)) \<and> byte_regions_unmodified \<^bsup>ta\<^esup>t_hrs \<^bsup>tb\<^esup>t_hrs \<longrightarrow> (case untypedZeroRange cap of None \<Rightarrow> True | Some (aa, b) \<Rightarrow> region_actually_is_bytes' aa (unat (b + 1 - aa)) (hrs_htd (hrs_mem_update (heap_update (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C''])) \<^bsup>t\<^esup>ret__struct_mdb_node_C) (hrs_mem_update (heap_update (cap_Ptr &(slota\<rightarrow>[''cap_C''])) capa) \<acute>t_hrs))) \<and> heap_list (hrs_mem \<^bsup>tb\<^esup>t_hrs) (unat (b + 1 - aa)) aa = replicate (unat (b + 1 - aa)) 0)))) \<and> (\<^bsup>s\<^esup>ret__unsigned = 0 \<longrightarrow> (\<forall>ta. hrs_htd \<^bsup>ta\<^esup>t_hrs = hrs_htd (hrs_mem_update (heap_update (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C''])) \<^bsup>t\<^esup>ret__struct_mdb_node_C) (hrs_mem_update (heap_update (cap_Ptr &(slota\<rightarrow>[''cap_C''])) capa) \<acute>t_hrs)) \<and> byte_regions_unmodified (hrs_mem_update (heap_update (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C''])) \<^bsup>t\<^esup>ret__struct_mdb_node_C) (hrs_mem_update (heap_update (cap_Ptr &(slota\<rightarrow>[''cap_C''])) capa) \<acute>t_hrs)) \<^bsup>ta\<^esup>t_hrs \<longrightarrow> (case untypedZeroRange cap of None \<Rightarrow> True | Some (aa, b) \<Rightarrow> region_actually_is_bytes' aa (unat (b + 1 - aa)) (hrs_htd (hrs_mem_update (heap_update (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C''])) \<^bsup>t\<^esup>ret__struct_mdb_node_C) (hrs_mem_update (heap_update (cap_Ptr &(slota\<rightarrow>[''cap_C''])) capa) \<acute>t_hrs))) \<and> heap_list (hrs_mem \<^bsup>ta\<^esup>t_hrs) (unat (b + 1 - aa)) aa = replicate (unat (b + 1 - aa)) 0)))\<rbrace> \<inter> \<lbrace>True\<rbrace>}}}
 2. \<And>slota parenta capa s s'. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; (s, s') \<in> rf_sr; (pspace_aligned' and valid_mdb' and valid_objs' and valid_cap' cap) s; s' \<in> {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0}\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) parent s \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. \<forall>cte. cte_wp_at' ((=) cte) parent a \<longrightarrow> ((\<lambda>a aa. (\<exists>cte. ctes_of aa slot = Some cte) \<longrightarrow> cte_wp_at' (\<lambda>_. True) slot aa \<and> is_aligned a 3 \<and> is_aligned parent 3 \<and> is_aligned a 3 \<and> (slot \<noteq> 0 \<longrightarrow> is_aligned slot 3) \<and> parent \<noteq> 0 \<and> (slot \<noteq> 0 \<longrightarrow> is_aligned slot 3) \<and> valid_objs' aa \<and> valid_cap' cap aa \<and> (if parent = slot then True else cte_wp_at' (\<lambda>c. True) parent aa) \<and> cte_wp_at' (\<lambda>_. True) slot aa) \<circ> (mdbNext \<circ> cteMDBNode)) cte a) and cte_wp_at' (\<lambda>_. True) (ptr_val parenta)) s) \<and> s' \<in> UNIV \<inter> ?R'682 slota parenta capa \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>capa. ccap_relation cap capa \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F680 (cte_Ptr slot) (cte_Ptr parent) capa\<^esub> (?R'682 (cte_Ptr slot) (cte_Ptr parent) capa) \<acute>ret__unsigned :== CALL mdb_node_get_mdbNext_'proc(h_val (hrs_mem \<acute>t_hrs) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C'']))) {s. (\<exists>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte') \<longrightarrow> (\<forall>t. mdb_node_lift (ret__struct_mdb_node_C_' t) = \<lparr>mdbNext_CL = ret__unsigned_' s && ~~ mask 3, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) true, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) true, mdbPrev_CL = parent && ~~ mask 3\<rparr> \<longrightarrow> s \<Turnstile>\<^sub>c cte_Ptr slot \<longrightarrow> (ret__unsigned_' s \<noteq> 0 \<longrightarrow> s \<Turnstile>\<^sub>c cte_Ptr (ret__unsigned_' s) \<longrightarrow> (\<forall>ta. hrs_htd (t_hrs_' (globals ta)) = hrs_htd (t_hrs_' (globals s)) \<and> byte_regions_unmodified (hrs_mem_update (heap_update (mdb_Ptr &(cte_Ptr slot\<rightarrow>[''cteMDBNode_C''])) (ret__struct_mdb_node_C_' t)) (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C''])) capa) (t_hrs_' (globals s)))) (t_hrs_' (globals ta)) \<longrightarrow> (\<forall>t. hrs_htd (t_hrs_' (globals t)) = hrs_htd (t_hrs_' (globals s)) \<and> byte_regions_unmodified (t_hrs_' (globals ta)) (t_hrs_' (globals t)) \<longrightarrow> (case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals t))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0)))) \<and> (ret__unsigned_' s = 0 \<longrightarrow> (\<forall>ta. hrs_htd (t_hrs_' (globals ta)) = hrs_htd (t_hrs_' (globals s)) \<and> byte_regions_unmodified (hrs_mem_update (heap_update (mdb_Ptr &(cte_Ptr slot\<rightarrow>[''cteMDBNode_C''])) (ret__struct_mdb_node_C_' t)) (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C''])) capa) (t_hrs_' (globals s)))) (t_hrs_' (globals ta)) \<longrightarrow> (case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals ta))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0))))}
 2. \<And>slota parenta capa s s'. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; (s, s') \<in> rf_sr; (pspace_aligned' and valid_mdb' and valid_objs' and valid_cap' cap) s; s' \<in> {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0}\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) parent s \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. \<forall>cte. cte_wp_at' ((=) cte) parent a \<longrightarrow> ((\<lambda>a aa. (\<exists>cte. ctes_of aa slot = Some cte) \<longrightarrow> cte_wp_at' (\<lambda>_. True) slot aa \<and> is_aligned a 3 \<and> is_aligned parent 3 \<and> is_aligned a 3 \<and> (slot \<noteq> 0 \<longrightarrow> is_aligned slot 3) \<and> parent \<noteq> 0 \<and> (slot \<noteq> 0 \<longrightarrow> is_aligned slot 3) \<and> valid_objs' aa \<and> valid_cap' cap aa \<and> (if parent = slot then True else cte_wp_at' (\<lambda>c. True) parent aa) \<and> cte_wp_at' (\<lambda>_. True) slot aa) \<circ> (mdbNext \<circ> cteMDBNode)) cte a) and cte_wp_at' (\<lambda>_. True) (ptr_val parenta)) s) \<and> s' \<in> UNIV \<inter> ?R'682 slota parenta capa \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>slota parenta capa s s'. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; (s, s') \<in> rf_sr; (pspace_aligned' and valid_mdb' and valid_objs' and valid_cap' cap) s; s' \<in> {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0}\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) parent s \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. \<forall>cte. cte_wp_at' ((=) cte) parent a \<longrightarrow> ((\<lambda>a aa. (\<exists>cte. ctes_of aa slot = Some cte) \<longrightarrow> cte_wp_at' (\<lambda>_. True) slot aa \<and> is_aligned a 3 \<and> is_aligned parent 3 \<and> is_aligned a 3 \<and> (slot \<noteq> 0 \<longrightarrow> is_aligned slot 3) \<and> parent \<noteq> 0 \<and> (slot \<noteq> 0 \<longrightarrow> is_aligned slot 3) \<and> valid_objs' aa \<and> valid_cap' cap aa \<and> (if parent = slot then True else cte_wp_at' (\<lambda>c. True) parent aa) \<and> cte_wp_at' (\<lambda>_. True) slot aa) \<circ> (mdbNext \<circ> cteMDBNode)) cte a) and cte_wp_at' (\<lambda>_. True) (ptr_val parenta)) s) \<and> s' \<in> UNIV \<inter> {s. \<forall>t. ret__unsigned_' t = mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(parenta\<rightarrow>[''cteMDBNode_C''])))) \<longrightarrow> (\<exists>cte'. (cte_lift \<circ>\<^sub>m cslift s) slota = Some cte' \<and> cl_valid_cte cte') \<longrightarrow> (\<forall>t. mdb_node_lift (ret__struct_mdb_node_C_' t) = \<lparr>mdbNext_CL = mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(parenta\<rightarrow>[''cteMDBNode_C''])))) && ~~ mask 3, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) true, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) true, mdbPrev_CL = parent && ~~ mask 3\<rparr> \<longrightarrow> s \<Turnstile>\<^sub>c slota \<longrightarrow> (mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(parenta\<rightarrow>[''cteMDBNode_C''])))) \<noteq> 0 \<longrightarrow> s \<Turnstile>\<^sub>c cte_Ptr (mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(parenta\<rightarrow>[''cteMDBNode_C'']))))) \<longrightarrow> (\<forall>ta. hrs_htd (t_hrs_' (globals ta)) = hrs_htd (t_hrs_' (globals s)) \<and> byte_regions_unmodified (hrs_mem_update (heap_update (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C''])) (ret__struct_mdb_node_C_' t)) (hrs_mem_update (heap_update (cap_Ptr &(slota\<rightarrow>[''cap_C''])) capa) (t_hrs_' (globals s)))) (t_hrs_' (globals ta)) \<longrightarrow> (\<forall>t. hrs_htd (t_hrs_' (globals t)) = hrs_htd (t_hrs_' (globals s)) \<and> byte_regions_unmodified (t_hrs_' (globals ta)) (t_hrs_' (globals t)) \<longrightarrow> (case untypedZeroRange cap of None \<Rightarrow> True | Some (aa, b) \<Rightarrow> region_actually_is_bytes aa (unat (b + 1 - aa)) s \<and> heap_list (hrs_mem (t_hrs_' (globals t))) (unat (b + 1 - aa)) aa = replicate (unat (b + 1 - aa)) 0)))) \<and> (mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(parenta\<rightarrow>[''cteMDBNode_C''])))) = 0 \<longrightarrow> (\<forall>ta. hrs_htd (t_hrs_' (globals ta)) = hrs_htd (t_hrs_' (globals s)) \<and> byte_regions_unmodified (hrs_mem_update (heap_update (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C''])) (ret__struct_mdb_node_C_' t)) (hrs_mem_update (heap_update (cap_Ptr &(slota\<rightarrow>[''cap_C''])) capa) (t_hrs_' (globals s)))) (t_hrs_' (globals ta)) \<longrightarrow> (case untypedZeroRange cap of None \<Rightarrow> True | Some (aa, b) \<Rightarrow> region_actually_is_bytes aa (unat (b + 1 - aa)) s \<and> heap_list (hrs_mem (t_hrs_' (globals ta))) (unat (b + 1 - aa)) aa = replicate (unat (b + 1 - aa)) 0))))} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>slota parenta capa s s'. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; (s, s') \<in> rf_sr; (pspace_aligned' and valid_mdb' and valid_objs' and valid_cap' cap) s; s' \<in> {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0}\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) parent s \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. \<forall>cte. cte_wp_at' ((=) cte) parent a \<longrightarrow> ((\<lambda>a aa. (\<exists>cte. ctes_of aa slot = Some cte) \<longrightarrow> cte_wp_at' (\<lambda>_. True) slot aa \<and> is_aligned a 3 \<and> is_aligned parent 3 \<and> is_aligned a 3 \<and> (slot \<noteq> 0 \<longrightarrow> is_aligned slot 3) \<and> parent \<noteq> 0 \<and> (slot \<noteq> 0 \<longrightarrow> is_aligned slot 3) \<and> valid_objs' aa \<and> valid_cap' cap aa \<and> (if parent = slot then True else cte_wp_at' (\<lambda>c. True) parent aa) \<and> cte_wp_at' (\<lambda>_. True) slot aa) \<circ> (mdbNext \<circ> cteMDBNode)) cte a) and cte_wp_at' (\<lambda>_. True) (ptr_val parenta)) s
 2. \<And>slota parenta capa s s'. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; (s, s') \<in> rf_sr; (pspace_aligned' and valid_mdb' and valid_objs' and valid_cap' cap) s; s' \<in> {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0}\<rbrakk> \<Longrightarrow> s' \<in> UNIV \<inter> {s. \<forall>t. ret__unsigned_' t = mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(parenta\<rightarrow>[''cteMDBNode_C''])))) \<longrightarrow> (\<exists>cte'. (cte_lift \<circ>\<^sub>m cslift s) slota = Some cte' \<and> cl_valid_cte cte') \<longrightarrow> (\<forall>t. mdb_node_lift (ret__struct_mdb_node_C_' t) = \<lparr>mdbNext_CL = mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(parenta\<rightarrow>[''cteMDBNode_C''])))) && ~~ mask 3, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) true, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) true, mdbPrev_CL = parent && ~~ mask 3\<rparr> \<longrightarrow> s \<Turnstile>\<^sub>c slota \<longrightarrow> (mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(parenta\<rightarrow>[''cteMDBNode_C''])))) \<noteq> 0 \<longrightarrow> s \<Turnstile>\<^sub>c cte_Ptr (mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(parenta\<rightarrow>[''cteMDBNode_C'']))))) \<longrightarrow> (\<forall>ta. hrs_htd (t_hrs_' (globals ta)) = hrs_htd (t_hrs_' (globals s)) \<and> byte_regions_unmodified (hrs_mem_update (heap_update (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C''])) (ret__struct_mdb_node_C_' t)) (hrs_mem_update (heap_update (cap_Ptr &(slota\<rightarrow>[''cap_C''])) capa) (t_hrs_' (globals s)))) (t_hrs_' (globals ta)) \<longrightarrow> (\<forall>t. hrs_htd (t_hrs_' (globals t)) = hrs_htd (t_hrs_' (globals s)) \<and> byte_regions_unmodified (t_hrs_' (globals ta)) (t_hrs_' (globals t)) \<longrightarrow> (case untypedZeroRange cap of None \<Rightarrow> True | Some (aa, b) \<Rightarrow> region_actually_is_bytes aa (unat (b + 1 - aa)) s \<and> heap_list (hrs_mem (t_hrs_' (globals t))) (unat (b + 1 - aa)) aa = replicate (unat (b + 1 - aa)) 0)))) \<and> (mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(parenta\<rightarrow>[''cteMDBNode_C''])))) = 0 \<longrightarrow> (\<forall>ta. hrs_htd (t_hrs_' (globals ta)) = hrs_htd (t_hrs_' (globals s)) \<and> byte_regions_unmodified (hrs_mem_update (heap_update (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C''])) (ret__struct_mdb_node_C_' t)) (hrs_mem_update (heap_update (cap_Ptr &(slota\<rightarrow>[''cap_C''])) capa) (t_hrs_' (globals s)))) (t_hrs_' (globals ta)) \<longrightarrow> (case untypedZeroRange cap of None \<Rightarrow> True | Some (aa, b) \<Rightarrow> region_actually_is_bytes aa (unat (b + 1 - aa)) s \<and> heap_list (hrs_mem (t_hrs_' (globals ta))) (unat (b + 1 - aa)) aa = replicate (unat (b + 1 - aa)) 0))))} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>slota parenta capa s s'. \<lbrakk>slota = cte_Ptr slot; parenta = cte_Ptr parent; ccap_relation cap capa; (s, s') \<in> rf_sr; (pspace_aligned' and valid_mdb' and valid_objs' and valid_cap' cap) s; s' \<in> {s. case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0}\<rbrakk> \<Longrightarrow> s' \<in> UNIV \<inter> {s. \<forall>t. ret__unsigned_' t = mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(parenta\<rightarrow>[''cteMDBNode_C''])))) \<longrightarrow> (\<exists>cte'. (cte_lift \<circ>\<^sub>m cslift s) slota = Some cte' \<and> cl_valid_cte cte') \<longrightarrow> (\<forall>t. mdb_node_lift (ret__struct_mdb_node_C_' t) = \<lparr>mdbNext_CL = mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(parenta\<rightarrow>[''cteMDBNode_C''])))) && ~~ mask 3, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) true, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) true, mdbPrev_CL = parent && ~~ mask 3\<rparr> \<longrightarrow> s \<Turnstile>\<^sub>c slota \<longrightarrow> (mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(parenta\<rightarrow>[''cteMDBNode_C''])))) \<noteq> 0 \<longrightarrow> s \<Turnstile>\<^sub>c cte_Ptr (mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(parenta\<rightarrow>[''cteMDBNode_C'']))))) \<longrightarrow> (\<forall>ta. hrs_htd (t_hrs_' (globals ta)) = hrs_htd (t_hrs_' (globals s)) \<and> byte_regions_unmodified (hrs_mem_update (heap_update (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C''])) (ret__struct_mdb_node_C_' t)) (hrs_mem_update (heap_update (cap_Ptr &(slota\<rightarrow>[''cap_C''])) capa) (t_hrs_' (globals s)))) (t_hrs_' (globals ta)) \<longrightarrow> (\<forall>t. hrs_htd (t_hrs_' (globals t)) = hrs_htd (t_hrs_' (globals s)) \<and> byte_regions_unmodified (t_hrs_' (globals ta)) (t_hrs_' (globals t)) \<longrightarrow> (case untypedZeroRange cap of None \<Rightarrow> True | Some (aa, b) \<Rightarrow> region_actually_is_bytes aa (unat (b + 1 - aa)) s \<and> heap_list (hrs_mem (t_hrs_' (globals t))) (unat (b + 1 - aa)) aa = replicate (unat (b + 1 - aa)) 0)))) \<and> (mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(parenta\<rightarrow>[''cteMDBNode_C''])))) = 0 \<longrightarrow> (\<forall>ta. hrs_htd (t_hrs_' (globals ta)) = hrs_htd (t_hrs_' (globals s)) \<and> byte_regions_unmodified (hrs_mem_update (heap_update (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C''])) (ret__struct_mdb_node_C_' t)) (hrs_mem_update (heap_update (cap_Ptr &(slota\<rightarrow>[''cap_C''])) capa) (t_hrs_' (globals s)))) (t_hrs_' (globals ta)) \<longrightarrow> (case untypedZeroRange cap of None \<Rightarrow> True | Some (aa, b) \<Rightarrow> region_actually_is_bytes aa (unat (b + 1 - aa)) s \<and> heap_list (hrs_mem (t_hrs_' (globals ta))) (unat (b + 1 - aa)) aa = replicate (unat (b + 1 - aa)) 0))))} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>capa s s' t cte' ta. \<lbrakk>ccap_relation cap capa; (s, s') \<in> rf_sr; case untypedZeroRange cap of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s' \<and> heap_list (hrs_mem (t_hrs_' (globals s'))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0; pspace_aligned' s; valid_mdb' s; valid_objs' s; valid_cap' cap s; ret__unsigned_' t = mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C''])))); (cte_lift \<circ>\<^sub>m cslift s') (cte_Ptr slot) = Some cte'; cl_valid_cte cte'; mdb_node_lift (ret__struct_mdb_node_C_' ta) = \<lparr>mdbNext_CL = mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C''])))) && ~~ mask 3, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) true, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) true, mdbPrev_CL = parent && ~~ mask 3\<rparr>; s' \<Turnstile>\<^sub>c cte_Ptr slot\<rbrakk> \<Longrightarrow> (mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C''])))) \<noteq> 0 \<longrightarrow> s' \<Turnstile>\<^sub>c cte_Ptr (mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C'']))))) \<longrightarrow> (\<forall>t. hrs_htd (t_hrs_' (globals t)) = hrs_htd (t_hrs_' (globals s')) \<and> byte_regions_unmodified (hrs_mem_update (heap_update (mdb_Ptr &(cte_Ptr slot\<rightarrow>[''cteMDBNode_C''])) (ret__struct_mdb_node_C_' ta)) (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C''])) capa) (t_hrs_' (globals s')))) (t_hrs_' (globals t)) \<longrightarrow> (\<forall>ta a b. untypedZeroRange cap = Some (a, b) \<longrightarrow> hrs_htd (t_hrs_' (globals ta)) = hrs_htd (t_hrs_' (globals s')) \<and> byte_regions_unmodified (t_hrs_' (globals t)) (t_hrs_' (globals ta)) \<longrightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s' \<and> heap_list (hrs_mem (t_hrs_' (globals ta))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0))) \<and> (mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C''])))) = 0 \<longrightarrow> (\<forall>t a b. untypedZeroRange cap = Some (a, b) \<longrightarrow> hrs_htd (t_hrs_' (globals t)) = hrs_htd (t_hrs_' (globals s')) \<and> byte_regions_unmodified (hrs_mem_update (heap_update (mdb_Ptr &(cte_Ptr slot\<rightarrow>[''cteMDBNode_C''])) (ret__struct_mdb_node_C_' ta)) (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C''])) capa) (t_hrs_' (globals s')))) (t_hrs_' (globals t)) \<longrightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s' \<and> heap_list (hrs_mem (t_hrs_' (globals t))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0)) proof (prove)
goal (2 subgoals):
 1. \<And>capa s s' t cte' ta tb tc a b. \<lbrakk>ccap_relation cap capa; (s, s') \<in> rf_sr; pspace_aligned' s; valid_mdb' s; valid_objs' s; valid_cap' cap s; ret__unsigned_' t = mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C''])))); (cte_lift \<circ>\<^sub>m cslift s') (cte_Ptr slot) = Some cte'; cl_valid_cte cte'; mdb_node_lift (ret__struct_mdb_node_C_' ta) = \<lparr>mdbNext_CL = mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C''])))) && ~~ mask 3, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) true, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) true, mdbPrev_CL = parent && ~~ mask 3\<rparr>; s' \<Turnstile>\<^sub>c cte_Ptr slot; mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C''])))) \<noteq> 0; s' \<Turnstile>\<^sub>c cte_Ptr (mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C'']))))); untypedZeroRange cap = Some (a, b); region_actually_is_bytes a (unat (b + 1 - a)) s'; heap_list (hrs_mem (t_hrs_' (globals s'))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0; hrs_htd (t_hrs_' (globals tb)) = hrs_htd (t_hrs_' (globals s')); byte_regions_unmodified (hrs_mem_update (heap_update (mdb_Ptr &(cte_Ptr slot\<rightarrow>[''cteMDBNode_C''])) (ret__struct_mdb_node_C_' ta)) (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C''])) capa) (t_hrs_' (globals s')))) (t_hrs_' (globals tb)); hrs_htd (t_hrs_' (globals tc)) = hrs_htd (t_hrs_' (globals s')); byte_regions_unmodified (t_hrs_' (globals tb)) (t_hrs_' (globals tc))\<rbrakk> \<Longrightarrow> heap_list (hrs_mem (t_hrs_' (globals tc))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0
 2. \<And>capa s s' t cte' ta tb a b. \<lbrakk>ccap_relation cap capa; (s, s') \<in> rf_sr; pspace_aligned' s; valid_mdb' s; valid_objs' s; valid_cap' cap s; ret__unsigned_' t = 0; (cte_lift \<circ>\<^sub>m cslift s') (cte_Ptr slot) = Some cte'; cl_valid_cte cte'; mdb_node_lift (ret__struct_mdb_node_C_' ta) = \<lparr>mdbNext_CL = 0, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) true, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) true, mdbPrev_CL = parent && ~~ mask 3\<rparr>; s' \<Turnstile>\<^sub>c cte_Ptr slot; mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C''])))) = 0; untypedZeroRange cap = Some (a, b); region_actually_is_bytes a (unat (b + 1 - a)) s'; heap_list (hrs_mem (t_hrs_' (globals s'))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0; hrs_htd (t_hrs_' (globals tb)) = hrs_htd (t_hrs_' (globals s')); byte_regions_unmodified (hrs_mem_update (heap_update (mdb_Ptr &(cte_Ptr slot\<rightarrow>[''cteMDBNode_C''])) (ret__struct_mdb_node_C_' ta)) (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C''])) capa) (t_hrs_' (globals s')))) (t_hrs_' (globals tb))\<rbrakk> \<Longrightarrow> heap_list (hrs_mem (t_hrs_' (globals tb))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0 proof (prove)
goal (2 subgoals):
 1. \<And>capa s s' t cte' ta tb tc a b x. \<lbrakk>ccap_relation cap capa; (s, s') \<in> rf_sr; pspace_aligned' s; valid_mdb' s; valid_objs' s; valid_cap' cap s; ret__unsigned_' t = mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C''])))); (cte_lift \<circ>\<^sub>m cslift s') (cte_Ptr slot) = Some cte'; cl_valid_cte cte'; mdb_node_lift (ret__struct_mdb_node_C_' ta) = \<lparr>mdbNext_CL = mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C''])))) && ~~ mask 3, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) true, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) true, mdbPrev_CL = parent && ~~ mask 3\<rparr>; s' \<Turnstile>\<^sub>c cte_Ptr slot; mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C''])))) \<noteq> 0; s' \<Turnstile>\<^sub>c cte_Ptr (mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C'']))))); untypedZeroRange cap = Some (a, b); region_actually_is_bytes a (unat (b + 1 - a)) s'; hrs_htd (t_hrs_' (globals tb)) = hrs_htd (t_hrs_' (globals s')); byte_regions_unmodified (hrs_mem_update (heap_update (mdb_Ptr &(cte_Ptr slot\<rightarrow>[''cteMDBNode_C''])) (ret__struct_mdb_node_C_' ta)) (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C''])) capa) (t_hrs_' (globals s')))) (t_hrs_' (globals tb)); hrs_htd (t_hrs_' (globals tc)) = hrs_htd (t_hrs_' (globals s')); byte_regions_unmodified (t_hrs_' (globals tb)) (t_hrs_' (globals tc)); x \<in> {a..+unat (b + 1 - a)}\<rbrakk> \<Longrightarrow> hrs_mem (t_hrs_' (globals tc)) x = hrs_mem (t_hrs_' (globals s')) x
 2. \<And>capa s s' t cte' ta tb a b. \<lbrakk>ccap_relation cap capa; (s, s') \<in> rf_sr; pspace_aligned' s; valid_mdb' s; valid_objs' s; valid_cap' cap s; ret__unsigned_' t = 0; (cte_lift \<circ>\<^sub>m cslift s') (cte_Ptr slot) = Some cte'; cl_valid_cte cte'; mdb_node_lift (ret__struct_mdb_node_C_' ta) = \<lparr>mdbNext_CL = 0, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) true, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) true, mdbPrev_CL = parent && ~~ mask 3\<rparr>; s' \<Turnstile>\<^sub>c cte_Ptr slot; mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C''])))) = 0; untypedZeroRange cap = Some (a, b); region_actually_is_bytes a (unat (b + 1 - a)) s'; heap_list (hrs_mem (t_hrs_' (globals s'))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0; hrs_htd (t_hrs_' (globals tb)) = hrs_htd (t_hrs_' (globals s')); byte_regions_unmodified (hrs_mem_update (heap_update (mdb_Ptr &(cte_Ptr slot\<rightarrow>[''cteMDBNode_C''])) (ret__struct_mdb_node_C_' ta)) (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C''])) capa) (t_hrs_' (globals s')))) (t_hrs_' (globals tb))\<rbrakk> \<Longrightarrow> heap_list (hrs_mem (t_hrs_' (globals tb))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0 proof (prove)
goal (4 subgoals):
 1. \<And>capa s s' t cte' ta tb tc a b x. \<lbrakk>ccap_relation cap capa; (s, s') \<in> rf_sr; pspace_aligned' s; valid_mdb' s; valid_objs' s; valid_cap' cap s; ret__unsigned_' t = mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C''])))); (cte_lift \<circ>\<^sub>m cslift s') (cte_Ptr slot) = Some cte'; cl_valid_cte cte'; mdb_node_lift (ret__struct_mdb_node_C_' ta) = \<lparr>mdbNext_CL = mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C''])))) && ~~ mask 3, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) true, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) true, mdbPrev_CL = parent && ~~ mask 3\<rparr>; s' \<Turnstile>\<^sub>c cte_Ptr slot; mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C''])))) \<noteq> 0; s' \<Turnstile>\<^sub>c cte_Ptr (mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C'']))))); untypedZeroRange cap = Some (a, b); region_actually_is_bytes a (unat (b + 1 - a)) s'; hrs_htd (t_hrs_' (globals tb)) = hrs_htd (t_hrs_' (globals s')); byte_regions_unmodified (hrs_mem_update (heap_update (mdb_Ptr &(cte_Ptr slot\<rightarrow>[''cteMDBNode_C''])) (ret__struct_mdb_node_C_' ta)) (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C''])) capa) (t_hrs_' (globals s')))) (t_hrs_' (globals tb)); hrs_htd (t_hrs_' (globals tc)) = hrs_htd (t_hrs_' (globals s')); byte_regions_unmodified (t_hrs_' (globals tb)) (t_hrs_' (globals tc)); x \<in> {a..+unat (b + 1 - a)}\<rbrakk> \<Longrightarrow> byte_regions_unmodified (t_hrs_' (globals s')) (t_hrs_' (globals tc))
 2. \<And>capa s s' t cte' ta tb tc a b x. \<lbrakk>ccap_relation cap capa; (s, s') \<in> rf_sr; pspace_aligned' s; valid_mdb' s; valid_objs' s; valid_cap' cap s; ret__unsigned_' t = mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C''])))); (cte_lift \<circ>\<^sub>m cslift s') (cte_Ptr slot) = Some cte'; cl_valid_cte cte'; mdb_node_lift (ret__struct_mdb_node_C_' ta) = \<lparr>mdbNext_CL = mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C''])))) && ~~ mask 3, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) true, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) true, mdbPrev_CL = parent && ~~ mask 3\<rparr>; s' \<Turnstile>\<^sub>c cte_Ptr slot; mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C''])))) \<noteq> 0; s' \<Turnstile>\<^sub>c cte_Ptr (mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C'']))))); untypedZeroRange cap = Some (a, b); region_actually_is_bytes a (unat (b + 1 - a)) s'; hrs_htd (t_hrs_' (globals tb)) = hrs_htd (t_hrs_' (globals s')); byte_regions_unmodified (hrs_mem_update (heap_update (mdb_Ptr &(cte_Ptr slot\<rightarrow>[''cteMDBNode_C''])) (ret__struct_mdb_node_C_' ta)) (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C''])) capa) (t_hrs_' (globals s')))) (t_hrs_' (globals tb)); hrs_htd (t_hrs_' (globals tc)) = hrs_htd (t_hrs_' (globals s')); byte_regions_unmodified (t_hrs_' (globals tb)) (t_hrs_' (globals tc)); x \<in> {a..+unat (b + 1 - a)}\<rbrakk> \<Longrightarrow> region_actually_is_bytes (?y1490 capa s s' t cte' ta tb tc a b x) (?n1490 capa s s' t cte' ta tb tc a b x) s'
 3. \<And>capa s s' t cte' ta tb tc a b x. \<lbrakk>ccap_relation cap capa; (s, s') \<in> rf_sr; pspace_aligned' s; valid_mdb' s; valid_objs' s; valid_cap' cap s; ret__unsigned_' t = mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C''])))); (cte_lift \<circ>\<^sub>m cslift s') (cte_Ptr slot) = Some cte'; cl_valid_cte cte'; mdb_node_lift (ret__struct_mdb_node_C_' ta) = \<lparr>mdbNext_CL = mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C''])))) && ~~ mask 3, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) true, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) true, mdbPrev_CL = parent && ~~ mask 3\<rparr>; s' \<Turnstile>\<^sub>c cte_Ptr slot; mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C''])))) \<noteq> 0; s' \<Turnstile>\<^sub>c cte_Ptr (mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C'']))))); untypedZeroRange cap = Some (a, b); region_actually_is_bytes a (unat (b + 1 - a)) s'; hrs_htd (t_hrs_' (globals tb)) = hrs_htd (t_hrs_' (globals s')); byte_regions_unmodified (hrs_mem_update (heap_update (mdb_Ptr &(cte_Ptr slot\<rightarrow>[''cteMDBNode_C''])) (ret__struct_mdb_node_C_' ta)) (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C''])) capa) (t_hrs_' (globals s')))) (t_hrs_' (globals tb)); hrs_htd (t_hrs_' (globals tc)) = hrs_htd (t_hrs_' (globals s')); byte_regions_unmodified (t_hrs_' (globals tb)) (t_hrs_' (globals tc)); x \<in> {a..+unat (b + 1 - a)}\<rbrakk> \<Longrightarrow> x \<in> {?y1490 capa s s' t cte' ta tb tc a b x..+?n1490 capa s s' t cte' ta tb tc a b x}
 4. \<And>capa s s' t cte' ta tb a b. \<lbrakk>ccap_relation cap capa; (s, s') \<in> rf_sr; pspace_aligned' s; valid_mdb' s; valid_objs' s; valid_cap' cap s; ret__unsigned_' t = 0; (cte_lift \<circ>\<^sub>m cslift s') (cte_Ptr slot) = Some cte'; cl_valid_cte cte'; mdb_node_lift (ret__struct_mdb_node_C_' ta) = \<lparr>mdbNext_CL = 0, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) true, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) true, mdbPrev_CL = parent && ~~ mask 3\<rparr>; s' \<Turnstile>\<^sub>c cte_Ptr slot; mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C''])))) = 0; untypedZeroRange cap = Some (a, b); region_actually_is_bytes a (unat (b + 1 - a)) s'; heap_list (hrs_mem (t_hrs_' (globals s'))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0; hrs_htd (t_hrs_' (globals tb)) = hrs_htd (t_hrs_' (globals s')); byte_regions_unmodified (hrs_mem_update (heap_update (mdb_Ptr &(cte_Ptr slot\<rightarrow>[''cteMDBNode_C''])) (ret__struct_mdb_node_C_' ta)) (hrs_mem_update (heap_update (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C''])) capa) (t_hrs_' (globals s')))) (t_hrs_' (globals tb))\<rbrakk> \<Longrightarrow> heap_list (hrs_mem (t_hrs_' (globals tb))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0 proof (prove)
goal (1 subgoal):
 1. \<And>capa s s' t cte' ta tb a b. \<lbrakk>ccap_relation cap capa; (s, s') \<in> rf_sr; pspace_aligned' s; valid_mdb' s; valid_objs' s; valid_cap' cap s; ret__unsigned_' t = 0; (cte_lift \<circ>\<^sub>m cslift s') (cte_Ptr slot) = Some cte'; cl_valid_cte cte'; mdb_node_lift (ret__struct_mdb_node_C_' ta) = \<lparr>mdbNext_CL = 0, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) true, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) true, mdbPrev_CL = parent && ~~ mask 3\<rparr>; s' \<Turnstile>\<^sub>c cte_Ptr slot; mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C''])))) = 0; untypedZeroRange cap = Some (a, b); region_actually_is_bytes a (unat (b + 1 - a)) s'; heap_list (hrs_mem (t_hrs_' (globals s'))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0; hrs_htd (t_hrs_' (globals tb)) = hrs_htd (t_hrs_' (globals s')); byte_regions_unmodified (hrs_mem_update (heap_update (cte_Ptr slot) (cteMDBNode_C_update (\<lambda>_. ret__struct_mdb_node_C_' ta) (cte_C.cap_C_update (\<lambda>_. capa) (h_val (hrs_mem (t_hrs_' (globals s'))) (cte_Ptr slot))))) (hrs_mem_update (heap_update (cte_Ptr slot) (cte_C.cap_C_update (\<lambda>_. capa) (h_val (hrs_mem (t_hrs_' (globals s'))) (cte_Ptr slot)))) (t_hrs_' (globals s')))) (t_hrs_' (globals tb))\<rbrakk> \<Longrightarrow> heap_list (hrs_mem (t_hrs_' (globals tb))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0 proof (prove)
goal (1 subgoal):
 1. \<And>capa s s' t cte' ta tb a b x. \<lbrakk>ccap_relation cap capa; (s, s') \<in> rf_sr; pspace_aligned' s; valid_mdb' s; valid_objs' s; valid_cap' cap s; ret__unsigned_' t = 0; (cte_lift \<circ>\<^sub>m cslift s') (cte_Ptr slot) = Some cte'; cl_valid_cte cte'; mdb_node_lift (ret__struct_mdb_node_C_' ta) = \<lparr>mdbNext_CL = 0, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) true, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) true, mdbPrev_CL = parent && ~~ mask 3\<rparr>; s' \<Turnstile>\<^sub>c cte_Ptr slot; mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C''])))) = 0; untypedZeroRange cap = Some (a, b); region_actually_is_bytes a (unat (b + 1 - a)) s'; hrs_htd (t_hrs_' (globals tb)) = hrs_htd (t_hrs_' (globals s')); byte_regions_unmodified (hrs_mem_update (heap_update (cte_Ptr slot) (cteMDBNode_C_update (\<lambda>_. ret__struct_mdb_node_C_' ta) (cte_C.cap_C_update (\<lambda>_. capa) (h_val (hrs_mem (t_hrs_' (globals s'))) (cte_Ptr slot))))) (hrs_mem_update (heap_update (cte_Ptr slot) (cte_C.cap_C_update (\<lambda>_. capa) (h_val (hrs_mem (t_hrs_' (globals s'))) (cte_Ptr slot)))) (t_hrs_' (globals s')))) (t_hrs_' (globals tb)); x \<in> {a..+unat (b + 1 - a)}\<rbrakk> \<Longrightarrow> hrs_mem (t_hrs_' (globals tb)) x = hrs_mem (t_hrs_' (globals s')) x proof (prove)
goal (3 subgoals):
 1. \<And>capa s s' t cte' ta tb a b x. \<lbrakk>ccap_relation cap capa; (s, s') \<in> rf_sr; pspace_aligned' s; valid_mdb' s; valid_objs' s; valid_cap' cap s; ret__unsigned_' t = 0; (cte_lift \<circ>\<^sub>m cslift s') (cte_Ptr slot) = Some cte'; cl_valid_cte cte'; mdb_node_lift (ret__struct_mdb_node_C_' ta) = \<lparr>mdbNext_CL = 0, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) true, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) true, mdbPrev_CL = parent && ~~ mask 3\<rparr>; s' \<Turnstile>\<^sub>c cte_Ptr slot; mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C''])))) = 0; untypedZeroRange cap = Some (a, b); region_actually_is_bytes a (unat (b + 1 - a)) s'; hrs_htd (t_hrs_' (globals tb)) = hrs_htd (t_hrs_' (globals s')); byte_regions_unmodified (hrs_mem_update (heap_update (cte_Ptr slot) (cteMDBNode_C_update (\<lambda>_. ret__struct_mdb_node_C_' ta) (cte_C.cap_C_update (\<lambda>_. capa) (h_val (hrs_mem (t_hrs_' (globals s'))) (cte_Ptr slot))))) (hrs_mem_update (heap_update (cte_Ptr slot) (cte_C.cap_C_update (\<lambda>_. capa) (h_val (hrs_mem (t_hrs_' (globals s'))) (cte_Ptr slot)))) (t_hrs_' (globals s')))) (t_hrs_' (globals tb)); x \<in> {a..+unat (b + 1 - a)}\<rbrakk> \<Longrightarrow> byte_regions_unmodified (t_hrs_' (globals s')) (t_hrs_' (globals tb))
 2. \<And>capa s s' t cte' ta tb a b x. \<lbrakk>ccap_relation cap capa; (s, s') \<in> rf_sr; pspace_aligned' s; valid_mdb' s; valid_objs' s; valid_cap' cap s; ret__unsigned_' t = 0; (cte_lift \<circ>\<^sub>m cslift s') (cte_Ptr slot) = Some cte'; cl_valid_cte cte'; mdb_node_lift (ret__struct_mdb_node_C_' ta) = \<lparr>mdbNext_CL = 0, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) true, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) true, mdbPrev_CL = parent && ~~ mask 3\<rparr>; s' \<Turnstile>\<^sub>c cte_Ptr slot; mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C''])))) = 0; untypedZeroRange cap = Some (a, b); region_actually_is_bytes a (unat (b + 1 - a)) s'; hrs_htd (t_hrs_' (globals tb)) = hrs_htd (t_hrs_' (globals s')); byte_regions_unmodified (hrs_mem_update (heap_update (cte_Ptr slot) (cteMDBNode_C_update (\<lambda>_. ret__struct_mdb_node_C_' ta) (cte_C.cap_C_update (\<lambda>_. capa) (h_val (hrs_mem (t_hrs_' (globals s'))) (cte_Ptr slot))))) (hrs_mem_update (heap_update (cte_Ptr slot) (cte_C.cap_C_update (\<lambda>_. capa) (h_val (hrs_mem (t_hrs_' (globals s'))) (cte_Ptr slot)))) (t_hrs_' (globals s')))) (t_hrs_' (globals tb)); x \<in> {a..+unat (b + 1 - a)}\<rbrakk> \<Longrightarrow> region_actually_is_bytes (?y1513 capa s s' t cte' ta tb a b x) (?n1513 capa s s' t cte' ta tb a b x) s'
 3. \<And>capa s s' t cte' ta tb a b x. \<lbrakk>ccap_relation cap capa; (s, s') \<in> rf_sr; pspace_aligned' s; valid_mdb' s; valid_objs' s; valid_cap' cap s; ret__unsigned_' t = 0; (cte_lift \<circ>\<^sub>m cslift s') (cte_Ptr slot) = Some cte'; cl_valid_cte cte'; mdb_node_lift (ret__struct_mdb_node_C_' ta) = \<lparr>mdbNext_CL = 0, mdbRevocable_CL = SCAST(32 signed \<rightarrow> 32) true, mdbFirstBadged_CL = SCAST(32 signed \<rightarrow> 32) true, mdbPrev_CL = parent && ~~ mask 3\<rparr>; s' \<Turnstile>\<^sub>c cte_Ptr slot; mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (mdb_Ptr &(cte_Ptr parent\<rightarrow>[''cteMDBNode_C''])))) = 0; untypedZeroRange cap = Some (a, b); region_actually_is_bytes a (unat (b + 1 - a)) s'; hrs_htd (t_hrs_' (globals tb)) = hrs_htd (t_hrs_' (globals s')); byte_regions_unmodified (hrs_mem_update (heap_update (cte_Ptr slot) (cteMDBNode_C_update (\<lambda>_. ret__struct_mdb_node_C_' ta) (cte_C.cap_C_update (\<lambda>_. capa) (h_val (hrs_mem (t_hrs_' (globals s'))) (cte_Ptr slot))))) (hrs_mem_update (heap_update (cte_Ptr slot) (cte_C.cap_C_update (\<lambda>_. capa) (h_val (hrs_mem (t_hrs_' (globals s'))) (cte_Ptr slot)))) (t_hrs_' (globals s')))) (t_hrs_' (globals tb)); x \<in> {a..+unat (b + 1 - a)}\<rbrakk> \<Longrightarrow> x \<in> {?y1513 capa s s' t cte' ta tb a b x..+?n1513 capa s s' t cte' ta tb a b x} proof (prove)
goal:
No subgoals!