theory Detype_R

lemma new_cap_object_comm_helper:
  "monad_commute
     (pspace_aligned' and pspace_distinct' and (\<lambda>s. no_0 (ctes_of s)) and
      (\<lambda>s. weak_valid_dlist (ctes_of s)) and
      (\<lambda>s. valid_nullcaps (ctes_of s)) and
      cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent and
      cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot and
      pspace_no_overlap' ptr (Types_H.getObjectSize ty us) and
      valid_arch_state' and
      K (Types_H.getObjectSize ty us<word_bits) and
      K (cap \<noteq> capability.NullCap) and
      K (is_aligned ptr (Types_H.getObjectSize ty us) \<and> ptr \<noteq> 0 \<and> parent \<noteq> 0))
     (RetypeDecls_H.createObject ty ptr us d) (insertNewCap parent slot cap)" apply (clarsimp simp:insertNewCap_def bind_assoc liftM_def) apply (rule monad_commute_guard_imp) apply (rule monad_commute_split[OF _ createObject_getCTE_commute])+ apply (rule monad_commute_split[OF _ commute_commute[OF assert_commute]]) apply (rule monad_commute_split[OF _ createObject_setCTE_commute]) apply (rule monad_commute_split[OF _ commute_commute[OF createObject_updateMDB_commute]]) apply (rule monad_commute_split[OF _ commute_commute[OF createObject_updateMDB_commute]]) apply (rule createObject_updateNewFreeIndex_commute) apply (wp getCTE_wp hoare_vcg_imp_lift hoare_vcg_disj_lift valid_arch_state'_updateMDB
         updateMDB_pspace_no_overlap' setCTE_pspace_no_overlap'
         | clarsimp simp:conj_comms)+ apply (clarsimp simp:cte_wp_at_ctes_of) apply (frule_tac slot = slot in pspace_no_overlapD2') apply simp+ apply (frule_tac slot = parent in pspace_no_overlapD2') apply simp+ apply (case_tac ctea,clarsimp) apply (frule_tac p = slot in nullcapsD') apply simp+ apply (subgoal_tac "(mdbNext (cteMDBNode cte) = 0 \<or>
           (\<exists>ctea. ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea))") apply (elim disjE) apply clarsimp+ apply (frule_tac slot = "(mdbNext (cteMDBNode cte))"
      in pspace_no_overlapD2') apply simp+ apply (clarsimp simp:weak_valid_dlist_def) apply (drule_tac x = "parent " in spec) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monad_commute (pspace_aligned' and pspace_distinct' and (\<lambda>s. no_0 (ctes_of s)) and (\<lambda>s. weak_valid_dlist (ctes_of s)) and (\<lambda>s. valid_nullcaps (ctes_of s)) and cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot and pspace_no_overlap' ptr (getObjectSize ty us) and valid_arch_state' and K (getObjectSize ty us < word_bits) and K (cap \<noteq> capability.NullCap) and K (is_aligned ptr (getObjectSize ty us) \<and> ptr \<noteq> 0 \<and> parent \<noteq> 0)) (global.createObject ty ptr us d) (insertNewCap parent slot cap) proof (prove)
goal (1 subgoal):
 1. monad_commute (pspace_aligned' and pspace_distinct' and (\<lambda>s. no_0 (ctes_of s)) and (\<lambda>s. weak_valid_dlist (ctes_of s)) and (\<lambda>s. valid_nullcaps (ctes_of s)) and cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot and pspace_no_overlap' ptr (getObjectSize ty us) and valid_arch_state' and (\<lambda>y. getObjectSize ty us < word_bits) and (\<lambda>y. cap \<noteq> capability.NullCap) and (\<lambda>y. is_aligned ptr (getObjectSize ty us) \<and> ptr \<noteq> 0 \<and> parent \<noteq> 0)) (global.createObject ty ptr us d) (do x <- getCTE parent;
oldCTE <- getCTE slot;
y <- assert (cteCap oldCTE = capability.NullCap \<and> mdbNext (cteMDBNode oldCTE) = nullPointer \<and> mdbPrev (cteMDBNode oldCTE) = nullPointer);
y <- setCTE slot (CTE cap (MDB (mdbNext (cteMDBNode x)) parent True True));
y <- updateMDB (mdbNext (cteMDBNode x)) (mdbPrev_update (\<lambda>_. slot));
y <- updateMDB parent (mdbNext_update (\<lambda>_. slot));
updateNewFreeIndex slot
od) proof (prove)
goal (2 subgoals):
 1. monad_commute ?P (global.createObject ty ptr us d) (do x <- getCTE parent;
oldCTE <- getCTE slot;
y <- assert (cteCap oldCTE = capability.NullCap \<and> mdbNext (cteMDBNode oldCTE) = nullPointer \<and> mdbPrev (cteMDBNode oldCTE) = nullPointer);
y <- setCTE slot (CTE cap (MDB (mdbNext (cteMDBNode x)) parent True True));
y <- updateMDB (mdbNext (cteMDBNode x)) (mdbPrev_update (\<lambda>_. slot));
y <- updateMDB parent (mdbNext_update (\<lambda>_. slot));
updateNewFreeIndex slot
od)
 2. \<And>s. (pspace_aligned' and pspace_distinct' and (\<lambda>s. no_0 (ctes_of s)) and (\<lambda>s. weak_valid_dlist (ctes_of s)) and (\<lambda>s. valid_nullcaps (ctes_of s)) and cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot and pspace_no_overlap' ptr (getObjectSize ty us) and valid_arch_state' and (\<lambda>y. getObjectSize ty us < word_bits) and (\<lambda>y. cap \<noteq> capability.NullCap) and (\<lambda>y. is_aligned ptr (getObjectSize ty us) \<and> ptr \<noteq> 0 \<and> parent \<noteq> 0)) s \<Longrightarrow> ?P s proof (prove)
goal (4 subgoals):
 1. \<And>r ra. monad_commute (?Q8 r ra) (global.createObject ty ptr us d) (do y <- assert (cteCap ra = capability.NullCap \<and> mdbNext (cteMDBNode ra) = nullPointer \<and> mdbPrev (cteMDBNode ra) = nullPointer);
y <- setCTE slot (CTE cap (MDB (mdbNext (cteMDBNode r)) parent True True));
y <- updateMDB (mdbNext (cteMDBNode r)) (mdbPrev_update (\<lambda>_. slot));
y <- updateMDB parent (mdbNext_update (\<lambda>_. slot));
updateNewFreeIndex slot
od)
 2. \<And>r. \<lbrace>?P'8 r\<rbrace> getCTE slot \<lbrace>?Q8 r\<rbrace>
 3. \<lbrace>?P'3\<rbrace> getCTE parent \<lbrace>\<lambda>r. cte_wp_at' (\<lambda>_. True) slot and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize ty us) and K (ptr \<noteq> slot) and K (getObjectSize ty us < word_bits) and K (is_aligned ptr (getObjectSize ty us)) and ?P'8 r\<rbrace>
 4. \<And>s. (pspace_aligned' and pspace_distinct' and (\<lambda>s. no_0 (ctes_of s)) and (\<lambda>s. weak_valid_dlist (ctes_of s)) and (\<lambda>s. valid_nullcaps (ctes_of s)) and cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot and pspace_no_overlap' ptr (getObjectSize ty us) and valid_arch_state' and (\<lambda>y. getObjectSize ty us < word_bits) and (\<lambda>y. cap \<noteq> capability.NullCap) and (\<lambda>y. is_aligned ptr (getObjectSize ty us) \<and> ptr \<noteq> 0 \<and> parent \<noteq> 0)) s \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) parent and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize ty us) and K (ptr \<noteq> parent) and K (getObjectSize ty us < word_bits) and K (is_aligned ptr (getObjectSize ty us)) and ?P'3) s proof (prove)
goal (5 subgoals):
 1. \<And>r ra rb. monad_commute (?Q13 r ra rb) (global.createObject ty ptr us d) (do y <- setCTE slot (CTE cap (MDB (mdbNext (cteMDBNode r)) parent True True));
y <- updateMDB (mdbNext (cteMDBNode r)) (mdbPrev_update (\<lambda>_. slot));
y <- updateMDB parent (mdbNext_update (\<lambda>_. slot));
updateNewFreeIndex slot
od)
 2. \<And>r ra. \<lbrace>?P'13 r ra\<rbrace> assert (cteCap ra = capability.NullCap \<and> mdbNext (cteMDBNode ra) = nullPointer \<and> mdbPrev (cteMDBNode ra) = nullPointer) \<lbrace>?Q13 r ra\<rbrace>
 3. \<And>r. \<lbrace>?P'8 r\<rbrace> getCTE slot \<lbrace>\<lambda>ra. K (cteCap ra = capability.NullCap \<and> mdbNext (cteMDBNode ra) = nullPointer \<and> mdbPrev (cteMDBNode ra) = nullPointer) and ?P'13 r ra\<rbrace>
 4. \<lbrace>?P'3\<rbrace> getCTE parent \<lbrace>\<lambda>r. cte_wp_at' (\<lambda>_. True) slot and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize ty us) and K (ptr \<noteq> slot) and K (getObjectSize ty us < word_bits) and K (is_aligned ptr (getObjectSize ty us)) and ?P'8 r\<rbrace>
 5. \<And>s. (pspace_aligned' and pspace_distinct' and (\<lambda>s. no_0 (ctes_of s)) and (\<lambda>s. weak_valid_dlist (ctes_of s)) and (\<lambda>s. valid_nullcaps (ctes_of s)) and cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot and pspace_no_overlap' ptr (getObjectSize ty us) and valid_arch_state' and (\<lambda>y. getObjectSize ty us < word_bits) and (\<lambda>y. cap \<noteq> capability.NullCap) and (\<lambda>y. is_aligned ptr (getObjectSize ty us) \<and> ptr \<noteq> 0 \<and> parent \<noteq> 0)) s \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) parent and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize ty us) and K (ptr \<noteq> parent) and K (getObjectSize ty us < word_bits) and K (is_aligned ptr (getObjectSize ty us)) and ?P'3) s proof (prove)
goal (6 subgoals):
 1. \<And>r ra rb rc. monad_commute (?Q19 r ra rb rc) (global.createObject ty ptr us d) (do y <- updateMDB (mdbNext (cteMDBNode r)) (mdbPrev_update (\<lambda>_. slot));
y <- updateMDB parent (mdbNext_update (\<lambda>_. slot));
updateNewFreeIndex slot
od)
 2. \<And>r ra rb. \<lbrace>?P'19 r ra rb\<rbrace> setCTE slot (CTE cap (MDB (mdbNext (cteMDBNode r)) parent True True)) \<lbrace>?Q19 r ra rb\<rbrace>
 3. \<And>r ra. \<lbrace>?P'13 r ra\<rbrace> assert (cteCap ra = capability.NullCap \<and> mdbNext (cteMDBNode ra) = nullPointer \<and> mdbPrev (cteMDBNode ra) = nullPointer) \<lbrace>\<lambda>rb. cte_wp_at' (\<lambda>_. True) slot and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize ty us) and valid_arch_state' and K (ptr \<noteq> slot) and K (is_aligned ptr (getObjectSize ty us)) and K (getObjectSize ty us < word_bits) and ?P'19 r ra rb\<rbrace>
 4. \<And>r. \<lbrace>?P'8 r\<rbrace> getCTE slot \<lbrace>\<lambda>ra. K (cteCap ra = capability.NullCap \<and> mdbNext (cteMDBNode ra) = nullPointer \<and> mdbPrev (cteMDBNode ra) = nullPointer) and ?P'13 r ra\<rbrace>
 5. \<lbrace>?P'3\<rbrace> getCTE parent \<lbrace>\<lambda>r. cte_wp_at' (\<lambda>_. True) slot and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize ty us) and K (ptr \<noteq> slot) and K (getObjectSize ty us < word_bits) and K (is_aligned ptr (getObjectSize ty us)) and ?P'8 r\<rbrace>
 6. \<And>s. (pspace_aligned' and pspace_distinct' and (\<lambda>s. no_0 (ctes_of s)) and (\<lambda>s. weak_valid_dlist (ctes_of s)) and (\<lambda>s. valid_nullcaps (ctes_of s)) and cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot and pspace_no_overlap' ptr (getObjectSize ty us) and valid_arch_state' and (\<lambda>y. getObjectSize ty us < word_bits) and (\<lambda>y. cap \<noteq> capability.NullCap) and (\<lambda>y. is_aligned ptr (getObjectSize ty us) \<and> ptr \<noteq> 0 \<and> parent \<noteq> 0)) s \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) parent and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize ty us) and K (ptr \<noteq> parent) and K (getObjectSize ty us < word_bits) and K (is_aligned ptr (getObjectSize ty us)) and ?P'3) s proof (prove)
goal (7 subgoals):
 1. \<And>r ra rb rc rd. monad_commute (?Q24 r ra rb rc rd) (global.createObject ty ptr us d) (do y <- updateMDB parent (mdbNext_update (\<lambda>_. slot));
updateNewFreeIndex slot
od)
 2. \<And>r ra rb rc. \<lbrace>?P'24 r ra rb rc\<rbrace> updateMDB (mdbNext (cteMDBNode r)) (mdbPrev_update (\<lambda>_. slot)) \<lbrace>?Q24 r ra rb rc\<rbrace>
 3. \<And>r ra rb. \<lbrace>?P'19 r ra rb\<rbrace> setCTE slot (CTE cap (MDB (mdbNext (cteMDBNode r)) parent True True)) \<lbrace>\<lambda>rc. (\<lambda>s. mdbNext (cteMDBNode r) \<noteq> 0 \<longrightarrow> cte_wp_at' (\<lambda>_. True) (mdbNext (cteMDBNode r)) s) and pspace_no_overlap' ptr (getObjectSize ty us) and pspace_aligned' and pspace_distinct' and valid_arch_state' and K (ptr \<noteq> mdbNext (cteMDBNode r)) and K (is_aligned ptr (getObjectSize ty us)) and K (getObjectSize ty us < word_bits) and ?P'24 r ra rb rc\<rbrace>
 4. \<And>r ra. \<lbrace>?P'13 r ra\<rbrace> assert (cteCap ra = capability.NullCap \<and> mdbNext (cteMDBNode ra) = nullPointer \<and> mdbPrev (cteMDBNode ra) = nullPointer) \<lbrace>\<lambda>rb. cte_wp_at' (\<lambda>_. True) slot and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize ty us) and valid_arch_state' and K (ptr \<noteq> slot) and K (is_aligned ptr (getObjectSize ty us)) and K (getObjectSize ty us < word_bits) and ?P'19 r ra rb\<rbrace>
 5. \<And>r. \<lbrace>?P'8 r\<rbrace> getCTE slot \<lbrace>\<lambda>ra. K (cteCap ra = capability.NullCap \<and> mdbNext (cteMDBNode ra) = nullPointer \<and> mdbPrev (cteMDBNode ra) = nullPointer) and ?P'13 r ra\<rbrace>
 6. \<lbrace>?P'3\<rbrace> getCTE parent \<lbrace>\<lambda>r. cte_wp_at' (\<lambda>_. True) slot and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize ty us) and K (ptr \<noteq> slot) and K (getObjectSize ty us < word_bits) and K (is_aligned ptr (getObjectSize ty us)) and ?P'8 r\<rbrace>
 7. \<And>s. (pspace_aligned' and pspace_distinct' and (\<lambda>s. no_0 (ctes_of s)) and (\<lambda>s. weak_valid_dlist (ctes_of s)) and (\<lambda>s. valid_nullcaps (ctes_of s)) and cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot and pspace_no_overlap' ptr (getObjectSize ty us) and valid_arch_state' and (\<lambda>y. getObjectSize ty us < word_bits) and (\<lambda>y. cap \<noteq> capability.NullCap) and (\<lambda>y. is_aligned ptr (getObjectSize ty us) \<and> ptr \<noteq> 0 \<and> parent \<noteq> 0)) s \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) parent and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize ty us) and K (ptr \<noteq> parent) and K (getObjectSize ty us < word_bits) and K (is_aligned ptr (getObjectSize ty us)) and ?P'3) s proof (prove)
goal (8 subgoals):
 1. \<And>r ra rb rc rd re. monad_commute (?Q30 r ra rb rc rd re) (global.createObject ty ptr us d) (updateNewFreeIndex slot)
 2. \<And>r ra rb rc rd. \<lbrace>?P'30 r ra rb rc rd\<rbrace> updateMDB parent (mdbNext_update (\<lambda>_. slot)) \<lbrace>?Q30 r ra rb rc rd\<rbrace>
 3. \<And>r ra rb rc. \<lbrace>?P'24 r ra rb rc\<rbrace> updateMDB (mdbNext (cteMDBNode r)) (mdbPrev_update (\<lambda>_. slot)) \<lbrace>\<lambda>rd. (\<lambda>s. parent \<noteq> 0 \<longrightarrow> cte_wp_at' (\<lambda>_. True) parent s) and pspace_no_overlap' ptr (getObjectSize ty us) and pspace_aligned' and pspace_distinct' and valid_arch_state' and K (ptr \<noteq> parent) and K (is_aligned ptr (getObjectSize ty us)) and K (getObjectSize ty us < word_bits) and ?P'30 r ra rb rc rd\<rbrace>
 4. \<And>r ra rb. \<lbrace>?P'19 r ra rb\<rbrace> setCTE slot (CTE cap (MDB (mdbNext (cteMDBNode r)) parent True True)) \<lbrace>\<lambda>rc. (\<lambda>s. mdbNext (cteMDBNode r) \<noteq> 0 \<longrightarrow> cte_wp_at' (\<lambda>_. True) (mdbNext (cteMDBNode r)) s) and pspace_no_overlap' ptr (getObjectSize ty us) and pspace_aligned' and pspace_distinct' and valid_arch_state' and K (ptr \<noteq> mdbNext (cteMDBNode r)) and K (is_aligned ptr (getObjectSize ty us)) and K (getObjectSize ty us < word_bits) and ?P'24 r ra rb rc\<rbrace>
 5. \<And>r ra. \<lbrace>?P'13 r ra\<rbrace> assert (cteCap ra = capability.NullCap \<and> mdbNext (cteMDBNode ra) = nullPointer \<and> mdbPrev (cteMDBNode ra) = nullPointer) \<lbrace>\<lambda>rb. cte_wp_at' (\<lambda>_. True) slot and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize ty us) and valid_arch_state' and K (ptr \<noteq> slot) and K (is_aligned ptr (getObjectSize ty us)) and K (getObjectSize ty us < word_bits) and ?P'19 r ra rb\<rbrace>
 6. \<And>r. \<lbrace>?P'8 r\<rbrace> getCTE slot \<lbrace>\<lambda>ra. K (cteCap ra = capability.NullCap \<and> mdbNext (cteMDBNode ra) = nullPointer \<and> mdbPrev (cteMDBNode ra) = nullPointer) and ?P'13 r ra\<rbrace>
 7. \<lbrace>?P'3\<rbrace> getCTE parent \<lbrace>\<lambda>r. cte_wp_at' (\<lambda>_. True) slot and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize ty us) and K (ptr \<noteq> slot) and K (getObjectSize ty us < word_bits) and K (is_aligned ptr (getObjectSize ty us)) and ?P'8 r\<rbrace>
 8. \<And>s. (pspace_aligned' and pspace_distinct' and (\<lambda>s. no_0 (ctes_of s)) and (\<lambda>s. weak_valid_dlist (ctes_of s)) and (\<lambda>s. valid_nullcaps (ctes_of s)) and cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot and pspace_no_overlap' ptr (getObjectSize ty us) and valid_arch_state' and (\<lambda>y. getObjectSize ty us < word_bits) and (\<lambda>y. cap \<noteq> capability.NullCap) and (\<lambda>y. is_aligned ptr (getObjectSize ty us) \<and> ptr \<noteq> 0 \<and> parent \<noteq> 0)) s \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) parent and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize ty us) and K (ptr \<noteq> parent) and K (getObjectSize ty us < word_bits) and K (is_aligned ptr (getObjectSize ty us)) and ?P'3) s proof (prove)
goal (7 subgoals):
 1. \<And>r ra rb rc rd. \<lbrace>?P'30 r ra rb rc rd\<rbrace> updateMDB parent (mdbNext_update (\<lambda>_. slot)) \<lbrace>\<lambda>r. cte_wp_at' (\<lambda>_. True) slot and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize ty us) and valid_arch_state' and K (ptr \<noteq> slot) and K (getObjectSize ty us < word_bits) and K (is_aligned ptr (getObjectSize ty us))\<rbrace>
 2. \<And>r ra rb rc. \<lbrace>?P'24 r ra rb rc\<rbrace> updateMDB (mdbNext (cteMDBNode r)) (mdbPrev_update (\<lambda>_. slot)) \<lbrace>\<lambda>rd. (\<lambda>s. parent \<noteq> 0 \<longrightarrow> cte_wp_at' (\<lambda>_. True) parent s) and pspace_no_overlap' ptr (getObjectSize ty us) and pspace_aligned' and pspace_distinct' and valid_arch_state' and K (ptr \<noteq> parent) and K (is_aligned ptr (getObjectSize ty us)) and K (getObjectSize ty us < word_bits) and ?P'30 r ra rb rc rd\<rbrace>
 3. \<And>r ra rb. \<lbrace>?P'19 r ra rb\<rbrace> setCTE slot (CTE cap (MDB (mdbNext (cteMDBNode r)) parent True True)) \<lbrace>\<lambda>rc. (\<lambda>s. mdbNext (cteMDBNode r) \<noteq> 0 \<longrightarrow> cte_wp_at' (\<lambda>_. True) (mdbNext (cteMDBNode r)) s) and pspace_no_overlap' ptr (getObjectSize ty us) and pspace_aligned' and pspace_distinct' and valid_arch_state' and K (ptr \<noteq> mdbNext (cteMDBNode r)) and K (is_aligned ptr (getObjectSize ty us)) and K (getObjectSize ty us < word_bits) and ?P'24 r ra rb rc\<rbrace>
 4. \<And>r ra. \<lbrace>?P'13 r ra\<rbrace> assert (cteCap ra = capability.NullCap \<and> mdbNext (cteMDBNode ra) = nullPointer \<and> mdbPrev (cteMDBNode ra) = nullPointer) \<lbrace>\<lambda>rb. cte_wp_at' (\<lambda>_. True) slot and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize ty us) and valid_arch_state' and K (ptr \<noteq> slot) and K (is_aligned ptr (getObjectSize ty us)) and K (getObjectSize ty us < word_bits) and ?P'19 r ra rb\<rbrace>
 5. \<And>r. \<lbrace>?P'8 r\<rbrace> getCTE slot \<lbrace>\<lambda>ra. K (cteCap ra = capability.NullCap \<and> mdbNext (cteMDBNode ra) = nullPointer \<and> mdbPrev (cteMDBNode ra) = nullPointer) and ?P'13 r ra\<rbrace>
 6. \<lbrace>?P'3\<rbrace> getCTE parent \<lbrace>\<lambda>r. cte_wp_at' (\<lambda>_. True) slot and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize ty us) and K (ptr \<noteq> slot) and K (getObjectSize ty us < word_bits) and K (is_aligned ptr (getObjectSize ty us)) and ?P'8 r\<rbrace>
 7. \<And>s. (pspace_aligned' and pspace_distinct' and (\<lambda>s. no_0 (ctes_of s)) and (\<lambda>s. weak_valid_dlist (ctes_of s)) and (\<lambda>s. valid_nullcaps (ctes_of s)) and cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot and pspace_no_overlap' ptr (getObjectSize ty us) and valid_arch_state' and (\<lambda>y. getObjectSize ty us < word_bits) and (\<lambda>y. cap \<noteq> capability.NullCap) and (\<lambda>y. is_aligned ptr (getObjectSize ty us) \<and> ptr \<noteq> 0 \<and> parent \<noteq> 0)) s \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) parent and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize ty us) and K (ptr \<noteq> parent) and K (getObjectSize ty us < word_bits) and K (is_aligned ptr (getObjectSize ty us)) and ?P'3) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pspace_aligned' s; pspace_distinct' s; valid_arch_state' s; weak_valid_dlist (ctes_of s); parent \<noteq> 0; ptr \<noteq> 0; cap \<noteq> capability.NullCap; no_0 (ctes_of s); valid_nullcaps (ctes_of s); is_aligned ptr (getObjectSize ty us); getObjectSize ty us < word_bits; pspace_no_overlap' ptr (getObjectSize ty us) s; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s\<rbrakk> \<Longrightarrow> ptr \<noteq> parent \<and> cte_wp_at' (\<lambda>_. True) parent s \<and> (cte_wp_at' (\<lambda>_. True) parent s \<longrightarrow> ptr \<noteq> slot \<and> cte_wp_at' (\<lambda>_. True) slot s \<and> (\<exists>cte. cte_wp_at' ((=) cte) parent s \<and> (\<exists>ctea. cteCap ctea = capability.NullCap \<and> mdbNext (cteMDBNode ctea) = nullPointer \<and> mdbPrev (cteMDBNode ctea) = nullPointer \<and> cte_wp_at' ((=) ctea) slot s \<and> (cteCap ctea = capability.NullCap \<and> mdbNext (cteMDBNode ctea) = nullPointer \<and> mdbPrev (cteMDBNode ctea) = nullPointer \<longrightarrow> ptr \<noteq> parent \<and> ptr \<noteq> slot \<and> ptr \<noteq> mdbNext (cteMDBNode cte) \<and> (mdbNext (cteMDBNode cte) = 0 \<or> cte_wp_at' (\<lambda>_. True) (mdbNext (cteMDBNode cte)) s))))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea. \<lbrakk>pspace_aligned' s; pspace_distinct' s; valid_arch_state' s; weak_valid_dlist (ctes_of s); parent \<noteq> 0; ptr \<noteq> 0; cap \<noteq> capability.NullCap; no_0 (ctes_of s); valid_nullcaps (ctes_of s); is_aligned ptr (getObjectSize ty us); getObjectSize ty us < word_bits; pspace_no_overlap' ptr (getObjectSize ty us) s; ctes_of s parent = Some cte; isUntypedCap (cteCap cte); ctes_of s slot = Some ctea; cteCap ctea = capability.NullCap\<rbrakk> \<Longrightarrow> ptr \<noteq> parent \<and> ptr \<noteq> slot \<and> mdbNext (cteMDBNode ctea) = nullPointer \<and> mdbPrev (cteMDBNode ctea) = nullPointer \<and> (mdbNext (cteMDBNode ctea) = nullPointer \<and> mdbPrev (cteMDBNode ctea) = nullPointer \<longrightarrow> ptr \<noteq> parent \<and> ptr \<noteq> slot \<and> ptr \<noteq> mdbNext (cteMDBNode cte) \<and> (mdbNext (cteMDBNode cte) = 0 \<or> (\<exists>ctea. ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea))) proof (prove)
goal (4 subgoals):
 1. \<And>s cte ctea. \<lbrakk>pspace_aligned' s; pspace_distinct' s; valid_arch_state' s; weak_valid_dlist (ctes_of s); parent \<noteq> 0; ptr \<noteq> 0; cap \<noteq> capability.NullCap; no_0 (ctes_of s); valid_nullcaps (ctes_of s); is_aligned ptr (getObjectSize ty us); getObjectSize ty us < word_bits; pspace_no_overlap' ptr (getObjectSize ty us) s; ctes_of s parent = Some cte; isUntypedCap (cteCap cte); ctes_of s slot = Some ctea; cteCap ctea = capability.NullCap\<rbrakk> \<Longrightarrow> pspace_no_overlap' ptr (getObjectSize ty us) (?s213 s cte ctea)
 2. \<And>s cte ctea. \<lbrakk>pspace_aligned' s; pspace_distinct' s; valid_arch_state' s; weak_valid_dlist (ctes_of s); parent \<noteq> 0; ptr \<noteq> 0; cap \<noteq> capability.NullCap; no_0 (ctes_of s); valid_nullcaps (ctes_of s); is_aligned ptr (getObjectSize ty us); getObjectSize ty us < word_bits; pspace_no_overlap' ptr (getObjectSize ty us) s; ctes_of s parent = Some cte; isUntypedCap (cteCap cte); ctes_of s slot = Some ctea; cteCap ctea = capability.NullCap\<rbrakk> \<Longrightarrow> getObjectSize ty us < word_bits
 3. \<And>s cte ctea. \<lbrakk>pspace_aligned' s; pspace_distinct' s; valid_arch_state' s; weak_valid_dlist (ctes_of s); parent \<noteq> 0; ptr \<noteq> 0; cap \<noteq> capability.NullCap; no_0 (ctes_of s); valid_nullcaps (ctes_of s); is_aligned ptr (getObjectSize ty us); getObjectSize ty us < word_bits; pspace_no_overlap' ptr (getObjectSize ty us) s; ctes_of s parent = Some cte; isUntypedCap (cteCap cte); ctes_of s slot = Some ctea; cteCap ctea = capability.NullCap\<rbrakk> \<Longrightarrow> ctes_of (?s213 s cte ctea) slot = Some (?cte213 s cte ctea)
 4. \<And>s cte ctea. \<lbrakk>pspace_aligned' s; pspace_distinct' s; valid_arch_state' s; weak_valid_dlist (ctes_of s); parent \<noteq> 0; ptr \<noteq> 0; cap \<noteq> capability.NullCap; no_0 (ctes_of s); valid_nullcaps (ctes_of s); is_aligned ptr (getObjectSize ty us); getObjectSize ty us < word_bits; pspace_no_overlap' ptr (getObjectSize ty us) s; ctes_of s parent = Some cte; isUntypedCap (cteCap cte); ctes_of s slot = Some ctea; cteCap ctea = capability.NullCap; slot \<noteq> ptr\<rbrakk> \<Longrightarrow> ptr \<noteq> parent \<and> ptr \<noteq> slot \<and> mdbNext (cteMDBNode ctea) = nullPointer \<and> mdbPrev (cteMDBNode ctea) = nullPointer \<and> (mdbNext (cteMDBNode ctea) = nullPointer \<and> mdbPrev (cteMDBNode ctea) = nullPointer \<longrightarrow> ptr \<noteq> parent \<and> ptr \<noteq> slot \<and> ptr \<noteq> mdbNext (cteMDBNode cte) \<and> (mdbNext (cteMDBNode cte) = 0 \<or> (\<exists>ctea. ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea. \<lbrakk>pspace_aligned' s; pspace_distinct' s; valid_arch_state' s; weak_valid_dlist (ctes_of s); parent \<noteq> 0; ptr \<noteq> 0; cap \<noteq> capability.NullCap; no_0 (ctes_of s); valid_nullcaps (ctes_of s); is_aligned ptr (getObjectSize ty us); getObjectSize ty us < word_bits; pspace_no_overlap' ptr (getObjectSize ty us) s; ctes_of s parent = Some cte; isUntypedCap (cteCap cte); ctes_of s slot = Some ctea; cteCap ctea = capability.NullCap; slot \<noteq> ptr\<rbrakk> \<Longrightarrow> ptr \<noteq> parent \<and> mdbNext (cteMDBNode ctea) = nullPointer \<and> mdbPrev (cteMDBNode ctea) = nullPointer \<and> (mdbNext (cteMDBNode ctea) = nullPointer \<and> mdbPrev (cteMDBNode ctea) = nullPointer \<longrightarrow> ptr \<noteq> parent \<and> ptr \<noteq> mdbNext (cteMDBNode cte) \<and> (mdbNext (cteMDBNode cte) = 0 \<or> (\<exists>ctea. ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea))) proof (prove)
goal (4 subgoals):
 1. \<And>s cte ctea. \<lbrakk>pspace_aligned' s; pspace_distinct' s; valid_arch_state' s; weak_valid_dlist (ctes_of s); parent \<noteq> 0; ptr \<noteq> 0; cap \<noteq> capability.NullCap; no_0 (ctes_of s); valid_nullcaps (ctes_of s); is_aligned ptr (getObjectSize ty us); getObjectSize ty us < word_bits; pspace_no_overlap' ptr (getObjectSize ty us) s; ctes_of s parent = Some cte; isUntypedCap (cteCap cte); ctes_of s slot = Some ctea; cteCap ctea = capability.NullCap; slot \<noteq> ptr\<rbrakk> \<Longrightarrow> pspace_no_overlap' ptr (getObjectSize ty us) (?s216 s cte ctea)
 2. \<And>s cte ctea. \<lbrakk>pspace_aligned' s; pspace_distinct' s; valid_arch_state' s; weak_valid_dlist (ctes_of s); parent \<noteq> 0; ptr \<noteq> 0; cap \<noteq> capability.NullCap; no_0 (ctes_of s); valid_nullcaps (ctes_of s); is_aligned ptr (getObjectSize ty us); getObjectSize ty us < word_bits; pspace_no_overlap' ptr (getObjectSize ty us) s; ctes_of s parent = Some cte; isUntypedCap (cteCap cte); ctes_of s slot = Some ctea; cteCap ctea = capability.NullCap; slot \<noteq> ptr\<rbrakk> \<Longrightarrow> getObjectSize ty us < word_bits
 3. \<And>s cte ctea. \<lbrakk>pspace_aligned' s; pspace_distinct' s; valid_arch_state' s; weak_valid_dlist (ctes_of s); parent \<noteq> 0; ptr \<noteq> 0; cap \<noteq> capability.NullCap; no_0 (ctes_of s); valid_nullcaps (ctes_of s); is_aligned ptr (getObjectSize ty us); getObjectSize ty us < word_bits; pspace_no_overlap' ptr (getObjectSize ty us) s; ctes_of s parent = Some cte; isUntypedCap (cteCap cte); ctes_of s slot = Some ctea; cteCap ctea = capability.NullCap; slot \<noteq> ptr\<rbrakk> \<Longrightarrow> ctes_of (?s216 s cte ctea) parent = Some (?cte216 s cte ctea)
 4. \<And>s cte ctea. \<lbrakk>pspace_aligned' s; pspace_distinct' s; valid_arch_state' s; weak_valid_dlist (ctes_of s); parent \<noteq> 0; ptr \<noteq> 0; cap \<noteq> capability.NullCap; no_0 (ctes_of s); valid_nullcaps (ctes_of s); is_aligned ptr (getObjectSize ty us); getObjectSize ty us < word_bits; pspace_no_overlap' ptr (getObjectSize ty us) s; ctes_of s parent = Some cte; isUntypedCap (cteCap cte); ctes_of s slot = Some ctea; cteCap ctea = capability.NullCap; slot \<noteq> ptr; parent \<noteq> ptr\<rbrakk> \<Longrightarrow> ptr \<noteq> parent \<and> mdbNext (cteMDBNode ctea) = nullPointer \<and> mdbPrev (cteMDBNode ctea) = nullPointer \<and> (mdbNext (cteMDBNode ctea) = nullPointer \<and> mdbPrev (cteMDBNode ctea) = nullPointer \<longrightarrow> ptr \<noteq> parent \<and> ptr \<noteq> mdbNext (cteMDBNode cte) \<and> (mdbNext (cteMDBNode cte) = 0 \<or> (\<exists>ctea. ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea. \<lbrakk>pspace_aligned' s; pspace_distinct' s; valid_arch_state' s; weak_valid_dlist (ctes_of s); parent \<noteq> 0; ptr \<noteq> 0; cap \<noteq> capability.NullCap; no_0 (ctes_of s); valid_nullcaps (ctes_of s); is_aligned ptr (getObjectSize ty us); getObjectSize ty us < word_bits; pspace_no_overlap' ptr (getObjectSize ty us) s; ctes_of s parent = Some cte; isUntypedCap (cteCap cte); ctes_of s slot = Some ctea; cteCap ctea = capability.NullCap; slot \<noteq> ptr; parent \<noteq> ptr\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode ctea) = nullPointer \<and> mdbPrev (cteMDBNode ctea) = nullPointer \<and> (mdbNext (cteMDBNode ctea) = nullPointer \<and> mdbPrev (cteMDBNode ctea) = nullPointer \<longrightarrow> ptr \<noteq> mdbNext (cteMDBNode cte) \<and> (mdbNext (cteMDBNode cte) = 0 \<or> (\<exists>ctea. ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte x2. \<lbrakk>pspace_aligned' s; pspace_distinct' s; valid_arch_state' s; weak_valid_dlist (ctes_of s); parent \<noteq> 0; ptr \<noteq> 0; cap \<noteq> capability.NullCap; no_0 (ctes_of s); valid_nullcaps (ctes_of s); is_aligned ptr (getObjectSize ty us); getObjectSize ty us < word_bits; pspace_no_overlap' ptr (getObjectSize ty us) s; ctes_of s parent = Some cte; isUntypedCap (cteCap cte); ctes_of s slot = Some (CTE capability.NullCap x2); slot \<noteq> ptr; parent \<noteq> ptr\<rbrakk> \<Longrightarrow> mdbNext x2 = nullPointer \<and> mdbPrev x2 = nullPointer \<and> (mdbNext x2 = nullPointer \<and> mdbPrev x2 = nullPointer \<longrightarrow> ptr \<noteq> mdbNext (cteMDBNode cte) \<and> (mdbNext (cteMDBNode cte) = 0 \<or> (\<exists>ctea. ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea))) proof (prove)
goal (2 subgoals):
 1. \<And>s cte x2. \<lbrakk>pspace_aligned' s; pspace_distinct' s; valid_arch_state' s; weak_valid_dlist (ctes_of s); parent \<noteq> 0; ptr \<noteq> 0; cap \<noteq> capability.NullCap; no_0 (ctes_of s); valid_nullcaps (ctes_of s); is_aligned ptr (getObjectSize ty us); getObjectSize ty us < word_bits; pspace_no_overlap' ptr (getObjectSize ty us) s; ctes_of s parent = Some cte; isUntypedCap (cteCap cte); ctes_of s slot = Some (CTE capability.NullCap x2); slot \<noteq> ptr; parent \<noteq> ptr\<rbrakk> \<Longrightarrow> valid_nullcaps (ctes_of s)
 2. \<And>s cte x2. \<lbrakk>pspace_aligned' s; pspace_distinct' s; valid_arch_state' s; weak_valid_dlist (ctes_of s); parent \<noteq> 0; ptr \<noteq> 0; cap \<noteq> capability.NullCap; no_0 (ctes_of s); valid_nullcaps (ctes_of s); is_aligned ptr (getObjectSize ty us); getObjectSize ty us < word_bits; pspace_no_overlap' ptr (getObjectSize ty us) s; ctes_of s parent = Some cte; isUntypedCap (cteCap cte); ctes_of s slot = Some (CTE capability.NullCap x2); slot \<noteq> ptr; parent \<noteq> ptr; x2 = nullMDBNode\<rbrakk> \<Longrightarrow> mdbNext x2 = nullPointer \<and> mdbPrev x2 = nullPointer \<and> (mdbNext x2 = nullPointer \<and> mdbPrev x2 = nullPointer \<longrightarrow> ptr \<noteq> mdbNext (cteMDBNode cte) \<and> (mdbNext (cteMDBNode cte) = 0 \<or> (\<exists>ctea. ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte x2. \<lbrakk>pspace_aligned' s; pspace_distinct' s; valid_arch_state' s; weak_valid_dlist (ctes_of s); parent \<noteq> 0; ptr \<noteq> 0; cap \<noteq> capability.NullCap; no_0 (ctes_of s); valid_nullcaps (ctes_of s); is_aligned ptr (getObjectSize ty us); getObjectSize ty us < word_bits; pspace_no_overlap' ptr (getObjectSize ty us) s; ctes_of s parent = Some cte; isUntypedCap (cteCap cte); ctes_of s slot = Some (CTE capability.NullCap nullMDBNode); slot \<noteq> ptr; parent \<noteq> ptr; x2 = nullMDBNode\<rbrakk> \<Longrightarrow> ptr \<noteq> mdbNext (cteMDBNode cte) \<and> (mdbNext (cteMDBNode cte) = 0 \<or> (\<exists>ctea. ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea)) proof (prove)
goal (2 subgoals):
 1. \<And>s cte x2. \<lbrakk>pspace_aligned' s; pspace_distinct' s; valid_arch_state' s; weak_valid_dlist (ctes_of s); parent \<noteq> 0; ptr \<noteq> 0; cap \<noteq> capability.NullCap; no_0 (ctes_of s); valid_nullcaps (ctes_of s); is_aligned ptr (getObjectSize ty us); getObjectSize ty us < word_bits; pspace_no_overlap' ptr (getObjectSize ty us) s; ctes_of s parent = Some cte; isUntypedCap (cteCap cte); ctes_of s slot = Some (CTE capability.NullCap nullMDBNode); slot \<noteq> ptr; parent \<noteq> ptr; x2 = nullMDBNode; mdbNext (cteMDBNode cte) = 0 \<or> (\<exists>ctea. ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea)\<rbrakk> \<Longrightarrow> ptr \<noteq> mdbNext (cteMDBNode cte) \<and> (mdbNext (cteMDBNode cte) = 0 \<or> (\<exists>ctea. ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea))
 2. \<And>s cte x2. \<lbrakk>pspace_aligned' s; pspace_distinct' s; valid_arch_state' s; weak_valid_dlist (ctes_of s); parent \<noteq> 0; ptr \<noteq> 0; cap \<noteq> capability.NullCap; no_0 (ctes_of s); valid_nullcaps (ctes_of s); is_aligned ptr (getObjectSize ty us); getObjectSize ty us < word_bits; pspace_no_overlap' ptr (getObjectSize ty us) s; ctes_of s parent = Some cte; isUntypedCap (cteCap cte); ctes_of s slot = Some (CTE capability.NullCap nullMDBNode); slot \<noteq> ptr; parent \<noteq> ptr; x2 = nullMDBNode\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode cte) = 0 \<or> (\<exists>ctea. ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea) proof (prove)
goal (3 subgoals):
 1. \<And>s cte x2. \<lbrakk>pspace_aligned' s; pspace_distinct' s; valid_arch_state' s; weak_valid_dlist (ctes_of s); parent \<noteq> 0; ptr \<noteq> 0; cap \<noteq> capability.NullCap; no_0 (ctes_of s); valid_nullcaps (ctes_of s); is_aligned ptr (getObjectSize ty us); getObjectSize ty us < word_bits; pspace_no_overlap' ptr (getObjectSize ty us) s; ctes_of s parent = Some cte; isUntypedCap (cteCap cte); ctes_of s slot = Some (CTE capability.NullCap nullMDBNode); slot \<noteq> ptr; parent \<noteq> ptr; x2 = nullMDBNode; mdbNext (cteMDBNode cte) = 0\<rbrakk> \<Longrightarrow> ptr \<noteq> mdbNext (cteMDBNode cte) \<and> (mdbNext (cteMDBNode cte) = 0 \<or> (\<exists>ctea. ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea))
 2. \<And>s cte x2. \<lbrakk>pspace_aligned' s; pspace_distinct' s; valid_arch_state' s; weak_valid_dlist (ctes_of s); parent \<noteq> 0; ptr \<noteq> 0; cap \<noteq> capability.NullCap; no_0 (ctes_of s); valid_nullcaps (ctes_of s); is_aligned ptr (getObjectSize ty us); getObjectSize ty us < word_bits; pspace_no_overlap' ptr (getObjectSize ty us) s; ctes_of s parent = Some cte; isUntypedCap (cteCap cte); ctes_of s slot = Some (CTE capability.NullCap nullMDBNode); slot \<noteq> ptr; parent \<noteq> ptr; x2 = nullMDBNode; \<exists>ctea. ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea\<rbrakk> \<Longrightarrow> ptr \<noteq> mdbNext (cteMDBNode cte) \<and> (mdbNext (cteMDBNode cte) = 0 \<or> (\<exists>ctea. ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea))
 3. \<And>s cte x2. \<lbrakk>pspace_aligned' s; pspace_distinct' s; valid_arch_state' s; weak_valid_dlist (ctes_of s); parent \<noteq> 0; ptr \<noteq> 0; cap \<noteq> capability.NullCap; no_0 (ctes_of s); valid_nullcaps (ctes_of s); is_aligned ptr (getObjectSize ty us); getObjectSize ty us < word_bits; pspace_no_overlap' ptr (getObjectSize ty us) s; ctes_of s parent = Some cte; isUntypedCap (cteCap cte); ctes_of s slot = Some (CTE capability.NullCap nullMDBNode); slot \<noteq> ptr; parent \<noteq> ptr; x2 = nullMDBNode\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode cte) = 0 \<or> (\<exists>ctea. ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea) proof (prove)
goal (2 subgoals):
 1. \<And>s cte ctea. \<lbrakk>pspace_aligned' s; pspace_distinct' s; valid_arch_state' s; weak_valid_dlist (ctes_of s); parent \<noteq> 0; mdbNext (cteMDBNode cte) \<noteq> 0; cap \<noteq> capability.NullCap; no_0 (ctes_of s); valid_nullcaps (ctes_of s); is_aligned (mdbNext (cteMDBNode cte)) (getObjectSize ty us); getObjectSize ty us < word_bits; pspace_no_overlap' (mdbNext (cteMDBNode cte)) (getObjectSize ty us) s; ctes_of s parent = Some cte; isUntypedCap (cteCap cte); ctes_of s slot = Some (CTE capability.NullCap nullMDBNode); slot \<noteq> mdbNext (cteMDBNode cte); parent \<noteq> mdbNext (cteMDBNode cte); ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea; ptr = mdbNext (cteMDBNode cte)\<rbrakk> \<Longrightarrow> False
 2. \<And>s cte x2. \<lbrakk>pspace_aligned' s; pspace_distinct' s; valid_arch_state' s; weak_valid_dlist (ctes_of s); parent \<noteq> 0; ptr \<noteq> 0; cap \<noteq> capability.NullCap; no_0 (ctes_of s); valid_nullcaps (ctes_of s); is_aligned ptr (getObjectSize ty us); getObjectSize ty us < word_bits; pspace_no_overlap' ptr (getObjectSize ty us) s; ctes_of s parent = Some cte; isUntypedCap (cteCap cte); ctes_of s slot = Some (CTE capability.NullCap nullMDBNode); slot \<noteq> ptr; parent \<noteq> ptr; x2 = nullMDBNode\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode cte) = 0 \<or> (\<exists>ctea. ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea) proof (prove)
goal (5 subgoals):
 1. \<And>s cte ctea. \<lbrakk>pspace_aligned' s; pspace_distinct' s; valid_arch_state' s; weak_valid_dlist (ctes_of s); parent \<noteq> 0; mdbNext (cteMDBNode cte) \<noteq> 0; cap \<noteq> capability.NullCap; no_0 (ctes_of s); valid_nullcaps (ctes_of s); is_aligned (mdbNext (cteMDBNode cte)) (getObjectSize ty us); getObjectSize ty us < word_bits; pspace_no_overlap' (mdbNext (cteMDBNode cte)) (getObjectSize ty us) s; ctes_of s parent = Some cte; isUntypedCap (cteCap cte); ctes_of s slot = Some (CTE capability.NullCap nullMDBNode); slot \<noteq> mdbNext (cteMDBNode cte); parent \<noteq> mdbNext (cteMDBNode cte); ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea; ptr = mdbNext (cteMDBNode cte)\<rbrakk> \<Longrightarrow> pspace_no_overlap' (mdbNext (cteMDBNode cte)) (getObjectSize ty us) (?s233 s cte ctea)
 2. \<And>s cte ctea. \<lbrakk>pspace_aligned' s; pspace_distinct' s; valid_arch_state' s; weak_valid_dlist (ctes_of s); parent \<noteq> 0; mdbNext (cteMDBNode cte) \<noteq> 0; cap \<noteq> capability.NullCap; no_0 (ctes_of s); valid_nullcaps (ctes_of s); is_aligned (mdbNext (cteMDBNode cte)) (getObjectSize ty us); getObjectSize ty us < word_bits; pspace_no_overlap' (mdbNext (cteMDBNode cte)) (getObjectSize ty us) s; ctes_of s parent = Some cte; isUntypedCap (cteCap cte); ctes_of s slot = Some (CTE capability.NullCap nullMDBNode); slot \<noteq> mdbNext (cteMDBNode cte); parent \<noteq> mdbNext (cteMDBNode cte); ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea; ptr = mdbNext (cteMDBNode cte)\<rbrakk> \<Longrightarrow> getObjectSize ty us < word_bits
 3. \<And>s cte ctea. \<lbrakk>pspace_aligned' s; pspace_distinct' s; valid_arch_state' s; weak_valid_dlist (ctes_of s); parent \<noteq> 0; mdbNext (cteMDBNode cte) \<noteq> 0; cap \<noteq> capability.NullCap; no_0 (ctes_of s); valid_nullcaps (ctes_of s); is_aligned (mdbNext (cteMDBNode cte)) (getObjectSize ty us); getObjectSize ty us < word_bits; pspace_no_overlap' (mdbNext (cteMDBNode cte)) (getObjectSize ty us) s; ctes_of s parent = Some cte; isUntypedCap (cteCap cte); ctes_of s slot = Some (CTE capability.NullCap nullMDBNode); slot \<noteq> mdbNext (cteMDBNode cte); parent \<noteq> mdbNext (cteMDBNode cte); ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea; ptr = mdbNext (cteMDBNode cte)\<rbrakk> \<Longrightarrow> ctes_of (?s233 s cte ctea) (mdbNext (cteMDBNode cte)) = Some (?cte233 s cte ctea)
 4. \<And>s cte ctea. \<lbrakk>pspace_aligned' s; pspace_distinct' s; valid_arch_state' s; weak_valid_dlist (ctes_of s); parent \<noteq> 0; mdbNext (cteMDBNode cte) \<noteq> 0; cap \<noteq> capability.NullCap; no_0 (ctes_of s); valid_nullcaps (ctes_of s); is_aligned (mdbNext (cteMDBNode cte)) (getObjectSize ty us); getObjectSize ty us < word_bits; pspace_no_overlap' (mdbNext (cteMDBNode cte)) (getObjectSize ty us) s; ctes_of s parent = Some cte; isUntypedCap (cteCap cte); ctes_of s slot = Some (CTE capability.NullCap nullMDBNode); slot \<noteq> mdbNext (cteMDBNode cte); parent \<noteq> mdbNext (cteMDBNode cte); ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea; ptr = mdbNext (cteMDBNode cte); mdbNext (cteMDBNode cte) \<noteq> mdbNext (cteMDBNode cte)\<rbrakk> \<Longrightarrow> False
 5. \<And>s cte x2. \<lbrakk>pspace_aligned' s; pspace_distinct' s; valid_arch_state' s; weak_valid_dlist (ctes_of s); parent \<noteq> 0; ptr \<noteq> 0; cap \<noteq> capability.NullCap; no_0 (ctes_of s); valid_nullcaps (ctes_of s); is_aligned ptr (getObjectSize ty us); getObjectSize ty us < word_bits; pspace_no_overlap' ptr (getObjectSize ty us) s; ctes_of s parent = Some cte; isUntypedCap (cteCap cte); ctes_of s slot = Some (CTE capability.NullCap nullMDBNode); slot \<noteq> ptr; parent \<noteq> ptr; x2 = nullMDBNode\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode cte) = 0 \<or> (\<exists>ctea. ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea) proof (prove)
goal (1 subgoal):
 1. \<And>s cte x2. \<lbrakk>pspace_aligned' s; pspace_distinct' s; valid_arch_state' s; weak_valid_dlist (ctes_of s); parent \<noteq> 0; ptr \<noteq> 0; cap \<noteq> capability.NullCap; no_0 (ctes_of s); valid_nullcaps (ctes_of s); is_aligned ptr (getObjectSize ty us); getObjectSize ty us < word_bits; pspace_no_overlap' ptr (getObjectSize ty us) s; ctes_of s parent = Some cte; isUntypedCap (cteCap cte); ctes_of s slot = Some (CTE capability.NullCap nullMDBNode); slot \<noteq> ptr; parent \<noteq> ptr; x2 = nullMDBNode\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode cte) = 0 \<or> (\<exists>ctea. ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea) proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>pspace_aligned' s; pspace_distinct' s; valid_arch_state' s; \<forall>p cte. ctes_of s p = Some cte \<longrightarrow> (let next = mdbNext (cteMDBNode cte) in next \<noteq> 0 \<longrightarrow> (\<exists>cte'. ctes_of s next = Some cte' \<and> cteCap cte' \<noteq> capability.NullCap)); parent \<noteq> 0; ptr \<noteq> 0; cap \<noteq> capability.NullCap; no_0 (ctes_of s); valid_nullcaps (ctes_of s); is_aligned ptr (getObjectSize ty us); getObjectSize ty us < word_bits; pspace_no_overlap' ptr (getObjectSize ty us) s; ctes_of s parent = Some cte; isUntypedCap (cteCap cte); ctes_of s slot = Some (CTE capability.NullCap nullMDBNode); slot \<noteq> ptr; parent \<noteq> ptr; ctes_of s (mdbNext (cteMDBNode cte)) = None\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode cte) = 0 proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>pspace_aligned' s; pspace_distinct' s; valid_arch_state' s; parent \<noteq> 0; ptr \<noteq> 0; cap \<noteq> capability.NullCap; no_0 (ctes_of s); valid_nullcaps (ctes_of s); is_aligned ptr (getObjectSize ty us); getObjectSize ty us < word_bits; pspace_no_overlap' ptr (getObjectSize ty us) s; ctes_of s parent = Some cte; isUntypedCap (cteCap cte); ctes_of s slot = Some (CTE capability.NullCap nullMDBNode); slot \<noteq> ptr; parent \<noteq> ptr; ctes_of s (mdbNext (cteMDBNode cte)) = None; \<forall>cte. ctes_of s parent = Some cte \<longrightarrow> (let next = mdbNext (cteMDBNode cte) in next \<noteq> 0 \<longrightarrow> (\<exists>cte'. ctes_of s next = Some cte' \<and> cteCap cte' \<noteq> capability.NullCap))\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode cte) = 0 proof (prove)
goal:
No subgoals!