theory CSpace1_R

lemma setUntypedCapAsFull_corres:
  "\<lbrakk>cap_relation c c'; src' = cte_map src;
    cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap;
    cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer \<and>
    mdbNext (cteMDBNode rv') = nullPointer\<rbrakk>
   \<Longrightarrow> corres dc (cte_wp_at ((=) src_cap) src and valid_objs and
                  pspace_aligned and pspace_distinct)
                 (cte_wp_at' ((=) srcCTE) (cte_map src) and
                  pspace_aligned' and pspace_distinct')
                 (set_untyped_cap_as_full src_cap c src)
                 (setUntypedCapAsFull (cteCap srcCTE) c' (cte_map src))" apply (clarsimp simp:set_untyped_cap_as_full_def setUntypedCapAsFull_def
    split:if_splits) apply (intro conjI impI) apply (clarsimp simp del:capFreeIndex_update.simps simp:updateCap_def) apply (rule corres_guard_imp) apply (rule corres_symb_exec_r) apply (rule_tac F="cte = srcCTE" in corres_gen_asm2) apply (simp) apply (rule setCTE_UntypedCap_corres) apply simp+ apply (clarsimp simp:free_index_update_def isCap_simps is_cap_simps) apply (subst identity_eq) apply (wp getCTE_sp getCTE_get)+ apply (clarsimp simp:cte_wp_at_ctes_of)+ apply (clarsimp simp:is_cap_simps isCap_simps)+ apply (case_tac c,simp_all) apply (case_tac src_cap,simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer \<and> mdbNext (cteMDBNode rv') = nullPointer\<rbrakk> \<Longrightarrow> corres dc (cte_wp_at ((=) src_cap) src and valid_objs and pspace_aligned and pspace_distinct) (cte_wp_at' ((=) srcCTE) (cte_map src) and pspace_aligned' and pspace_distinct') (set_untyped_cap_as_full src_cap c src) (setUntypedCapAsFull (cteCap srcCTE) c' (cte_map src)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer\<rbrakk> \<Longrightarrow> (is_untyped_cap src_cap \<and> is_untyped_cap c \<and> obj_ref_of src_cap = obj_ref_of c \<and> cap_bits_untyped src_cap = cap_bits_untyped c \<longrightarrow> (isUntypedCap (cteCap srcCTE) \<and> isUntypedCap c' \<and> capPtr (cteCap srcCTE) = capPtr c' \<and> capBlockSize (cteCap srcCTE) = capBlockSize c' \<longrightarrow> corres dc (cte_wp_at ((=) src_cap) src and valid_objs and pspace_aligned and pspace_distinct) (cte_wp_at' ((=) srcCTE) (cte_map src) and pspace_aligned' and pspace_distinct') (set_cap (max_free_index_update src_cap) src) (updateCap (cte_map src) (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c')) (cteCap srcCTE)))) \<and> ((capPtr (cteCap srcCTE) = capPtr c' \<longrightarrow> isUntypedCap c' \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize c') \<longrightarrow> corres dc (cte_wp_at ((=) src_cap) src and valid_objs and pspace_aligned and pspace_distinct) (cte_wp_at' ((=) srcCTE) (cte_map src) and pspace_aligned' and pspace_distinct') (set_cap (max_free_index_update src_cap) src) (return ()))) \<and> ((obj_ref_of src_cap = obj_ref_of c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped c) \<longrightarrow> isUntypedCap (cteCap srcCTE) \<and> isUntypedCap c' \<and> capPtr (cteCap srcCTE) = capPtr c' \<and> capBlockSize (cteCap srcCTE) = capBlockSize c' \<longrightarrow> corres dc (cte_wp_at ((=) src_cap) src and valid_objs and pspace_aligned and pspace_distinct) (cte_wp_at' ((=) srcCTE) (cte_map src) and pspace_aligned' and pspace_distinct') (return ()) (updateCap (cte_map src) (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c')) (cteCap srcCTE)))) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap \<and> is_untyped_cap c \<and> obj_ref_of src_cap = obj_ref_of c \<and> cap_bits_untyped src_cap = cap_bits_untyped c; isUntypedCap (cteCap srcCTE) \<and> isUntypedCap c' \<and> capPtr (cteCap srcCTE) = capPtr c' \<and> capBlockSize (cteCap srcCTE) = capBlockSize c'\<rbrakk> \<Longrightarrow> corres dc (cte_wp_at ((=) src_cap) src and valid_objs and pspace_aligned and pspace_distinct) (cte_wp_at' ((=) srcCTE) (cte_map src) and pspace_aligned' and pspace_distinct') (set_cap (max_free_index_update src_cap) src) (updateCap (cte_map src) (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c')) (cteCap srcCTE)))
 2. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap \<and> is_untyped_cap c \<and> obj_ref_of src_cap = obj_ref_of c \<and> cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c' \<longrightarrow> isUntypedCap c' \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize c'\<rbrakk> \<Longrightarrow> corres dc (cte_wp_at ((=) src_cap) src and valid_objs and pspace_aligned and pspace_distinct) (cte_wp_at' ((=) srcCTE) (cte_map src) and pspace_aligned' and pspace_distinct') (set_cap (max_free_index_update src_cap) src) (return ())
 3. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; obj_ref_of src_cap = obj_ref_of c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped c; isUntypedCap (cteCap srcCTE) \<and> isUntypedCap c' \<and> capPtr (cteCap srcCTE) = capPtr c' \<and> capBlockSize (cteCap srcCTE) = capBlockSize c'\<rbrakk> \<Longrightarrow> corres dc (cte_wp_at ((=) src_cap) src and valid_objs and pspace_aligned and pspace_distinct) (cte_wp_at' ((=) srcCTE) (cte_map src) and pspace_aligned' and pspace_distinct') (return ()) (updateCap (cte_map src) (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c')) (cteCap srcCTE))) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap; isUntypedCap (cteCap srcCTE); is_untyped_cap c; isUntypedCap c'; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c'; capBlockSize (cteCap srcCTE) = capBlockSize c'\<rbrakk> \<Longrightarrow> corres dc (cte_wp_at ((=) src_cap) src and valid_objs and pspace_aligned and pspace_distinct) (cte_wp_at' ((=) srcCTE) (cte_map src) and pspace_aligned' and pspace_distinct') (set_cap (max_free_index_update src_cap) src) (do cte <- getCTE (cte_map src);
setCTE (cte_map src) (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c')) (cteCap srcCTE)) cte)
od)
 2. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap \<and> is_untyped_cap c \<and> obj_ref_of src_cap = obj_ref_of c \<and> cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c' \<longrightarrow> isUntypedCap c' \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize c'\<rbrakk> \<Longrightarrow> corres dc (cte_wp_at ((=) src_cap) src and valid_objs and pspace_aligned and pspace_distinct) (cte_wp_at' ((=) srcCTE) (cte_map src) and pspace_aligned' and pspace_distinct') (set_cap (max_free_index_update src_cap) src) (return ())
 3. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; obj_ref_of src_cap = obj_ref_of c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped c; isUntypedCap (cteCap srcCTE) \<and> isUntypedCap c' \<and> capPtr (cteCap srcCTE) = capPtr c' \<and> capBlockSize (cteCap srcCTE) = capBlockSize c'\<rbrakk> \<Longrightarrow> corres dc (cte_wp_at ((=) src_cap) src and valid_objs and pspace_aligned and pspace_distinct) (cte_wp_at' ((=) srcCTE) (cte_map src) and pspace_aligned' and pspace_distinct') (return ()) (updateCap (cte_map src) (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c')) (cteCap srcCTE))) proof (prove)
goal (5 subgoals):
 1. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap; isUntypedCap (cteCap srcCTE); is_untyped_cap c; isUntypedCap c'; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c'; capBlockSize (cteCap srcCTE) = capBlockSize c'\<rbrakk> \<Longrightarrow> corres dc ?Q30 ?Q'30 (set_cap (max_free_index_update src_cap) src) (do cte <- getCTE (cte_map src);
setCTE (cte_map src) (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c')) (cteCap srcCTE)) cte)
od)
 2. \<And>s. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap; isUntypedCap (cteCap srcCTE); is_untyped_cap c; isUntypedCap c'; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c'; capBlockSize (cteCap srcCTE) = capBlockSize c'; (cte_wp_at ((=) src_cap) src and valid_objs and pspace_aligned and pspace_distinct) s\<rbrakk> \<Longrightarrow> ?Q30 s
 3. \<And>s. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap; isUntypedCap (cteCap srcCTE); is_untyped_cap c; isUntypedCap c'; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c'; capBlockSize (cteCap srcCTE) = capBlockSize c'; (cte_wp_at' ((=) srcCTE) (cte_map src) and pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> ?Q'30 s
 4. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap \<and> is_untyped_cap c \<and> obj_ref_of src_cap = obj_ref_of c \<and> cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c' \<longrightarrow> isUntypedCap c' \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize c'\<rbrakk> \<Longrightarrow> corres dc (cte_wp_at ((=) src_cap) src and valid_objs and pspace_aligned and pspace_distinct) (cte_wp_at' ((=) srcCTE) (cte_map src) and pspace_aligned' and pspace_distinct') (set_cap (max_free_index_update src_cap) src) (return ())
 5. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; obj_ref_of src_cap = obj_ref_of c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped c; isUntypedCap (cteCap srcCTE) \<and> isUntypedCap c' \<and> capPtr (cteCap srcCTE) = capPtr c' \<and> capBlockSize (cteCap srcCTE) = capBlockSize c'\<rbrakk> \<Longrightarrow> corres dc (cte_wp_at ((=) src_cap) src and valid_objs and pspace_aligned and pspace_distinct) (cte_wp_at' ((=) srcCTE) (cte_map src) and pspace_aligned' and pspace_distinct') (return ()) (updateCap (cte_map src) (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c')) (cteCap srcCTE))) proof (prove)
goal (8 subgoals):
 1. \<And>cte. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap; isUntypedCap (cteCap srcCTE); is_untyped_cap c; isUntypedCap c'; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c'; capBlockSize (cteCap srcCTE) = capBlockSize c'\<rbrakk> \<Longrightarrow> corres dc ?Q30 (?Q'34 cte) (set_cap (max_free_index_update src_cap) src) (setCTE (cte_map src) (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c')) (cteCap srcCTE)) cte))
 2. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap; isUntypedCap (cteCap srcCTE); is_untyped_cap c; isUntypedCap c'; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c'; capBlockSize (cteCap srcCTE) = capBlockSize c'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'30\<rbrace> getCTE (cte_map src) \<lbrace>?Q'34\<rbrace>
 3. \<And>s. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap; isUntypedCap (cteCap srcCTE); is_untyped_cap c; isUntypedCap c'; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c'; capBlockSize (cteCap srcCTE) = capBlockSize c'; ?Q'30 s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> getCTE (cte_map src) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap; isUntypedCap (cteCap srcCTE); is_untyped_cap c; isUntypedCap c'; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c'; capBlockSize (cteCap srcCTE) = capBlockSize c'; True\<rbrakk> \<Longrightarrow> no_fail ?Q'30 (getCTE (cte_map src))
 5. \<And>s. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap; isUntypedCap (cteCap srcCTE); is_untyped_cap c; isUntypedCap c'; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c'; capBlockSize (cteCap srcCTE) = capBlockSize c'; (cte_wp_at ((=) src_cap) src and valid_objs and pspace_aligned and pspace_distinct) s\<rbrakk> \<Longrightarrow> ?Q30 s
 6. \<And>s. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap; isUntypedCap (cteCap srcCTE); is_untyped_cap c; isUntypedCap c'; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c'; capBlockSize (cteCap srcCTE) = capBlockSize c'; (cte_wp_at' ((=) srcCTE) (cte_map src) and pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> ?Q'30 s
 7. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap \<and> is_untyped_cap c \<and> obj_ref_of src_cap = obj_ref_of c \<and> cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c' \<longrightarrow> isUntypedCap c' \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize c'\<rbrakk> \<Longrightarrow> corres dc (cte_wp_at ((=) src_cap) src and valid_objs and pspace_aligned and pspace_distinct) (cte_wp_at' ((=) srcCTE) (cte_map src) and pspace_aligned' and pspace_distinct') (set_cap (max_free_index_update src_cap) src) (return ())
 8. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; obj_ref_of src_cap = obj_ref_of c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped c; isUntypedCap (cteCap srcCTE) \<and> isUntypedCap c' \<and> capPtr (cteCap srcCTE) = capPtr c' \<and> capBlockSize (cteCap srcCTE) = capBlockSize c'\<rbrakk> \<Longrightarrow> corres dc (cte_wp_at ((=) src_cap) src and valid_objs and pspace_aligned and pspace_distinct) (cte_wp_at' ((=) srcCTE) (cte_map src) and pspace_aligned' and pspace_distinct') (return ()) (updateCap (cte_map src) (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c')) (cteCap srcCTE))) proof (prove)
goal (8 subgoals):
 1. \<And>cte. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap; isUntypedCap (cteCap srcCTE); is_untyped_cap c; isUntypedCap c'; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c'; capBlockSize (cteCap srcCTE) = capBlockSize c'; cte = srcCTE\<rbrakk> \<Longrightarrow> corres dc ?Q30 (?P'39 cte) (set_cap (max_free_index_update src_cap) src) (setCTE (cte_map src) (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c')) (cteCap srcCTE)) cte))
 2. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap; isUntypedCap (cteCap srcCTE); is_untyped_cap c; isUntypedCap c'; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c'; capBlockSize (cteCap srcCTE) = capBlockSize c'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'30\<rbrace> getCTE (cte_map src) \<lbrace>\<lambda>cte. ?P'39 cte and (\<lambda>s. cte = srcCTE)\<rbrace>
 3. \<And>s. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap; isUntypedCap (cteCap srcCTE); is_untyped_cap c; isUntypedCap c'; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c'; capBlockSize (cteCap srcCTE) = capBlockSize c'; ?Q'30 s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> getCTE (cte_map src) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap; isUntypedCap (cteCap srcCTE); is_untyped_cap c; isUntypedCap c'; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c'; capBlockSize (cteCap srcCTE) = capBlockSize c'; True\<rbrakk> \<Longrightarrow> no_fail ?Q'30 (getCTE (cte_map src))
 5. \<And>s. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap; isUntypedCap (cteCap srcCTE); is_untyped_cap c; isUntypedCap c'; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c'; capBlockSize (cteCap srcCTE) = capBlockSize c'; (cte_wp_at ((=) src_cap) src and valid_objs and pspace_aligned and pspace_distinct) s\<rbrakk> \<Longrightarrow> ?Q30 s
 6. \<And>s. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap; isUntypedCap (cteCap srcCTE); is_untyped_cap c; isUntypedCap c'; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c'; capBlockSize (cteCap srcCTE) = capBlockSize c'; (cte_wp_at' ((=) srcCTE) (cte_map src) and pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> ?Q'30 s
 7. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap \<and> is_untyped_cap c \<and> obj_ref_of src_cap = obj_ref_of c \<and> cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c' \<longrightarrow> isUntypedCap c' \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize c'\<rbrakk> \<Longrightarrow> corres dc (cte_wp_at ((=) src_cap) src and valid_objs and pspace_aligned and pspace_distinct) (cte_wp_at' ((=) srcCTE) (cte_map src) and pspace_aligned' and pspace_distinct') (set_cap (max_free_index_update src_cap) src) (return ())
 8. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; obj_ref_of src_cap = obj_ref_of c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped c; isUntypedCap (cteCap srcCTE) \<and> isUntypedCap c' \<and> capPtr (cteCap srcCTE) = capPtr c' \<and> capBlockSize (cteCap srcCTE) = capBlockSize c'\<rbrakk> \<Longrightarrow> corres dc (cte_wp_at ((=) src_cap) src and valid_objs and pspace_aligned and pspace_distinct) (cte_wp_at' ((=) srcCTE) (cte_map src) and pspace_aligned' and pspace_distinct') (return ()) (updateCap (cte_map src) (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c')) (cteCap srcCTE))) proof (prove)
goal (8 subgoals):
 1. \<And>cte. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap; isUntypedCap (cteCap srcCTE); is_untyped_cap c; isUntypedCap c'; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c'; capBlockSize (cteCap srcCTE) = capBlockSize c'; cte = srcCTE\<rbrakk> \<Longrightarrow> corres dc ?Q30 (?P'39 srcCTE) (set_cap (max_free_index_update src_cap) src) (setCTE (cte_map src) (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c')) (cteCap srcCTE)) srcCTE))
 2. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap; isUntypedCap (cteCap srcCTE); is_untyped_cap c; isUntypedCap c'; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c'; capBlockSize (cteCap srcCTE) = capBlockSize c'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'30\<rbrace> getCTE (cte_map src) \<lbrace>\<lambda>cte. ?P'39 cte and (\<lambda>s. cte = srcCTE)\<rbrace>
 3. \<And>s. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap; isUntypedCap (cteCap srcCTE); is_untyped_cap c; isUntypedCap c'; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c'; capBlockSize (cteCap srcCTE) = capBlockSize c'; ?Q'30 s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> getCTE (cte_map src) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap; isUntypedCap (cteCap srcCTE); is_untyped_cap c; isUntypedCap c'; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c'; capBlockSize (cteCap srcCTE) = capBlockSize c'; True\<rbrakk> \<Longrightarrow> no_fail ?Q'30 (getCTE (cte_map src))
 5. \<And>s. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap; isUntypedCap (cteCap srcCTE); is_untyped_cap c; isUntypedCap c'; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c'; capBlockSize (cteCap srcCTE) = capBlockSize c'; (cte_wp_at ((=) src_cap) src and valid_objs and pspace_aligned and pspace_distinct) s\<rbrakk> \<Longrightarrow> ?Q30 s
 6. \<And>s. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap; isUntypedCap (cteCap srcCTE); is_untyped_cap c; isUntypedCap c'; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c'; capBlockSize (cteCap srcCTE) = capBlockSize c'; (cte_wp_at' ((=) srcCTE) (cte_map src) and pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> ?Q'30 s
 7. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap \<and> is_untyped_cap c \<and> obj_ref_of src_cap = obj_ref_of c \<and> cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c' \<longrightarrow> isUntypedCap c' \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize c'\<rbrakk> \<Longrightarrow> corres dc (cte_wp_at ((=) src_cap) src and valid_objs and pspace_aligned and pspace_distinct) (cte_wp_at' ((=) srcCTE) (cte_map src) and pspace_aligned' and pspace_distinct') (set_cap (max_free_index_update src_cap) src) (return ())
 8. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; obj_ref_of src_cap = obj_ref_of c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped c; isUntypedCap (cteCap srcCTE) \<and> isUntypedCap c' \<and> capPtr (cteCap srcCTE) = capPtr c' \<and> capBlockSize (cteCap srcCTE) = capBlockSize c'\<rbrakk> \<Longrightarrow> corres dc (cte_wp_at ((=) src_cap) src and valid_objs and pspace_aligned and pspace_distinct) (cte_wp_at' ((=) srcCTE) (cte_map src) and pspace_aligned' and pspace_distinct') (return ()) (updateCap (cte_map src) (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c')) (cteCap srcCTE))) proof (prove)
goal (10 subgoals):
 1. \<And>cte. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap; isUntypedCap (cteCap srcCTE); is_untyped_cap c; isUntypedCap c'; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c'; capBlockSize (cteCap srcCTE) = capBlockSize c'; cte = srcCTE\<rbrakk> \<Longrightarrow> cap_relation src_cap (cteCap srcCTE)
 2. \<And>cte. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap; isUntypedCap (cteCap srcCTE); is_untyped_cap c; isUntypedCap c'; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c'; capBlockSize (cteCap srcCTE) = capBlockSize c'; cte = srcCTE\<rbrakk> \<Longrightarrow> is_untyped_cap src_cap
 3. \<And>cte. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap; isUntypedCap (cteCap srcCTE); is_untyped_cap c; isUntypedCap c'; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c'; capBlockSize (cteCap srcCTE) = capBlockSize c'; cte = srcCTE\<rbrakk> \<Longrightarrow> max_free_index (capBlockSize c') = max_free_index (untyped_sz_bits src_cap)
 4. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap; isUntypedCap (cteCap srcCTE); is_untyped_cap c; isUntypedCap c'; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c'; capBlockSize (cteCap srcCTE) = capBlockSize c'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'30\<rbrace> getCTE (cte_map src) \<lbrace>\<lambda>cte. cte_wp_at' ((=) cte) (cte_map src) and pspace_distinct' and pspace_aligned' and (\<lambda>s. cte = srcCTE)\<rbrace>
 5. \<And>s. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap; isUntypedCap (cteCap srcCTE); is_untyped_cap c; isUntypedCap c'; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c'; capBlockSize (cteCap srcCTE) = capBlockSize c'; ?Q'30 s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> getCTE (cte_map src) \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap; isUntypedCap (cteCap srcCTE); is_untyped_cap c; isUntypedCap c'; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c'; capBlockSize (cteCap srcCTE) = capBlockSize c'; True\<rbrakk> \<Longrightarrow> no_fail ?Q'30 (getCTE (cte_map src))
 7. \<And>s. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap; isUntypedCap (cteCap srcCTE); is_untyped_cap c; isUntypedCap c'; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c'; capBlockSize (cteCap srcCTE) = capBlockSize c'; (cte_wp_at ((=) src_cap) src and valid_objs and pspace_aligned and pspace_distinct) s\<rbrakk> \<Longrightarrow> (cte_wp_at ((=) src_cap) src and valid_objs and pspace_aligned and pspace_distinct) s
 8. \<And>s. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap; isUntypedCap (cteCap srcCTE); is_untyped_cap c; isUntypedCap c'; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c'; capBlockSize (cteCap srcCTE) = capBlockSize c'; (cte_wp_at' ((=) srcCTE) (cte_map src) and pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> ?Q'30 s
 9. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap \<and> is_untyped_cap c \<and> obj_ref_of src_cap = obj_ref_of c \<and> cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c' \<longrightarrow> isUntypedCap c' \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize c'\<rbrakk> \<Longrightarrow> corres dc (cte_wp_at ((=) src_cap) src and valid_objs and pspace_aligned and pspace_distinct) (cte_wp_at' ((=) srcCTE) (cte_map src) and pspace_aligned' and pspace_distinct') (set_cap (max_free_index_update src_cap) src) (return ())
 10. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; obj_ref_of src_cap = obj_ref_of c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped c; isUntypedCap (cteCap srcCTE) \<and> isUntypedCap c' \<and> capPtr (cteCap srcCTE) = capPtr c' \<and> capBlockSize (cteCap srcCTE) = capBlockSize c'\<rbrakk> \<Longrightarrow> corres dc (cte_wp_at ((=) src_cap) src and valid_objs and pspace_aligned and pspace_distinct) (cte_wp_at' ((=) srcCTE) (cte_map src) and pspace_aligned' and pspace_distinct') (return ()) (updateCap (cte_map src) (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c')) (cteCap srcCTE))) proof (prove)
goal (8 subgoals):
 1. \<And>cte. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap; isUntypedCap (cteCap srcCTE); is_untyped_cap c; isUntypedCap c'; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c'; capBlockSize (cteCap srcCTE) = capBlockSize c'; cte = srcCTE\<rbrakk> \<Longrightarrow> max_free_index (capBlockSize c') = max_free_index (untyped_sz_bits src_cap)
 2. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap; isUntypedCap (cteCap srcCTE); is_untyped_cap c; isUntypedCap c'; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c'; capBlockSize (cteCap srcCTE) = capBlockSize c'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'30\<rbrace> getCTE (cte_map src) \<lbrace>\<lambda>cte. cte_wp_at' ((=) cte) (cte_map src) and pspace_distinct' and pspace_aligned' and (\<lambda>s. cte = srcCTE)\<rbrace>
 3. \<And>s. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap; isUntypedCap (cteCap srcCTE); is_untyped_cap c; isUntypedCap c'; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c'; capBlockSize (cteCap srcCTE) = capBlockSize c'; ?Q'30 s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> getCTE (cte_map src) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap; isUntypedCap (cteCap srcCTE); is_untyped_cap c; isUntypedCap c'; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c'; capBlockSize (cteCap srcCTE) = capBlockSize c'; True\<rbrakk> \<Longrightarrow> no_fail ?Q'30 (getCTE (cte_map src))
 5. \<And>s. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap; isUntypedCap (cteCap srcCTE); is_untyped_cap c; isUntypedCap c'; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c'; capBlockSize (cteCap srcCTE) = capBlockSize c'; (cte_wp_at ((=) src_cap) src and valid_objs and pspace_aligned and pspace_distinct) s\<rbrakk> \<Longrightarrow> (cte_wp_at ((=) src_cap) src and valid_objs and pspace_aligned and pspace_distinct) s
 6. \<And>s. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap; isUntypedCap (cteCap srcCTE); is_untyped_cap c; isUntypedCap c'; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c'; capBlockSize (cteCap srcCTE) = capBlockSize c'; (cte_wp_at' ((=) srcCTE) (cte_map src) and pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> ?Q'30 s
 7. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap \<and> is_untyped_cap c \<and> obj_ref_of src_cap = obj_ref_of c \<and> cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c' \<longrightarrow> isUntypedCap c' \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize c'\<rbrakk> \<Longrightarrow> corres dc (cte_wp_at ((=) src_cap) src and valid_objs and pspace_aligned and pspace_distinct) (cte_wp_at' ((=) srcCTE) (cte_map src) and pspace_aligned' and pspace_distinct') (set_cap (max_free_index_update src_cap) src) (return ())
 8. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; obj_ref_of src_cap = obj_ref_of c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped c; isUntypedCap (cteCap srcCTE) \<and> isUntypedCap c' \<and> capPtr (cteCap srcCTE) = capPtr c' \<and> capBlockSize (cteCap srcCTE) = capBlockSize c'\<rbrakk> \<Longrightarrow> corres dc (cte_wp_at ((=) src_cap) src and valid_objs and pspace_aligned and pspace_distinct) (cte_wp_at' ((=) srcCTE) (cte_map src) and pspace_aligned' and pspace_distinct') (return ()) (updateCap (cte_map src) (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c')) (cteCap srcCTE))) proof (prove)
goal (7 subgoals):
 1. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap; isUntypedCap (cteCap srcCTE); is_untyped_cap c; isUntypedCap c'; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c'; capBlockSize (cteCap srcCTE) = capBlockSize c'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'30\<rbrace> getCTE (cte_map src) \<lbrace>\<lambda>cte. cte_wp_at' ((=) cte) (cte_map src) and pspace_distinct' and pspace_aligned' and (\<lambda>s. cte = srcCTE)\<rbrace>
 2. \<And>s. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap; isUntypedCap (cteCap srcCTE); is_untyped_cap c; isUntypedCap c'; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c'; capBlockSize (cteCap srcCTE) = capBlockSize c'; ?Q'30 s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> getCTE (cte_map src) \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap; isUntypedCap (cteCap srcCTE); is_untyped_cap c; isUntypedCap c'; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c'; capBlockSize (cteCap srcCTE) = capBlockSize c'; True\<rbrakk> \<Longrightarrow> no_fail ?Q'30 (getCTE (cte_map src))
 4. \<And>s. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap; isUntypedCap (cteCap srcCTE); is_untyped_cap c; isUntypedCap c'; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c'; capBlockSize (cteCap srcCTE) = capBlockSize c'; (cte_wp_at ((=) src_cap) src and valid_objs and pspace_aligned and pspace_distinct) s\<rbrakk> \<Longrightarrow> (cte_wp_at ((=) src_cap) src and valid_objs and pspace_aligned and pspace_distinct) s
 5. \<And>s. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap; isUntypedCap (cteCap srcCTE); is_untyped_cap c; isUntypedCap c'; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c'; capBlockSize (cteCap srcCTE) = capBlockSize c'; (cte_wp_at' ((=) srcCTE) (cte_map src) and pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> ?Q'30 s
 6. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap \<and> is_untyped_cap c \<and> obj_ref_of src_cap = obj_ref_of c \<and> cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c' \<longrightarrow> isUntypedCap c' \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize c'\<rbrakk> \<Longrightarrow> corres dc (cte_wp_at ((=) src_cap) src and valid_objs and pspace_aligned and pspace_distinct) (cte_wp_at' ((=) srcCTE) (cte_map src) and pspace_aligned' and pspace_distinct') (set_cap (max_free_index_update src_cap) src) (return ())
 7. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; obj_ref_of src_cap = obj_ref_of c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped c; isUntypedCap (cteCap srcCTE) \<and> isUntypedCap c' \<and> capPtr (cteCap srcCTE) = capPtr c' \<and> capBlockSize (cteCap srcCTE) = capBlockSize c'\<rbrakk> \<Longrightarrow> corres dc (cte_wp_at ((=) src_cap) src and valid_objs and pspace_aligned and pspace_distinct) (cte_wp_at' ((=) srcCTE) (cte_map src) and pspace_aligned' and pspace_distinct') (return ()) (updateCap (cte_map src) (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c')) (cteCap srcCTE))) proof (prove)
goal (7 subgoals):
 1. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap; isUntypedCap (cteCap srcCTE); is_untyped_cap c; isUntypedCap c'; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c'; capBlockSize (cteCap srcCTE) = capBlockSize c'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'30\<rbrace> getCTE (cte_map src) \<lbrace>\<lambda>cte. cte_wp_at' (\<lambda>c. c = cte) (cte_map src) and pspace_distinct' and pspace_aligned' and (\<lambda>s. cte = srcCTE)\<rbrace>
 2. \<And>s. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap; isUntypedCap (cteCap srcCTE); is_untyped_cap c; isUntypedCap c'; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c'; capBlockSize (cteCap srcCTE) = capBlockSize c'; ?Q'30 s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> getCTE (cte_map src) \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap; isUntypedCap (cteCap srcCTE); is_untyped_cap c; isUntypedCap c'; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c'; capBlockSize (cteCap srcCTE) = capBlockSize c'; True\<rbrakk> \<Longrightarrow> no_fail ?Q'30 (getCTE (cte_map src))
 4. \<And>s. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap; isUntypedCap (cteCap srcCTE); is_untyped_cap c; isUntypedCap c'; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c'; capBlockSize (cteCap srcCTE) = capBlockSize c'; (cte_wp_at ((=) src_cap) src and valid_objs and pspace_aligned and pspace_distinct) s\<rbrakk> \<Longrightarrow> (cte_wp_at ((=) src_cap) src and valid_objs and pspace_aligned and pspace_distinct) s
 5. \<And>s. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap; isUntypedCap (cteCap srcCTE); is_untyped_cap c; isUntypedCap c'; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c'; capBlockSize (cteCap srcCTE) = capBlockSize c'; (cte_wp_at' ((=) srcCTE) (cte_map src) and pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> ?Q'30 s
 6. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap \<and> is_untyped_cap c \<and> obj_ref_of src_cap = obj_ref_of c \<and> cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c' \<longrightarrow> isUntypedCap c' \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize c'\<rbrakk> \<Longrightarrow> corres dc (cte_wp_at ((=) src_cap) src and valid_objs and pspace_aligned and pspace_distinct) (cte_wp_at' ((=) srcCTE) (cte_map src) and pspace_aligned' and pspace_distinct') (set_cap (max_free_index_update src_cap) src) (return ())
 7. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; obj_ref_of src_cap = obj_ref_of c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped c; isUntypedCap (cteCap srcCTE) \<and> isUntypedCap c' \<and> capPtr (cteCap srcCTE) = capPtr c' \<and> capBlockSize (cteCap srcCTE) = capBlockSize c'\<rbrakk> \<Longrightarrow> corres dc (cte_wp_at ((=) src_cap) src and valid_objs and pspace_aligned and pspace_distinct) (cte_wp_at' ((=) srcCTE) (cte_map src) and pspace_aligned' and pspace_distinct') (return ()) (updateCap (cte_map src) (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c')) (cteCap srcCTE))) proof (prove)
goal (5 subgoals):
 1. \<And>s. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap; isUntypedCap (cteCap srcCTE); is_untyped_cap c; isUntypedCap c'; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c'; capBlockSize (cteCap srcCTE) = capBlockSize c'; True; pspace_distinct' s \<and> pspace_aligned' s \<and> cte_wp_at' (\<lambda>rv. rv = srcCTE) (cte_map src) s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (cte_map src) s
 2. \<And>s. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap; isUntypedCap (cteCap srcCTE); is_untyped_cap c; isUntypedCap c'; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c'; capBlockSize (cteCap srcCTE) = capBlockSize c'; (cte_wp_at ((=) src_cap) src and valid_objs and pspace_aligned and pspace_distinct) s\<rbrakk> \<Longrightarrow> (cte_wp_at ((=) src_cap) src and valid_objs and pspace_aligned and pspace_distinct) s
 3. \<And>s. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap; isUntypedCap (cteCap srcCTE); is_untyped_cap c; isUntypedCap c'; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c'; capBlockSize (cteCap srcCTE) = capBlockSize c'; (cte_wp_at' ((=) srcCTE) (cte_map src) and pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> pspace_distinct' s \<and> pspace_aligned' s \<and> cte_wp_at' (\<lambda>rv. rv = srcCTE) (cte_map src) s
 4. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; is_untyped_cap src_cap \<and> is_untyped_cap c \<and> obj_ref_of src_cap = obj_ref_of c \<and> cap_bits_untyped src_cap = cap_bits_untyped c; capPtr (cteCap srcCTE) = capPtr c' \<longrightarrow> isUntypedCap c' \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize c'\<rbrakk> \<Longrightarrow> corres dc (cte_wp_at ((=) src_cap) src and valid_objs and pspace_aligned and pspace_distinct) (cte_wp_at' ((=) srcCTE) (cte_map src) and pspace_aligned' and pspace_distinct') (set_cap (max_free_index_update src_cap) src) (return ())
 5. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; obj_ref_of src_cap = obj_ref_of c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped c; isUntypedCap (cteCap srcCTE) \<and> isUntypedCap c' \<and> capPtr (cteCap srcCTE) = capPtr c' \<and> capBlockSize (cteCap srcCTE) = capBlockSize c'\<rbrakk> \<Longrightarrow> corres dc (cte_wp_at ((=) src_cap) src and valid_objs and pspace_aligned and pspace_distinct) (cte_wp_at' ((=) srcCTE) (cte_map src) and pspace_aligned' and pspace_distinct') (return ()) (updateCap (cte_map src) (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c')) (cteCap srcCTE))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; capPtr (cteCap srcCTE) = capPtr c' \<longrightarrow> isUntypedCap c' \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize c'; is_untyped_cap src_cap; is_untyped_cap c; obj_ref_of src_cap = obj_ref_of c; cap_bits_untyped src_cap = cap_bits_untyped c\<rbrakk> \<Longrightarrow> corres dc (cte_wp_at ((=) src_cap) src and valid_objs and pspace_aligned and pspace_distinct) (cte_wp_at' ((=) srcCTE) (cte_map src) and pspace_aligned' and pspace_distinct') (set_cap (max_free_index_update src_cap) src) (return ())
 2. \<lbrakk>cap_relation c c'; src' = cte_map src; cap_relation src_cap (cteCap srcCTE); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; obj_ref_of src_cap = obj_ref_of c \<longrightarrow> is_untyped_cap c \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped c; isUntypedCap (cteCap srcCTE) \<and> isUntypedCap c' \<and> capPtr (cteCap srcCTE) = capPtr c' \<and> capBlockSize (cteCap srcCTE) = capBlockSize c'\<rbrakk> \<Longrightarrow> corres dc (cte_wp_at ((=) src_cap) src and valid_objs and pspace_aligned and pspace_distinct) (cte_wp_at' ((=) srcCTE) (cte_map src) and pspace_aligned' and pspace_distinct') (return ()) (updateCap (cte_map src) (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c')) (cteCap srcCTE))) proof (prove)
goal (1 subgoal):
 1. \<And>d f da v0a v1a fa. \<lbrakk>cap_relation c (capability.UntypedCap da v0a v1a fa); src' = cte_map src; cap_relation src_cap (capability.UntypedCap d v0a v1a f); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; obj_ref_of src_cap = obj_ref_of c \<longrightarrow> (\<exists>dev r bits f. c = cap.UntypedCap dev r bits f) \<longrightarrow> (\<exists>dev r bits f. src_cap = cap.UntypedCap dev r bits f) \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped c; cteCap srcCTE = capability.UntypedCap d v0a v1a f; c' = capability.UntypedCap da v0a v1a fa\<rbrakk> \<Longrightarrow> corres dc (cte_wp_at ((=) src_cap) src and valid_objs and pspace_aligned and pspace_distinct) (cte_wp_at' ((=) srcCTE) (cte_map src) and pspace_aligned' and pspace_distinct') (return ()) (updateCap (cte_map src) (capability.UntypedCap d v0a v1a (max_free_index v1a))) proof (prove)
goal (1 subgoal):
 1. \<And>d f da v0a v1a fa. \<lbrakk>src' = cte_map src; cap_relation src_cap (capability.UntypedCap d v0a v1a f); rv = cap.NullCap; cteCap rv' = capability.NullCap; mdbPrev (cteMDBNode rv') = nullPointer; mdbNext (cteMDBNode rv') = nullPointer; obj_ref_of src_cap = v0a \<longrightarrow> (\<exists>dev r bits f. src_cap = cap.UntypedCap dev r bits f) \<longrightarrow> cap_bits_untyped src_cap \<noteq> v1a; cteCap srcCTE = capability.UntypedCap d v0a v1a f; c' = capability.UntypedCap da v0a v1a fa; c = cap.UntypedCap da v0a v1a fa\<rbrakk> \<Longrightarrow> corres dc (cte_wp_at ((=) src_cap) src and valid_objs and pspace_aligned and pspace_distinct) (cte_wp_at' ((=) srcCTE) (cte_map src) and pspace_aligned' and pspace_distinct') (return ()) (updateCap (cte_map src) (capability.UntypedCap d v0a v1a (max_free_index v1a))) proof (prove)
goal:
No subgoals!