theory Invoke_C

lemma checkFreeIndex_ccorres:
  "ccap_relation cp cap \<Longrightarrow>
  ccorresG rf_sr \<Gamma> (intr_and_se_rel \<currency> (\<lambda>r (fi, r'). r' = from_bool r
          \<and> (case r of True \<Rightarrow> fi = 0 | False \<Rightarrow> capFreeIndex cp = unat (fi << 4))))
      (liftxf errstate (K (scast EXCEPTION_NONE)) id (\<lambda>s. (freeIndex_' s, reset_' s)))
  (cte_wp_at' (\<lambda>cte. (cteCap cte = cp \<and> isUntypedCap cp)) slot and valid_objs' and valid_mdb') UNIV hs
  (liftE $ constOnFailure False (doE y \<leftarrow> ensureNoChildren slot; returnOk True odE))
  (\<acute>status :== CALL ensureNoChildren(cte_Ptr slot);;
  (Cond \<lbrace>\<acute>status \<noteq> scast EXCEPTION_NONE\<rbrace>
    (\<acute>ret__unsigned :== CALL cap_untyped_cap_get_capFreeIndex(cap)
        ;; \<acute>freeIndex :== \<acute>ret__unsigned
        ;; \<acute>reset :== scast false)
    (\<acute>freeIndex :== 0
        ;; \<acute>reset :== scast true)))" apply (simp add: constOnFailure_def catch_def liftE_def bindE_bind_linearise bind_assoc case_sum_distrib) apply (rule ccorres_guard_imp2) apply (rule ccorres_split_nothrow_case_sum) apply (ctac add:ensureNoChildren_ccorres) apply (ceqv) apply (rule ccorres_from_vcg[where P' = UNIV]) apply (clarsimp simp add: returnOk_def, simp add: return_def) apply (rule conseqPre) apply vcg apply clarsimp apply simp apply (rule ccorres_from_vcg[where P'= UNIV]) apply (simp, clarsimp simp:return_def) apply (rule conseqPre) apply vcg apply clarsimp apply (rule context_conjI) apply (clarsimp simp:cap_get_tag_isCap) apply assumption apply (clarsimp simp: ccap_relation_def isCap_simps cap_untyped_cap_lift_def cap_lift_def
                           cap_to_H_def
                     split: if_splits
                     cong: if_cong) apply (rule ensureNoChildren_wp[where P = dc]) apply clarsimp apply (vcg exspec=ensureNoChildren_modifies) apply (clarsimp simp: cte_wp_at_ctes_of) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccap_relation cp cap \<Longrightarrow> ccorres (intr_and_se_rel \<currency> (\<lambda>r (fi, r'). r' = from_bool r \<and> (case r of True \<Rightarrow> fi = 0 | False \<Rightarrow> capFreeIndex cp = unat (fi << 4)))) (liftxf errstate (K (SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)) id (\<lambda>s. (freeIndex_' s, reset_' s))) (cte_wp_at' (\<lambda>cte. cteCap cte = cp \<and> isUntypedCap cp) slot and valid_objs' and valid_mdb') UNIV hs (liftE $ constOnFailure False (doE y <- ensureNoChildren slot;
returnOk True
odE)) (\<acute>status :== CALL ensureNoChildren_'proc(cte_Ptr slot);;
IF \<acute>status \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  \<acute>ret__unsigned :== CALL cap_untyped_cap_get_capFreeIndex_'proc(cap);;
\<acute>freeIndex :== \<acute>ret__unsigned;;
\<acute>reset :== SCAST(32 signed \<rightarrow> 32) false
ELSE
  \<acute>freeIndex :== 0;;
\<acute>reset :== SCAST(32 signed \<rightarrow> 32) true
FI) proof (prove)
goal (1 subgoal):
 1. ccap_relation cp cap \<Longrightarrow> ccorres (intr_and_se_rel \<currency> (\<lambda>r (fi, r'). r' = from_bool r \<and> (case r of True \<Rightarrow> fi = 0 | False \<Rightarrow> capFreeIndex cp = unat (fi << 4)))) (liftxf errstate (K (SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)) id (\<lambda>s. (freeIndex_' s, reset_' s))) (cte_wp_at' (\<lambda>cte. cteCap cte = cp \<and> isUntypedCap cp) slot and valid_objs' and valid_mdb') UNIV hs (do x <- ensureNoChildren slot;
case x of Inl x \<Rightarrow> do r <- (case_sum (const (return False)) return \<circ> Inl) x;
return (Inr r)
od | Inr x \<Rightarrow> do r <- returnOk True >>= case_sum (const (return False)) return;
return (Inr r)
od
od) (\<acute>status :== CALL ensureNoChildren_'proc(cte_Ptr slot);;
IF \<acute>status \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  \<acute>ret__unsigned :== CALL cap_untyped_cap_get_capFreeIndex_'proc(cap);;
\<acute>freeIndex :== \<acute>ret__unsigned;;
\<acute>reset :== SCAST(32 signed \<rightarrow> 32) false
ELSE
  \<acute>freeIndex :== 0;;
\<acute>reset :== SCAST(32 signed \<rightarrow> 32) true
FI) proof (prove)
goal (2 subgoals):
 1. ccap_relation cp cap \<Longrightarrow> ccorres (intr_and_se_rel \<currency> (\<lambda>r (fi, r'). r' = from_bool r \<and> (case r of True \<Rightarrow> fi = 0 | False \<Rightarrow> capFreeIndex cp = unat (fi << 4)))) (liftxf errstate (K (SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)) id (\<lambda>s. (freeIndex_' s, reset_' s))) ?Q6 ?Q'6 hs (do x <- ensureNoChildren slot;
case x of Inl x \<Rightarrow> do r <- (case_sum (const (return False)) return \<circ> Inl) x;
return (Inr r)
od | Inr x \<Rightarrow> do r <- returnOk True >>= case_sum (const (return False)) return;
return (Inr r)
od
od) (\<acute>status :== CALL ensureNoChildren_'proc(cte_Ptr slot);;
IF \<acute>status \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  \<acute>ret__unsigned :== CALL cap_untyped_cap_get_capFreeIndex_'proc(cap);;
\<acute>freeIndex :== \<acute>ret__unsigned;;
\<acute>reset :== SCAST(32 signed \<rightarrow> 32) false
ELSE
  \<acute>freeIndex :== 0;;
\<acute>reset :== SCAST(32 signed \<rightarrow> 32) true
FI)
 2. \<And>s s'. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>cte. cteCap cte = cp \<and> isUntypedCap cp) slot and valid_objs' and valid_mdb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q6 s \<and> s' \<in> ?Q'6 proof (prove)
goal (7 subgoals):
 1. ccap_relation cp cap \<Longrightarrow> ccorres (?f'9 \<currency> ?r'9) (liftxf ?es9 ?ef'9 ?vf'9 ?xf'9) ?P9 ?P'9 hs (ensureNoChildren slot) (\<acute>status :== CALL ensureNoChildren_'proc(cte_Ptr slot))
 2. \<And>rv' t t'. ccap_relation cp cap \<Longrightarrow> ceqv \<Gamma> ?xf'9 rv' t t' (IF \<acute>status \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  \<acute>ret__unsigned :== CALL cap_untyped_cap_get_capFreeIndex_'proc(cap);;
\<acute>freeIndex :== \<acute>ret__unsigned;;
\<acute>reset :== SCAST(32 signed \<rightarrow> 32) false
ELSE
  \<acute>freeIndex :== 0;;
\<acute>reset :== SCAST(32 signed \<rightarrow> 32) true
FI) (?d'9 rv')
 3. \<And>rv rv'. \<lbrakk>ccap_relation cp cap; ?r'9 rv (?vf'9 rv'); ?ef'9 rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres (intr_and_se_rel \<currency> (\<lambda>r (fi, r'). r' = from_bool r \<and> (case r of True \<Rightarrow> fi = 0 | False \<Rightarrow> capFreeIndex cp = unat (fi << 4)))) (liftxf errstate (K (SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)) id (\<lambda>s. (freeIndex_' s, reset_' s))) (?Q9 rv) (?Q'9 rv rv') hs (do r <- returnOk True >>= case_sum (const (return False)) return;
return (Inr r)
od) (?d'9 rv')
 4. \<And>err rv' err'. \<lbrakk>ccap_relation cp cap; ?ef'9 rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; ?f'9 err (?ef'9 rv') err'\<rbrakk> \<Longrightarrow> ccorres (intr_and_se_rel \<currency> (\<lambda>r (fi, r'). r' = from_bool r \<and> (case r of True \<Rightarrow> fi = 0 | False \<Rightarrow> capFreeIndex cp = unat (fi << 4)))) (liftxf errstate (K (SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)) id (\<lambda>s. (freeIndex_' s, reset_' s))) (?QE9 err) (?Q''9 err rv' err') hs (do r <- (case_sum (const (return False)) return \<circ> Inl) err;
return (Inr r)
od) (?d'9 rv')
 5. ccap_relation cp cap \<Longrightarrow> \<lbrace>?R9\<rbrace> ensureNoChildren slot \<lbrace>?Q9\<rbrace>, \<lbrace>?QE9\<rbrace>
 6. ccap_relation cp cap \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'9 \<acute>status :== CALL ensureNoChildren_'proc(cte_Ptr slot) {s. (\<forall>rv'. ?ef'9 (?xf'9 s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> ?r'9 rv' (?vf'9 (?xf'9 s)) \<longrightarrow> s \<in> ?Q'9 rv' (?xf'9 s)) \<and> (\<forall>ft. ?ef'9 (?xf'9 s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> ?f'9 ft (?ef'9 (?xf'9 s)) (?es9 s) \<longrightarrow> s \<in> ?Q''9 ft (?xf'9 s) (?es9 s))}
 7. \<And>s s'. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>cte. cteCap cte = cp \<and> isUntypedCap cp) slot and valid_objs' and valid_mdb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (?P9 and ?R9) s \<and> s' \<in> ?P'9 \<inter> ?R'9 proof (prove)
goal (6 subgoals):
 1. \<And>rv' t t'. ccap_relation cp cap \<Longrightarrow> ceqv \<Gamma> status_' rv' t t' (IF \<acute>status \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  \<acute>ret__unsigned :== CALL cap_untyped_cap_get_capFreeIndex_'proc(cap);;
\<acute>freeIndex :== \<acute>ret__unsigned;;
\<acute>reset :== SCAST(32 signed \<rightarrow> 32) false
ELSE
  \<acute>freeIndex :== 0;;
\<acute>reset :== SCAST(32 signed \<rightarrow> 32) true
FI) (?d'9 rv')
 2. \<And>rv rv'. \<lbrakk>ccap_relation cp cap; dc rv (undefined rv'); id rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres (intr_and_se_rel \<currency> (\<lambda>r (fi, r'). r' = from_bool r \<and> (case r of True \<Rightarrow> fi = 0 | False \<Rightarrow> capFreeIndex cp = unat (fi << 4)))) (liftxf errstate (K (SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)) id (\<lambda>s. (freeIndex_' s, reset_' s))) (?Q9 rv) (?Q'9 rv rv') hs (do r <- returnOk True >>= case_sum (const (return False)) return;
return (Inr r)
od) (?d'9 rv')
 3. \<And>err rv' err'. \<lbrakk>ccap_relation cp cap; id rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; syscall_error_rel err (id rv') err'\<rbrakk> \<Longrightarrow> ccorres (intr_and_se_rel \<currency> (\<lambda>r (fi, r'). r' = from_bool r \<and> (case r of True \<Rightarrow> fi = 0 | False \<Rightarrow> capFreeIndex cp = unat (fi << 4)))) (liftxf errstate (K (SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)) id (\<lambda>s. (freeIndex_' s, reset_' s))) (?QE9 err) (?Q''9 err rv' err') hs (do r <- (case_sum (const (return False)) return \<circ> Inl) err;
return (Inr r)
od) (?d'9 rv')
 4. ccap_relation cp cap \<Longrightarrow> \<lbrace>?R9\<rbrace> ensureNoChildren slot \<lbrace>?Q9\<rbrace>, \<lbrace>?QE9\<rbrace>
 5. ccap_relation cp cap \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'9 \<acute>status :== CALL ensureNoChildren_'proc(cte_Ptr slot) {s. (\<forall>rv'. id (status_' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> dc rv' (undefined (status_' s)) \<longrightarrow> s \<in> ?Q'9 rv' (status_' s)) \<and> (\<forall>ft. id (status_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> syscall_error_rel ft (id (status_' s)) (errstate s) \<longrightarrow> s \<in> ?Q''9 ft (status_' s) (errstate s))}
 6. \<And>s s'. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>cte. cteCap cte = cp \<and> isUntypedCap cp) slot and valid_objs' and valid_mdb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>s. valid_objs' s \<and> valid_mdb' s) and ?R9) s \<and> s' \<in> {s. slot_'_update (\<lambda>_. cte_Ptr slot) s \<in> UNIV \<inter> \<lbrace>slot = ptr_val \<acute>slot\<rbrace>} \<inter> ?R'9 proof (prove)
goal (5 subgoals):
 1. \<And>rv rv'. \<lbrakk>ccap_relation cp cap; dc rv (undefined rv'); id rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres (intr_and_se_rel \<currency> (\<lambda>r (fi, r'). r' = from_bool r \<and> (case r of True \<Rightarrow> fi = 0 | False \<Rightarrow> capFreeIndex cp = unat (fi << 4)))) (liftxf errstate (K (SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)) id (\<lambda>s. (freeIndex_' s, reset_' s))) (?Q9 rv) (?Q'9 rv rv') hs (do r <- returnOk True >>= case_sum (const (return False)) return;
return (Inr r)
od) (IF rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  \<acute>ret__unsigned :== CALL cap_untyped_cap_get_capFreeIndex_'proc(cap);;
\<acute>freeIndex :== \<acute>ret__unsigned;;
\<acute>reset :== SCAST(32 signed \<rightarrow> 32) false
ELSE
  \<acute>freeIndex :== 0;;
\<acute>reset :== SCAST(32 signed \<rightarrow> 32) true
FI)
 2. \<And>err rv' err'. \<lbrakk>ccap_relation cp cap; id rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; syscall_error_rel err (id rv') err'\<rbrakk> \<Longrightarrow> ccorres (intr_and_se_rel \<currency> (\<lambda>r (fi, r'). r' = from_bool r \<and> (case r of True \<Rightarrow> fi = 0 | False \<Rightarrow> capFreeIndex cp = unat (fi << 4)))) (liftxf errstate (K (SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)) id (\<lambda>s. (freeIndex_' s, reset_' s))) (?QE9 err) (?Q''9 err rv' err') hs (do r <- (case_sum (const (return False)) return \<circ> Inl) err;
return (Inr r)
od) (IF rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  \<acute>ret__unsigned :== CALL cap_untyped_cap_get_capFreeIndex_'proc(cap);;
\<acute>freeIndex :== \<acute>ret__unsigned;;
\<acute>reset :== SCAST(32 signed \<rightarrow> 32) false
ELSE
  \<acute>freeIndex :== 0;;
\<acute>reset :== SCAST(32 signed \<rightarrow> 32) true
FI)
 3. ccap_relation cp cap \<Longrightarrow> \<lbrace>?R9\<rbrace> ensureNoChildren slot \<lbrace>?Q9\<rbrace>, \<lbrace>?QE9\<rbrace>
 4. ccap_relation cp cap \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'9 \<acute>status :== CALL ensureNoChildren_'proc(cte_Ptr slot) {s. (\<forall>rv'. id (status_' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> dc rv' (undefined (status_' s)) \<longrightarrow> s \<in> ?Q'9 rv' (status_' s)) \<and> (\<forall>ft. id (status_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> syscall_error_rel ft (id (status_' s)) (errstate s) \<longrightarrow> s \<in> ?Q''9 ft (status_' s) (errstate s))}
 5. \<And>s s'. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>cte. cteCap cte = cp \<and> isUntypedCap cp) slot and valid_objs' and valid_mdb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>s. valid_objs' s \<and> valid_mdb' s) and ?R9) s \<and> s' \<in> {s. slot_'_update (\<lambda>_. cte_Ptr slot) s \<in> UNIV \<inter> \<lbrace>slot = ptr_val \<acute>slot\<rbrace>} \<inter> ?R'9 proof (prove)
goal (5 subgoals):
 1. \<And>rv rv'. \<lbrakk>ccap_relation cp cap; dc rv (undefined rv'); id rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. ?Q9 rv \<sigma> \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} IF rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  \<acute>ret__unsigned :== CALL cap_untyped_cap_get_capFreeIndex_'proc(cap);;
\<acute>freeIndex :== \<acute>ret__unsigned;;
\<acute>reset :== SCAST(32 signed \<rightarrow> 32) false
ELSE
  \<acute>freeIndex :== 0;;
\<acute>reset :== SCAST(32 signed \<rightarrow> 32) true
FI {s. \<exists>(rv, \<sigma>')\<in>fst ((do r <- returnOk True >>= case_sum (const (return False)) return;
return (Inr r)
od) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> (intr_and_se_rel \<currency> (\<lambda>r (fi, r'). r' = from_bool r \<and> (case r of True \<Rightarrow> fi = 0 | False \<Rightarrow> capFreeIndex cp = unat (fi << 4)))) rv (liftxf errstate (K (SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)) id (\<lambda>s. (freeIndex_' s, reset_' s)) s)}
 2. \<And>err rv' err'. \<lbrakk>ccap_relation cp cap; id rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; syscall_error_rel err (id rv') err'\<rbrakk> \<Longrightarrow> ccorres (intr_and_se_rel \<currency> (\<lambda>r (fi, r'). r' = from_bool r \<and> (case r of True \<Rightarrow> fi = 0 | False \<Rightarrow> capFreeIndex cp = unat (fi << 4)))) (liftxf errstate (K (SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)) id (\<lambda>s. (freeIndex_' s, reset_' s))) (?QE9 err) (?Q''9 err rv' err') hs (do r <- (case_sum (const (return False)) return \<circ> Inl) err;
return (Inr r)
od) (IF rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  \<acute>ret__unsigned :== CALL cap_untyped_cap_get_capFreeIndex_'proc(cap);;
\<acute>freeIndex :== \<acute>ret__unsigned;;
\<acute>reset :== SCAST(32 signed \<rightarrow> 32) false
ELSE
  \<acute>freeIndex :== 0;;
\<acute>reset :== SCAST(32 signed \<rightarrow> 32) true
FI)
 3. ccap_relation cp cap \<Longrightarrow> \<lbrace>?R9\<rbrace> ensureNoChildren slot \<lbrace>?Q9\<rbrace>, \<lbrace>?QE9\<rbrace>
 4. ccap_relation cp cap \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'9 \<acute>status :== CALL ensureNoChildren_'proc(cte_Ptr slot) {s. (\<forall>rv'. id (status_' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> dc rv' (undefined (status_' s)) \<longrightarrow> s \<in> UNIV) \<and> (\<forall>ft. id (status_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> syscall_error_rel ft (id (status_' s)) (errstate s) \<longrightarrow> s \<in> ?Q''9 ft (status_' s) (errstate s))}
 5. \<And>s s'. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>cte. cteCap cte = cp \<and> isUntypedCap cp) slot and valid_objs' and valid_mdb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>s. valid_objs' s \<and> valid_mdb' s) and ?R9) s \<and> s' \<in> {s. slot_'_update (\<lambda>_. cte_Ptr slot) s \<in> UNIV \<inter> \<lbrace>slot = ptr_val \<acute>slot\<rbrace>} \<inter> ?R'9 proof (prove)
goal (5 subgoals):
 1. \<And>\<sigma>. ccap_relation cp cap \<Longrightarrow> \<Gamma>\<turnstile> {s. ?Q9 () \<sigma> \<and> (\<sigma>, s) \<in> rf_sr} Cond {} (\<acute>ret__unsigned :== CALL cap_untyped_cap_get_capFreeIndex_'proc(cap);;
\<acute>freeIndex :== \<acute>ret__unsigned;;
\<acute>reset :== SCAST(32 signed \<rightarrow> 32) false) (\<acute>freeIndex :== 0;;
\<acute>reset :== SCAST(32 signed \<rightarrow> 32) true) {s. (\<sigma>, s) \<in> rf_sr \<and> reset_' s = SCAST(32 signed \<rightarrow> 32) true \<and> freeIndex_' s = 0}
 2. \<And>err rv' err'. \<lbrakk>ccap_relation cp cap; id rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; syscall_error_rel err (id rv') err'\<rbrakk> \<Longrightarrow> ccorres (intr_and_se_rel \<currency> (\<lambda>r (fi, r'). r' = from_bool r \<and> (case r of True \<Rightarrow> fi = 0 | False \<Rightarrow> capFreeIndex cp = unat (fi << 4)))) (liftxf errstate (K (SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)) id (\<lambda>s. (freeIndex_' s, reset_' s))) (?QE9 err) (?Q''9 err rv' err') hs (do r <- (case_sum (const (return False)) return \<circ> Inl) err;
return (Inr r)
od) (IF rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  \<acute>ret__unsigned :== CALL cap_untyped_cap_get_capFreeIndex_'proc(cap);;
\<acute>freeIndex :== \<acute>ret__unsigned;;
\<acute>reset :== SCAST(32 signed \<rightarrow> 32) false
ELSE
  \<acute>freeIndex :== 0;;
\<acute>reset :== SCAST(32 signed \<rightarrow> 32) true
FI)
 3. ccap_relation cp cap \<Longrightarrow> \<lbrace>?R9\<rbrace> ensureNoChildren slot \<lbrace>?Q9\<rbrace>, \<lbrace>?QE9\<rbrace>
 4. ccap_relation cp cap \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'9 \<acute>status :== CALL ensureNoChildren_'proc(cte_Ptr slot) {s. (\<forall>rv'. id (status_' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> dc rv' (undefined (status_' s)) \<longrightarrow> s \<in> UNIV) \<and> (\<forall>ft. id (status_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> syscall_error_rel ft (id (status_' s)) (errstate s) \<longrightarrow> s \<in> ?Q''9 ft (status_' s) (errstate s))}
 5. \<And>s s'. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>cte. cteCap cte = cp \<and> isUntypedCap cp) slot and valid_objs' and valid_mdb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>s. valid_objs' s \<and> valid_mdb' s) and ?R9) s \<and> s' \<in> {s. slot_'_update (\<lambda>_. cte_Ptr slot) s \<in> UNIV \<inter> \<lbrace>slot = ptr_val \<acute>slot\<rbrace>} \<inter> ?R'9 proof (prove)
goal (6 subgoals):
 1. \<And>\<sigma>. ccap_relation cp cap \<Longrightarrow> \<Gamma>\<turnstile> (?P'123 \<sigma>) Cond {} (\<acute>ret__unsigned :== CALL cap_untyped_cap_get_capFreeIndex_'proc(cap);;
\<acute>freeIndex :== \<acute>ret__unsigned;;
\<acute>reset :== SCAST(32 signed \<rightarrow> 32) false) (\<acute>freeIndex :== 0;;
\<acute>reset :== SCAST(32 signed \<rightarrow> 32) true) {s. (\<sigma>, s) \<in> rf_sr \<and> reset_' s = SCAST(32 signed \<rightarrow> 32) true \<and> freeIndex_' s = 0}
 2. \<And>\<sigma>. ccap_relation cp cap \<Longrightarrow> {s. ?Q9 () \<sigma> \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> ?P'123 \<sigma>
 3. \<And>err rv' err'. \<lbrakk>ccap_relation cp cap; id rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; syscall_error_rel err (id rv') err'\<rbrakk> \<Longrightarrow> ccorres (intr_and_se_rel \<currency> (\<lambda>r (fi, r'). r' = from_bool r \<and> (case r of True \<Rightarrow> fi = 0 | False \<Rightarrow> capFreeIndex cp = unat (fi << 4)))) (liftxf errstate (K (SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)) id (\<lambda>s. (freeIndex_' s, reset_' s))) (?QE9 err) (?Q''9 err rv' err') hs (do r <- (case_sum (const (return False)) return \<circ> Inl) err;
return (Inr r)
od) (IF rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  \<acute>ret__unsigned :== CALL cap_untyped_cap_get_capFreeIndex_'proc(cap);;
\<acute>freeIndex :== \<acute>ret__unsigned;;
\<acute>reset :== SCAST(32 signed \<rightarrow> 32) false
ELSE
  \<acute>freeIndex :== 0;;
\<acute>reset :== SCAST(32 signed \<rightarrow> 32) true
FI)
 4. ccap_relation cp cap \<Longrightarrow> \<lbrace>?R9\<rbrace> ensureNoChildren slot \<lbrace>?Q9\<rbrace>, \<lbrace>?QE9\<rbrace>
 5. ccap_relation cp cap \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'9 \<acute>status :== CALL ensureNoChildren_'proc(cte_Ptr slot) {s. (\<forall>rv'. id (status_' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> dc rv' (undefined (status_' s)) \<longrightarrow> s \<in> UNIV) \<and> (\<forall>ft. id (status_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> syscall_error_rel ft (id (status_' s)) (errstate s) \<longrightarrow> s \<in> ?Q''9 ft (status_' s) (errstate s))}
 6. \<And>s s'. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>cte. cteCap cte = cp \<and> isUntypedCap cp) slot and valid_objs' and valid_mdb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>s. valid_objs' s \<and> valid_mdb' s) and ?R9) s \<and> s' \<in> {s. slot_'_update (\<lambda>_. cte_Ptr slot) s \<in> UNIV \<inter> \<lbrace>slot = ptr_val \<acute>slot\<rbrace>} \<inter> ?R'9 proof (prove)
goal (5 subgoals):
 1. \<And>\<sigma>. ccap_relation cp cap \<Longrightarrow> {s. ?Q9 () \<sigma> \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. (False \<longrightarrow> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> (\<forall>t. ret__unsigned_' t = capFreeIndex_CL (cap_untyped_cap_lift cap) \<longrightarrow> (\<sigma>, reset_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (freeIndex_'_update (\<lambda>_. capFreeIndex_CL (cap_untyped_cap_lift cap)) (s\<lparr>ret__unsigned_' := capFreeIndex_CL (cap_untyped_cap_lift cap)\<rparr>))) \<in> rf_sr \<and> SCAST(32 signed \<rightarrow> 32) false = SCAST(32 signed \<rightarrow> 32) true \<and> capFreeIndex_CL (cap_untyped_cap_lift cap) = 0)) \<and> (\<not> False \<longrightarrow> (\<sigma>, reset_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) (freeIndex_'_update (\<lambda>_. 0) s)) \<in> rf_sr \<and> SCAST(32 signed \<rightarrow> 32) true = SCAST(32 signed \<rightarrow> 32) true \<and> 0 = 0)}
 2. \<And>err rv' err'. \<lbrakk>ccap_relation cp cap; id rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; syscall_error_rel err (id rv') err'\<rbrakk> \<Longrightarrow> ccorres (intr_and_se_rel \<currency> (\<lambda>r (fi, r'). r' = from_bool r \<and> (case r of True \<Rightarrow> fi = 0 | False \<Rightarrow> capFreeIndex cp = unat (fi << 4)))) (liftxf errstate (K (SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)) id (\<lambda>s. (freeIndex_' s, reset_' s))) (?QE9 err) (?Q''9 err rv' err') hs (do r <- (case_sum (const (return False)) return \<circ> Inl) err;
return (Inr r)
od) (IF rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  \<acute>ret__unsigned :== CALL cap_untyped_cap_get_capFreeIndex_'proc(cap);;
\<acute>freeIndex :== \<acute>ret__unsigned;;
\<acute>reset :== SCAST(32 signed \<rightarrow> 32) false
ELSE
  \<acute>freeIndex :== 0;;
\<acute>reset :== SCAST(32 signed \<rightarrow> 32) true
FI)
 3. ccap_relation cp cap \<Longrightarrow> \<lbrace>?R9\<rbrace> ensureNoChildren slot \<lbrace>?Q9\<rbrace>, \<lbrace>?QE9\<rbrace>
 4. ccap_relation cp cap \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'9 \<acute>status :== CALL ensureNoChildren_'proc(cte_Ptr slot) {s. (\<forall>rv'. id (status_' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> dc rv' (undefined (status_' s)) \<longrightarrow> s \<in> UNIV) \<and> (\<forall>ft. id (status_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> syscall_error_rel ft (id (status_' s)) (errstate s) \<longrightarrow> s \<in> ?Q''9 ft (status_' s) (errstate s))}
 5. \<And>s s'. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>cte. cteCap cte = cp \<and> isUntypedCap cp) slot and valid_objs' and valid_mdb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>s. valid_objs' s \<and> valid_mdb' s) and ?R9) s \<and> s' \<in> {s. slot_'_update (\<lambda>_. cte_Ptr slot) s \<in> UNIV \<inter> \<lbrace>slot = ptr_val \<acute>slot\<rbrace>} \<inter> ?R'9 proof (prove)
goal (4 subgoals):
 1. \<And>err rv' err'. \<lbrakk>ccap_relation cp cap; id rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; syscall_error_rel err (id rv') err'\<rbrakk> \<Longrightarrow> ccorres (intr_and_se_rel \<currency> (\<lambda>r (fi, r'). r' = from_bool r \<and> (case r of True \<Rightarrow> fi = 0 | False \<Rightarrow> capFreeIndex cp = unat (fi << 4)))) (liftxf errstate (K (SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)) id (\<lambda>s. (freeIndex_' s, reset_' s))) (?QE9 err) (?Q''9 err rv' err') hs (do r <- (case_sum (const (return False)) return \<circ> Inl) err;
return (Inr r)
od) (IF rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  \<acute>ret__unsigned :== CALL cap_untyped_cap_get_capFreeIndex_'proc(cap);;
\<acute>freeIndex :== \<acute>ret__unsigned;;
\<acute>reset :== SCAST(32 signed \<rightarrow> 32) false
ELSE
  \<acute>freeIndex :== 0;;
\<acute>reset :== SCAST(32 signed \<rightarrow> 32) true
FI)
 2. ccap_relation cp cap \<Longrightarrow> \<lbrace>?R9\<rbrace> ensureNoChildren slot \<lbrace>?Q9\<rbrace>, \<lbrace>?QE9\<rbrace>
 3. ccap_relation cp cap \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'9 \<acute>status :== CALL ensureNoChildren_'proc(cte_Ptr slot) {s. (\<forall>rv'. id (status_' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> dc rv' (undefined (status_' s)) \<longrightarrow> s \<in> UNIV) \<and> (\<forall>ft. id (status_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> syscall_error_rel ft (id (status_' s)) (errstate s) \<longrightarrow> s \<in> ?Q''9 ft (status_' s) (errstate s))}
 4. \<And>s s'. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>cte. cteCap cte = cp \<and> isUntypedCap cp) slot and valid_objs' and valid_mdb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>s. valid_objs' s \<and> valid_mdb' s) and ?R9) s \<and> s' \<in> {s. slot_'_update (\<lambda>_. cte_Ptr slot) s \<in> UNIV \<inter> \<lbrace>slot = ptr_val \<acute>slot\<rbrace>} \<inter> ?R'9 proof (prove)
goal (4 subgoals):
 1. \<And>err rv' err'. \<lbrakk>ccap_relation cp cap; rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; syscall_error_rel err rv' err'\<rbrakk> \<Longrightarrow> ccorres (intr_and_se_rel \<currency> (\<lambda>r (fi, r'). r' = from_bool r \<and> (case r of True \<Rightarrow> fi = 0 | False \<Rightarrow> capFreeIndex cp = unat (fi << 4)))) (liftxf errstate (K (SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)) id (\<lambda>s. (freeIndex_' s, reset_' s))) (?QE9 err) (?Q''9 err rv' err') hs (return (Inr False)) (Cond UNIV (\<acute>ret__unsigned :== CALL cap_untyped_cap_get_capFreeIndex_'proc(cap);;
\<acute>freeIndex :== \<acute>ret__unsigned;;
\<acute>reset :== SCAST(32 signed \<rightarrow> 32) false) (\<acute>freeIndex :== 0;;
\<acute>reset :== SCAST(32 signed \<rightarrow> 32) true))
 2. ccap_relation cp cap \<Longrightarrow> \<lbrace>?R9\<rbrace> ensureNoChildren slot \<lbrace>?Q9\<rbrace>, \<lbrace>?QE9\<rbrace>
 3. ccap_relation cp cap \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'9 \<acute>status :== CALL ensureNoChildren_'proc(cte_Ptr slot) {s. (\<forall>rv'. id (status_' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> dc rv' (undefined (status_' s)) \<longrightarrow> s \<in> UNIV) \<and> (\<forall>ft. id (status_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> syscall_error_rel ft (id (status_' s)) (errstate s) \<longrightarrow> s \<in> ?Q''9 ft (status_' s) (errstate s))}
 4. \<And>s s'. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>cte. cteCap cte = cp \<and> isUntypedCap cp) slot and valid_objs' and valid_mdb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>s. valid_objs' s \<and> valid_mdb' s) and ?R9) s \<and> s' \<in> {s. slot_'_update (\<lambda>_. cte_Ptr slot) s \<in> UNIV \<inter> \<lbrace>slot = ptr_val \<acute>slot\<rbrace>} \<inter> ?R'9 proof (prove)
goal (4 subgoals):
 1. \<And>err rv' err'. \<lbrakk>ccap_relation cp cap; rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; syscall_error_rel err rv' err'\<rbrakk> \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. ?QE9 err \<sigma> \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} Cond UNIV (\<acute>ret__unsigned :== CALL cap_untyped_cap_get_capFreeIndex_'proc(cap);;
\<acute>freeIndex :== \<acute>ret__unsigned;;
\<acute>reset :== SCAST(32 signed \<rightarrow> 32) false) (\<acute>freeIndex :== 0;;
\<acute>reset :== SCAST(32 signed \<rightarrow> 32) true) {s. \<exists>(rv, \<sigma>')\<in>fst (return (Inr False) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> (intr_and_se_rel \<currency> (\<lambda>r (fi, r'). r' = from_bool r \<and> (case r of True \<Rightarrow> fi = 0 | False \<Rightarrow> capFreeIndex cp = unat (fi << 4)))) rv (liftxf errstate (K (SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)) id (\<lambda>s. (freeIndex_' s, reset_' s)) s)}
 2. ccap_relation cp cap \<Longrightarrow> \<lbrace>?R9\<rbrace> ensureNoChildren slot \<lbrace>?Q9\<rbrace>, \<lbrace>?QE9\<rbrace>
 3. ccap_relation cp cap \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'9 \<acute>status :== CALL ensureNoChildren_'proc(cte_Ptr slot) {s. (\<forall>rv'. id (status_' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> dc rv' (undefined (status_' s)) \<longrightarrow> s \<in> UNIV) \<and> (\<forall>ft. id (status_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> syscall_error_rel ft (id (status_' s)) (errstate s) \<longrightarrow> s \<in> UNIV)}
 4. \<And>s s'. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>cte. cteCap cte = cp \<and> isUntypedCap cp) slot and valid_objs' and valid_mdb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>s. valid_objs' s \<and> valid_mdb' s) and ?R9) s \<and> s' \<in> {s. slot_'_update (\<lambda>_. cte_Ptr slot) s \<in> UNIV \<inter> \<lbrace>slot = ptr_val \<acute>slot\<rbrace>} \<inter> ?R'9 proof (prove)
goal (4 subgoals):
 1. \<And>err rv' err' \<sigma>. \<lbrakk>ccap_relation cp cap; rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; syscall_error_rel err rv' err'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> {s. ?QE9 err \<sigma> \<and> (\<sigma>, s) \<in> rf_sr} Cond UNIV (\<acute>ret__unsigned :== CALL cap_untyped_cap_get_capFreeIndex_'proc(cap);;
\<acute>freeIndex :== \<acute>ret__unsigned;;
\<acute>reset :== SCAST(32 signed \<rightarrow> 32) false) (\<acute>freeIndex :== 0;;
\<acute>reset :== SCAST(32 signed \<rightarrow> 32) true) {s. (\<sigma>, s) \<in> rf_sr \<and> reset_' s = SCAST(32 signed \<rightarrow> 32) false \<and> capFreeIndex cp = unat (freeIndex_' s << 4)}
 2. ccap_relation cp cap \<Longrightarrow> \<lbrace>?R9\<rbrace> ensureNoChildren slot \<lbrace>?Q9\<rbrace>, \<lbrace>?QE9\<rbrace>
 3. ccap_relation cp cap \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'9 \<acute>status :== CALL ensureNoChildren_'proc(cte_Ptr slot) {s. (\<forall>rv'. id (status_' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> dc rv' (undefined (status_' s)) \<longrightarrow> s \<in> UNIV) \<and> (\<forall>ft. id (status_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> syscall_error_rel ft (id (status_' s)) (errstate s) \<longrightarrow> s \<in> UNIV)}
 4. \<And>s s'. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>cte. cteCap cte = cp \<and> isUntypedCap cp) slot and valid_objs' and valid_mdb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>s. valid_objs' s \<and> valid_mdb' s) and ?R9) s \<and> s' \<in> {s. slot_'_update (\<lambda>_. cte_Ptr slot) s \<in> UNIV \<inter> \<lbrace>slot = ptr_val \<acute>slot\<rbrace>} \<inter> ?R'9 proof (prove)
goal (5 subgoals):
 1. \<And>err rv' err' \<sigma>. \<lbrakk>ccap_relation cp cap; rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; syscall_error_rel err rv' err'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?P'165 err rv' err' \<sigma>) Cond UNIV (\<acute>ret__unsigned :== CALL cap_untyped_cap_get_capFreeIndex_'proc(cap);;
\<acute>freeIndex :== \<acute>ret__unsigned;;
\<acute>reset :== SCAST(32 signed \<rightarrow> 32) false) (\<acute>freeIndex :== 0;;
\<acute>reset :== SCAST(32 signed \<rightarrow> 32) true) {s. (\<sigma>, s) \<in> rf_sr \<and> reset_' s = SCAST(32 signed \<rightarrow> 32) false \<and> capFreeIndex cp = unat (freeIndex_' s << 4)}
 2. \<And>err rv' err' \<sigma>. \<lbrakk>ccap_relation cp cap; rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; syscall_error_rel err rv' err'\<rbrakk> \<Longrightarrow> {s. ?QE9 err \<sigma> \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> ?P'165 err rv' err' \<sigma>
 3. ccap_relation cp cap \<Longrightarrow> \<lbrace>?R9\<rbrace> ensureNoChildren slot \<lbrace>?Q9\<rbrace>, \<lbrace>?QE9\<rbrace>
 4. ccap_relation cp cap \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'9 \<acute>status :== CALL ensureNoChildren_'proc(cte_Ptr slot) {s. (\<forall>rv'. id (status_' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> dc rv' (undefined (status_' s)) \<longrightarrow> s \<in> UNIV) \<and> (\<forall>ft. id (status_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> syscall_error_rel ft (id (status_' s)) (errstate s) \<longrightarrow> s \<in> UNIV)}
 5. \<And>s s'. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>cte. cteCap cte = cp \<and> isUntypedCap cp) slot and valid_objs' and valid_mdb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>s. valid_objs' s \<and> valid_mdb' s) and ?R9) s \<and> s' \<in> {s. slot_'_update (\<lambda>_. cte_Ptr slot) s \<in> UNIV \<inter> \<lbrace>slot = ptr_val \<acute>slot\<rbrace>} \<inter> ?R'9 proof (prove)
goal (4 subgoals):
 1. \<And>err rv' err' \<sigma>. \<lbrakk>ccap_relation cp cap; rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; syscall_error_rel err rv' err'\<rbrakk> \<Longrightarrow> {s. ?QE9 err \<sigma> \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. (True \<longrightarrow> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> (\<forall>t. ret__unsigned_' t = capFreeIndex_CL (cap_untyped_cap_lift cap) \<longrightarrow> (\<sigma>, reset_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) (freeIndex_'_update (\<lambda>_. capFreeIndex_CL (cap_untyped_cap_lift cap)) (s\<lparr>ret__unsigned_' := capFreeIndex_CL (cap_untyped_cap_lift cap)\<rparr>))) \<in> rf_sr \<and> capFreeIndex cp = unat (capFreeIndex_CL (cap_untyped_cap_lift cap) << 4))) \<and> (\<not> True \<longrightarrow> (\<sigma>, reset_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) (freeIndex_'_update (\<lambda>_. 0) s)) \<in> rf_sr \<and> SCAST(32 signed \<rightarrow> 32) true = SCAST(32 signed \<rightarrow> 32) false \<and> capFreeIndex cp = unat (0 << 4))}
 2. ccap_relation cp cap \<Longrightarrow> \<lbrace>?R9\<rbrace> ensureNoChildren slot \<lbrace>?Q9\<rbrace>, \<lbrace>?QE9\<rbrace>
 3. ccap_relation cp cap \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'9 \<acute>status :== CALL ensureNoChildren_'proc(cte_Ptr slot) {s. (\<forall>rv'. id (status_' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> dc rv' (undefined (status_' s)) \<longrightarrow> s \<in> UNIV) \<and> (\<forall>ft. id (status_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> syscall_error_rel ft (id (status_' s)) (errstate s) \<longrightarrow> s \<in> UNIV)}
 4. \<And>s s'. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>cte. cteCap cte = cp \<and> isUntypedCap cp) slot and valid_objs' and valid_mdb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>s. valid_objs' s \<and> valid_mdb' s) and ?R9) s \<and> s' \<in> {s. slot_'_update (\<lambda>_. cte_Ptr slot) s \<in> UNIV \<inter> \<lbrace>slot = ptr_val \<acute>slot\<rbrace>} \<inter> ?R'9 proof (prove)
goal (4 subgoals):
 1. \<And>err rv' err' \<sigma> x. \<lbrakk>ccap_relation cp cap; rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; syscall_error_rel err rv' err'; ?QE9 err \<sigma>; (\<sigma>, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> ((\<exists>t. ret__unsigned_' t = capFreeIndex_CL (cap_untyped_cap_lift cap)) \<longrightarrow> capFreeIndex cp = unat (capFreeIndex_CL (cap_untyped_cap_lift cap) << 4))
 2. ccap_relation cp cap \<Longrightarrow> \<lbrace>?R9\<rbrace> ensureNoChildren slot \<lbrace>?Q9\<rbrace>, \<lbrace>?QE9\<rbrace>
 3. ccap_relation cp cap \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'9 \<acute>status :== CALL ensureNoChildren_'proc(cte_Ptr slot) {s. (\<forall>rv'. id (status_' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> dc rv' (undefined (status_' s)) \<longrightarrow> s \<in> UNIV) \<and> (\<forall>ft. id (status_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> syscall_error_rel ft (id (status_' s)) (errstate s) \<longrightarrow> s \<in> UNIV)}
 4. \<And>s s'. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>cte. cteCap cte = cp \<and> isUntypedCap cp) slot and valid_objs' and valid_mdb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>s. valid_objs' s \<and> valid_mdb' s) and ?R9) s \<and> s' \<in> {s. slot_'_update (\<lambda>_. cte_Ptr slot) s \<in> UNIV \<inter> \<lbrace>slot = ptr_val \<acute>slot\<rbrace>} \<inter> ?R'9 proof (prove)
goal (5 subgoals):
 1. \<And>err rv' err' \<sigma> x. \<lbrakk>ccap_relation cp cap; rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; syscall_error_rel err rv' err'; ?QE9 err \<sigma>; (\<sigma>, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap
 2. \<And>err rv' err' \<sigma> x. \<lbrakk>ccap_relation cp cap; rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; syscall_error_rel err rv' err'; ?QE9 err \<sigma>; (\<sigma>, x) \<in> rf_sr; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap\<rbrakk> \<Longrightarrow> (\<exists>t. ret__unsigned_' t = capFreeIndex_CL (cap_untyped_cap_lift cap)) \<longrightarrow> capFreeIndex cp = unat (capFreeIndex_CL (cap_untyped_cap_lift cap) << 4)
 3. ccap_relation cp cap \<Longrightarrow> \<lbrace>?R9\<rbrace> ensureNoChildren slot \<lbrace>?Q9\<rbrace>, \<lbrace>?QE9\<rbrace>
 4. ccap_relation cp cap \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'9 \<acute>status :== CALL ensureNoChildren_'proc(cte_Ptr slot) {s. (\<forall>rv'. id (status_' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> dc rv' (undefined (status_' s)) \<longrightarrow> s \<in> UNIV) \<and> (\<forall>ft. id (status_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> syscall_error_rel ft (id (status_' s)) (errstate s) \<longrightarrow> s \<in> UNIV)}
 5. \<And>s s'. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>cte. cteCap cte = cp \<and> isUntypedCap cp) slot and valid_objs' and valid_mdb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>s. valid_objs' s \<and> valid_mdb' s) and ?R9) s \<and> s' \<in> {s. slot_'_update (\<lambda>_. cte_Ptr slot) s \<in> UNIV \<inter> \<lbrace>slot = ptr_val \<acute>slot\<rbrace>} \<inter> ?R'9 proof (prove)
goal (5 subgoals):
 1. \<And>err rv' err' \<sigma> x. \<lbrakk>ccap_relation cp cap; rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; syscall_error_rel err rv' err'; ?QE9 err \<sigma>; (\<sigma>, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> isUntypedCap cp
 2. \<And>err rv' err' \<sigma> x. \<lbrakk>ccap_relation cp cap; rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; syscall_error_rel err rv' err'; ?QE9 err \<sigma>; (\<sigma>, x) \<in> rf_sr; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap\<rbrakk> \<Longrightarrow> (\<exists>t. ret__unsigned_' t = capFreeIndex_CL (cap_untyped_cap_lift cap)) \<longrightarrow> capFreeIndex cp = unat (capFreeIndex_CL (cap_untyped_cap_lift cap) << 4)
 3. ccap_relation cp cap \<Longrightarrow> \<lbrace>?R9\<rbrace> ensureNoChildren slot \<lbrace>?Q9\<rbrace>, \<lbrace>?QE9\<rbrace>
 4. ccap_relation cp cap \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'9 \<acute>status :== CALL ensureNoChildren_'proc(cte_Ptr slot) {s. (\<forall>rv'. id (status_' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> dc rv' (undefined (status_' s)) \<longrightarrow> s \<in> UNIV) \<and> (\<forall>ft. id (status_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> syscall_error_rel ft (id (status_' s)) (errstate s) \<longrightarrow> s \<in> UNIV)}
 5. \<And>s s'. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>cte. cteCap cte = cp \<and> isUntypedCap cp) slot and valid_objs' and valid_mdb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>s. valid_objs' s \<and> valid_mdb' s) and ?R9) s \<and> s' \<in> {s. slot_'_update (\<lambda>_. cte_Ptr slot) s \<in> UNIV \<inter> \<lbrace>slot = ptr_val \<acute>slot\<rbrace>} \<inter> ?R'9 proof (prove)
goal (4 subgoals):
 1. \<And>err rv' err' \<sigma> x. \<lbrakk>ccap_relation cp cap; rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; syscall_error_rel err rv' err'; isUntypedCap cp; (\<sigma>, x) \<in> rf_sr; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap\<rbrakk> \<Longrightarrow> (\<exists>t. ret__unsigned_' t = capFreeIndex_CL (cap_untyped_cap_lift cap)) \<longrightarrow> capFreeIndex cp = unat (capFreeIndex_CL (cap_untyped_cap_lift cap) << 4)
 2. ccap_relation cp cap \<Longrightarrow> \<lbrace>?R9\<rbrace> ensureNoChildren slot \<lbrace>?Q9\<rbrace>, \<lbrace>\<lambda>err \<sigma>. isUntypedCap cp\<rbrace>
 3. ccap_relation cp cap \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'9 \<acute>status :== CALL ensureNoChildren_'proc(cte_Ptr slot) {s. (\<forall>rv'. id (status_' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> dc rv' (undefined (status_' s)) \<longrightarrow> s \<in> UNIV) \<and> (\<forall>ft. id (status_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> syscall_error_rel ft (id (status_' s)) (errstate s) \<longrightarrow> s \<in> UNIV)}
 4. \<And>s s'. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>cte. cteCap cte = cp \<and> isUntypedCap cp) slot and valid_objs' and valid_mdb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>s. valid_objs' s \<and> valid_mdb' s) and ?R9) s \<and> s' \<in> {s. slot_'_update (\<lambda>_. cte_Ptr slot) s \<in> UNIV \<inter> \<lbrace>slot = ptr_val \<acute>slot\<rbrace>} \<inter> ?R'9 proof (prove)
goal (3 subgoals):
 1. ccap_relation cp cap \<Longrightarrow> \<lbrace>?R9\<rbrace> ensureNoChildren slot \<lbrace>?Q9\<rbrace>, \<lbrace>\<lambda>err \<sigma>. isUntypedCap cp\<rbrace>
 2. ccap_relation cp cap \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'9 \<acute>status :== CALL ensureNoChildren_'proc(cte_Ptr slot) {s. (\<forall>rv'. id (status_' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> dc rv' (undefined (status_' s)) \<longrightarrow> s \<in> UNIV) \<and> (\<forall>ft. id (status_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> syscall_error_rel ft (id (status_' s)) (errstate s) \<longrightarrow> s \<in> UNIV)}
 3. \<And>s s'. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>cte. cteCap cte = cp \<and> isUntypedCap cp) slot and valid_objs' and valid_mdb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>s. valid_objs' s \<and> valid_mdb' s) and ?R9) s \<and> s' \<in> {s. slot_'_update (\<lambda>_. cte_Ptr slot) s \<in> UNIV \<inter> \<lbrace>slot = ptr_val \<acute>slot\<rbrace>} \<inter> ?R'9 proof (prove)
goal (2 subgoals):
 1. ccap_relation cp cap \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'9 \<acute>status :== CALL ensureNoChildren_'proc(cte_Ptr slot) {s. (\<forall>rv'. id (status_' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> dc rv' (undefined (status_' s)) \<longrightarrow> s \<in> UNIV) \<and> (\<forall>ft. id (status_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> syscall_error_rel ft (id (status_' s)) (errstate s) \<longrightarrow> s \<in> UNIV)}
 2. \<And>s s'. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>cte. cteCap cte = cp \<and> isUntypedCap cp) slot and valid_objs' and valid_mdb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>s. valid_objs' s \<and> valid_mdb' s) and (\<lambda>s. (descendants_of' slot (ctes_of s) \<noteq> {} \<longrightarrow> isUntypedCap cp) \<and> (descendants_of' slot (ctes_of s) = {} \<longrightarrow> dc () s))) s \<and> s' \<in> {s. slot_'_update (\<lambda>_. cte_Ptr slot) s \<in> UNIV \<inter> \<lbrace>slot = ptr_val \<acute>slot\<rbrace>} \<inter> ?R'9 proof (prove)
goal (2 subgoals):
 1. ccap_relation cp cap \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'9 \<acute>status :== CALL ensureNoChildren_'proc(cte_Ptr slot) UNIV
 2. \<And>s s'. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>cte. cteCap cte = cp \<and> isUntypedCap cp) slot and valid_objs' and valid_mdb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>s. valid_objs' s \<and> valid_mdb' s) and (\<lambda>s. (descendants_of' slot (ctes_of s) \<noteq> {} \<longrightarrow> isUntypedCap cp) \<and> (descendants_of' slot (ctes_of s) = {} \<longrightarrow> dc () s))) s \<and> s' \<in> {s. slot_'_update (\<lambda>_. cte_Ptr slot) s \<in> UNIV \<inter> \<lbrace>slot = ptr_val \<acute>slot\<rbrace>} \<inter> ?R'9 proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>ccap_relation cp cap; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>cte. cteCap cte = cp \<and> isUntypedCap cp) slot and valid_objs' and valid_mdb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>s. valid_objs' s \<and> valid_mdb' s) and (\<lambda>s. (descendants_of' slot (ctes_of s) \<noteq> {} \<longrightarrow> isUntypedCap cp) \<and> (descendants_of' slot (ctes_of s) = {} \<longrightarrow> dc () s))) s \<and> s' \<in> {s. slot_'_update (\<lambda>_. cte_Ptr slot) s \<in> UNIV \<inter> \<lbrace>slot = ptr_val \<acute>slot\<rbrace>} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal:
No subgoals!