theory Finalise_C

lemma cteDeleteOne_ccorres:
  "ccorres dc xfdc
   (invs' and cte_wp_at' (\<lambda>ct. w = -1 \<or> cteCap ct = NullCap
        \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = w)) slot)
   ({s. gs_get_assn cteDeleteOne_'proc (ghost'state_' (globals s)) = w}
        \<inter> {s. slot_' s = Ptr slot}) []
   (cteDeleteOne slot) (Call cteDeleteOne_'proc)" unfolding cteDeleteOne_def apply (rule ccorres_symb_exec_l'
                [OF _ getCTE_inv getCTE_sp empty_fail_getCTE]) apply (cinit' lift: slot_' cong: call_ignore_cong) apply (rule ccorres_move_c_guard_cte) apply csymbr apply (rule ccorres_abstract_cleanup) apply csymbr apply (rule ccorres_gen_asm2,
          erule_tac t="ret__unsigned = scast cap_null_cap"
                and s="cteCap cte = NullCap"
                 in ssubst) apply (clarsimp simp only: when_def unless_def) apply (rule ccorres_cond2[where R=\<top>]) apply (clarsimp simp: Collect_const_mem) apply (rule ccorres_rhs_assoc)+ apply csymbr apply csymbr apply (rule ccorres_Guard_Seq) apply (rule ccorres_basic_srnoop) apply (ctac(no_vcg) add: isFinalCapability_ccorres[where slot=slot]) apply (rule_tac A="invs'  and cte_wp_at' ((=) cte) slot"
                     in ccorres_guard_imp2[where A'=UNIV]) apply (simp add: split_def
                    del: Collect_const) apply (rule ccorres_move_c_guard_cte) apply (ctac(no_vcg) add: finaliseCap_True_standin_ccorres) apply (rule ccorres_assert) apply simp apply csymbr apply (ctac add: emptySlot_ccorres) apply (simp add: pred_conj_def finaliseCapTrue_standin_simple_def) apply (strengthen invs_mdb_strengthen' invs_urz) apply (wp typ_at_lifts isFinalCapability_inv
            | strengthen invs_valid_objs')+ apply (clarsimp simp: irq_opt_relation_def invs_pspace_aligned' cte_wp_at_ctes_of) apply (erule(1) cmap_relationE1 [OF cmap_relation_cte]) apply (clarsimp simp: typ_heap_simps ccte_relation_ccap_relation ccap_relation_NullCap_iff) apply (wp isFinalCapability_inv) apply simp apply (simp del: Collect_const) apply (rule ccorres_return_Skip) apply (clarsimp simp: Collect_const_mem cte_wp_at_ctes_of) apply (erule(1) cmap_relationE1 [OF cmap_relation_cte]) apply (clarsimp simp: typ_heap_simps cap_get_tag_isCap
                 dest!: ccte_relation_ccap_relation) apply (auto simp: o_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (invs' and cte_wp_at' (\<lambda>ct. w = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = w)) slot) (\<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = w\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr slot\<rbrace>) [] (cteDeleteOne slot) (Call cteDeleteOne_'proc) proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (invs' and cte_wp_at' (\<lambda>ct. w = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = w)) slot) (\<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = w\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr slot\<rbrace>) [] (do cte <- getCTE slot;
unless (isNullCap $ cteCap cte) $ do final <- isFinalCapability cte;
(remainder, info) <- finaliseCapTrue_standin (cteCap cte) final;
haskell_assert (capRemovable remainder slot \<and> isNullCap info) $ [];
emptySlot slot capability.NullCap
od
od) (Call cteDeleteOne_'proc) proof (prove)
goal (1 subgoal):
 1. \<And>cte. ccorres dc xfdc (cte_wp_at' (\<lambda>c. c = cte) slot and (invs' and cte_wp_at' (\<lambda>ct. w = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = w)) slot)) (\<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = w\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr slot\<rbrace>) [] (unless (isNullCap $ cteCap cte) $ do final <- isFinalCapability cte;
(remainder, info) <- finaliseCapTrue_standin (cteCap cte) final;
haskell_assert (capRemovable remainder slot \<and> isNullCap info) $ [];
emptySlot slot capability.NullCap
od) (Call cteDeleteOne_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>cte slota. slota = cte_Ptr slot \<Longrightarrow> ccorres dc xfdc (?Q485 cte slota) (?Q'485 cte slota) [SKIP] (unless (cteCap cte = capability.NullCap) (do final <- isFinalCapability cte;
(remainder, info) <- finaliseCapTrue_standin (cteCap cte) final;
y <- assert (capRemovable remainder slot \<and> info = capability.NullCap);
emptySlot slot capability.NullCap
od)) (Guard C_Guard {s. s \<Turnstile>\<^sub>c slota} (\<acute>ret__unsigned :== CALL cap_get_capType_'proc(h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slota\<rightarrow>[''cap_C'']))));;
(\<acute>cap_type :== \<acute>ret__unsigned;;
IF \<acute>cap_type \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap THEN
  lvar_nondet_init final_' final_'_update;;
lvar_nondet_init fc_ret_' fc_ret_'_update;;
Guard GhostStateError \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = - 1 \<or> gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = \<acute>cap_type\<rbrace> (\<acute>globals :== ghost'state_'_update id);;
\<acute>final :== CALL isFinalCapability_'proc(slota);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c slota} (\<acute>fc_ret :== CALL finaliseCap_'proc(h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slota\<rightarrow>[''cap_C''])),\<acute>final,SCAST(32 signed \<rightarrow> 32) true));;
\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
CALL emptySlot_'proc(slota,\<acute>ret__struct_cap_C)
FI))
 2. \<And>cte slota s s'. \<lbrakk>slota = cte_Ptr slot; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. c = cte) slot and (invs' and cte_wp_at' (\<lambda>ct. w = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = w)) slot)) s; s' \<in> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = w\<rbrace>\<rbrakk> \<Longrightarrow> ?Q485 cte slota s \<and> s' \<in> ?Q'485 cte slota proof (prove)
goal (2 subgoals):
 1. \<And>cte slota. slota = cte_Ptr slot \<Longrightarrow> ccorres dc xfdc (?A491 cte slota) (?C'491 cte slota) [SKIP] (unless (cteCap cte = capability.NullCap) (do final <- isFinalCapability cte;
(remainder, info) <- finaliseCapTrue_standin (cteCap cte) final;
y <- assert (capRemovable remainder slot \<and> info = capability.NullCap);
emptySlot slot capability.NullCap
od)) (\<acute>ret__unsigned :== CALL cap_get_capType_'proc(h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slota\<rightarrow>[''cap_C''])));;
(\<acute>cap_type :== \<acute>ret__unsigned;;
IF \<acute>cap_type \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap THEN
  lvar_nondet_init final_' final_'_update;;
lvar_nondet_init fc_ret_' fc_ret_'_update;;
Guard GhostStateError \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = - 1 \<or> gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = \<acute>cap_type\<rbrace> (\<acute>globals :== ghost'state_'_update id);;
\<acute>final :== CALL isFinalCapability_'proc(slota);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c slota} (\<acute>fc_ret :== CALL finaliseCap_'proc(h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slota\<rightarrow>[''cap_C''])),\<acute>final,SCAST(32 signed \<rightarrow> 32) true));;
\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
CALL emptySlot_'proc(slota,\<acute>ret__struct_cap_C)
FI))
 2. \<And>cte slota s s'. \<lbrakk>slota = cte_Ptr slot; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. c = cte) slot and (invs' and cte_wp_at' (\<lambda>ct. w = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = w)) slot)) s; s' \<in> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = w\<rbrace>\<rbrakk> \<Longrightarrow> (?A491 cte slota and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s \<and> s' \<in> ?C'491 cte slota \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>cte slota ret__unsigned. slota = cte_Ptr slot \<Longrightarrow> ccorres dc xfdc (?A491 cte slota) (?G'496 cte slota ret__unsigned \<inter> \<lbrace>ret__unsigned = cap_get_tag (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slota\<rightarrow>[''cap_C''])))\<rbrace>) [SKIP] (unless (cteCap cte = capability.NullCap) (do final <- isFinalCapability cte;
(remainder, info) <- finaliseCapTrue_standin (cteCap cte) final;
y <- assert (capRemovable remainder slot \<and> info = capability.NullCap);
emptySlot slot capability.NullCap
od)) (\<acute>cap_type :== ret__unsigned;;
IF \<acute>cap_type \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap THEN
  lvar_nondet_init final_' final_'_update;;
lvar_nondet_init fc_ret_' fc_ret_'_update;;
Guard GhostStateError \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = - 1 \<or> gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = \<acute>cap_type\<rbrace> (\<acute>globals :== ghost'state_'_update id);;
\<acute>final :== CALL isFinalCapability_'proc(slota);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c slota} (\<acute>fc_ret :== CALL finaliseCap_'proc(h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slota\<rightarrow>[''cap_C''])),\<acute>final,SCAST(32 signed \<rightarrow> 32) true));;
\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
CALL emptySlot_'proc(slota,\<acute>ret__struct_cap_C)
FI)
 2. \<And>cte slota s s'. \<lbrakk>slota = cte_Ptr slot; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. c = cte) slot and (invs' and cte_wp_at' (\<lambda>ct. w = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = w)) slot)) s; s' \<in> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = w\<rbrace>\<rbrakk> \<Longrightarrow> (?A491 cte slota and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s \<and> s' \<in> {s. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slota\<rightarrow>[''cap_C'']))) s)) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> ?G'496 cte slota v} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>cte slota ret__unsigned. slota = cte_Ptr slot \<Longrightarrow> ccorres dc xfdc (?A491 cte slota) (?G'698 cte slota ret__unsigned) [SKIP] (unless (cteCap cte = capability.NullCap) (do final <- isFinalCapability cte;
(remainder, info) <- finaliseCapTrue_standin (cteCap cte) final;
y <- assert (capRemovable remainder slot \<and> info = capability.NullCap);
emptySlot slot capability.NullCap
od)) (\<acute>cap_type :== ret__unsigned;;
IF \<acute>cap_type \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap THEN
  lvar_nondet_init final_' final_'_update;;
lvar_nondet_init fc_ret_' fc_ret_'_update;;
Guard GhostStateError \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = - 1 \<or> gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = \<acute>cap_type\<rbrace> (\<acute>globals :== ghost'state_'_update id);;
\<acute>final :== CALL isFinalCapability_'proc(slota);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c slota} (\<acute>fc_ret :== CALL finaliseCap_'proc(h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slota\<rightarrow>[''cap_C''])),\<acute>final,SCAST(32 signed \<rightarrow> 32) true));;
\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
CALL emptySlot_'proc(slota,\<acute>ret__struct_cap_C)
FI)
 2. \<And>cte slota s s'. \<lbrakk>slota = cte_Ptr slot; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. c = cte) slot and (invs' and cte_wp_at' (\<lambda>ct. w = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = w)) slot)) s; s' \<in> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = w\<rbrace>\<rbrakk> \<Longrightarrow> (?A491 cte slota and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s \<and> s' \<in> {s. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slota\<rightarrow>[''cap_C'']))) s)) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> \<lbrace>v = cap_get_tag (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slota\<rightarrow>[''cap_C''])))\<rbrace> \<longrightarrow> s \<in> ?G'698 cte slota v}} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>cte slota ret__unsigned. slota = cte_Ptr slot \<Longrightarrow> ccorres dc xfdc (?A491 cte slota) (?G'702 cte slota ret__unsigned) [SKIP] (unless (cteCap cte = capability.NullCap) (do final <- isFinalCapability cte;
(remainder, info) <- finaliseCapTrue_standin (cteCap cte) final;
y <- assert (capRemovable remainder slot \<and> info = capability.NullCap);
emptySlot slot capability.NullCap
od)) (IF ret__unsigned \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap THEN
  lvar_nondet_init final_' final_'_update;;
lvar_nondet_init fc_ret_' fc_ret_'_update;;
Guard GhostStateError \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = - 1 \<or> gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = ret__unsigned\<rbrace> (\<acute>globals :== ghost'state_'_update id);;
\<acute>final :== CALL isFinalCapability_'proc(slota);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c slota} (\<acute>fc_ret :== CALL finaliseCap_'proc(h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slota\<rightarrow>[''cap_C''])),\<acute>final,SCAST(32 signed \<rightarrow> 32) true));;
\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
CALL emptySlot_'proc(slota,\<acute>ret__struct_cap_C)
FI)
 2. \<And>cte slota s s'. \<lbrakk>slota = cte_Ptr slot; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. c = cte) slot and (invs' and cte_wp_at' (\<lambda>ct. w = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = w)) slot)) s; s' \<in> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = w\<rbrace>\<rbrakk> \<Longrightarrow> (?A491 cte slota and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s \<and> s' \<in> {s. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slota\<rightarrow>[''cap_C'']))) s)) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> \<lbrace>v = cap_get_tag (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slota\<rightarrow>[''cap_C''])))\<rbrace> \<longrightarrow> s \<in> {s. cap_type_'_update (\<lambda>_. v) s \<in> ?G'702 cte slota v}}} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>cte slota ret__unsigned. slota = cte_Ptr slot \<Longrightarrow> ccorres dc xfdc (?A491 cte slota) (?G'892 cte slota ret__unsigned (cteCap cte = capability.NullCap)) [SKIP] (unless (cteCap cte = capability.NullCap) (do final <- isFinalCapability cte;
a <- finaliseCapTrue_standin (cteCap cte) final;
case a of (remainder, info) \<Rightarrow> do y <- assert (capRemovable remainder slot \<and> info = capability.NullCap);
emptySlot slot capability.NullCap
od
od)) (IF cteCap cte \<noteq> capability.NullCap THEN
  lvar_nondet_init final_' final_'_update;;
lvar_nondet_init fc_ret_' fc_ret_'_update;;
Guard GhostStateError \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = - 1 \<or> gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = ret__unsigned\<rbrace> (\<acute>globals :== ghost'state_'_update id);;
\<acute>final :== CALL isFinalCapability_'proc(slota);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c slota} (\<acute>fc_ret :== CALL finaliseCap_'proc(h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slota\<rightarrow>[''cap_C''])),\<acute>final,SCAST(32 signed \<rightarrow> 32) true));;
\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
CALL emptySlot_'proc(slota,\<acute>ret__struct_cap_C)
FI)
 2. \<And>cte slota s s'. \<lbrakk>slota = cte_Ptr slot; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. c = cte) slot and (invs' and cte_wp_at' (\<lambda>ct. w = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = w)) slot)) s; s' \<in> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = w\<rbrace>\<rbrakk> \<Longrightarrow> (?A491 cte slota and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s \<and> s' \<in> {s. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slota\<rightarrow>[''cap_C'']))) s)) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> \<lbrace>v = cap_get_tag (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slota\<rightarrow>[''cap_C''])))\<rbrace> \<longrightarrow> s \<in> {s. cap_type_'_update (\<lambda>_. v) s \<in> ?G'892 cte slota v (v = SCAST(32 signed \<rightarrow> 32) cap_null_cap) \<inter> \<lbrace>(v = SCAST(32 signed \<rightarrow> 32) cap_null_cap) = (cteCap cte = capability.NullCap)\<rbrace>}}} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>cte slota ret__unsigned. ccorres dc xfdc (?A491 cte (cte_Ptr slot)) (?G'892 cte (cte_Ptr slot) ret__unsigned (cteCap cte = capability.NullCap)) [SKIP] (if cteCap cte \<noteq> capability.NullCap then do final <- isFinalCapability cte;
(remainder, info) <- finaliseCapTrue_standin (cteCap cte) final;
y <- assert (capRemovable remainder slot \<and> info = capability.NullCap);
emptySlot slot capability.NullCap
od else return ()) (IF cteCap cte \<noteq> capability.NullCap THEN
  lvar_nondet_init final_' final_'_update;;
lvar_nondet_init fc_ret_' fc_ret_'_update;;
Guard GhostStateError \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = - 1 \<or> gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = ret__unsigned\<rbrace> (\<acute>globals :== ghost'state_'_update id);;
\<acute>final :== CALL isFinalCapability_'proc(cte_Ptr slot);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr slot} (\<acute>fc_ret :== CALL finaliseCap_'proc(h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C''])),\<acute>final,SCAST(32 signed \<rightarrow> 32) true));;
\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
CALL emptySlot_'proc(cte_Ptr slot,\<acute>ret__struct_cap_C)
FI)
 2. \<And>cte slota s s'. \<lbrakk>slota = cte_Ptr slot; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. c = cte) slot and (invs' and cte_wp_at' (\<lambda>ct. w = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = w)) slot)) s; s' \<in> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = w\<rbrace>\<rbrakk> \<Longrightarrow> (?A491 cte slota and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s \<and> s' \<in> {s. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slota\<rightarrow>[''cap_C'']))) s)) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> \<lbrace>v = cap_get_tag (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slota\<rightarrow>[''cap_C''])))\<rbrace> \<longrightarrow> s \<in> {s. cap_type_'_update (\<lambda>_. v) s \<in> ?G'892 cte slota v (v = SCAST(32 signed \<rightarrow> 32) cap_null_cap) \<inter> \<lbrace>(v = SCAST(32 signed \<rightarrow> 32) cap_null_cap) = (cteCap cte = capability.NullCap)\<rbrace>}}} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>cte slota ret__unsigned. \<forall>s s'. (s, s') \<in> rf_sr \<and> True \<longrightarrow> (cteCap cte \<noteq> capability.NullCap) = (s' \<in> \<lbrace>cteCap cte \<noteq> capability.NullCap\<rbrace>)
 2. \<And>cte slota ret__unsigned. ccorres dc xfdc (?Pt909 cte (cte_Ptr slot)) (?Rt905 cte (cte_Ptr slot) ret__unsigned (cteCap cte = capability.NullCap)) [SKIP] (do final <- isFinalCapability cte;
a <- finaliseCapTrue_standin (cteCap cte) final;
case a of (remainder, info) \<Rightarrow> do y <- assert (capRemovable remainder slot \<and> info = capability.NullCap);
emptySlot slot capability.NullCap
od
od) (lvar_nondet_init final_' final_'_update;;
lvar_nondet_init fc_ret_' fc_ret_'_update;;
Guard GhostStateError \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = - 1 \<or> gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = ret__unsigned\<rbrace> (\<acute>globals :== ghost'state_'_update id);;
\<acute>final :== CALL isFinalCapability_'proc(cte_Ptr slot);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr slot} (\<acute>fc_ret :== CALL finaliseCap_'proc(h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C''])),\<acute>final,SCAST(32 signed \<rightarrow> 32) true));;
\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
CALL emptySlot_'proc(cte_Ptr slot,\<acute>ret__struct_cap_C))
 3. \<And>cte slota ret__unsigned. ccorres dc xfdc (?Pf907 cte (cte_Ptr slot)) (?Rf903 cte (cte_Ptr slot) ret__unsigned (cteCap cte = capability.NullCap)) [SKIP] (return ()) SKIP
 4. \<And>cte slota s s'. \<lbrakk>slota = cte_Ptr slot; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. c = cte) slot and (invs' and cte_wp_at' (\<lambda>ct. w = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = w)) slot)) s; s' \<in> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = w\<rbrace>\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. cteCap cte \<noteq> capability.NullCap \<longrightarrow> ?Pt909 cte slota s) and (\<lambda>s. \<not> cteCap cte \<noteq> capability.NullCap \<longrightarrow> ?Pf907 cte slota s) and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s \<and> s' \<in> {s. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slota\<rightarrow>[''cap_C'']))) s)) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> \<lbrace>v = cap_get_tag (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slota\<rightarrow>[''cap_C''])))\<rbrace> \<longrightarrow> s \<in> {s. cap_type_'_update (\<lambda>_. v) s \<in> {s. (s \<in> \<lbrace>v \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrace> \<longrightarrow> s \<in> ?Rt905 cte slota v (v = SCAST(32 signed \<rightarrow> 32) cap_null_cap)) \<and> (s \<notin> \<lbrace>v \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrace> \<longrightarrow> s \<in> ?Rf903 cte slota v (v = SCAST(32 signed \<rightarrow> 32) cap_null_cap))} \<inter> \<lbrace>(v = SCAST(32 signed \<rightarrow> 32) cap_null_cap) = (cteCap cte = capability.NullCap)\<rbrace>}}} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>cte slota ret__unsigned. ccorres dc xfdc (?Pt909 cte (cte_Ptr slot)) (?Rt905 cte (cte_Ptr slot) ret__unsigned (cteCap cte = capability.NullCap)) [SKIP] (do final <- isFinalCapability cte;
a <- finaliseCapTrue_standin (cteCap cte) final;
case a of (remainder, info) \<Rightarrow> do y <- assert (capRemovable remainder slot \<and> info = capability.NullCap);
emptySlot slot capability.NullCap
od
od) (lvar_nondet_init final_' final_'_update;;
lvar_nondet_init fc_ret_' fc_ret_'_update;;
Guard GhostStateError \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = - 1 \<or> gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = ret__unsigned\<rbrace> (\<acute>globals :== ghost'state_'_update id);;
\<acute>final :== CALL isFinalCapability_'proc(cte_Ptr slot);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr slot} (\<acute>fc_ret :== CALL finaliseCap_'proc(h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C''])),\<acute>final,SCAST(32 signed \<rightarrow> 32) true));;
\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
CALL emptySlot_'proc(cte_Ptr slot,\<acute>ret__struct_cap_C))
 2. \<And>cte slota ret__unsigned. ccorres dc xfdc (?Pf907 cte (cte_Ptr slot)) (?Rf903 cte (cte_Ptr slot) ret__unsigned (cteCap cte = capability.NullCap)) [SKIP] (return ()) SKIP
 3. \<And>cte slota s s'. \<lbrakk>slota = cte_Ptr slot; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. c = cte) slot and (invs' and cte_wp_at' (\<lambda>ct. w = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = w)) slot)) s; s' \<in> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = w\<rbrace>\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. cteCap cte \<noteq> capability.NullCap \<longrightarrow> ?Pt909 cte slota s) and (\<lambda>s. \<not> cteCap cte \<noteq> capability.NullCap \<longrightarrow> ?Pf907 cte slota s) and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s \<and> s' \<in> {s. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slota\<rightarrow>[''cap_C'']))) s)) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> \<lbrace>v = cap_get_tag (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slota\<rightarrow>[''cap_C''])))\<rbrace> \<longrightarrow> s \<in> {s. cap_type_'_update (\<lambda>_. v) s \<in> {s. (s \<in> \<lbrace>v \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrace> \<longrightarrow> s \<in> ?Rt905 cte slota v (v = SCAST(32 signed \<rightarrow> 32) cap_null_cap)) \<and> (s \<notin> \<lbrace>v \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrace> \<longrightarrow> s \<in> ?Rf903 cte slota v (v = SCAST(32 signed \<rightarrow> 32) cap_null_cap))} \<inter> \<lbrace>(v = SCAST(32 signed \<rightarrow> 32) cap_null_cap) = (cteCap cte = capability.NullCap)\<rbrace>}}} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>cte slota ret__unsigned. ccorres dc xfdc (?Pt909 cte (cte_Ptr slot)) (?Rt905 cte (cte_Ptr slot) ret__unsigned (cteCap cte = capability.NullCap)) [SKIP] (do final <- isFinalCapability cte;
a <- finaliseCapTrue_standin (cteCap cte) final;
case a of (remainder, info) \<Rightarrow> do y <- assert (capRemovable remainder slot \<and> info = capability.NullCap);
emptySlot slot capability.NullCap
od
od) (lvar_nondet_init final_' final_'_update;;
(lvar_nondet_init fc_ret_' fc_ret_'_update;;
(Guard GhostStateError \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = - 1 \<or> gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = ret__unsigned\<rbrace> (\<acute>globals :== ghost'state_'_update id);;
(\<acute>final :== CALL isFinalCapability_'proc(cte_Ptr slot);;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr slot} (\<acute>fc_ret :== CALL finaliseCap_'proc(h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C''])),\<acute>final,SCAST(32 signed \<rightarrow> 32) true));;
(\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
CALL emptySlot_'proc(cte_Ptr slot,\<acute>ret__struct_cap_C)))))))
 2. \<And>cte slota ret__unsigned. ccorres dc xfdc (?Pf907 cte (cte_Ptr slot)) (?Rf903 cte (cte_Ptr slot) ret__unsigned (cteCap cte = capability.NullCap)) [SKIP] (return ()) SKIP
 3. \<And>cte slota s s'. \<lbrakk>slota = cte_Ptr slot; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. c = cte) slot and (invs' and cte_wp_at' (\<lambda>ct. w = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = w)) slot)) s; s' \<in> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = w\<rbrace>\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. cteCap cte \<noteq> capability.NullCap \<longrightarrow> ?Pt909 cte slota s) and (\<lambda>s. \<not> cteCap cte \<noteq> capability.NullCap \<longrightarrow> ?Pf907 cte slota s) and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s \<and> s' \<in> {s. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slota\<rightarrow>[''cap_C'']))) s)) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> \<lbrace>v = cap_get_tag (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slota\<rightarrow>[''cap_C''])))\<rbrace> \<longrightarrow> s \<in> {s. cap_type_'_update (\<lambda>_. v) s \<in> {s. (s \<in> \<lbrace>v \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrace> \<longrightarrow> s \<in> ?Rt905 cte slota v (v = SCAST(32 signed \<rightarrow> 32) cap_null_cap)) \<and> (s \<notin> \<lbrace>v \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrace> \<longrightarrow> s \<in> ?Rf903 cte slota v (v = SCAST(32 signed \<rightarrow> 32) cap_null_cap))} \<inter> \<lbrace>(v = SCAST(32 signed \<rightarrow> 32) cap_null_cap) = (cteCap cte = capability.NullCap)\<rbrace>}}} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>cte slota ret__unsigned. ccorres dc xfdc (?Pt909 cte (cte_Ptr slot)) (?G'941 cte (cte_Ptr slot) ret__unsigned (cteCap cte = capability.NullCap)) [SKIP] (do final <- isFinalCapability cte;
(remainder, info) <- finaliseCapTrue_standin (cteCap cte) final;
y <- assert (capRemovable remainder slot \<and> info = capability.NullCap);
emptySlot slot capability.NullCap
od) (lvar_nondet_init fc_ret_' fc_ret_'_update;;
(Guard GhostStateError \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = - 1 \<or> gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = ret__unsigned\<rbrace> (\<acute>globals :== ghost'state_'_update id);;
(\<acute>final :== CALL isFinalCapability_'proc(cte_Ptr slot);;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr slot} (\<acute>fc_ret :== CALL finaliseCap_'proc(h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C''])),\<acute>final,SCAST(32 signed \<rightarrow> 32) true));;
(\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
CALL emptySlot_'proc(cte_Ptr slot,\<acute>ret__struct_cap_C))))))
 2. \<And>cte slota ret__unsigned. ccorres dc xfdc (?Pf907 cte (cte_Ptr slot)) (?Rf903 cte (cte_Ptr slot) ret__unsigned (cteCap cte = capability.NullCap)) [SKIP] (return ()) SKIP
 3. \<And>cte slota s s'. \<lbrakk>slota = cte_Ptr slot; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. c = cte) slot and (invs' and cte_wp_at' (\<lambda>ct. w = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = w)) slot)) s; s' \<in> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = w\<rbrace>\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. cteCap cte \<noteq> capability.NullCap \<longrightarrow> ?Pt909 cte slota s) and (\<lambda>s. \<not> cteCap cte \<noteq> capability.NullCap \<longrightarrow> ?Pf907 cte slota s) and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s \<and> s' \<in> {s. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slota\<rightarrow>[''cap_C'']))) s)) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> \<lbrace>v = cap_get_tag (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slota\<rightarrow>[''cap_C''])))\<rbrace> \<longrightarrow> s \<in> {s. cap_type_'_update (\<lambda>_. v) s \<in> {s. (s \<in> \<lbrace>v \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrace> \<longrightarrow> s \<in> {s. \<forall>va. final_'_update (\<lambda>a. va) s \<in> ?G'941 cte slota v (v = SCAST(32 signed \<rightarrow> 32) cap_null_cap)}) \<and> (s \<notin> \<lbrace>v \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrace> \<longrightarrow> s \<in> ?Rf903 cte slota v (v = SCAST(32 signed \<rightarrow> 32) cap_null_cap))} \<inter> \<lbrace>(v = SCAST(32 signed \<rightarrow> 32) cap_null_cap) = (cteCap cte = capability.NullCap)\<rbrace>}}} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>cte slota ret__unsigned. ccorres dc xfdc (?Pt909 cte (cte_Ptr slot)) (?G'960 cte (cte_Ptr slot) ret__unsigned (cteCap cte = capability.NullCap)) [SKIP] (do final <- isFinalCapability cte;
(remainder, info) <- finaliseCapTrue_standin (cteCap cte) final;
y <- assert (capRemovable remainder slot \<and> info = capability.NullCap);
emptySlot slot capability.NullCap
od) (Guard GhostStateError \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = - 1 \<or> gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = ret__unsigned\<rbrace> (\<acute>globals :== ghost'state_'_update id);;
(\<acute>final :== CALL isFinalCapability_'proc(cte_Ptr slot);;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr slot} (\<acute>fc_ret :== CALL finaliseCap_'proc(h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C''])),\<acute>final,SCAST(32 signed \<rightarrow> 32) true));;
(\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
CALL emptySlot_'proc(cte_Ptr slot,\<acute>ret__struct_cap_C)))))
 2. \<And>cte slota ret__unsigned. ccorres dc xfdc (?Pf907 cte (cte_Ptr slot)) (?Rf903 cte (cte_Ptr slot) ret__unsigned (cteCap cte = capability.NullCap)) [SKIP] (return ()) SKIP
 3. \<And>cte slota s s'. \<lbrakk>slota = cte_Ptr slot; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. c = cte) slot and (invs' and cte_wp_at' (\<lambda>ct. w = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = w)) slot)) s; s' \<in> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = w\<rbrace>\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. cteCap cte \<noteq> capability.NullCap \<longrightarrow> ?Pt909 cte slota s) and (\<lambda>s. \<not> cteCap cte \<noteq> capability.NullCap \<longrightarrow> ?Pf907 cte slota s) and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s \<and> s' \<in> {s. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slota\<rightarrow>[''cap_C'']))) s)) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> \<lbrace>v = cap_get_tag (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slota\<rightarrow>[''cap_C''])))\<rbrace> \<longrightarrow> s \<in> {s. cap_type_'_update (\<lambda>_. v) s \<in> {s. (s \<in> \<lbrace>v \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrace> \<longrightarrow> s \<in> {s. \<forall>va. final_'_update (\<lambda>a. va) s \<in> {s. \<forall>va. fc_ret_'_update (\<lambda>_. va) s \<in> ?G'960 cte slota v (v = SCAST(32 signed \<rightarrow> 32) cap_null_cap)}}) \<and> (s \<notin> \<lbrace>v \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrace> \<longrightarrow> s \<in> ?Rf903 cte slota v (v = SCAST(32 signed \<rightarrow> 32) cap_null_cap))} \<inter> \<lbrace>(v = SCAST(32 signed \<rightarrow> 32) cap_null_cap) = (cteCap cte = capability.NullCap)\<rbrace>}}} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>cte slota ret__unsigned. ccorres dc xfdc (?Pt909 cte (cte_Ptr slot)) (?C'973 cte (cte_Ptr slot) ret__unsigned (cteCap cte = capability.NullCap)) [SKIP] (do final <- isFinalCapability cte;
(remainder, info) <- finaliseCapTrue_standin (cteCap cte) final;
y <- assert (capRemovable remainder slot \<and> info = capability.NullCap);
emptySlot slot capability.NullCap
od) (\<acute>globals :== ghost'state_'_update id;;
(\<acute>final :== CALL isFinalCapability_'proc(cte_Ptr slot);;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr slot} (\<acute>fc_ret :== CALL finaliseCap_'proc(h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C''])),\<acute>final,SCAST(32 signed \<rightarrow> 32) true));;
(\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
CALL emptySlot_'proc(cte_Ptr slot,\<acute>ret__struct_cap_C)))))
 2. \<And>cte slota ret__unsigned. ccorres dc xfdc (?Pf907 cte (cte_Ptr slot)) (?Rf903 cte (cte_Ptr slot) ret__unsigned (cteCap cte = capability.NullCap)) [SKIP] (return ()) SKIP
 3. \<And>cte slota s s'. \<lbrakk>slota = cte_Ptr slot; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. c = cte) slot and (invs' and cte_wp_at' (\<lambda>ct. w = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = w)) slot)) s; s' \<in> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = w\<rbrace>\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. cteCap cte \<noteq> capability.NullCap \<longrightarrow> ?Pt909 cte slota s) and (\<lambda>s. \<not> cteCap cte \<noteq> capability.NullCap \<longrightarrow> ?Pf907 cte slota s) and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s \<and> s' \<in> {s. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slota\<rightarrow>[''cap_C'']))) s)) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> \<lbrace>v = cap_get_tag (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slota\<rightarrow>[''cap_C''])))\<rbrace> \<longrightarrow> s \<in> {s. cap_type_'_update (\<lambda>_. v) s \<in> {s. (s \<in> \<lbrace>v \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrace> \<longrightarrow> s \<in> {s. \<forall>va. final_'_update (\<lambda>a. va) s \<in> {s. \<forall>va. fc_ret_'_update (\<lambda>_. va) s \<in> ?C'973 cte slota v (v = SCAST(32 signed \<rightarrow> 32) cap_null_cap) \<inter> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = - 1 \<or> gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = v\<rbrace>}}) \<and> (s \<notin> \<lbrace>v \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrace> \<longrightarrow> s \<in> ?Rf903 cte slota v (v = SCAST(32 signed \<rightarrow> 32) cap_null_cap))} \<inter> \<lbrace>(v = SCAST(32 signed \<rightarrow> 32) cap_null_cap) = (cteCap cte = capability.NullCap)\<rbrace>}}} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>cte slota ret__unsigned. ccorres dc xfdc (?Pt909 cte (cte_Ptr slot)) (?C'973 cte (cte_Ptr slot) ret__unsigned (cteCap cte = capability.NullCap)) [SKIP] (do final <- isFinalCapability cte;
(remainder, info) <- finaliseCapTrue_standin (cteCap cte) final;
y <- assert (capRemovable remainder slot \<and> info = capability.NullCap);
emptySlot slot capability.NullCap
od) (\<acute>final :== CALL isFinalCapability_'proc(cte_Ptr slot);;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr slot} (\<acute>fc_ret :== CALL finaliseCap_'proc(h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C''])),\<acute>final,SCAST(32 signed \<rightarrow> 32) true));;
(\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
CALL emptySlot_'proc(cte_Ptr slot,\<acute>ret__struct_cap_C))))
 2. \<And>cte slota ret__unsigned s'. globals (globals_update (ghost'state_'_update id) s') = globals s'
 3. \<And>cte slota ret__unsigned s'. s' \<in> ?C'973 cte (cte_Ptr slot) ret__unsigned (cteCap cte = capability.NullCap) \<Longrightarrow> globals_update (ghost'state_'_update id) s' \<in> ?C'973 cte (cte_Ptr slot) ret__unsigned (cteCap cte = capability.NullCap)
 4. \<And>cte slota ret__unsigned. ccorres dc xfdc (?Pf907 cte (cte_Ptr slot)) (?Rf903 cte (cte_Ptr slot) ret__unsigned (cteCap cte = capability.NullCap)) [SKIP] (return ()) SKIP
 5. \<And>cte slota s s'. \<lbrakk>slota = cte_Ptr slot; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. c = cte) slot and (invs' and cte_wp_at' (\<lambda>ct. w = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = w)) slot)) s; s' \<in> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = w\<rbrace>\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. cteCap cte \<noteq> capability.NullCap \<longrightarrow> ?Pt909 cte slota s) and (\<lambda>s. \<not> cteCap cte \<noteq> capability.NullCap \<longrightarrow> ?Pf907 cte slota s) and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s \<and> s' \<in> {s. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slota\<rightarrow>[''cap_C'']))) s)) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> \<lbrace>v = cap_get_tag (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slota\<rightarrow>[''cap_C''])))\<rbrace> \<longrightarrow> s \<in> {s. cap_type_'_update (\<lambda>_. v) s \<in> {s. (s \<in> \<lbrace>v \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrace> \<longrightarrow> s \<in> {s. \<forall>va. final_'_update (\<lambda>a. va) s \<in> {s. \<forall>va. fc_ret_'_update (\<lambda>_. va) s \<in> ?C'973 cte slota v (v = SCAST(32 signed \<rightarrow> 32) cap_null_cap) \<inter> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = - 1 \<or> gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = v\<rbrace>}}) \<and> (s \<notin> \<lbrace>v \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrace> \<longrightarrow> s \<in> ?Rf903 cte slota v (v = SCAST(32 signed \<rightarrow> 32) cap_null_cap))} \<inter> \<lbrace>(v = SCAST(32 signed \<rightarrow> 32) cap_null_cap) = (cteCap cte = capability.NullCap)\<rbrace>}}} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>cte slota ret__unsigned rv final. ((=) \<circ> from_bool) rv final \<Longrightarrow> ccorres dc xfdc (?Q987 cte slota ret__unsigned rv) (?Q'1001 cte ret__unsigned rv final) [SKIP] (do (remainder, info) <- finaliseCapTrue_standin (cteCap cte) rv;
y <- assert (capRemovable remainder slot \<and> info = capability.NullCap);
emptySlot slot capability.NullCap
od) (Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr slot} (\<acute>fc_ret :== CALL finaliseCap_'proc(h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C''])),final,SCAST(32 signed \<rightarrow> 32) true));;
(\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
CALL emptySlot_'proc(cte_Ptr slot,\<acute>ret__struct_cap_C)))
 2. \<And>cte slota ret__unsigned. \<lbrace>?R995 cte (cte_Ptr slot)\<rbrace> isFinalCapability cte \<lbrace>?Q987 cte slota ret__unsigned\<rbrace>
 3. \<And>cte slota ret__unsigned s'. globals (globals_update (ghost'state_'_update id) s') = globals s'
 4. \<And>cte slota ret__unsigned s'. s' \<in> {s. cte_'_update (\<lambda>_. cte_Ptr slot) s \<in> UNIV \<inter> \<lbrace>\<acute>cte = cte_Ptr slot\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> from_bool) rv (ret__unsigned_long_' t) \<longrightarrow> final_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> ?Q'1000 cte (cte_Ptr slot) ret__unsigned (cteCap cte = capability.NullCap) t rv} \<Longrightarrow> globals_update (ghost'state_'_update id) s' \<in> {s. cte_'_update (\<lambda>_. cte_Ptr slot) s \<in> UNIV \<inter> \<lbrace>\<acute>cte = cte_Ptr slot\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> from_bool) rv (ret__unsigned_long_' t) \<longrightarrow> final_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> ?Q'1000 cte (cte_Ptr slot) ret__unsigned (cteCap cte = capability.NullCap) t rv}
 5. \<And>cte slota ret__unsigned. ccorres dc xfdc (?Pf907 cte (cte_Ptr slot)) (?Rf903 cte (cte_Ptr slot) ret__unsigned (cteCap cte = capability.NullCap)) [SKIP] (return ()) SKIP
 6. \<And>cte slota s s'. \<lbrakk>slota = cte_Ptr slot; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. c = cte) slot and (invs' and cte_wp_at' (\<lambda>ct. w = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = w)) slot)) s; s' \<in> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = w\<rbrace>\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. cteCap cte \<noteq> capability.NullCap \<longrightarrow> (cte_wp_at' ((=) cte) slot and invs' and ?R995 cte slota) s) and (\<lambda>s. \<not> cteCap cte \<noteq> capability.NullCap \<longrightarrow> ?Pf907 cte slota s) and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s \<and> s' \<in> {s. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slota\<rightarrow>[''cap_C'']))) s)) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> \<lbrace>v = cap_get_tag (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slota\<rightarrow>[''cap_C''])))\<rbrace> \<longrightarrow> s \<in> {s. cap_type_'_update (\<lambda>_. v) s \<in> {s. (s \<in> \<lbrace>v \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrace> \<longrightarrow> s \<in> {s. \<forall>va. final_'_update (\<lambda>a. va) s \<in> {s. \<forall>va. fc_ret_'_update (\<lambda>_. va) s \<in> {s. cte_'_update (\<lambda>_. slota) s \<in> UNIV \<inter> \<lbrace>\<acute>cte = slota\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> from_bool) rv (ret__unsigned_long_' t) \<longrightarrow> final_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> ?Q'1000 cte slota v (v = SCAST(32 signed \<rightarrow> 32) cap_null_cap) t rv} \<inter> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = - 1 \<or> gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = v\<rbrace>}}) \<and> (s \<notin> \<lbrace>v \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrace> \<longrightarrow> s \<in> ?Rf903 cte slota v (v = SCAST(32 signed \<rightarrow> 32) cap_null_cap))} \<inter> \<lbrace>(v = SCAST(32 signed \<rightarrow> 32) cap_null_cap) = (cteCap cte = capability.NullCap)\<rbrace>}}} \<inter> \<lbrace>True\<rbrace>
flex-flex pairs:
\<lambda>cte ret__unsigned t rv. ?Q'1001 cte ret__unsigned rv (ret__unsigned_long_' t) \<equiv>\<^sup>? \<lambda>cte ret__unsigned. ?Q'1000 cte (cte_Ptr slot) ret__unsigned (cteCap cte = capability.NullCap) proof (prove)
goal (7 subgoals):
 1. \<And>cte slota ret__unsigned rv final. ((=) \<circ> from_bool) rv final \<Longrightarrow> ccorres dc xfdc (?Q1123 cte slota ret__unsigned rv final) (?Q'1123 cte slota ret__unsigned rv final) [SKIP] (do (remainder, info) <- finaliseCapTrue_standin (cteCap cte) rv;
y <- assert (capRemovable remainder slot \<and> info = capability.NullCap);
emptySlot slot capability.NullCap
od) (Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr slot} (\<acute>fc_ret :== CALL finaliseCap_'proc(h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C''])),final,SCAST(32 signed \<rightarrow> 32) true));;
(\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
CALL emptySlot_'proc(cte_Ptr slot,\<acute>ret__struct_cap_C)))
 2. \<And>cte slota ret__unsigned rv final s s'. \<lbrakk>((=) \<circ> from_bool) rv final; (s, s') \<in> rf_sr; (invs' and cte_wp_at' ((=) cte) slot) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q1123 cte slota ret__unsigned rv final s \<and> s' \<in> ?Q'1123 cte slota ret__unsigned rv final
 3. \<And>cte slota ret__unsigned. \<lbrace>?R995 cte (cte_Ptr slot)\<rbrace> isFinalCapability cte \<lbrace>\<lambda>a. invs' and cte_wp_at' ((=) cte) slot\<rbrace>
 4. \<And>cte slota ret__unsigned s'. globals (globals_update (ghost'state_'_update id) s') = globals s'
 5. \<And>cte slota ret__unsigned s'. s' \<in> {s. cte_'_update (\<lambda>_. cte_Ptr slot) s \<in> UNIV \<inter> \<lbrace>\<acute>cte = cte_Ptr slot\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> from_bool) rv (ret__unsigned_long_' t) \<longrightarrow> final_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV} \<Longrightarrow> globals_update (ghost'state_'_update id) s' \<in> {s. cte_'_update (\<lambda>_. cte_Ptr slot) s \<in> UNIV \<inter> \<lbrace>\<acute>cte = cte_Ptr slot\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> from_bool) rv (ret__unsigned_long_' t) \<longrightarrow> final_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV}
 6. \<And>cte slota ret__unsigned. ccorres dc xfdc (?Pf907 cte (cte_Ptr slot)) (?Rf903 cte (cte_Ptr slot) ret__unsigned (cteCap cte = capability.NullCap)) [SKIP] (return ()) SKIP
 7. \<And>cte slota s s'. \<lbrakk>slota = cte_Ptr slot; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. c = cte) slot and (invs' and cte_wp_at' (\<lambda>ct. w = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = w)) slot)) s; s' \<in> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = w\<rbrace>\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. cteCap cte \<noteq> capability.NullCap \<longrightarrow> (cte_wp_at' ((=) cte) slot and invs' and ?R995 cte slota) s) and (\<lambda>s. \<not> cteCap cte \<noteq> capability.NullCap \<longrightarrow> ?Pf907 cte slota s) and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s \<and> s' \<in> {s. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slota\<rightarrow>[''cap_C'']))) s)) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> \<lbrace>v = cap_get_tag (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slota\<rightarrow>[''cap_C''])))\<rbrace> \<longrightarrow> s \<in> {s. cap_type_'_update (\<lambda>_. v) s \<in> {s. (s \<in> \<lbrace>v \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrace> \<longrightarrow> s \<in> {s. \<forall>va. final_'_update (\<lambda>a. va) s \<in> {s. \<forall>va. fc_ret_'_update (\<lambda>_. va) s \<in> {s. cte_'_update (\<lambda>_. slota) s \<in> UNIV \<inter> \<lbrace>\<acute>cte = slota\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> from_bool) rv (ret__unsigned_long_' t) \<longrightarrow> final_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV} \<inter> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = - 1 \<or> gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = v\<rbrace>}}) \<and> (s \<notin> \<lbrace>v \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrace> \<longrightarrow> s \<in> ?Rf903 cte slota v (v = SCAST(32 signed \<rightarrow> 32) cap_null_cap))} \<inter> \<lbrace>(v = SCAST(32 signed \<rightarrow> 32) cap_null_cap) = (cteCap cte = capability.NullCap)\<rbrace>}}} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>cte slota ret__unsigned rv. ccorres dc xfdc (?Q1123 cte slota ret__unsigned rv (from_bool rv)) (?Q'1123 cte slota ret__unsigned rv (from_bool rv)) [SKIP] (do p <- finaliseCapTrue_standin (cteCap cte) rv;
y <- assert (capRemovable (fst p) slot \<and> snd p = capability.NullCap);
emptySlot slot capability.NullCap
od) (Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr slot} (\<acute>fc_ret :== CALL finaliseCap_'proc(h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C''])),from_bool rv,SCAST(32 signed \<rightarrow> 32) true));;
(\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
CALL emptySlot_'proc(cte_Ptr slot,\<acute>ret__struct_cap_C)))
 2. \<And>cte slota ret__unsigned rv final s s'. \<lbrakk>((=) \<circ> from_bool) rv final; (s, s') \<in> rf_sr; (invs' and cte_wp_at' ((=) cte) slot) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q1123 cte slota ret__unsigned rv final s \<and> s' \<in> ?Q'1123 cte slota ret__unsigned rv final
 3. \<And>cte slota ret__unsigned. \<lbrace>?R995 cte (cte_Ptr slot)\<rbrace> isFinalCapability cte \<lbrace>\<lambda>a. invs' and cte_wp_at' ((=) cte) slot\<rbrace>
 4. \<And>cte slota ret__unsigned s'. globals (globals_update (ghost'state_'_update id) s') = globals s'
 5. \<And>cte slota ret__unsigned s'. s' \<in> {s. cte_'_update (\<lambda>_. cte_Ptr slot) s \<in> UNIV \<inter> \<lbrace>\<acute>cte = cte_Ptr slot\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> from_bool) rv (ret__unsigned_long_' t) \<longrightarrow> final_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV} \<Longrightarrow> globals_update (ghost'state_'_update id) s' \<in> {s. cte_'_update (\<lambda>_. cte_Ptr slot) s \<in> UNIV \<inter> \<lbrace>\<acute>cte = cte_Ptr slot\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> from_bool) rv (ret__unsigned_long_' t) \<longrightarrow> final_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV}
 6. \<And>cte slota ret__unsigned. ccorres dc xfdc (?Pf907 cte (cte_Ptr slot)) (?Rf903 cte (cte_Ptr slot) ret__unsigned (cteCap cte = capability.NullCap)) [SKIP] (return ()) SKIP
 7. \<And>cte slota s s'. \<lbrakk>slota = cte_Ptr slot; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. c = cte) slot and (invs' and cte_wp_at' (\<lambda>ct. w = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = w)) slot)) s; s' \<in> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = w\<rbrace>\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. cteCap cte \<noteq> capability.NullCap \<longrightarrow> (cte_wp_at' ((=) cte) slot and invs' and ?R995 cte slota) s) and (\<lambda>s. \<not> cteCap cte \<noteq> capability.NullCap \<longrightarrow> ?Pf907 cte slota s) and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s \<and> s' \<in> {s. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slota\<rightarrow>[''cap_C'']))) s)) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> \<lbrace>v = cap_get_tag (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slota\<rightarrow>[''cap_C''])))\<rbrace> \<longrightarrow> s \<in> {s. cap_type_'_update (\<lambda>_. v) s \<in> {s. (s \<in> \<lbrace>v \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrace> \<longrightarrow> s \<in> {s. \<forall>va. final_'_update (\<lambda>a. va) s \<in> {s. \<forall>va. fc_ret_'_update (\<lambda>_. va) s \<in> {s. cte_'_update (\<lambda>_. slota) s \<in> UNIV \<inter> \<lbrace>\<acute>cte = slota\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> from_bool) rv (ret__unsigned_long_' t) \<longrightarrow> final_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV} \<inter> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = - 1 \<or> gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = v\<rbrace>}}) \<and> (s \<notin> \<lbrace>v \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrace> \<longrightarrow> s \<in> ?Rf903 cte slota v (v = SCAST(32 signed \<rightarrow> 32) cap_null_cap))} \<inter> \<lbrace>(v = SCAST(32 signed \<rightarrow> 32) cap_null_cap) = (cteCap cte = capability.NullCap)\<rbrace>}}} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>cte slota ret__unsigned rv. ccorres dc xfdc (?A1138 cte slota ret__unsigned rv (from_bool rv)) (?C'1136 cte slota ret__unsigned rv (from_bool rv)) [SKIP] (do p <- finaliseCapTrue_standin (cteCap cte) rv;
y <- assert (capRemovable (fst p) slot \<and> snd p = capability.NullCap);
emptySlot slot capability.NullCap
od) (\<acute>fc_ret :== CALL finaliseCap_'proc(h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C''])),from_bool rv,SCAST(32 signed \<rightarrow> 32) true);;
(\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
CALL emptySlot_'proc(cte_Ptr slot,\<acute>ret__struct_cap_C)))
 2. \<And>cte slota ret__unsigned rv final s s'. \<lbrakk>((=) \<circ> from_bool) rv final; (s, s') \<in> rf_sr; (invs' and cte_wp_at' ((=) cte) slot) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (?A1138 cte slota ret__unsigned rv final and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr slot))) s \<and> s' \<in> ?C'1136 cte slota ret__unsigned rv final \<inter> \<lbrace>True\<rbrace>
 3. \<And>cte slota ret__unsigned. \<lbrace>?R995 cte (cte_Ptr slot)\<rbrace> isFinalCapability cte \<lbrace>\<lambda>a. invs' and cte_wp_at' ((=) cte) slot\<rbrace>
 4. \<And>cte slota ret__unsigned s'. globals (globals_update (ghost'state_'_update id) s') = globals s'
 5. \<And>cte slota ret__unsigned s'. s' \<in> {s. cte_'_update (\<lambda>_. cte_Ptr slot) s \<in> UNIV \<inter> \<lbrace>\<acute>cte = cte_Ptr slot\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> from_bool) rv (ret__unsigned_long_' t) \<longrightarrow> final_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV} \<Longrightarrow> globals_update (ghost'state_'_update id) s' \<in> {s. cte_'_update (\<lambda>_. cte_Ptr slot) s \<in> UNIV \<inter> \<lbrace>\<acute>cte = cte_Ptr slot\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> from_bool) rv (ret__unsigned_long_' t) \<longrightarrow> final_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV}
 6. \<And>cte slota ret__unsigned. ccorres dc xfdc (?Pf907 cte (cte_Ptr slot)) (?Rf903 cte (cte_Ptr slot) ret__unsigned (cteCap cte = capability.NullCap)) [SKIP] (return ()) SKIP
 7. \<And>cte slota s s'. \<lbrakk>slota = cte_Ptr slot; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. c = cte) slot and (invs' and cte_wp_at' (\<lambda>ct. w = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = w)) slot)) s; s' \<in> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = w\<rbrace>\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. cteCap cte \<noteq> capability.NullCap \<longrightarrow> (cte_wp_at' ((=) cte) slot and invs' and ?R995 cte slota) s) and (\<lambda>s. \<not> cteCap cte \<noteq> capability.NullCap \<longrightarrow> ?Pf907 cte slota s) and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s \<and> s' \<in> {s. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slota\<rightarrow>[''cap_C'']))) s)) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> \<lbrace>v = cap_get_tag (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slota\<rightarrow>[''cap_C''])))\<rbrace> \<longrightarrow> s \<in> {s. cap_type_'_update (\<lambda>_. v) s \<in> {s. (s \<in> \<lbrace>v \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrace> \<longrightarrow> s \<in> {s. \<forall>va. final_'_update (\<lambda>a. va) s \<in> {s. \<forall>va. fc_ret_'_update (\<lambda>_. va) s \<in> {s. cte_'_update (\<lambda>_. slota) s \<in> UNIV \<inter> \<lbrace>\<acute>cte = slota\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> from_bool) rv (ret__unsigned_long_' t) \<longrightarrow> final_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV} \<inter> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = - 1 \<or> gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = v\<rbrace>}}) \<and> (s \<notin> \<lbrace>v \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrace> \<longrightarrow> s \<in> ?Rf903 cte slota v (v = SCAST(32 signed \<rightarrow> 32) cap_null_cap))} \<inter> \<lbrace>(v = SCAST(32 signed \<rightarrow> 32) cap_null_cap) = (cteCap cte = capability.NullCap)\<rbrace>}}} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>cte slota ret__unsigned rv rva fc_ret. ccap_relation (fst rva) (remainder_C fc_ret) \<and> ccap_relation (snd rva) (finaliseCap_ret_C.cleanupInfo_C fc_ret) \<Longrightarrow> ccorres dc xfdc (?Q1142 cte slota ret__unsigned rv rva) (?Q'1142 cte slota ret__unsigned rv rva fc_ret) [SKIP] (do y <- assert (capRemovable (fst rva) slot \<and> snd rva = capability.NullCap);
emptySlot slot capability.NullCap
od) (\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
CALL emptySlot_'proc(cte_Ptr slot,\<acute>ret__struct_cap_C))
 2. \<And>cte slota ret__unsigned rv. \<lbrace>?R1151 cte slota ret__unsigned rv (from_bool rv)\<rbrace> finaliseCapTrue_standin (cteCap cte) rv \<lbrace>?Q1142 cte slota ret__unsigned rv\<rbrace>
 3. \<And>cte slota ret__unsigned rv final s s'. \<lbrakk>((=) \<circ> from_bool) rv final; (s, s') \<in> rf_sr; (invs' and cte_wp_at' ((=) cte) slot) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and ?R1151 cte slota ret__unsigned rv final and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr slot))) s \<and> s' \<in> {s. exposed_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) (final_'_update (\<lambda>_. final) (cap_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C'']))) s)) \<in> UNIV \<inter> \<lbrace>ccap_relation (cteCap cte) \<acute>cap\<rbrace> \<inter> \<lbrace>\<acute>final = final\<rbrace> \<inter> \<lbrace>\<acute>exposed = from_bool True\<rbrace>} \<inter> {s'. \<forall>t rva. ccap_relation (fst rva) (remainder_C (ret__struct_finaliseCap_ret_C_' t)) \<and> ccap_relation (snd rva) (finaliseCap_ret_C.cleanupInfo_C (ret__struct_finaliseCap_ret_C_' t)) \<longrightarrow> fc_ret_'_update (\<lambda>_. ret__struct_finaliseCap_ret_C_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> ?Q'1148 cte slota ret__unsigned rv final t rva} \<inter> \<lbrace>True\<rbrace>
 4. \<And>cte slota ret__unsigned. \<lbrace>?R995 cte (cte_Ptr slot)\<rbrace> isFinalCapability cte \<lbrace>\<lambda>a. invs' and cte_wp_at' ((=) cte) slot\<rbrace>
 5. \<And>cte slota ret__unsigned s'. globals (globals_update (ghost'state_'_update id) s') = globals s'
 6. \<And>cte slota ret__unsigned s'. s' \<in> {s. cte_'_update (\<lambda>_. cte_Ptr slot) s \<in> UNIV \<inter> \<lbrace>\<acute>cte = cte_Ptr slot\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> from_bool) rv (ret__unsigned_long_' t) \<longrightarrow> final_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV} \<Longrightarrow> globals_update (ghost'state_'_update id) s' \<in> {s. cte_'_update (\<lambda>_. cte_Ptr slot) s \<in> UNIV \<inter> \<lbrace>\<acute>cte = cte_Ptr slot\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> from_bool) rv (ret__unsigned_long_' t) \<longrightarrow> final_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV}
 7. \<And>cte slota ret__unsigned. ccorres dc xfdc (?Pf907 cte (cte_Ptr slot)) (?Rf903 cte (cte_Ptr slot) ret__unsigned (cteCap cte = capability.NullCap)) [SKIP] (return ()) SKIP
 8. \<And>cte slota s s'. \<lbrakk>slota = cte_Ptr slot; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. c = cte) slot and (invs' and cte_wp_at' (\<lambda>ct. w = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = w)) slot)) s; s' \<in> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = w\<rbrace>\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. cteCap cte \<noteq> capability.NullCap \<longrightarrow> (cte_wp_at' ((=) cte) slot and invs' and ?R995 cte slota) s) and (\<lambda>s. \<not> cteCap cte \<noteq> capability.NullCap \<longrightarrow> ?Pf907 cte slota s) and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s \<and> s' \<in> {s. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slota\<rightarrow>[''cap_C'']))) s)) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> \<lbrace>v = cap_get_tag (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slota\<rightarrow>[''cap_C''])))\<rbrace> \<longrightarrow> s \<in> {s. cap_type_'_update (\<lambda>_. v) s \<in> {s. (s \<in> \<lbrace>v \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrace> \<longrightarrow> s \<in> {s. \<forall>va. final_'_update (\<lambda>a. va) s \<in> {s. \<forall>va. fc_ret_'_update (\<lambda>_. va) s \<in> {s. cte_'_update (\<lambda>_. slota) s \<in> UNIV \<inter> \<lbrace>\<acute>cte = slota\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> from_bool) rv (ret__unsigned_long_' t) \<longrightarrow> final_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV} \<inter> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = - 1 \<or> gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = v\<rbrace>}}) \<and> (s \<notin> \<lbrace>v \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrace> \<longrightarrow> s \<in> ?Rf903 cte slota v (v = SCAST(32 signed \<rightarrow> 32) cap_null_cap))} \<inter> \<lbrace>(v = SCAST(32 signed \<rightarrow> 32) cap_null_cap) = (cteCap cte = capability.NullCap)\<rbrace>}}} \<inter> \<lbrace>True\<rbrace>
flex-flex pairs:
\<lambda>cte slota ret__unsigned rv. ?Q'1148 cte slota ret__unsigned rv (from_bool rv) \<equiv>\<^sup>? \<lambda>cte slota ret__unsigned rv t rva. ?Q'1142 cte slota ret__unsigned rv rva (ret__struct_finaliseCap_ret_C_' t) proof (prove)
goal (8 subgoals):
 1. \<And>cte slota ret__unsigned rv rva fc_ret. \<lbrakk>ccap_relation (fst rva) (remainder_C fc_ret) \<and> ccap_relation (snd rva) (finaliseCap_ret_C.cleanupInfo_C fc_ret); capRemovable (fst rva) slot \<and> snd rva = capability.NullCap\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1142 cte slota ret__unsigned rv rva) (?Q'1142 cte slota ret__unsigned rv rva fc_ret) [SKIP] (emptySlot slot capability.NullCap) (\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
CALL emptySlot_'proc(cte_Ptr slot,\<acute>ret__struct_cap_C))
 2. \<And>cte slota ret__unsigned rv. \<lbrace>?R1151 cte slota ret__unsigned rv (from_bool rv)\<rbrace> finaliseCapTrue_standin (cteCap cte) rv \<lbrace>?Q1142 cte slota ret__unsigned rv\<rbrace>
 3. \<And>cte slota ret__unsigned rv final s s'. \<lbrakk>((=) \<circ> from_bool) rv final; (s, s') \<in> rf_sr; (invs' and cte_wp_at' ((=) cte) slot) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and ?R1151 cte slota ret__unsigned rv final and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr slot))) s \<and> s' \<in> {s. exposed_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) (final_'_update (\<lambda>_. final) (cap_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C'']))) s)) \<in> UNIV \<inter> \<lbrace>ccap_relation (cteCap cte) \<acute>cap\<rbrace> \<inter> \<lbrace>\<acute>final = final\<rbrace> \<inter> \<lbrace>\<acute>exposed = from_bool True\<rbrace>} \<inter> {s'. \<forall>t rva. ccap_relation (fst rva) (remainder_C (ret__struct_finaliseCap_ret_C_' t)) \<and> ccap_relation (snd rva) (finaliseCap_ret_C.cleanupInfo_C (ret__struct_finaliseCap_ret_C_' t)) \<longrightarrow> fc_ret_'_update (\<lambda>_. ret__struct_finaliseCap_ret_C_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> ?Q'1148 cte slota ret__unsigned rv final t rva} \<inter> \<lbrace>True\<rbrace>
 4. \<And>cte slota ret__unsigned. \<lbrace>?R995 cte (cte_Ptr slot)\<rbrace> isFinalCapability cte \<lbrace>\<lambda>a. invs' and cte_wp_at' ((=) cte) slot\<rbrace>
 5. \<And>cte slota ret__unsigned s'. globals (globals_update (ghost'state_'_update id) s') = globals s'
 6. \<And>cte slota ret__unsigned s'. s' \<in> {s. cte_'_update (\<lambda>_. cte_Ptr slot) s \<in> UNIV \<inter> \<lbrace>\<acute>cte = cte_Ptr slot\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> from_bool) rv (ret__unsigned_long_' t) \<longrightarrow> final_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV} \<Longrightarrow> globals_update (ghost'state_'_update id) s' \<in> {s. cte_'_update (\<lambda>_. cte_Ptr slot) s \<in> UNIV \<inter> \<lbrace>\<acute>cte = cte_Ptr slot\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> from_bool) rv (ret__unsigned_long_' t) \<longrightarrow> final_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV}
 7. \<And>cte slota ret__unsigned. ccorres dc xfdc (?Pf907 cte (cte_Ptr slot)) (?Rf903 cte (cte_Ptr slot) ret__unsigned (cteCap cte = capability.NullCap)) [SKIP] (return ()) SKIP
 8. \<And>cte slota s s'. \<lbrakk>slota = cte_Ptr slot; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. c = cte) slot and (invs' and cte_wp_at' (\<lambda>ct. w = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = w)) slot)) s; s' \<in> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = w\<rbrace>\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. cteCap cte \<noteq> capability.NullCap \<longrightarrow> (cte_wp_at' ((=) cte) slot and invs' and ?R995 cte slota) s) and (\<lambda>s. \<not> cteCap cte \<noteq> capability.NullCap \<longrightarrow> ?Pf907 cte slota s) and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s \<and> s' \<in> {s. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slota\<rightarrow>[''cap_C'']))) s)) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> \<lbrace>v = cap_get_tag (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slota\<rightarrow>[''cap_C''])))\<rbrace> \<longrightarrow> s \<in> {s. cap_type_'_update (\<lambda>_. v) s \<in> {s. (s \<in> \<lbrace>v \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrace> \<longrightarrow> s \<in> {s. \<forall>va. final_'_update (\<lambda>a. va) s \<in> {s. \<forall>va. fc_ret_'_update (\<lambda>_. va) s \<in> {s. cte_'_update (\<lambda>_. slota) s \<in> UNIV \<inter> \<lbrace>\<acute>cte = slota\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> from_bool) rv (ret__unsigned_long_' t) \<longrightarrow> final_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV} \<inter> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = - 1 \<or> gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = v\<rbrace>}}) \<and> (s \<notin> \<lbrace>v \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrace> \<longrightarrow> s \<in> ?Rf903 cte slota v (v = SCAST(32 signed \<rightarrow> 32) cap_null_cap))} \<inter> \<lbrace>(v = SCAST(32 signed \<rightarrow> 32) cap_null_cap) = (cteCap cte = capability.NullCap)\<rbrace>}}} \<inter> \<lbrace>True\<rbrace>
flex-flex pairs:
\<lambda>cte slota ret__unsigned rv. ?Q'1148 cte slota ret__unsigned rv (from_bool rv) \<equiv>\<^sup>? \<lambda>cte slota ret__unsigned rv t rva. ?Q'1142 cte slota ret__unsigned rv rva (ret__struct_finaliseCap_ret_C_' t) proof (prove)
goal (8 subgoals):
 1. \<And>cte slota ret__unsigned rv rva fc_ret. \<lbrakk>ccap_relation (fst rva) (remainder_C fc_ret) \<and> ccap_relation capability.NullCap (finaliseCap_ret_C.cleanupInfo_C fc_ret); capRemovable (fst rva) slot \<and> snd rva = capability.NullCap\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1142 cte slota ret__unsigned rv rva) (?Q'1142 cte slota ret__unsigned rv rva fc_ret) [SKIP] (emptySlot slot capability.NullCap) (\<acute>ret__struct_cap_C :== CALL cap_null_cap_new_'proc();;
CALL emptySlot_'proc(cte_Ptr slot,\<acute>ret__struct_cap_C))
 2. \<And>cte slota ret__unsigned rv. \<lbrace>?R1151 cte slota ret__unsigned rv (from_bool rv)\<rbrace> finaliseCapTrue_standin (cteCap cte) rv \<lbrace>?Q1142 cte slota ret__unsigned rv\<rbrace>
 3. \<And>cte slota ret__unsigned rv final s s'. \<lbrakk>((=) \<circ> from_bool) rv final; (s, s') \<in> rf_sr; (invs' and cte_wp_at' ((=) cte) slot) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and ?R1151 cte slota ret__unsigned rv final and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr slot))) s \<and> s' \<in> {s. exposed_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) (final_'_update (\<lambda>_. final) (cap_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C'']))) s)) \<in> UNIV \<inter> \<lbrace>ccap_relation (cteCap cte) \<acute>cap\<rbrace> \<inter> \<lbrace>\<acute>final = final\<rbrace> \<inter> \<lbrace>\<acute>exposed = from_bool True\<rbrace>} \<inter> {s'. \<forall>t rva. ccap_relation (fst rva) (remainder_C (ret__struct_finaliseCap_ret_C_' t)) \<and> ccap_relation (snd rva) (finaliseCap_ret_C.cleanupInfo_C (ret__struct_finaliseCap_ret_C_' t)) \<longrightarrow> fc_ret_'_update (\<lambda>_. ret__struct_finaliseCap_ret_C_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> ?Q'1148 cte slota ret__unsigned rv final t rva} \<inter> \<lbrace>True\<rbrace>
 4. \<And>cte slota ret__unsigned. \<lbrace>?R995 cte (cte_Ptr slot)\<rbrace> isFinalCapability cte \<lbrace>\<lambda>a. invs' and cte_wp_at' ((=) cte) slot\<rbrace>
 5. \<And>cte slota ret__unsigned s'. globals (globals_update (ghost'state_'_update id) s') = globals s'
 6. \<And>cte slota ret__unsigned s'. s' \<in> {s. cte_'_update (\<lambda>_. cte_Ptr slot) s \<in> UNIV \<inter> \<lbrace>\<acute>cte = cte_Ptr slot\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> from_bool) rv (ret__unsigned_long_' t) \<longrightarrow> final_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV} \<Longrightarrow> globals_update (ghost'state_'_update id) s' \<in> {s. cte_'_update (\<lambda>_. cte_Ptr slot) s \<in> UNIV \<inter> \<lbrace>\<acute>cte = cte_Ptr slot\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> from_bool) rv (ret__unsigned_long_' t) \<longrightarrow> final_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV}
 7. \<And>cte slota ret__unsigned. ccorres dc xfdc (?Pf907 cte (cte_Ptr slot)) (?Rf903 cte (cte_Ptr slot) ret__unsigned (cteCap cte = capability.NullCap)) [SKIP] (return ()) SKIP
 8. \<And>cte slota s s'. \<lbrakk>slota = cte_Ptr slot; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. c = cte) slot and (invs' and cte_wp_at' (\<lambda>ct. w = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = w)) slot)) s; s' \<in> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = w\<rbrace>\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. cteCap cte \<noteq> capability.NullCap \<longrightarrow> (cte_wp_at' ((=) cte) slot and invs' and ?R995 cte slota) s) and (\<lambda>s. \<not> cteCap cte \<noteq> capability.NullCap \<longrightarrow> ?Pf907 cte slota s) and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s \<and> s' \<in> {s. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slota\<rightarrow>[''cap_C'']))) s)) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> \<lbrace>v = cap_get_tag (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slota\<rightarrow>[''cap_C''])))\<rbrace> \<longrightarrow> s \<in> {s. cap_type_'_update (\<lambda>_. v) s \<in> {s. (s \<in> \<lbrace>v \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrace> \<longrightarrow> s \<in> {s. \<forall>va. final_'_update (\<lambda>a. va) s \<in> {s. \<forall>va. fc_ret_'_update (\<lambda>_. va) s \<in> {s. cte_'_update (\<lambda>_. slota) s \<in> UNIV \<inter> \<lbrace>\<acute>cte = slota\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> from_bool) rv (ret__unsigned_long_' t) \<longrightarrow> final_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV} \<inter> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = - 1 \<or> gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = v\<rbrace>}}) \<and> (s \<notin> \<lbrace>v \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrace> \<longrightarrow> s \<in> ?Rf903 cte slota v (v = SCAST(32 signed \<rightarrow> 32) cap_null_cap))} \<inter> \<lbrace>(v = SCAST(32 signed \<rightarrow> 32) cap_null_cap) = (cteCap cte = capability.NullCap)\<rbrace>}}} \<inter> \<lbrace>True\<rbrace>
flex-flex pairs:
\<lambda>cte slota ret__unsigned rv. ?Q'1148 cte slota ret__unsigned rv (from_bool rv) \<equiv>\<^sup>? \<lambda>cte slota ret__unsigned rv t rva. ?Q'1142 cte slota ret__unsigned rv rva (ret__struct_finaliseCap_ret_C_' t) proof (prove)
goal (8 subgoals):
 1. \<And>cte slota ret__unsigned rv rva fc_ret ret__struct_cap_C. \<lbrakk>ccap_relation (fst rva) (remainder_C fc_ret) \<and> ccap_relation capability.NullCap (finaliseCap_ret_C.cleanupInfo_C fc_ret); capRemovable (fst rva) slot \<and> snd rva = capability.NullCap; cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q1142 cte slota ret__unsigned rv rva) (?G'1238 cte slota ret__unsigned rv rva fc_ret ret__struct_cap_C) [SKIP] (emptySlot slot capability.NullCap) (CALL emptySlot_'proc(cte_Ptr slot,ret__struct_cap_C))
 2. \<And>cte slota ret__unsigned rv. \<lbrace>?R1151 cte slota ret__unsigned rv (from_bool rv)\<rbrace> finaliseCapTrue_standin (cteCap cte) rv \<lbrace>?Q1142 cte slota ret__unsigned rv\<rbrace>
 3. \<And>cte slota ret__unsigned rv final s s'. \<lbrakk>((=) \<circ> from_bool) rv final; (s, s') \<in> rf_sr; (invs' and cte_wp_at' ((=) cte) slot) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and ?R1151 cte slota ret__unsigned rv final and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr slot))) s \<and> s' \<in> {s. exposed_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) (final_'_update (\<lambda>_. final) (cap_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C'']))) s)) \<in> UNIV \<inter> \<lbrace>ccap_relation (cteCap cte) \<acute>cap\<rbrace> \<inter> \<lbrace>\<acute>final = final\<rbrace> \<inter> \<lbrace>\<acute>exposed = from_bool True\<rbrace>} \<inter> {s'. \<forall>t rva. ccap_relation (fst rva) (remainder_C (ret__struct_finaliseCap_ret_C_' t)) \<and> ccap_relation (snd rva) (finaliseCap_ret_C.cleanupInfo_C (ret__struct_finaliseCap_ret_C_' t)) \<longrightarrow> fc_ret_'_update (\<lambda>_. ret__struct_finaliseCap_ret_C_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. \<forall>v. cap_get_tag v = SCAST(32 signed \<rightarrow> 32) cap_null_cap \<longrightarrow> s\<lparr>ret__struct_cap_C_' := v\<rparr> \<in> ?G'1242 cte slota ret__unsigned rv final t rva v}} \<inter> \<lbrace>True\<rbrace>
 4. \<And>cte slota ret__unsigned. \<lbrace>?R995 cte (cte_Ptr slot)\<rbrace> isFinalCapability cte \<lbrace>\<lambda>a. invs' and cte_wp_at' ((=) cte) slot\<rbrace>
 5. \<And>cte slota ret__unsigned s'. globals (globals_update (ghost'state_'_update id) s') = globals s'
 6. \<And>cte slota ret__unsigned s'. s' \<in> {s. cte_'_update (\<lambda>_. cte_Ptr slot) s \<in> UNIV \<inter> \<lbrace>\<acute>cte = cte_Ptr slot\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> from_bool) rv (ret__unsigned_long_' t) \<longrightarrow> final_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV} \<Longrightarrow> globals_update (ghost'state_'_update id) s' \<in> {s. cte_'_update (\<lambda>_. cte_Ptr slot) s \<in> UNIV \<inter> \<lbrace>\<acute>cte = cte_Ptr slot\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> from_bool) rv (ret__unsigned_long_' t) \<longrightarrow> final_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV}
 7. \<And>cte slota ret__unsigned. ccorres dc xfdc (?Pf907 cte (cte_Ptr slot)) (?Rf903 cte (cte_Ptr slot) ret__unsigned (cteCap cte = capability.NullCap)) [SKIP] (return ()) SKIP
 8. \<And>cte slota s s'. \<lbrakk>slota = cte_Ptr slot; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. c = cte) slot and (invs' and cte_wp_at' (\<lambda>ct. w = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = w)) slot)) s; s' \<in> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = w\<rbrace>\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. cteCap cte \<noteq> capability.NullCap \<longrightarrow> (cte_wp_at' ((=) cte) slot and invs' and ?R995 cte slota) s) and (\<lambda>s. \<not> cteCap cte \<noteq> capability.NullCap \<longrightarrow> ?Pf907 cte slota s) and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s \<and> s' \<in> {s. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slota\<rightarrow>[''cap_C'']))) s)) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> \<lbrace>v = cap_get_tag (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slota\<rightarrow>[''cap_C''])))\<rbrace> \<longrightarrow> s \<in> {s. cap_type_'_update (\<lambda>_. v) s \<in> {s. (s \<in> \<lbrace>v \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrace> \<longrightarrow> s \<in> {s. \<forall>va. final_'_update (\<lambda>a. va) s \<in> {s. \<forall>va. fc_ret_'_update (\<lambda>_. va) s \<in> {s. cte_'_update (\<lambda>_. slota) s \<in> UNIV \<inter> \<lbrace>\<acute>cte = slota\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> from_bool) rv (ret__unsigned_long_' t) \<longrightarrow> final_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV} \<inter> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = - 1 \<or> gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = v\<rbrace>}}) \<and> (s \<notin> \<lbrace>v \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrace> \<longrightarrow> s \<in> ?Rf903 cte slota v (v = SCAST(32 signed \<rightarrow> 32) cap_null_cap))} \<inter> \<lbrace>(v = SCAST(32 signed \<rightarrow> 32) cap_null_cap) = (cteCap cte = capability.NullCap)\<rbrace>}}} \<inter> \<lbrace>True\<rbrace>
flex-flex pairs:
\<lambda>cte slota ret__unsigned rv. ?G'1242 cte slota ret__unsigned rv (from_bool rv) \<equiv>\<^sup>? \<lambda>cte slota ret__unsigned rv t rva. ?G'1238 cte slota ret__unsigned rv rva (ret__struct_finaliseCap_ret_C_' t) proof (prove)
goal (7 subgoals):
 1. \<And>cte slota ret__unsigned rv. \<lbrace>?R1151 cte slota ret__unsigned rv (from_bool rv)\<rbrace> finaliseCapTrue_standin (cteCap cte) rv \<lbrace>\<lambda>a. valid_mdb' and valid_objs' and pspace_aligned' and untyped_ranges_zero'\<rbrace>
 2. \<And>cte slota ret__unsigned rv final s s'. \<lbrakk>((=) \<circ> from_bool) rv final; (s, s') \<in> rf_sr; (invs' and cte_wp_at' ((=) cte) slot) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and ?R1151 cte slota ret__unsigned rv final and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr slot))) s \<and> s' \<in> {s. exposed_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) (final_'_update (\<lambda>_. final) (cap_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C'']))) s)) \<in> UNIV \<inter> \<lbrace>ccap_relation (cteCap cte) \<acute>cap\<rbrace> \<inter> \<lbrace>\<acute>final = final\<rbrace> \<inter> \<lbrace>\<acute>exposed = from_bool True\<rbrace>} \<inter> {s'. \<forall>t rv. ccap_relation (fst rv) (remainder_C (ret__struct_finaliseCap_ret_C_' t)) \<and> ccap_relation (snd rv) (finaliseCap_ret_C.cleanupInfo_C (ret__struct_finaliseCap_ret_C_' t)) \<longrightarrow> fc_ret_'_update (\<lambda>_. ret__struct_finaliseCap_ret_C_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. \<forall>v. cap_get_tag v = SCAST(32 signed \<rightarrow> 32) cap_null_cap \<longrightarrow> s\<lparr>ret__struct_cap_C_' := v\<rparr> \<in> {s. cleanupInfo_'_update (\<lambda>_. v) (slot_'_update (\<lambda>_. cte_Ptr slot) s) \<in> UNIV \<inter> \<lbrace>\<acute>slot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>ccap_relation capability.NullCap \<acute>cleanupInfo \<and> cleanup_info_wf' capability.NullCap\<rbrace>}}} \<inter> \<lbrace>True\<rbrace>
 3. \<And>cte slota ret__unsigned. \<lbrace>?R995 cte (cte_Ptr slot)\<rbrace> isFinalCapability cte \<lbrace>\<lambda>a. invs' and cte_wp_at' ((=) cte) slot\<rbrace>
 4. \<And>cte slota ret__unsigned s'. globals (globals_update (ghost'state_'_update id) s') = globals s'
 5. \<And>cte slota ret__unsigned s'. s' \<in> {s. cte_'_update (\<lambda>_. cte_Ptr slot) s \<in> UNIV \<inter> \<lbrace>\<acute>cte = cte_Ptr slot\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> from_bool) rv (ret__unsigned_long_' t) \<longrightarrow> final_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV} \<Longrightarrow> globals_update (ghost'state_'_update id) s' \<in> {s. cte_'_update (\<lambda>_. cte_Ptr slot) s \<in> UNIV \<inter> \<lbrace>\<acute>cte = cte_Ptr slot\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> from_bool) rv (ret__unsigned_long_' t) \<longrightarrow> final_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV}
 6. \<And>cte slota ret__unsigned. ccorres dc xfdc (?Pf907 cte (cte_Ptr slot)) (?Rf903 cte (cte_Ptr slot) ret__unsigned (cteCap cte = capability.NullCap)) [SKIP] (return ()) SKIP
 7. \<And>cte slota s s'. \<lbrakk>slota = cte_Ptr slot; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. c = cte) slot and (invs' and cte_wp_at' (\<lambda>ct. w = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = w)) slot)) s; s' \<in> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = w\<rbrace>\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. cteCap cte \<noteq> capability.NullCap \<longrightarrow> (cte_wp_at' ((=) cte) slot and invs' and ?R995 cte slota) s) and (\<lambda>s. \<not> cteCap cte \<noteq> capability.NullCap \<longrightarrow> ?Pf907 cte slota s) and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s \<and> s' \<in> {s. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slota\<rightarrow>[''cap_C'']))) s)) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> \<lbrace>v = cap_get_tag (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slota\<rightarrow>[''cap_C''])))\<rbrace> \<longrightarrow> s \<in> {s. cap_type_'_update (\<lambda>_. v) s \<in> {s. (s \<in> \<lbrace>v \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrace> \<longrightarrow> s \<in> {s. \<forall>va. final_'_update (\<lambda>a. va) s \<in> {s. \<forall>va. fc_ret_'_update (\<lambda>_. va) s \<in> {s. cte_'_update (\<lambda>_. slota) s \<in> UNIV \<inter> \<lbrace>\<acute>cte = slota\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> from_bool) rv (ret__unsigned_long_' t) \<longrightarrow> final_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV} \<inter> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = - 1 \<or> gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = v\<rbrace>}}) \<and> (s \<notin> \<lbrace>v \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrace> \<longrightarrow> s \<in> ?Rf903 cte slota v (v = SCAST(32 signed \<rightarrow> 32) cap_null_cap))} \<inter> \<lbrace>(v = SCAST(32 signed \<rightarrow> 32) cap_null_cap) = (cteCap cte = capability.NullCap)\<rbrace>}}} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>cte slota ret__unsigned rv. \<lbrace>?R1151 cte slota ret__unsigned rv (from_bool rv)\<rbrace> global.finaliseCap (cteCap cte) rv True \<lbrace>\<lambda>a b. valid_mdb' b \<and> valid_objs' b \<and> pspace_aligned' b \<and> untyped_ranges_zero' b\<rbrace>
 2. \<And>cte slota ret__unsigned rv final s s'. \<lbrakk>((=) \<circ> from_bool) rv final; (s, s') \<in> rf_sr; (invs' and cte_wp_at' ((=) cte) slot) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and ?R1151 cte slota ret__unsigned rv final and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr slot))) s \<and> s' \<in> {s. exposed_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) (final_'_update (\<lambda>_. final) (cap_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C'']))) s)) \<in> UNIV \<inter> \<lbrace>ccap_relation (cteCap cte) \<acute>cap\<rbrace> \<inter> \<lbrace>\<acute>final = final\<rbrace> \<inter> \<lbrace>\<acute>exposed = from_bool True\<rbrace>} \<inter> {s'. \<forall>t rv. ccap_relation (fst rv) (remainder_C (ret__struct_finaliseCap_ret_C_' t)) \<and> ccap_relation (snd rv) (finaliseCap_ret_C.cleanupInfo_C (ret__struct_finaliseCap_ret_C_' t)) \<longrightarrow> fc_ret_'_update (\<lambda>_. ret__struct_finaliseCap_ret_C_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. \<forall>v. cap_get_tag v = SCAST(32 signed \<rightarrow> 32) cap_null_cap \<longrightarrow> s\<lparr>ret__struct_cap_C_' := v\<rparr> \<in> {s. cleanupInfo_'_update (\<lambda>_. v) (slot_'_update (\<lambda>_. cte_Ptr slot) s) \<in> UNIV \<inter> \<lbrace>\<acute>slot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>ccap_relation capability.NullCap \<acute>cleanupInfo \<and> cleanup_info_wf' capability.NullCap\<rbrace>}}} \<inter> \<lbrace>True\<rbrace>
 3. \<And>cte slota ret__unsigned. \<lbrace>?R995 cte (cte_Ptr slot)\<rbrace> isFinalCapability cte \<lbrace>\<lambda>a. invs' and cte_wp_at' ((=) cte) slot\<rbrace>
 4. \<And>cte slota ret__unsigned s'. globals (globals_update (ghost'state_'_update id) s') = globals s'
 5. \<And>cte slota ret__unsigned s'. s' \<in> {s. cte_'_update (\<lambda>_. cte_Ptr slot) s \<in> UNIV \<inter> \<lbrace>\<acute>cte = cte_Ptr slot\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> from_bool) rv (ret__unsigned_long_' t) \<longrightarrow> final_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV} \<Longrightarrow> globals_update (ghost'state_'_update id) s' \<in> {s. cte_'_update (\<lambda>_. cte_Ptr slot) s \<in> UNIV \<inter> \<lbrace>\<acute>cte = cte_Ptr slot\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> from_bool) rv (ret__unsigned_long_' t) \<longrightarrow> final_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV}
 6. \<And>cte slota ret__unsigned. ccorres dc xfdc (?Pf907 cte (cte_Ptr slot)) (?Rf903 cte (cte_Ptr slot) ret__unsigned (cteCap cte = capability.NullCap)) [SKIP] (return ()) SKIP
 7. \<And>cte slota s s'. \<lbrakk>slota = cte_Ptr slot; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. c = cte) slot and (invs' and cte_wp_at' (\<lambda>ct. w = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = w)) slot)) s; s' \<in> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = w\<rbrace>\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. cteCap cte \<noteq> capability.NullCap \<longrightarrow> (cte_wp_at' ((=) cte) slot and invs' and ?R995 cte slota) s) and (\<lambda>s. \<not> cteCap cte \<noteq> capability.NullCap \<longrightarrow> ?Pf907 cte slota s) and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s \<and> s' \<in> {s. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slota\<rightarrow>[''cap_C'']))) s)) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> \<lbrace>v = cap_get_tag (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slota\<rightarrow>[''cap_C''])))\<rbrace> \<longrightarrow> s \<in> {s. cap_type_'_update (\<lambda>_. v) s \<in> {s. (s \<in> \<lbrace>v \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrace> \<longrightarrow> s \<in> {s. \<forall>va. final_'_update (\<lambda>a. va) s \<in> {s. \<forall>va. fc_ret_'_update (\<lambda>_. va) s \<in> {s. cte_'_update (\<lambda>_. slota) s \<in> UNIV \<inter> \<lbrace>\<acute>cte = slota\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> from_bool) rv (ret__unsigned_long_' t) \<longrightarrow> final_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV} \<inter> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = - 1 \<or> gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = v\<rbrace>}}) \<and> (s \<notin> \<lbrace>v \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrace> \<longrightarrow> s \<in> ?Rf903 cte slota v (v = SCAST(32 signed \<rightarrow> 32) cap_null_cap))} \<inter> \<lbrace>(v = SCAST(32 signed \<rightarrow> 32) cap_null_cap) = (cteCap cte = capability.NullCap)\<rbrace>}}} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>cte slota ret__unsigned rv. \<lbrace>?R1151 cte slota ret__unsigned rv (from_bool rv)\<rbrace> global.finaliseCap (cteCap cte) rv True \<lbrace>\<lambda>r s. invs' s \<and> valid_objs' s \<and> pspace_aligned' s \<and> invs' s\<rbrace>
 2. \<And>cte slota ret__unsigned rv final s s'. \<lbrakk>((=) \<circ> from_bool) rv final; (s, s') \<in> rf_sr; (invs' and cte_wp_at' ((=) cte) slot) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and ?R1151 cte slota ret__unsigned rv final and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr slot))) s \<and> s' \<in> {s. exposed_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) (final_'_update (\<lambda>_. final) (cap_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C'']))) s)) \<in> UNIV \<inter> \<lbrace>ccap_relation (cteCap cte) \<acute>cap\<rbrace> \<inter> \<lbrace>\<acute>final = final\<rbrace> \<inter> \<lbrace>\<acute>exposed = from_bool True\<rbrace>} \<inter> {s'. \<forall>t rv. ccap_relation (fst rv) (remainder_C (ret__struct_finaliseCap_ret_C_' t)) \<and> ccap_relation (snd rv) (finaliseCap_ret_C.cleanupInfo_C (ret__struct_finaliseCap_ret_C_' t)) \<longrightarrow> fc_ret_'_update (\<lambda>_. ret__struct_finaliseCap_ret_C_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. \<forall>v. cap_get_tag v = SCAST(32 signed \<rightarrow> 32) cap_null_cap \<longrightarrow> s\<lparr>ret__struct_cap_C_' := v\<rparr> \<in> {s. cleanupInfo_'_update (\<lambda>_. v) (slot_'_update (\<lambda>_. cte_Ptr slot) s) \<in> UNIV \<inter> \<lbrace>\<acute>slot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>ccap_relation capability.NullCap \<acute>cleanupInfo \<and> cleanup_info_wf' capability.NullCap\<rbrace>}}} \<inter> \<lbrace>True\<rbrace>
 3. \<And>cte slota ret__unsigned. \<lbrace>?R995 cte (cte_Ptr slot)\<rbrace> isFinalCapability cte \<lbrace>\<lambda>a. invs' and cte_wp_at' ((=) cte) slot\<rbrace>
 4. \<And>cte slota ret__unsigned s'. globals (globals_update (ghost'state_'_update id) s') = globals s'
 5. \<And>cte slota ret__unsigned s'. s' \<in> {s. cte_'_update (\<lambda>_. cte_Ptr slot) s \<in> UNIV \<inter> \<lbrace>\<acute>cte = cte_Ptr slot\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> from_bool) rv (ret__unsigned_long_' t) \<longrightarrow> final_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV} \<Longrightarrow> globals_update (ghost'state_'_update id) s' \<in> {s. cte_'_update (\<lambda>_. cte_Ptr slot) s \<in> UNIV \<inter> \<lbrace>\<acute>cte = cte_Ptr slot\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> from_bool) rv (ret__unsigned_long_' t) \<longrightarrow> final_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV}
 6. \<And>cte slota ret__unsigned. ccorres dc xfdc (?Pf907 cte (cte_Ptr slot)) (?Rf903 cte (cte_Ptr slot) ret__unsigned (cteCap cte = capability.NullCap)) [SKIP] (return ()) SKIP
 7. \<And>cte slota s s'. \<lbrakk>slota = cte_Ptr slot; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. c = cte) slot and (invs' and cte_wp_at' (\<lambda>ct. w = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = w)) slot)) s; s' \<in> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = w\<rbrace>\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. cteCap cte \<noteq> capability.NullCap \<longrightarrow> (cte_wp_at' ((=) cte) slot and invs' and ?R995 cte slota) s) and (\<lambda>s. \<not> cteCap cte \<noteq> capability.NullCap \<longrightarrow> ?Pf907 cte slota s) and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s \<and> s' \<in> {s. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slota\<rightarrow>[''cap_C'']))) s)) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> \<lbrace>v = cap_get_tag (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slota\<rightarrow>[''cap_C''])))\<rbrace> \<longrightarrow> s \<in> {s. cap_type_'_update (\<lambda>_. v) s \<in> {s. (s \<in> \<lbrace>v \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrace> \<longrightarrow> s \<in> {s. \<forall>va. final_'_update (\<lambda>a. va) s \<in> {s. \<forall>va. fc_ret_'_update (\<lambda>_. va) s \<in> {s. cte_'_update (\<lambda>_. slota) s \<in> UNIV \<inter> \<lbrace>\<acute>cte = slota\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> from_bool) rv (ret__unsigned_long_' t) \<longrightarrow> final_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV} \<inter> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = - 1 \<or> gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = v\<rbrace>}}) \<and> (s \<notin> \<lbrace>v \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrace> \<longrightarrow> s \<in> ?Rf903 cte slota v (v = SCAST(32 signed \<rightarrow> 32) cap_null_cap))} \<inter> \<lbrace>(v = SCAST(32 signed \<rightarrow> 32) cap_null_cap) = (cteCap cte = capability.NullCap)\<rbrace>}}} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>cte slota ret__unsigned rv final s s'. \<lbrakk>((=) \<circ> from_bool) rv final; (s, s') \<in> rf_sr; (invs' and cte_wp_at' ((=) cte) slot) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and (\<lambda>a. invs' a \<and> invs' a \<and> pspace_aligned' a \<and> invs' a) and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr slot))) s \<and> s' \<in> {s. exposed_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) (final_'_update (\<lambda>_. final) (cap_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C'']))) s)) \<in> UNIV \<inter> \<lbrace>ccap_relation (cteCap cte) \<acute>cap\<rbrace> \<inter> \<lbrace>\<acute>final = final\<rbrace> \<inter> \<lbrace>\<acute>exposed = from_bool True\<rbrace>} \<inter> {s'. \<forall>t rv. ccap_relation (fst rv) (remainder_C (ret__struct_finaliseCap_ret_C_' t)) \<and> ccap_relation (snd rv) (finaliseCap_ret_C.cleanupInfo_C (ret__struct_finaliseCap_ret_C_' t)) \<longrightarrow> fc_ret_'_update (\<lambda>_. ret__struct_finaliseCap_ret_C_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. \<forall>v. cap_get_tag v = SCAST(32 signed \<rightarrow> 32) cap_null_cap \<longrightarrow> s\<lparr>ret__struct_cap_C_' := v\<rparr> \<in> {s. cleanupInfo_'_update (\<lambda>_. v) (slot_'_update (\<lambda>_. cte_Ptr slot) s) \<in> UNIV \<inter> \<lbrace>\<acute>slot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>ccap_relation capability.NullCap \<acute>cleanupInfo \<and> cleanup_info_wf' capability.NullCap\<rbrace>}}} \<inter> \<lbrace>True\<rbrace>
 2. \<And>cte slota ret__unsigned. \<lbrace>?R995 cte (cte_Ptr slot)\<rbrace> isFinalCapability cte \<lbrace>\<lambda>a. invs' and cte_wp_at' ((=) cte) slot\<rbrace>
 3. \<And>cte slota ret__unsigned s'. globals (globals_update (ghost'state_'_update id) s') = globals s'
 4. \<And>cte slota ret__unsigned s'. s' \<in> {s. cte_'_update (\<lambda>_. cte_Ptr slot) s \<in> UNIV \<inter> \<lbrace>\<acute>cte = cte_Ptr slot\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> from_bool) rv (ret__unsigned_long_' t) \<longrightarrow> final_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV} \<Longrightarrow> globals_update (ghost'state_'_update id) s' \<in> {s. cte_'_update (\<lambda>_. cte_Ptr slot) s \<in> UNIV \<inter> \<lbrace>\<acute>cte = cte_Ptr slot\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> from_bool) rv (ret__unsigned_long_' t) \<longrightarrow> final_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV}
 5. \<And>cte slota ret__unsigned. ccorres dc xfdc (?Pf907 cte (cte_Ptr slot)) (?Rf903 cte (cte_Ptr slot) ret__unsigned (cteCap cte = capability.NullCap)) [SKIP] (return ()) SKIP
 6. \<And>cte slota s s'. \<lbrakk>slota = cte_Ptr slot; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. c = cte) slot and (invs' and cte_wp_at' (\<lambda>ct. w = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = w)) slot)) s; s' \<in> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = w\<rbrace>\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. cteCap cte \<noteq> capability.NullCap \<longrightarrow> (cte_wp_at' ((=) cte) slot and invs' and ?R995 cte slota) s) and (\<lambda>s. \<not> cteCap cte \<noteq> capability.NullCap \<longrightarrow> ?Pf907 cte slota s) and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s \<and> s' \<in> {s. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slota\<rightarrow>[''cap_C'']))) s)) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> \<lbrace>v = cap_get_tag (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slota\<rightarrow>[''cap_C''])))\<rbrace> \<longrightarrow> s \<in> {s. cap_type_'_update (\<lambda>_. v) s \<in> {s. (s \<in> \<lbrace>v \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrace> \<longrightarrow> s \<in> {s. \<forall>va. final_'_update (\<lambda>a. va) s \<in> {s. \<forall>va. fc_ret_'_update (\<lambda>_. va) s \<in> {s. cte_'_update (\<lambda>_. slota) s \<in> UNIV \<inter> \<lbrace>\<acute>cte = slota\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> from_bool) rv (ret__unsigned_long_' t) \<longrightarrow> final_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV} \<inter> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = - 1 \<or> gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = v\<rbrace>}}) \<and> (s \<notin> \<lbrace>v \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrace> \<longrightarrow> s \<in> ?Rf903 cte slota v (v = SCAST(32 signed \<rightarrow> 32) cap_null_cap))} \<inter> \<lbrace>(v = SCAST(32 signed \<rightarrow> 32) cap_null_cap) = (cteCap cte = capability.NullCap)\<rbrace>}}} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>cte s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; ctes_of s slot = Some cte\<rbrakk> \<Longrightarrow> ccap_relation (cteCap cte) (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C'']))) \<and> (\<forall>t. (\<exists>a. ccap_relation a (remainder_C (ret__struct_finaliseCap_ret_C_' t))) \<and> (\<exists>b. ccap_relation b (finaliseCap_ret_C.cleanupInfo_C (ret__struct_finaliseCap_ret_C_' t))) \<longrightarrow> (\<forall>v. cap_get_tag v = SCAST(32 signed \<rightarrow> 32) cap_null_cap \<longrightarrow> s'\<lparr>globals := globals t, fc_ret_' := ret__struct_finaliseCap_ret_C_' t, ret__struct_cap_C_' := v\<rparr> \<in> (if ccap_relation capability.NullCap v then UNIV else {})))
 2. \<And>cte slota ret__unsigned. \<lbrace>?R995 cte (cte_Ptr slot)\<rbrace> isFinalCapability cte \<lbrace>\<lambda>a. invs' and cte_wp_at' ((=) cte) slot\<rbrace>
 3. \<And>cte slota ret__unsigned s'. globals (globals_update (ghost'state_'_update id) s') = globals s'
 4. \<And>cte slota ret__unsigned s'. s' \<in> {s. cte_'_update (\<lambda>_. cte_Ptr slot) s \<in> UNIV \<inter> \<lbrace>\<acute>cte = cte_Ptr slot\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> from_bool) rv (ret__unsigned_long_' t) \<longrightarrow> final_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV} \<Longrightarrow> globals_update (ghost'state_'_update id) s' \<in> {s. cte_'_update (\<lambda>_. cte_Ptr slot) s \<in> UNIV \<inter> \<lbrace>\<acute>cte = cte_Ptr slot\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> from_bool) rv (ret__unsigned_long_' t) \<longrightarrow> final_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV}
 5. \<And>cte slota ret__unsigned. ccorres dc xfdc (?Pf907 cte (cte_Ptr slot)) (?Rf903 cte (cte_Ptr slot) ret__unsigned (cteCap cte = capability.NullCap)) [SKIP] (return ()) SKIP
 6. \<And>cte slota s s'. \<lbrakk>slota = cte_Ptr slot; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. c = cte) slot and (invs' and cte_wp_at' (\<lambda>ct. w = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = w)) slot)) s; s' \<in> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = w\<rbrace>\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. cteCap cte \<noteq> capability.NullCap \<longrightarrow> (cte_wp_at' ((=) cte) slot and invs' and ?R995 cte slota) s) and (\<lambda>s. \<not> cteCap cte \<noteq> capability.NullCap \<longrightarrow> ?Pf907 cte slota s) and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s \<and> s' \<in> {s. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slota\<rightarrow>[''cap_C'']))) s)) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> \<lbrace>v = cap_get_tag (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slota\<rightarrow>[''cap_C''])))\<rbrace> \<longrightarrow> s \<in> {s. cap_type_'_update (\<lambda>_. v) s \<in> {s. (s \<in> \<lbrace>v \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrace> \<longrightarrow> s \<in> {s. \<forall>va. final_'_update (\<lambda>a. va) s \<in> {s. \<forall>va. fc_ret_'_update (\<lambda>_. va) s \<in> {s. cte_'_update (\<lambda>_. slota) s \<in> UNIV \<inter> \<lbrace>\<acute>cte = slota\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> from_bool) rv (ret__unsigned_long_' t) \<longrightarrow> final_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV} \<inter> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = - 1 \<or> gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = v\<rbrace>}}) \<and> (s \<notin> \<lbrace>v \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrace> \<longrightarrow> s \<in> ?Rf903 cte slota v (v = SCAST(32 signed \<rightarrow> 32) cap_null_cap))} \<inter> \<lbrace>(v = SCAST(32 signed \<rightarrow> 32) cap_null_cap) = (cteCap cte = capability.NullCap)\<rbrace>}}} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>cte s s' y'. \<lbrakk>invs' s; ctes_of s slot = Some cte; ctes_of s slot = Some cte; ccte_relation cte y'; cslift s' (cte_Ptr slot) = Some y'\<rbrakk> \<Longrightarrow> ccap_relation (cteCap cte) (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C'']))) \<and> (\<forall>t. (\<exists>a. ccap_relation a (remainder_C (ret__struct_finaliseCap_ret_C_' t))) \<and> (\<exists>b. ccap_relation b (finaliseCap_ret_C.cleanupInfo_C (ret__struct_finaliseCap_ret_C_' t))) \<longrightarrow> (\<forall>v. cap_get_tag v = SCAST(32 signed \<rightarrow> 32) cap_null_cap \<longrightarrow> s'\<lparr>globals := globals t, fc_ret_' := ret__struct_finaliseCap_ret_C_' t, ret__struct_cap_C_' := v\<rparr> \<in> (if ccap_relation capability.NullCap v then UNIV else {})))
 2. \<And>cte slota ret__unsigned. \<lbrace>?R995 cte (cte_Ptr slot)\<rbrace> isFinalCapability cte \<lbrace>\<lambda>a. invs' and cte_wp_at' ((=) cte) slot\<rbrace>
 3. \<And>cte slota ret__unsigned s'. globals (globals_update (ghost'state_'_update id) s') = globals s'
 4. \<And>cte slota ret__unsigned s'. s' \<in> {s. cte_'_update (\<lambda>_. cte_Ptr slot) s \<in> UNIV \<inter> \<lbrace>\<acute>cte = cte_Ptr slot\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> from_bool) rv (ret__unsigned_long_' t) \<longrightarrow> final_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV} \<Longrightarrow> globals_update (ghost'state_'_update id) s' \<in> {s. cte_'_update (\<lambda>_. cte_Ptr slot) s \<in> UNIV \<inter> \<lbrace>\<acute>cte = cte_Ptr slot\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> from_bool) rv (ret__unsigned_long_' t) \<longrightarrow> final_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV}
 5. \<And>cte slota ret__unsigned. ccorres dc xfdc (?Pf907 cte (cte_Ptr slot)) (?Rf903 cte (cte_Ptr slot) ret__unsigned (cteCap cte = capability.NullCap)) [SKIP] (return ()) SKIP
 6. \<And>cte slota s s'. \<lbrakk>slota = cte_Ptr slot; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. c = cte) slot and (invs' and cte_wp_at' (\<lambda>ct. w = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = w)) slot)) s; s' \<in> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = w\<rbrace>\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. cteCap cte \<noteq> capability.NullCap \<longrightarrow> (cte_wp_at' ((=) cte) slot and invs' and ?R995 cte slota) s) and (\<lambda>s. \<not> cteCap cte \<noteq> capability.NullCap \<longrightarrow> ?Pf907 cte slota s) and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s \<and> s' \<in> {s. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slota\<rightarrow>[''cap_C'']))) s)) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> \<lbrace>v = cap_get_tag (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slota\<rightarrow>[''cap_C''])))\<rbrace> \<longrightarrow> s \<in> {s. cap_type_'_update (\<lambda>_. v) s \<in> {s. (s \<in> \<lbrace>v \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrace> \<longrightarrow> s \<in> {s. \<forall>va. final_'_update (\<lambda>a. va) s \<in> {s. \<forall>va. fc_ret_'_update (\<lambda>_. va) s \<in> {s. cte_'_update (\<lambda>_. slota) s \<in> UNIV \<inter> \<lbrace>\<acute>cte = slota\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> from_bool) rv (ret__unsigned_long_' t) \<longrightarrow> final_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV} \<inter> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = - 1 \<or> gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = v\<rbrace>}}) \<and> (s \<notin> \<lbrace>v \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrace> \<longrightarrow> s \<in> ?Rf903 cte slota v (v = SCAST(32 signed \<rightarrow> 32) cap_null_cap))} \<inter> \<lbrace>(v = SCAST(32 signed \<rightarrow> 32) cap_null_cap) = (cteCap cte = capability.NullCap)\<rbrace>}}} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>cte slota ret__unsigned. \<lbrace>?R995 cte (cte_Ptr slot)\<rbrace> isFinalCapability cte \<lbrace>\<lambda>a. invs' and cte_wp_at' ((=) cte) slot\<rbrace>
 2. \<And>cte slota ret__unsigned s'. globals (globals_update (ghost'state_'_update id) s') = globals s'
 3. \<And>cte slota ret__unsigned s'. s' \<in> {s. cte_'_update (\<lambda>_. cte_Ptr slot) s \<in> UNIV \<inter> \<lbrace>\<acute>cte = cte_Ptr slot\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> from_bool) rv (ret__unsigned_long_' t) \<longrightarrow> final_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV} \<Longrightarrow> globals_update (ghost'state_'_update id) s' \<in> {s. cte_'_update (\<lambda>_. cte_Ptr slot) s \<in> UNIV \<inter> \<lbrace>\<acute>cte = cte_Ptr slot\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> from_bool) rv (ret__unsigned_long_' t) \<longrightarrow> final_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV}
 4. \<And>cte slota ret__unsigned. ccorres dc xfdc (?Pf907 cte (cte_Ptr slot)) (?Rf903 cte (cte_Ptr slot) ret__unsigned (cteCap cte = capability.NullCap)) [SKIP] (return ()) SKIP
 5. \<And>cte slota s s'. \<lbrakk>slota = cte_Ptr slot; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. c = cte) slot and (invs' and cte_wp_at' (\<lambda>ct. w = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = w)) slot)) s; s' \<in> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = w\<rbrace>\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. cteCap cte \<noteq> capability.NullCap \<longrightarrow> (cte_wp_at' ((=) cte) slot and invs' and ?R995 cte slota) s) and (\<lambda>s. \<not> cteCap cte \<noteq> capability.NullCap \<longrightarrow> ?Pf907 cte slota s) and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s \<and> s' \<in> {s. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slota\<rightarrow>[''cap_C'']))) s)) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> \<lbrace>v = cap_get_tag (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slota\<rightarrow>[''cap_C''])))\<rbrace> \<longrightarrow> s \<in> {s. cap_type_'_update (\<lambda>_. v) s \<in> {s. (s \<in> \<lbrace>v \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrace> \<longrightarrow> s \<in> {s. \<forall>va. final_'_update (\<lambda>a. va) s \<in> {s. \<forall>va. fc_ret_'_update (\<lambda>_. va) s \<in> {s. cte_'_update (\<lambda>_. slota) s \<in> UNIV \<inter> \<lbrace>\<acute>cte = slota\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> from_bool) rv (ret__unsigned_long_' t) \<longrightarrow> final_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV} \<inter> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = - 1 \<or> gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = v\<rbrace>}}) \<and> (s \<notin> \<lbrace>v \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrace> \<longrightarrow> s \<in> ?Rf903 cte slota v (v = SCAST(32 signed \<rightarrow> 32) cap_null_cap))} \<inter> \<lbrace>(v = SCAST(32 signed \<rightarrow> 32) cap_null_cap) = (cteCap cte = capability.NullCap)\<rbrace>}}} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>cte slota ret__unsigned s'. globals (globals_update (ghost'state_'_update id) s') = globals s'
 2. \<And>cte slota ret__unsigned s'. s' \<in> {s. cte_'_update (\<lambda>_. cte_Ptr slot) s \<in> UNIV \<inter> \<lbrace>\<acute>cte = cte_Ptr slot\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> from_bool) rv (ret__unsigned_long_' t) \<longrightarrow> final_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV} \<Longrightarrow> globals_update (ghost'state_'_update id) s' \<in> {s. cte_'_update (\<lambda>_. cte_Ptr slot) s \<in> UNIV \<inter> \<lbrace>\<acute>cte = cte_Ptr slot\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> from_bool) rv (ret__unsigned_long_' t) \<longrightarrow> final_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV}
 3. \<And>cte slota ret__unsigned. ccorres dc xfdc (?Pf907 cte (cte_Ptr slot)) (?Rf903 cte (cte_Ptr slot) ret__unsigned (cteCap cte = capability.NullCap)) [SKIP] (return ()) SKIP
 4. \<And>cte slota s s'. \<lbrakk>slota = cte_Ptr slot; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. c = cte) slot and (invs' and cte_wp_at' (\<lambda>ct. w = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = w)) slot)) s; s' \<in> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = w\<rbrace>\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. cteCap cte \<noteq> capability.NullCap \<longrightarrow> (cte_wp_at' ((=) cte) slot and invs' and (invs' and cte_wp_at' ((=) cte) slot)) s) and (\<lambda>s. \<not> cteCap cte \<noteq> capability.NullCap \<longrightarrow> ?Pf907 cte slota s) and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s \<and> s' \<in> {s. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slota\<rightarrow>[''cap_C'']))) s)) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> \<lbrace>v = cap_get_tag (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slota\<rightarrow>[''cap_C''])))\<rbrace> \<longrightarrow> s \<in> {s. cap_type_'_update (\<lambda>_. v) s \<in> {s. (s \<in> \<lbrace>v \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrace> \<longrightarrow> s \<in> {s. \<forall>va. final_'_update (\<lambda>a. va) s \<in> {s. \<forall>va. fc_ret_'_update (\<lambda>_. va) s \<in> {s. cte_'_update (\<lambda>_. slota) s \<in> UNIV \<inter> \<lbrace>\<acute>cte = slota\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> from_bool) rv (ret__unsigned_long_' t) \<longrightarrow> final_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV} \<inter> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = - 1 \<or> gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = v\<rbrace>}}) \<and> (s \<notin> \<lbrace>v \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrace> \<longrightarrow> s \<in> ?Rf903 cte slota v (v = SCAST(32 signed \<rightarrow> 32) cap_null_cap))} \<inter> \<lbrace>(v = SCAST(32 signed \<rightarrow> 32) cap_null_cap) = (cteCap cte = capability.NullCap)\<rbrace>}}} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>cte slota ret__unsigned s'. s' \<in> {s. cte_'_update (\<lambda>_. cte_Ptr slot) s \<in> UNIV \<inter> \<lbrace>\<acute>cte = cte_Ptr slot\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> from_bool) rv (ret__unsigned_long_' t) \<longrightarrow> final_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV} \<Longrightarrow> globals_update (ghost'state_'_update id) s' \<in> {s. cte_'_update (\<lambda>_. cte_Ptr slot) s \<in> UNIV \<inter> \<lbrace>\<acute>cte = cte_Ptr slot\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> from_bool) rv (ret__unsigned_long_' t) \<longrightarrow> final_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV}
 2. \<And>cte slota ret__unsigned. ccorres dc xfdc (?Pf907 cte (cte_Ptr slot)) (?Rf903 cte (cte_Ptr slot) ret__unsigned (cteCap cte = capability.NullCap)) [SKIP] (return ()) SKIP
 3. \<And>cte slota s s'. \<lbrakk>slota = cte_Ptr slot; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. c = cte) slot and (invs' and cte_wp_at' (\<lambda>ct. w = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = w)) slot)) s; s' \<in> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = w\<rbrace>\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. cteCap cte \<noteq> capability.NullCap \<longrightarrow> (cte_wp_at' ((=) cte) slot and invs' and (invs' and cte_wp_at' ((=) cte) slot)) s) and (\<lambda>s. \<not> cteCap cte \<noteq> capability.NullCap \<longrightarrow> ?Pf907 cte slota s) and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s \<and> s' \<in> {s. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slota\<rightarrow>[''cap_C'']))) s)) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> \<lbrace>v = cap_get_tag (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slota\<rightarrow>[''cap_C''])))\<rbrace> \<longrightarrow> s \<in> {s. cap_type_'_update (\<lambda>_. v) s \<in> {s. (s \<in> \<lbrace>v \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrace> \<longrightarrow> s \<in> {s. \<forall>va. final_'_update (\<lambda>a. va) s \<in> {s. \<forall>va. fc_ret_'_update (\<lambda>_. va) s \<in> {s. cte_'_update (\<lambda>_. slota) s \<in> UNIV \<inter> \<lbrace>\<acute>cte = slota\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> from_bool) rv (ret__unsigned_long_' t) \<longrightarrow> final_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV} \<inter> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = - 1 \<or> gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = v\<rbrace>}}) \<and> (s \<notin> \<lbrace>v \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrace> \<longrightarrow> s \<in> ?Rf903 cte slota v (v = SCAST(32 signed \<rightarrow> 32) cap_null_cap))} \<inter> \<lbrace>(v = SCAST(32 signed \<rightarrow> 32) cap_null_cap) = (cteCap cte = capability.NullCap)\<rbrace>}}} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>cte slota ret__unsigned. ccorres dc xfdc (?Pf907 cte (cte_Ptr slot)) (?Rf903 cte (cte_Ptr slot) ret__unsigned (cteCap cte = capability.NullCap)) [SKIP] (return ()) SKIP
 2. \<And>cte slota s s'. \<lbrakk>slota = cte_Ptr slot; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. c = cte) slot and (invs' and cte_wp_at' (\<lambda>ct. w = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = w)) slot)) s; s' \<in> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = w\<rbrace>\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. cteCap cte \<noteq> capability.NullCap \<longrightarrow> (cte_wp_at' ((=) cte) slot and invs' and (invs' and cte_wp_at' ((=) cte) slot)) s) and (\<lambda>s. \<not> cteCap cte \<noteq> capability.NullCap \<longrightarrow> ?Pf907 cte slota s) and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s \<and> s' \<in> {s. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slota\<rightarrow>[''cap_C'']))) s)) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> \<lbrace>v = cap_get_tag (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slota\<rightarrow>[''cap_C''])))\<rbrace> \<longrightarrow> s \<in> {s. cap_type_'_update (\<lambda>_. v) s \<in> {s. (s \<in> \<lbrace>v \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrace> \<longrightarrow> s \<in> {s. \<forall>va. final_'_update (\<lambda>a. va) s \<in> {s. \<forall>va. fc_ret_'_update (\<lambda>_. va) s \<in> {s. cte_'_update (\<lambda>_. slota) s \<in> UNIV \<inter> \<lbrace>\<acute>cte = slota\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> from_bool) rv (ret__unsigned_long_' t) \<longrightarrow> final_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV} \<inter> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = - 1 \<or> gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = v\<rbrace>}}) \<and> (s \<notin> \<lbrace>v \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrace> \<longrightarrow> s \<in> ?Rf903 cte slota v (v = SCAST(32 signed \<rightarrow> 32) cap_null_cap))} \<inter> \<lbrace>(v = SCAST(32 signed \<rightarrow> 32) cap_null_cap) = (cteCap cte = capability.NullCap)\<rbrace>}}} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cte slota s s'. \<lbrakk>slota = cte_Ptr slot; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>c. c = cte) slot and (invs' and cte_wp_at' (\<lambda>ct. w = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = w)) slot)) s; s' \<in> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = w\<rbrace>\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. cteCap cte \<noteq> capability.NullCap \<longrightarrow> (cte_wp_at' ((=) cte) slot and invs' and (invs' and cte_wp_at' ((=) cte) slot)) s) and (\<lambda>s. \<not> cteCap cte \<noteq> capability.NullCap \<longrightarrow> True) and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s \<and> s' \<in> {s. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slota\<rightarrow>[''cap_C'']))) s)) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> \<lbrace>v = cap_get_tag (h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slota\<rightarrow>[''cap_C''])))\<rbrace> \<longrightarrow> s \<in> {s. cap_type_'_update (\<lambda>_. v) s \<in> {s. (s \<in> \<lbrace>v \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrace> \<longrightarrow> s \<in> {s. \<forall>va. final_'_update (\<lambda>a. va) s \<in> {s. \<forall>va. fc_ret_'_update (\<lambda>_. va) s \<in> {s. cte_'_update (\<lambda>_. slota) s \<in> UNIV \<inter> \<lbrace>\<acute>cte = slota\<rbrace>} \<inter> {s'. \<forall>t rv. ((=) \<circ> from_bool) rv (ret__unsigned_long_' t) \<longrightarrow> final_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> UNIV} \<inter> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = - 1 \<or> gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = v\<rbrace>}}) \<and> (s \<notin> \<lbrace>v \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrace> \<longrightarrow> s \<in> UNIV)} \<inter> \<lbrace>(v = SCAST(32 signed \<rightarrow> 32) cap_null_cap) = (cteCap cte = capability.NullCap)\<rbrace>}}} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cte s s'. \<lbrakk>(s, s') \<in> rf_sr; w = gs_get_assn cteDeleteOne_'proc (ghost'state_' (globals s')); invs' s; ctes_of s slot = Some cte; gs_get_assn cteDeleteOne_'proc (ghost'state_' (globals s')) = - 1 \<or> cteCap cte = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap cte) cap' \<longrightarrow> cap_get_tag cap' = gs_get_assn cteDeleteOne_'proc (ghost'state_' (globals s')))\<rbrakk> \<Longrightarrow> (cap_get_tag (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C'']))) \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap \<longrightarrow> ghost_assertion_data_get cteDeleteOne_'proc (\<lambda>a. snd (snd a)) (ghost'state_' (globals s')) = - 1 \<or> ghost_assertion_data_get cteDeleteOne_'proc (\<lambda>a. snd (snd a)) (ghost'state_' (globals s')) = cap_get_tag (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C''])))) \<and> (cap_get_tag (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C'']))) = SCAST(32 signed \<rightarrow> 32) cap_null_cap) = (cteCap cte = capability.NullCap) proof (prove)
goal (1 subgoal):
 1. \<And>cte s s' y'. \<lbrakk>w = gs_get_assn cteDeleteOne_'proc (ghost'state_' (globals s')); invs' s; ctes_of s slot = Some cte; gs_get_assn cteDeleteOne_'proc (ghost'state_' (globals s')) = - 1 \<or> cteCap cte = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap cte) cap' \<longrightarrow> cap_get_tag cap' = gs_get_assn cteDeleteOne_'proc (ghost'state_' (globals s'))); ctes_of s slot = Some cte; ccte_relation cte y'; cslift s' (cte_Ptr slot) = Some y'\<rbrakk> \<Longrightarrow> (cap_get_tag (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C'']))) \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap \<longrightarrow> ghost_assertion_data_get cteDeleteOne_'proc (\<lambda>a. snd (snd a)) (ghost'state_' (globals s')) = - 1 \<or> ghost_assertion_data_get cteDeleteOne_'proc (\<lambda>a. snd (snd a)) (ghost'state_' (globals s')) = cap_get_tag (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C''])))) \<and> (cap_get_tag (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr slot\<rightarrow>[''cap_C'']))) = SCAST(32 signed \<rightarrow> 32) cap_null_cap) = (cteCap cte = capability.NullCap) proof (prove)
goal (1 subgoal):
 1. \<And>cte s s' y'. \<lbrakk>w = gs_get_assn cteDeleteOne_'proc (ghost'state_' (globals s')); invs' s; gs_get_assn cteDeleteOne_'proc (ghost'state_' (globals s')) = - 1 \<or> (\<forall>cap'. ccap_relation (cteCap cte) cap' \<longrightarrow> cap_get_tag cap' = gs_get_assn cteDeleteOne_'proc (ghost'state_' (globals s'))); ctes_of s slot = Some cte; cslift s' (cte_Ptr slot) = Some y'; ccap_relation (cteCap cte) (cte_C.cap_C y'); cteCap cte \<noteq> capability.NullCap; ghost_assertion_data_get cteDeleteOne_'proc (\<lambda>a. snd (snd a)) (ghost'state_' (globals s')) \<noteq> cap_get_tag (cte_C.cap_C y')\<rbrakk> \<Longrightarrow> ghost_assertion_data_get cteDeleteOne_'proc (\<lambda>a. snd (snd a)) (ghost'state_' (globals s')) = - 1 proof (prove)
goal:
No subgoals!