theory Delete_C

lemma cteDelete_ccorres1:
  assumes fs_cc:
    "ccorres (cintr \<currency> (\<lambda>(success, cap) (success', cap'). success' = from_bool success \<and> ccap_relation cap cap' \<and> cleanup_info_wf' cap))
     (liftxf errstate finaliseSlot_ret_C.status_C (\<lambda>v. (success_C v, finaliseSlot_ret_C.cleanupInfo_C v))
                   ret__struct_finaliseSlot_ret_C_')
     (\<lambda>s. invs' s \<and> sch_act_simple s \<and> (expo \<or> ex_cte_cap_to' slot s))
     (UNIV \<inter> {s. slot_' s = Ptr slot} \<inter> {s. immediate_' s = from_bool expo}) []
     (cutMon ((=) s) (finaliseSlot slot expo)) (Call finaliseSlot_'proc)"
  shows
  "ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_' )
     (\<lambda>s. invs' s \<and> sch_act_simple s \<and> (expo \<or> ex_cte_cap_to' slot s))
     (UNIV \<inter> {s. slot_' s = Ptr slot} \<inter> {s. exposed_' s = from_bool expo}) []
     (cutMon ((=) s) (cteDelete slot expo)) (Call cteDelete_'proc)" apply (cinit' lift: slot_' exposed_' cong: call_ignore_cong) apply (simp add: cteDelete_def split_def cutMon_walk_bindE
               del: Collect_const cong: call_ignore_cong) apply (clarsimp simp del: Collect_const cong: call_ignore_cong) apply (ctac(no_vcg) add: fs_cc) apply (rule ccorres_drop_cutMon) apply (simp add: from_bool_0 whenE_def split_def
                      Collect_False
                 del: Collect_const) apply (rule ccorres_if_lhs) apply (simp only: imp_conv_disj simp_thms) apply (simp add: liftE_liftM liftM_def) apply (ctac(no_vcg) add: emptySlot_ccorres) apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV]) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: return_def) apply wp apply (simp only: imp_conv_disj simp_thms) apply (simp add: returnOk_def) apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV]) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: return_def) apply simp apply (rule ccorres_split_throws) apply (rule ccorres_return_C_errorE, simp+)[1] apply vcg apply wp apply (rule_tac Q'="\<lambda>rv. invs'" in hoare_post_imp_R) apply (wp cutMon_validE_drop finaliseSlot_invs) apply fastforce apply (auto simp: cintr_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (\<lambda>s. invs' s \<and> sch_act_simple s \<and> (expo \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s)) (UNIV \<inter> \<lbrace>\<acute>slot = cte_Ptr slot\<rbrace> \<inter> \<lbrace>\<acute>exposed = from_bool expo\<rbrace>) [] (cutMon ((=) s) (cteDelete slot expo)) (Call cteDelete_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>exposed slota. \<lbrakk>exposed = from_bool expo; slota = cte_Ptr slot\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q297 exposed slota) (?Q'297 exposed slota) [SKIP] (cutMon ((=) s) (cteDelete slot expo)) (\<acute>fs_ret :== CALL finaliseSlot_'proc(slota,exposed);;
(IF finaliseSlot_ret_C.status_C \<acute>fs_ret \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. finaliseSlot_ret_C.status_C (fs_ret_' s))
FI;;
(IF exposed = 0 \<longrightarrow> finaliseSlot_ret_C.success_C \<acute>fs_ret \<noteq> 0 THEN
  CALL emptySlot_'proc(slota,finaliseSlot_ret_C.cleanupInfo_C \<acute>fs_ret)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))))
 2. \<And>exposed slota s s'. \<lbrakk>exposed = from_bool expo; slota = cte_Ptr slot; (s, s') \<in> rf_sr; invs' s \<and> sch_act_simple s \<and> (expo \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q297 exposed slota s \<and> s' \<in> ?Q'297 exposed slota proof (prove)
goal (2 subgoals):
 1. \<And>exposed slota. \<lbrakk>exposed = from_bool expo; slota = cte_Ptr slot\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q297 (from_bool expo) (cte_Ptr slot)) (?Q'297 (from_bool expo) (cte_Ptr slot)) [SKIP] (doE rv <- cutMon ((=) s) (finaliseSlot slot expo);
cutMon (\<lambda>s'. (Inr rv, s') \<in> fst (finaliseSlot slot expo s)) (whenE (expo \<or> fst rv) (liftE (emptySlot slot (snd rv))))
odE) (\<acute>fs_ret :== CALL finaliseSlot_'proc(slota,exposed);;
(IF finaliseSlot_ret_C.status_C \<acute>fs_ret \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. finaliseSlot_ret_C.status_C (fs_ret_' s))
FI;;
(IF from_bool expo = 0 \<longrightarrow> finaliseSlot_ret_C.success_C \<acute>fs_ret \<noteq> 0 THEN
  CALL emptySlot_'proc(slota,finaliseSlot_ret_C.cleanupInfo_C \<acute>fs_ret)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))))
 2. \<And>exposed slota s s'. \<lbrakk>exposed = from_bool expo; slota = cte_Ptr slot; (s, s') \<in> rf_sr; invs' s \<and> sch_act_simple s \<and> (expo \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q297 exposed slota s \<and> s' \<in> ?Q'297 exposed slota proof (prove)
goal (2 subgoals):
 1. ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q297 (from_bool expo) (cte_Ptr slot)) (?Q'297 (from_bool expo) (cte_Ptr slot)) [SKIP] (doE rv <- cutMon ((=) s) (finaliseSlot slot expo);
cutMon (\<lambda>s'. (Inr rv, s') \<in> fst (finaliseSlot slot expo s)) (whenE (expo \<or> fst rv) (liftE (emptySlot slot (snd rv))))
odE) (\<acute>fs_ret :== CALL finaliseSlot_'proc(cte_Ptr slot,from_bool expo);;
(IF finaliseSlot_ret_C.status_C \<acute>fs_ret \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. finaliseSlot_ret_C.status_C (fs_ret_' s))
FI;;
(IF from_bool expo = 0 \<longrightarrow> finaliseSlot_ret_C.success_C \<acute>fs_ret \<noteq> 0 THEN
  CALL emptySlot_'proc(cte_Ptr slot,finaliseSlot_ret_C.cleanupInfo_C \<acute>fs_ret)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))))
 2. \<And>exposed slota s s'. \<lbrakk>exposed = from_bool expo; slota = cte_Ptr slot; (s, s') \<in> rf_sr; invs' s \<and> sch_act_simple s \<and> (expo \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q297 exposed slota s \<and> s' \<in> ?Q'297 exposed slota proof (prove)
goal (4 subgoals):
 1. \<And>rv fs_ret. \<lbrakk>(case rv of (success, cap) \<Rightarrow> \<lambda>(success', cap'). success' = from_bool success \<and> ccap_relation cap cap' \<and> cleanup_info_wf' cap) (finaliseSlot_ret_C.success_C fs_ret, finaliseSlot_ret_C.cleanupInfo_C fs_ret); finaliseSlot_ret_C.status_C fs_ret = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q310 rv) (?Q'310 rv fs_ret) [SKIP] (cutMon (\<lambda>s'. (Inr rv, s') \<in> fst (finaliseSlot slot expo s)) (whenE (expo \<or> fst rv) (liftE (emptySlot slot (snd rv))))) (IF finaliseSlot_ret_C.status_C fs_ret \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  return_C ret__unsigned_long_'_update (\<lambda>a. finaliseSlot_ret_C.status_C fs_ret)
FI;;
(IF from_bool expo = 0 \<longrightarrow> finaliseSlot_ret_C.success_C fs_ret \<noteq> 0 THEN
  CALL emptySlot_'proc(cte_Ptr slot,finaliseSlot_ret_C.cleanupInfo_C fs_ret)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>a. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))
 2. \<And>err rv' fs_ret. \<lbrakk>finaliseSlot_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; cintr err (finaliseSlot_ret_C.status_C rv') fs_ret\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?QE310 err) (?Q''310 err rv' fs_ret) [SKIP] (throwError err) (IF finaliseSlot_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  return_C ret__unsigned_long_'_update (\<lambda>a. finaliseSlot_ret_C.status_C rv')
FI;;
(IF from_bool expo = 0 \<longrightarrow> finaliseSlot_ret_C.success_C rv' \<noteq> 0 THEN
  CALL emptySlot_'proc(cte_Ptr slot,finaliseSlot_ret_C.cleanupInfo_C rv')
FI;;
return_C ret__unsigned_long_'_update (\<lambda>a. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))
 3. \<lbrace>?R327 (from_bool expo) (cte_Ptr slot)\<rbrace> cutMon ((=) s) (finaliseSlot slot expo) \<lbrace>?Q310\<rbrace>, \<lbrace>?QE310\<rbrace>
 4. \<And>exposed slota s s'. \<lbrakk>exposed = from_bool expo; slota = cte_Ptr slot; (s, s') \<in> rf_sr; invs' s \<and> sch_act_simple s \<and> (expo \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. invs' a \<and> sch_act_simple a \<and> (expo \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot a)) and ?R327 exposed slota) s \<and> s' \<in> {s. immediate_'_update (\<lambda>_. exposed) (slot_'_update (\<lambda>_. slota) s) \<in> UNIV \<inter> \<lbrace>\<acute>slot = slota\<rbrace> \<inter> \<lbrace>\<acute>immediate = exposed\<rbrace>} \<inter> {s. \<forall>t. (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. (case rv of (success, cap) \<Rightarrow> \<lambda>a. case a of (success', cap') \<Rightarrow> success' = from_bool success \<and> ccap_relation cap cap' \<and> cleanup_info_wf' cap) (finaliseSlot_ret_C.success_C (ret__struct_finaliseSlot_ret_C_' t), finaliseSlot_ret_C.cleanupInfo_C (ret__struct_finaliseSlot_ret_C_' t)) \<longrightarrow> fs_ret_'_update (\<lambda>_. ret__struct_finaliseSlot_ret_C_' t) (s\<lparr>globals := globals t\<rparr>) \<in> ?Q'323 exposed slota t rv)) \<and> (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. cintr err (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t)) (errstate t) \<longrightarrow> fs_ret_'_update (\<lambda>_. ret__struct_finaliseSlot_ret_C_' t) (s\<lparr>globals := globals t\<rparr>) \<in> ?Q''320 exposed slota t err))}
flex-flex pairs:
?Q'323 (from_bool expo) (cte_Ptr slot) \<equiv>\<^sup>? \<lambda>t rv. ?Q'310 rv (ret__struct_finaliseSlot_ret_C_' t)
?Q''320 (from_bool expo) (cte_Ptr slot) \<equiv>\<^sup>? \<lambda>t err. ?Q''310 err (ret__struct_finaliseSlot_ret_C_' t) (errstate t) proof (prove)
goal (4 subgoals):
 1. \<And>rv fs_ret. \<lbrakk>(case rv of (success, cap) \<Rightarrow> \<lambda>(success', cap'). success' = from_bool success \<and> ccap_relation cap cap' \<and> cleanup_info_wf' cap) (finaliseSlot_ret_C.success_C fs_ret, finaliseSlot_ret_C.cleanupInfo_C fs_ret); finaliseSlot_ret_C.status_C fs_ret = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q310 rv) (?Q'310 rv fs_ret) [SKIP] (whenE (expo \<or> fst rv) (liftE (emptySlot slot (snd rv)))) (IF finaliseSlot_ret_C.status_C fs_ret \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  return_C ret__unsigned_long_'_update (\<lambda>a. finaliseSlot_ret_C.status_C fs_ret)
FI;;
(IF from_bool expo = 0 \<longrightarrow> finaliseSlot_ret_C.success_C fs_ret \<noteq> 0 THEN
  CALL emptySlot_'proc(cte_Ptr slot,finaliseSlot_ret_C.cleanupInfo_C fs_ret)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>a. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))
 2. \<And>err rv' fs_ret. \<lbrakk>finaliseSlot_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; cintr err (finaliseSlot_ret_C.status_C rv') fs_ret\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?QE310 err) (?Q''310 err rv' fs_ret) [SKIP] (throwError err) (IF finaliseSlot_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  return_C ret__unsigned_long_'_update (\<lambda>a. finaliseSlot_ret_C.status_C rv')
FI;;
(IF from_bool expo = 0 \<longrightarrow> finaliseSlot_ret_C.success_C rv' \<noteq> 0 THEN
  CALL emptySlot_'proc(cte_Ptr slot,finaliseSlot_ret_C.cleanupInfo_C rv')
FI;;
return_C ret__unsigned_long_'_update (\<lambda>a. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))
 3. \<lbrace>?R327 (from_bool expo) (cte_Ptr slot)\<rbrace> cutMon ((=) s) (finaliseSlot slot expo) \<lbrace>?Q310\<rbrace>, \<lbrace>?QE310\<rbrace>
 4. \<And>exposed slota s s'. \<lbrakk>exposed = from_bool expo; slota = cte_Ptr slot; (s, s') \<in> rf_sr; invs' s \<and> sch_act_simple s \<and> (expo \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. invs' a \<and> sch_act_simple a \<and> (expo \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot a)) and ?R327 exposed slota) s \<and> s' \<in> {s. immediate_'_update (\<lambda>_. exposed) (slot_'_update (\<lambda>_. slota) s) \<in> UNIV \<inter> \<lbrace>\<acute>slot = slota\<rbrace> \<inter> \<lbrace>\<acute>immediate = exposed\<rbrace>} \<inter> {s. \<forall>t. (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. (case rv of (success, cap) \<Rightarrow> \<lambda>a. case a of (success', cap') \<Rightarrow> success' = from_bool success \<and> ccap_relation cap cap' \<and> cleanup_info_wf' cap) (finaliseSlot_ret_C.success_C (ret__struct_finaliseSlot_ret_C_' t), finaliseSlot_ret_C.cleanupInfo_C (ret__struct_finaliseSlot_ret_C_' t)) \<longrightarrow> fs_ret_'_update (\<lambda>_. ret__struct_finaliseSlot_ret_C_' t) (s\<lparr>globals := globals t\<rparr>) \<in> ?Q'323 exposed slota t rv)) \<and> (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. cintr err (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t)) (errstate t) \<longrightarrow> fs_ret_'_update (\<lambda>_. ret__struct_finaliseSlot_ret_C_' t) (s\<lparr>globals := globals t\<rparr>) \<in> ?Q''320 exposed slota t err))}
flex-flex pairs:
?Q'323 (from_bool expo) (cte_Ptr slot) \<equiv>\<^sup>? \<lambda>t rv. ?Q'310 rv (ret__struct_finaliseSlot_ret_C_' t)
?Q''320 (from_bool expo) (cte_Ptr slot) \<equiv>\<^sup>? \<lambda>t err. ?Q''310 err (ret__struct_finaliseSlot_ret_C_' t) (errstate t) proof (prove)
goal (4 subgoals):
 1. \<And>rv fs_ret. \<lbrakk>finaliseSlot_ret_C.success_C fs_ret = from_bool (fst rv) \<and> ccap_relation (snd rv) (finaliseSlot_ret_C.cleanupInfo_C fs_ret) \<and> cleanup_info_wf' (snd rv); finaliseSlot_ret_C.status_C fs_ret = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q310 rv) (?Q'310 rv fs_ret) [SKIP] (if expo \<or> fst rv then liftE (emptySlot slot (snd rv)) else returnOk ()) (IF \<not> expo \<longrightarrow> fst rv THEN
  CALL emptySlot_'proc(cte_Ptr slot,finaliseSlot_ret_C.cleanupInfo_C fs_ret)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>a. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>err rv' fs_ret. \<lbrakk>finaliseSlot_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; cintr err (finaliseSlot_ret_C.status_C rv') fs_ret\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?QE310 err) (?Q''310 err rv' fs_ret) [SKIP] (throwError err) (IF finaliseSlot_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  return_C ret__unsigned_long_'_update (\<lambda>a. finaliseSlot_ret_C.status_C rv')
FI;;
(IF from_bool expo = 0 \<longrightarrow> finaliseSlot_ret_C.success_C rv' \<noteq> 0 THEN
  CALL emptySlot_'proc(cte_Ptr slot,finaliseSlot_ret_C.cleanupInfo_C rv')
FI;;
return_C ret__unsigned_long_'_update (\<lambda>a. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))
 3. \<lbrace>?R327 (from_bool expo) (cte_Ptr slot)\<rbrace> cutMon ((=) s) (finaliseSlot slot expo) \<lbrace>?Q310\<rbrace>, \<lbrace>?QE310\<rbrace>
 4. \<And>exposed slota s s'. \<lbrakk>exposed = from_bool expo; slota = cte_Ptr slot; (s, s') \<in> rf_sr; invs' s \<and> sch_act_simple s \<and> (expo \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. invs' a \<and> sch_act_simple a \<and> (expo \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot a)) and ?R327 exposed slota) s \<and> s' \<in> {s. immediate_'_update (\<lambda>_. exposed) (slot_'_update (\<lambda>_. slota) s) \<in> UNIV \<inter> \<lbrace>\<acute>slot = slota\<rbrace> \<inter> \<lbrace>\<acute>immediate = exposed\<rbrace>} \<inter> {s. \<forall>t. (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. (case rv of (success, cap) \<Rightarrow> \<lambda>a. case a of (success', cap') \<Rightarrow> success' = from_bool success \<and> ccap_relation cap cap' \<and> cleanup_info_wf' cap) (finaliseSlot_ret_C.success_C (ret__struct_finaliseSlot_ret_C_' t), finaliseSlot_ret_C.cleanupInfo_C (ret__struct_finaliseSlot_ret_C_' t)) \<longrightarrow> fs_ret_'_update (\<lambda>_. ret__struct_finaliseSlot_ret_C_' t) (s\<lparr>globals := globals t\<rparr>) \<in> ?Q'323 exposed slota t rv)) \<and> (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. cintr err (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t)) (errstate t) \<longrightarrow> fs_ret_'_update (\<lambda>_. ret__struct_finaliseSlot_ret_C_' t) (s\<lparr>globals := globals t\<rparr>) \<in> ?Q''320 exposed slota t err))}
flex-flex pairs:
?Q'323 (from_bool expo) (cte_Ptr slot) \<equiv>\<^sup>? \<lambda>t rv. ?Q'310 rv (ret__struct_finaliseSlot_ret_C_' t)
?Q''320 (from_bool expo) (cte_Ptr slot) \<equiv>\<^sup>? \<lambda>t err. ?Q''310 err (ret__struct_finaliseSlot_ret_C_' t) (errstate t) proof (prove)
goal (5 subgoals):
 1. \<And>rv fs_ret. \<lbrakk>finaliseSlot_ret_C.success_C fs_ret = from_bool (fst rv) \<and> ccap_relation (snd rv) (finaliseSlot_ret_C.cleanupInfo_C fs_ret) \<and> cleanup_info_wf' (snd rv); finaliseSlot_ret_C.status_C fs_ret = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; expo \<or> fst rv\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q482 rv) (?S476 rv fs_ret) [SKIP] (liftE (emptySlot slot (snd rv))) (IF \<not> expo \<longrightarrow> fst rv THEN
  CALL emptySlot_'proc(cte_Ptr slot,finaliseSlot_ret_C.cleanupInfo_C fs_ret)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>a. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>rv fs_ret. \<lbrakk>finaliseSlot_ret_C.success_C fs_ret = from_bool (fst rv) \<and> ccap_relation (snd rv) (finaliseSlot_ret_C.cleanupInfo_C fs_ret) \<and> cleanup_info_wf' (snd rv); finaliseSlot_ret_C.status_C fs_ret = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; \<not> (expo \<or> fst rv)\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R481 rv) (?T476 rv fs_ret) [SKIP] (returnOk ()) (IF \<not> expo \<longrightarrow> fst rv THEN
  CALL emptySlot_'proc(cte_Ptr slot,finaliseSlot_ret_C.cleanupInfo_C fs_ret)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>a. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 3. \<And>err rv' fs_ret. \<lbrakk>finaliseSlot_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; cintr err (finaliseSlot_ret_C.status_C rv') fs_ret\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?QE310 err) (?Q''310 err rv' fs_ret) [SKIP] (throwError err) (IF finaliseSlot_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  return_C ret__unsigned_long_'_update (\<lambda>a. finaliseSlot_ret_C.status_C rv')
FI;;
(IF from_bool expo = 0 \<longrightarrow> finaliseSlot_ret_C.success_C rv' \<noteq> 0 THEN
  CALL emptySlot_'proc(cte_Ptr slot,finaliseSlot_ret_C.cleanupInfo_C rv')
FI;;
return_C ret__unsigned_long_'_update (\<lambda>a. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))
 4. \<lbrace>?R327 (from_bool expo) (cte_Ptr slot)\<rbrace> cutMon ((=) s) (finaliseSlot slot expo) \<lbrace>\<lambda>a b. (expo \<or> fst a \<longrightarrow> ?Q482 a b) \<and> (\<not> (expo \<or> fst a) \<longrightarrow> ?R481 a b)\<rbrace>, \<lbrace>?QE310\<rbrace>
 5. \<And>exposed slota s s'. \<lbrakk>exposed = from_bool expo; slota = cte_Ptr slot; (s, s') \<in> rf_sr; invs' s \<and> sch_act_simple s \<and> (expo \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. invs' a \<and> sch_act_simple a \<and> (expo \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot a)) and ?R327 exposed slota) s \<and> s' \<in> {s. immediate_'_update (\<lambda>_. exposed) (slot_'_update (\<lambda>_. slota) s) \<in> UNIV \<inter> \<lbrace>\<acute>slot = slota\<rbrace> \<inter> \<lbrace>\<acute>immediate = exposed\<rbrace>} \<inter> {s. \<forall>t. (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. (case rv of (success, cap) \<Rightarrow> \<lambda>a. case a of (success', cap') \<Rightarrow> success' = from_bool success \<and> ccap_relation cap cap' \<and> cleanup_info_wf' cap) (finaliseSlot_ret_C.success_C (ret__struct_finaliseSlot_ret_C_' t), finaliseSlot_ret_C.cleanupInfo_C (ret__struct_finaliseSlot_ret_C_' t)) \<longrightarrow> fs_ret_'_update (\<lambda>_. ret__struct_finaliseSlot_ret_C_' t) (s\<lparr>globals := globals t\<rparr>) \<in> {s. (expo \<or> fst rv \<longrightarrow> s \<in> ?S484 exposed slota t rv) \<and> (\<not> (expo \<or> fst rv) \<longrightarrow> s \<in> ?T483 exposed slota t rv)})) \<and> (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. cintr err (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t)) (errstate t) \<longrightarrow> fs_ret_'_update (\<lambda>_. ret__struct_finaliseSlot_ret_C_' t) (s\<lparr>globals := globals t\<rparr>) \<in> ?Q''320 exposed slota t err))}
flex-flex pairs:
?S484 (from_bool expo) (cte_Ptr slot) \<equiv>\<^sup>? \<lambda>t rv. ?S476 rv (ret__struct_finaliseSlot_ret_C_' t)
?T483 (from_bool expo) (cte_Ptr slot) \<equiv>\<^sup>? \<lambda>t rv. ?T476 rv (ret__struct_finaliseSlot_ret_C_' t)
?Q''320 (from_bool expo) (cte_Ptr slot) \<equiv>\<^sup>? \<lambda>t err. ?Q''310 err (ret__struct_finaliseSlot_ret_C_' t) (errstate t) proof (prove)
goal (5 subgoals):
 1. \<And>rv fs_ret. \<lbrakk>finaliseSlot_ret_C.success_C fs_ret = from_bool (fst rv) \<and> ccap_relation (snd rv) (finaliseSlot_ret_C.cleanupInfo_C fs_ret) \<and> cleanup_info_wf' (snd rv); finaliseSlot_ret_C.status_C fs_ret = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; expo \<or> fst rv\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q482 rv) (?S476 rv fs_ret) [SKIP] (liftE (emptySlot slot (snd rv))) (IF True THEN
  CALL emptySlot_'proc(cte_Ptr slot,finaliseSlot_ret_C.cleanupInfo_C fs_ret)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>a. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>rv fs_ret. \<lbrakk>finaliseSlot_ret_C.success_C fs_ret = from_bool (fst rv) \<and> ccap_relation (snd rv) (finaliseSlot_ret_C.cleanupInfo_C fs_ret) \<and> cleanup_info_wf' (snd rv); finaliseSlot_ret_C.status_C fs_ret = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; \<not> (expo \<or> fst rv)\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R481 rv) (?T476 rv fs_ret) [SKIP] (returnOk ()) (IF \<not> expo \<longrightarrow> fst rv THEN
  CALL emptySlot_'proc(cte_Ptr slot,finaliseSlot_ret_C.cleanupInfo_C fs_ret)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>a. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 3. \<And>err rv' fs_ret. \<lbrakk>finaliseSlot_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; cintr err (finaliseSlot_ret_C.status_C rv') fs_ret\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?QE310 err) (?Q''310 err rv' fs_ret) [SKIP] (throwError err) (IF finaliseSlot_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  return_C ret__unsigned_long_'_update (\<lambda>a. finaliseSlot_ret_C.status_C rv')
FI;;
(IF from_bool expo = 0 \<longrightarrow> finaliseSlot_ret_C.success_C rv' \<noteq> 0 THEN
  CALL emptySlot_'proc(cte_Ptr slot,finaliseSlot_ret_C.cleanupInfo_C rv')
FI;;
return_C ret__unsigned_long_'_update (\<lambda>a. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))
 4. \<lbrace>?R327 (from_bool expo) (cte_Ptr slot)\<rbrace> cutMon ((=) s) (finaliseSlot slot expo) \<lbrace>\<lambda>a b. (expo \<or> fst a \<longrightarrow> ?Q482 a b) \<and> (\<not> (expo \<or> fst a) \<longrightarrow> ?R481 a b)\<rbrace>, \<lbrace>?QE310\<rbrace>
 5. \<And>exposed slota s s'. \<lbrakk>exposed = from_bool expo; slota = cte_Ptr slot; (s, s') \<in> rf_sr; invs' s \<and> sch_act_simple s \<and> (expo \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. invs' a \<and> sch_act_simple a \<and> (expo \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot a)) and ?R327 exposed slota) s \<and> s' \<in> {s. immediate_'_update (\<lambda>_. exposed) (slot_'_update (\<lambda>_. slota) s) \<in> UNIV \<inter> \<lbrace>\<acute>slot = slota\<rbrace> \<inter> \<lbrace>\<acute>immediate = exposed\<rbrace>} \<inter> {s. \<forall>t. (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. (case rv of (success, cap) \<Rightarrow> \<lambda>a. case a of (success', cap') \<Rightarrow> success' = from_bool success \<and> ccap_relation cap cap' \<and> cleanup_info_wf' cap) (finaliseSlot_ret_C.success_C (ret__struct_finaliseSlot_ret_C_' t), finaliseSlot_ret_C.cleanupInfo_C (ret__struct_finaliseSlot_ret_C_' t)) \<longrightarrow> fs_ret_'_update (\<lambda>_. ret__struct_finaliseSlot_ret_C_' t) (s\<lparr>globals := globals t\<rparr>) \<in> {s. (expo \<or> fst rv \<longrightarrow> s \<in> ?S484 exposed slota t rv) \<and> (\<not> (expo \<or> fst rv) \<longrightarrow> s \<in> ?T483 exposed slota t rv)})) \<and> (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. cintr err (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t)) (errstate t) \<longrightarrow> fs_ret_'_update (\<lambda>_. ret__struct_finaliseSlot_ret_C_' t) (s\<lparr>globals := globals t\<rparr>) \<in> ?Q''320 exposed slota t err))}
flex-flex pairs:
?S484 (from_bool expo) (cte_Ptr slot) \<equiv>\<^sup>? \<lambda>t rv. ?S476 rv (ret__struct_finaliseSlot_ret_C_' t)
?T483 (from_bool expo) (cte_Ptr slot) \<equiv>\<^sup>? \<lambda>t rv. ?T476 rv (ret__struct_finaliseSlot_ret_C_' t)
?Q''320 (from_bool expo) (cte_Ptr slot) \<equiv>\<^sup>? \<lambda>t err. ?Q''310 err (ret__struct_finaliseSlot_ret_C_' t) (errstate t) proof (prove)
goal (5 subgoals):
 1. \<And>rv fs_ret. \<lbrakk>finaliseSlot_ret_C.success_C fs_ret = from_bool (fst rv) \<and> ccap_relation (snd rv) (finaliseSlot_ret_C.cleanupInfo_C fs_ret) \<and> cleanup_info_wf' (snd rv); finaliseSlot_ret_C.status_C fs_ret = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; expo \<or> fst rv\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q482 rv) (?S476 rv fs_ret) [SKIP] (do x <- emptySlot slot (snd rv);
return (Inr ())
od) (CALL emptySlot_'proc(cte_Ptr slot,finaliseSlot_ret_C.cleanupInfo_C fs_ret);;
return_C ret__unsigned_long_'_update (\<lambda>a. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>rv fs_ret. \<lbrakk>finaliseSlot_ret_C.success_C fs_ret = from_bool (fst rv) \<and> ccap_relation (snd rv) (finaliseSlot_ret_C.cleanupInfo_C fs_ret) \<and> cleanup_info_wf' (snd rv); finaliseSlot_ret_C.status_C fs_ret = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; \<not> (expo \<or> fst rv)\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R481 rv) (?T476 rv fs_ret) [SKIP] (returnOk ()) (IF \<not> expo \<longrightarrow> fst rv THEN
  CALL emptySlot_'proc(cte_Ptr slot,finaliseSlot_ret_C.cleanupInfo_C fs_ret)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>a. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 3. \<And>err rv' fs_ret. \<lbrakk>finaliseSlot_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; cintr err (finaliseSlot_ret_C.status_C rv') fs_ret\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?QE310 err) (?Q''310 err rv' fs_ret) [SKIP] (throwError err) (IF finaliseSlot_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  return_C ret__unsigned_long_'_update (\<lambda>a. finaliseSlot_ret_C.status_C rv')
FI;;
(IF from_bool expo = 0 \<longrightarrow> finaliseSlot_ret_C.success_C rv' \<noteq> 0 THEN
  CALL emptySlot_'proc(cte_Ptr slot,finaliseSlot_ret_C.cleanupInfo_C rv')
FI;;
return_C ret__unsigned_long_'_update (\<lambda>a. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))
 4. \<lbrace>?R327 (from_bool expo) (cte_Ptr slot)\<rbrace> cutMon ((=) s) (finaliseSlot slot expo) \<lbrace>\<lambda>a b. (expo \<or> fst a \<longrightarrow> ?Q482 a b) \<and> (\<not> (expo \<or> fst a) \<longrightarrow> ?R481 a b)\<rbrace>, \<lbrace>?QE310\<rbrace>
 5. \<And>exposed slota s s'. \<lbrakk>exposed = from_bool expo; slota = cte_Ptr slot; (s, s') \<in> rf_sr; invs' s \<and> sch_act_simple s \<and> (expo \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. invs' a \<and> sch_act_simple a \<and> (expo \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot a)) and ?R327 exposed slota) s \<and> s' \<in> {s. immediate_'_update (\<lambda>_. exposed) (slot_'_update (\<lambda>_. slota) s) \<in> UNIV \<inter> \<lbrace>\<acute>slot = slota\<rbrace> \<inter> \<lbrace>\<acute>immediate = exposed\<rbrace>} \<inter> {s. \<forall>t. (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. (case rv of (success, cap) \<Rightarrow> \<lambda>a. case a of (success', cap') \<Rightarrow> success' = from_bool success \<and> ccap_relation cap cap' \<and> cleanup_info_wf' cap) (finaliseSlot_ret_C.success_C (ret__struct_finaliseSlot_ret_C_' t), finaliseSlot_ret_C.cleanupInfo_C (ret__struct_finaliseSlot_ret_C_' t)) \<longrightarrow> fs_ret_'_update (\<lambda>_. ret__struct_finaliseSlot_ret_C_' t) (s\<lparr>globals := globals t\<rparr>) \<in> {s. (expo \<or> fst rv \<longrightarrow> s \<in> ?S484 exposed slota t rv) \<and> (\<not> (expo \<or> fst rv) \<longrightarrow> s \<in> ?T483 exposed slota t rv)})) \<and> (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. cintr err (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t)) (errstate t) \<longrightarrow> fs_ret_'_update (\<lambda>_. ret__struct_finaliseSlot_ret_C_' t) (s\<lparr>globals := globals t\<rparr>) \<in> ?Q''320 exposed slota t err))}
flex-flex pairs:
?S484 (from_bool expo) (cte_Ptr slot) \<equiv>\<^sup>? \<lambda>t rv. ?S476 rv (ret__struct_finaliseSlot_ret_C_' t)
?T483 (from_bool expo) (cte_Ptr slot) \<equiv>\<^sup>? \<lambda>t rv. ?T476 rv (ret__struct_finaliseSlot_ret_C_' t)
?Q''320 (from_bool expo) (cte_Ptr slot) \<equiv>\<^sup>? \<lambda>t err. ?Q''310 err (ret__struct_finaliseSlot_ret_C_' t) (errstate t) proof (prove)
goal (6 subgoals):
 1. \<And>rv fs_ret rva xfdc. \<lbrakk>finaliseSlot_ret_C.success_C fs_ret = from_bool (fst rv) \<and> ccap_relation (snd rv) (finaliseSlot_ret_C.cleanupInfo_C fs_ret) \<and> cleanup_info_wf' (snd rv); finaliseSlot_ret_C.status_C fs_ret = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; expo \<or> fst rv; dc rva xfdc\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q497 rv fs_ret rva) (?Q'497 rv fs_ret rva xfdc) [SKIP] (return (Inr ())) (return_C ret__unsigned_long_'_update (\<lambda>a. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>rv fs_ret. \<lbrakk>finaliseSlot_ret_C.success_C fs_ret = from_bool (fst rv) \<and> ccap_relation (snd rv) (finaliseSlot_ret_C.cleanupInfo_C fs_ret) \<and> cleanup_info_wf' (snd rv); finaliseSlot_ret_C.status_C fs_ret = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; expo \<or> fst rv\<rbrakk> \<Longrightarrow> \<lbrace>?R504 rv\<rbrace> emptySlot slot (snd rv) \<lbrace>?Q497 rv fs_ret\<rbrace>
 3. \<And>rv fs_ret. \<lbrakk>finaliseSlot_ret_C.success_C fs_ret = from_bool (fst rv) \<and> ccap_relation (snd rv) (finaliseSlot_ret_C.cleanupInfo_C fs_ret) \<and> cleanup_info_wf' (snd rv); finaliseSlot_ret_C.status_C fs_ret = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; \<not> (expo \<or> fst rv)\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R481 rv) (?T476 rv fs_ret) [SKIP] (returnOk ()) (IF \<not> expo \<longrightarrow> fst rv THEN
  CALL emptySlot_'proc(cte_Ptr slot,finaliseSlot_ret_C.cleanupInfo_C fs_ret)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>a. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 4. \<And>err rv' fs_ret. \<lbrakk>finaliseSlot_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; cintr err (finaliseSlot_ret_C.status_C rv') fs_ret\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?QE310 err) (?Q''310 err rv' fs_ret) [SKIP] (throwError err) (IF finaliseSlot_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  return_C ret__unsigned_long_'_update (\<lambda>a. finaliseSlot_ret_C.status_C rv')
FI;;
(IF from_bool expo = 0 \<longrightarrow> finaliseSlot_ret_C.success_C rv' \<noteq> 0 THEN
  CALL emptySlot_'proc(cte_Ptr slot,finaliseSlot_ret_C.cleanupInfo_C rv')
FI;;
return_C ret__unsigned_long_'_update (\<lambda>a. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))
 5. \<lbrace>?R327 (from_bool expo) (cte_Ptr slot)\<rbrace> cutMon ((=) s) (finaliseSlot slot expo) \<lbrace>\<lambda>a b. (expo \<or> fst a \<longrightarrow> (valid_mdb' and valid_objs' and pspace_aligned' and untyped_ranges_zero' and ?R504 a) b) \<and> (\<not> (expo \<or> fst a) \<longrightarrow> ?R481 a b)\<rbrace>, \<lbrace>?QE310\<rbrace>
 6. \<And>exposed slota s s'. \<lbrakk>exposed = from_bool expo; slota = cte_Ptr slot; (s, s') \<in> rf_sr; invs' s \<and> sch_act_simple s \<and> (expo \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. invs' a \<and> sch_act_simple a \<and> (expo \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot a)) and ?R327 exposed slota) s \<and> s' \<in> {s. immediate_'_update (\<lambda>_. exposed) (slot_'_update (\<lambda>_. slota) s) \<in> UNIV \<inter> \<lbrace>\<acute>slot = slota\<rbrace> \<inter> \<lbrace>\<acute>immediate = exposed\<rbrace>} \<inter> {s. \<forall>t. (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. (case rv of (success, cap) \<Rightarrow> \<lambda>a. case a of (success', cap') \<Rightarrow> success' = from_bool success \<and> ccap_relation cap cap' \<and> cleanup_info_wf' cap) (finaliseSlot_ret_C.success_C (ret__struct_finaliseSlot_ret_C_' t), finaliseSlot_ret_C.cleanupInfo_C (ret__struct_finaliseSlot_ret_C_' t)) \<longrightarrow> fs_ret_'_update (\<lambda>_. ret__struct_finaliseSlot_ret_C_' t) (s\<lparr>globals := globals t\<rparr>) \<in> {s. (expo \<or> fst rv \<longrightarrow> s \<in> {s. cleanupInfo_'_update (\<lambda>_. finaliseSlot_ret_C.cleanupInfo_C (ret__struct_finaliseSlot_ret_C_' t)) (slot_'_update (\<lambda>_. slota) s) \<in> UNIV \<inter> \<lbrace>\<acute>slot = slota\<rbrace> \<inter> \<lbrace>ccap_relation (snd rv) \<acute>cleanupInfo \<and> cleanup_info_wf' (snd rv)\<rbrace>} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> ?Q'507 exposed slota t rv ta rva}) \<and> (\<not> (expo \<or> fst rv) \<longrightarrow> s \<in> ?T483 exposed slota t rv)})) \<and> (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. cintr err (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t)) (errstate t) \<longrightarrow> fs_ret_'_update (\<lambda>_. ret__struct_finaliseSlot_ret_C_' t) (s\<lparr>globals := globals t\<rparr>) \<in> ?Q''320 exposed slota t err))}
flex-flex pairs:
?Q'507 (from_bool expo) (cte_Ptr slot) \<equiv>\<^sup>? \<lambda>t rv ta rva. ?Q'497 rv (ret__struct_finaliseSlot_ret_C_' t) rva (xfdc ta)
?T483 (from_bool expo) (cte_Ptr slot) \<equiv>\<^sup>? \<lambda>t rv. ?T476 rv (ret__struct_finaliseSlot_ret_C_' t)
?Q''320 (from_bool expo) (cte_Ptr slot) \<equiv>\<^sup>? \<lambda>t err. ?Q''310 err (ret__struct_finaliseSlot_ret_C_' t) (errstate t) proof (prove)
goal (6 subgoals):
 1. \<And>rv fs_ret rva xfdc. \<lbrakk>finaliseSlot_ret_C.success_C fs_ret = from_bool (fst rv) \<and> ccap_relation (snd rv) (finaliseSlot_ret_C.cleanupInfo_C fs_ret) \<and> cleanup_info_wf' (snd rv); finaliseSlot_ret_C.status_C fs_ret = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; expo \<or> fst rv; dc rva xfdc\<rbrakk> \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} return_C ret__unsigned_long_'_update (\<lambda>a. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) {},{s. \<exists>(rv, \<sigma>')\<in>fst (return (Inr ()) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> (cintr \<currency> dc) rv (liftxf errstate id (K ()) ret__unsigned_long_' s)}
 2. \<And>rv fs_ret. \<lbrakk>finaliseSlot_ret_C.success_C fs_ret = from_bool (fst rv) \<and> ccap_relation (snd rv) (finaliseSlot_ret_C.cleanupInfo_C fs_ret) \<and> cleanup_info_wf' (snd rv); finaliseSlot_ret_C.status_C fs_ret = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; expo \<or> fst rv\<rbrakk> \<Longrightarrow> \<lbrace>?R504 rv\<rbrace> emptySlot slot (snd rv) \<lbrace>\<lambda>a b. True\<rbrace>
 3. \<And>rv fs_ret. \<lbrakk>finaliseSlot_ret_C.success_C fs_ret = from_bool (fst rv) \<and> ccap_relation (snd rv) (finaliseSlot_ret_C.cleanupInfo_C fs_ret) \<and> cleanup_info_wf' (snd rv); finaliseSlot_ret_C.status_C fs_ret = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; \<not> (expo \<or> fst rv)\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R481 rv) (?T476 rv fs_ret) [SKIP] (returnOk ()) (IF \<not> expo \<longrightarrow> fst rv THEN
  CALL emptySlot_'proc(cte_Ptr slot,finaliseSlot_ret_C.cleanupInfo_C fs_ret)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>a. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 4. \<And>err rv' fs_ret. \<lbrakk>finaliseSlot_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; cintr err (finaliseSlot_ret_C.status_C rv') fs_ret\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?QE310 err) (?Q''310 err rv' fs_ret) [SKIP] (throwError err) (IF finaliseSlot_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  return_C ret__unsigned_long_'_update (\<lambda>a. finaliseSlot_ret_C.status_C rv')
FI;;
(IF from_bool expo = 0 \<longrightarrow> finaliseSlot_ret_C.success_C rv' \<noteq> 0 THEN
  CALL emptySlot_'proc(cte_Ptr slot,finaliseSlot_ret_C.cleanupInfo_C rv')
FI;;
return_C ret__unsigned_long_'_update (\<lambda>a. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))
 5. \<lbrace>?R327 (from_bool expo) (cte_Ptr slot)\<rbrace> cutMon ((=) s) (finaliseSlot slot expo) \<lbrace>\<lambda>a b. (expo \<or> fst a \<longrightarrow> (valid_mdb' and valid_objs' and pspace_aligned' and untyped_ranges_zero' and ?R504 a) b) \<and> (\<not> (expo \<or> fst a) \<longrightarrow> ?R481 a b)\<rbrace>, \<lbrace>?QE310\<rbrace>
 6. \<And>exposed slota s s'. \<lbrakk>exposed = from_bool expo; slota = cte_Ptr slot; (s, s') \<in> rf_sr; invs' s \<and> sch_act_simple s \<and> (expo \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. invs' a \<and> sch_act_simple a \<and> (expo \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot a)) and ?R327 exposed slota) s \<and> s' \<in> {s. immediate_'_update (\<lambda>_. exposed) (slot_'_update (\<lambda>_. slota) s) \<in> UNIV \<inter> \<lbrace>\<acute>slot = slota\<rbrace> \<inter> \<lbrace>\<acute>immediate = exposed\<rbrace>} \<inter> {s. \<forall>t. (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. (case rv of (success, cap) \<Rightarrow> \<lambda>a. case a of (success', cap') \<Rightarrow> success' = from_bool success \<and> ccap_relation cap cap' \<and> cleanup_info_wf' cap) (finaliseSlot_ret_C.success_C (ret__struct_finaliseSlot_ret_C_' t), finaliseSlot_ret_C.cleanupInfo_C (ret__struct_finaliseSlot_ret_C_' t)) \<longrightarrow> fs_ret_'_update (\<lambda>_. ret__struct_finaliseSlot_ret_C_' t) (s\<lparr>globals := globals t\<rparr>) \<in> {s. (expo \<or> fst rv \<longrightarrow> s \<in> {s. cleanupInfo_'_update (\<lambda>_. finaliseSlot_ret_C.cleanupInfo_C (ret__struct_finaliseSlot_ret_C_' t)) (slot_'_update (\<lambda>_. slota) s) \<in> UNIV \<inter> \<lbrace>\<acute>slot = slota\<rbrace> \<inter> \<lbrace>ccap_relation (snd rv) \<acute>cleanupInfo \<and> cleanup_info_wf' (snd rv)\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}) \<and> (\<not> (expo \<or> fst rv) \<longrightarrow> s \<in> ?T483 exposed slota t rv)})) \<and> (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. cintr err (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t)) (errstate t) \<longrightarrow> fs_ret_'_update (\<lambda>_. ret__struct_finaliseSlot_ret_C_' t) (s\<lparr>globals := globals t\<rparr>) \<in> ?Q''320 exposed slota t err))}
flex-flex pairs:
?T483 (from_bool expo) (cte_Ptr slot) \<equiv>\<^sup>? \<lambda>t rv. ?T476 rv (ret__struct_finaliseSlot_ret_C_' t)
?Q''320 (from_bool expo) (cte_Ptr slot) \<equiv>\<^sup>? \<lambda>t err. ?Q''310 err (ret__struct_finaliseSlot_ret_C_' t) (errstate t) proof (prove)
goal (6 subgoals):
 1. \<And>rv fs_ret rva xfdc \<sigma>. \<lbrakk>finaliseSlot_ret_C.success_C fs_ret = from_bool (fst rv) \<and> ccap_relation (snd rv) (finaliseSlot_ret_C.cleanupInfo_C fs_ret) \<and> cleanup_info_wf' (snd rv); finaliseSlot_ret_C.status_C fs_ret = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; expo \<or> fst rv; dc rva xfdc\<rbrakk> \<Longrightarrow> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (return (Inr ()) \<sigma>). (\<sigma>', s\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>) \<in> rf_sr \<and> (cintr \<currency> dc) rv (liftxf errstate id (K ()) ret__unsigned_long_' (s\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>))}
 2. \<And>rv fs_ret. \<lbrakk>finaliseSlot_ret_C.success_C fs_ret = from_bool (fst rv) \<and> ccap_relation (snd rv) (finaliseSlot_ret_C.cleanupInfo_C fs_ret) \<and> cleanup_info_wf' (snd rv); finaliseSlot_ret_C.status_C fs_ret = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; expo \<or> fst rv\<rbrakk> \<Longrightarrow> \<lbrace>?R504 rv\<rbrace> emptySlot slot (snd rv) \<lbrace>\<lambda>a b. True\<rbrace>
 3. \<And>rv fs_ret. \<lbrakk>finaliseSlot_ret_C.success_C fs_ret = from_bool (fst rv) \<and> ccap_relation (snd rv) (finaliseSlot_ret_C.cleanupInfo_C fs_ret) \<and> cleanup_info_wf' (snd rv); finaliseSlot_ret_C.status_C fs_ret = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; \<not> (expo \<or> fst rv)\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R481 rv) (?T476 rv fs_ret) [SKIP] (returnOk ()) (IF \<not> expo \<longrightarrow> fst rv THEN
  CALL emptySlot_'proc(cte_Ptr slot,finaliseSlot_ret_C.cleanupInfo_C fs_ret)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>a. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 4. \<And>err rv' fs_ret. \<lbrakk>finaliseSlot_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; cintr err (finaliseSlot_ret_C.status_C rv') fs_ret\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?QE310 err) (?Q''310 err rv' fs_ret) [SKIP] (throwError err) (IF finaliseSlot_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  return_C ret__unsigned_long_'_update (\<lambda>a. finaliseSlot_ret_C.status_C rv')
FI;;
(IF from_bool expo = 0 \<longrightarrow> finaliseSlot_ret_C.success_C rv' \<noteq> 0 THEN
  CALL emptySlot_'proc(cte_Ptr slot,finaliseSlot_ret_C.cleanupInfo_C rv')
FI;;
return_C ret__unsigned_long_'_update (\<lambda>a. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))
 5. \<lbrace>?R327 (from_bool expo) (cte_Ptr slot)\<rbrace> cutMon ((=) s) (finaliseSlot slot expo) \<lbrace>\<lambda>a b. (expo \<or> fst a \<longrightarrow> (valid_mdb' and valid_objs' and pspace_aligned' and untyped_ranges_zero' and ?R504 a) b) \<and> (\<not> (expo \<or> fst a) \<longrightarrow> ?R481 a b)\<rbrace>, \<lbrace>?QE310\<rbrace>
 6. \<And>exposed slota s s'. \<lbrakk>exposed = from_bool expo; slota = cte_Ptr slot; (s, s') \<in> rf_sr; invs' s \<and> sch_act_simple s \<and> (expo \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. invs' a \<and> sch_act_simple a \<and> (expo \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot a)) and ?R327 exposed slota) s \<and> s' \<in> {s. immediate_'_update (\<lambda>_. exposed) (slot_'_update (\<lambda>_. slota) s) \<in> UNIV \<inter> \<lbrace>\<acute>slot = slota\<rbrace> \<inter> \<lbrace>\<acute>immediate = exposed\<rbrace>} \<inter> {s. \<forall>t. (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. (case rv of (success, cap) \<Rightarrow> \<lambda>a. case a of (success', cap') \<Rightarrow> success' = from_bool success \<and> ccap_relation cap cap' \<and> cleanup_info_wf' cap) (finaliseSlot_ret_C.success_C (ret__struct_finaliseSlot_ret_C_' t), finaliseSlot_ret_C.cleanupInfo_C (ret__struct_finaliseSlot_ret_C_' t)) \<longrightarrow> fs_ret_'_update (\<lambda>_. ret__struct_finaliseSlot_ret_C_' t) (s\<lparr>globals := globals t\<rparr>) \<in> {s. (expo \<or> fst rv \<longrightarrow> s \<in> {s. cleanupInfo_'_update (\<lambda>_. finaliseSlot_ret_C.cleanupInfo_C (ret__struct_finaliseSlot_ret_C_' t)) (slot_'_update (\<lambda>_. slota) s) \<in> UNIV \<inter> \<lbrace>\<acute>slot = slota\<rbrace> \<inter> \<lbrace>ccap_relation (snd rv) \<acute>cleanupInfo \<and> cleanup_info_wf' (snd rv)\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}) \<and> (\<not> (expo \<or> fst rv) \<longrightarrow> s \<in> ?T483 exposed slota t rv)})) \<and> (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. cintr err (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t)) (errstate t) \<longrightarrow> fs_ret_'_update (\<lambda>_. ret__struct_finaliseSlot_ret_C_' t) (s\<lparr>globals := globals t\<rparr>) \<in> ?Q''320 exposed slota t err))}
flex-flex pairs:
?T483 (from_bool expo) (cte_Ptr slot) \<equiv>\<^sup>? \<lambda>t rv. ?T476 rv (ret__struct_finaliseSlot_ret_C_' t)
?Q''320 (from_bool expo) (cte_Ptr slot) \<equiv>\<^sup>? \<lambda>t err. ?Q''310 err (ret__struct_finaliseSlot_ret_C_' t) (errstate t) proof (prove)
goal (5 subgoals):
 1. \<And>rv fs_ret. \<lbrakk>finaliseSlot_ret_C.success_C fs_ret = from_bool (fst rv) \<and> ccap_relation (snd rv) (finaliseSlot_ret_C.cleanupInfo_C fs_ret) \<and> cleanup_info_wf' (snd rv); finaliseSlot_ret_C.status_C fs_ret = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; expo \<or> fst rv\<rbrakk> \<Longrightarrow> \<lbrace>?R504 rv\<rbrace> emptySlot slot (snd rv) \<lbrace>\<lambda>a b. True\<rbrace>
 2. \<And>rv fs_ret. \<lbrakk>finaliseSlot_ret_C.success_C fs_ret = from_bool (fst rv) \<and> ccap_relation (snd rv) (finaliseSlot_ret_C.cleanupInfo_C fs_ret) \<and> cleanup_info_wf' (snd rv); finaliseSlot_ret_C.status_C fs_ret = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; \<not> (expo \<or> fst rv)\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R481 rv) (?T476 rv fs_ret) [SKIP] (returnOk ()) (IF \<not> expo \<longrightarrow> fst rv THEN
  CALL emptySlot_'proc(cte_Ptr slot,finaliseSlot_ret_C.cleanupInfo_C fs_ret)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>a. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 3. \<And>err rv' fs_ret. \<lbrakk>finaliseSlot_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; cintr err (finaliseSlot_ret_C.status_C rv') fs_ret\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?QE310 err) (?Q''310 err rv' fs_ret) [SKIP] (throwError err) (IF finaliseSlot_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  return_C ret__unsigned_long_'_update (\<lambda>a. finaliseSlot_ret_C.status_C rv')
FI;;
(IF from_bool expo = 0 \<longrightarrow> finaliseSlot_ret_C.success_C rv' \<noteq> 0 THEN
  CALL emptySlot_'proc(cte_Ptr slot,finaliseSlot_ret_C.cleanupInfo_C rv')
FI;;
return_C ret__unsigned_long_'_update (\<lambda>a. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))
 4. \<lbrace>?R327 (from_bool expo) (cte_Ptr slot)\<rbrace> cutMon ((=) s) (finaliseSlot slot expo) \<lbrace>\<lambda>a b. (expo \<or> fst a \<longrightarrow> (valid_mdb' and valid_objs' and pspace_aligned' and untyped_ranges_zero' and ?R504 a) b) \<and> (\<not> (expo \<or> fst a) \<longrightarrow> ?R481 a b)\<rbrace>, \<lbrace>?QE310\<rbrace>
 5. \<And>exposed slota s s'. \<lbrakk>exposed = from_bool expo; slota = cte_Ptr slot; (s, s') \<in> rf_sr; invs' s \<and> sch_act_simple s \<and> (expo \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. invs' a \<and> sch_act_simple a \<and> (expo \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot a)) and ?R327 exposed slota) s \<and> s' \<in> {s. immediate_'_update (\<lambda>_. exposed) (slot_'_update (\<lambda>_. slota) s) \<in> UNIV \<inter> \<lbrace>\<acute>slot = slota\<rbrace> \<inter> \<lbrace>\<acute>immediate = exposed\<rbrace>} \<inter> {s. \<forall>t. (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. (case rv of (success, cap) \<Rightarrow> \<lambda>a. case a of (success', cap') \<Rightarrow> success' = from_bool success \<and> ccap_relation cap cap' \<and> cleanup_info_wf' cap) (finaliseSlot_ret_C.success_C (ret__struct_finaliseSlot_ret_C_' t), finaliseSlot_ret_C.cleanupInfo_C (ret__struct_finaliseSlot_ret_C_' t)) \<longrightarrow> fs_ret_'_update (\<lambda>_. ret__struct_finaliseSlot_ret_C_' t) (s\<lparr>globals := globals t\<rparr>) \<in> {s. (expo \<or> fst rv \<longrightarrow> s \<in> {s. cleanupInfo_'_update (\<lambda>_. finaliseSlot_ret_C.cleanupInfo_C (ret__struct_finaliseSlot_ret_C_' t)) (slot_'_update (\<lambda>_. slota) s) \<in> UNIV \<inter> \<lbrace>\<acute>slot = slota\<rbrace> \<inter> \<lbrace>ccap_relation (snd rv) \<acute>cleanupInfo \<and> cleanup_info_wf' (snd rv)\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}) \<and> (\<not> (expo \<or> fst rv) \<longrightarrow> s \<in> ?T483 exposed slota t rv)})) \<and> (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. cintr err (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t)) (errstate t) \<longrightarrow> fs_ret_'_update (\<lambda>_. ret__struct_finaliseSlot_ret_C_' t) (s\<lparr>globals := globals t\<rparr>) \<in> ?Q''320 exposed slota t err))}
flex-flex pairs:
?T483 (from_bool expo) (cte_Ptr slot) \<equiv>\<^sup>? \<lambda>t rv. ?T476 rv (ret__struct_finaliseSlot_ret_C_' t)
?Q''320 (from_bool expo) (cte_Ptr slot) \<equiv>\<^sup>? \<lambda>t err. ?Q''310 err (ret__struct_finaliseSlot_ret_C_' t) (errstate t) proof (prove)
goal (4 subgoals):
 1. \<And>rv fs_ret. \<lbrakk>finaliseSlot_ret_C.success_C fs_ret = from_bool (fst rv) \<and> ccap_relation (snd rv) (finaliseSlot_ret_C.cleanupInfo_C fs_ret) \<and> cleanup_info_wf' (snd rv); finaliseSlot_ret_C.status_C fs_ret = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; \<not> (expo \<or> fst rv)\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R481 rv) (?T476 rv fs_ret) [SKIP] (returnOk ()) (IF \<not> expo \<longrightarrow> fst rv THEN
  CALL emptySlot_'proc(cte_Ptr slot,finaliseSlot_ret_C.cleanupInfo_C fs_ret)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>a. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>err rv' fs_ret. \<lbrakk>finaliseSlot_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; cintr err (finaliseSlot_ret_C.status_C rv') fs_ret\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?QE310 err) (?Q''310 err rv' fs_ret) [SKIP] (throwError err) (IF finaliseSlot_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  return_C ret__unsigned_long_'_update (\<lambda>a. finaliseSlot_ret_C.status_C rv')
FI;;
(IF from_bool expo = 0 \<longrightarrow> finaliseSlot_ret_C.success_C rv' \<noteq> 0 THEN
  CALL emptySlot_'proc(cte_Ptr slot,finaliseSlot_ret_C.cleanupInfo_C rv')
FI;;
return_C ret__unsigned_long_'_update (\<lambda>a. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))
 3. \<lbrace>?R327 (from_bool expo) (cte_Ptr slot)\<rbrace> cutMon ((=) s) (finaliseSlot slot expo) \<lbrace>\<lambda>a b. (expo \<or> fst a \<longrightarrow> (valid_mdb' and valid_objs' and pspace_aligned' and untyped_ranges_zero' and (\<lambda>a. True)) b) \<and> (\<not> (expo \<or> fst a) \<longrightarrow> ?R481 a b)\<rbrace>, \<lbrace>?QE310\<rbrace>
 4. \<And>exposed slota s s'. \<lbrakk>exposed = from_bool expo; slota = cte_Ptr slot; (s, s') \<in> rf_sr; invs' s \<and> sch_act_simple s \<and> (expo \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. invs' a \<and> sch_act_simple a \<and> (expo \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot a)) and ?R327 exposed slota) s \<and> s' \<in> {s. immediate_'_update (\<lambda>_. exposed) (slot_'_update (\<lambda>_. slota) s) \<in> UNIV \<inter> \<lbrace>\<acute>slot = slota\<rbrace> \<inter> \<lbrace>\<acute>immediate = exposed\<rbrace>} \<inter> {s. \<forall>t. (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. (case rv of (success, cap) \<Rightarrow> \<lambda>a. case a of (success', cap') \<Rightarrow> success' = from_bool success \<and> ccap_relation cap cap' \<and> cleanup_info_wf' cap) (finaliseSlot_ret_C.success_C (ret__struct_finaliseSlot_ret_C_' t), finaliseSlot_ret_C.cleanupInfo_C (ret__struct_finaliseSlot_ret_C_' t)) \<longrightarrow> fs_ret_'_update (\<lambda>_. ret__struct_finaliseSlot_ret_C_' t) (s\<lparr>globals := globals t\<rparr>) \<in> {s. (expo \<or> fst rv \<longrightarrow> s \<in> {s. cleanupInfo_'_update (\<lambda>_. finaliseSlot_ret_C.cleanupInfo_C (ret__struct_finaliseSlot_ret_C_' t)) (slot_'_update (\<lambda>_. slota) s) \<in> UNIV \<inter> \<lbrace>\<acute>slot = slota\<rbrace> \<inter> \<lbrace>ccap_relation (snd rv) \<acute>cleanupInfo \<and> cleanup_info_wf' (snd rv)\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}) \<and> (\<not> (expo \<or> fst rv) \<longrightarrow> s \<in> ?T483 exposed slota t rv)})) \<and> (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. cintr err (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t)) (errstate t) \<longrightarrow> fs_ret_'_update (\<lambda>_. ret__struct_finaliseSlot_ret_C_' t) (s\<lparr>globals := globals t\<rparr>) \<in> ?Q''320 exposed slota t err))}
flex-flex pairs:
?T483 (from_bool expo) (cte_Ptr slot) \<equiv>\<^sup>? \<lambda>t rv. ?T476 rv (ret__struct_finaliseSlot_ret_C_' t)
?Q''320 (from_bool expo) (cte_Ptr slot) \<equiv>\<^sup>? \<lambda>t err. ?Q''310 err (ret__struct_finaliseSlot_ret_C_' t) (errstate t) proof (prove)
goal (4 subgoals):
 1. \<And>rv fs_ret. \<lbrakk>finaliseSlot_ret_C.success_C fs_ret = from_bool (fst rv) \<and> ccap_relation (snd rv) (finaliseSlot_ret_C.cleanupInfo_C fs_ret) \<and> cleanup_info_wf' (snd rv); finaliseSlot_ret_C.status_C fs_ret = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; \<not> (expo \<or> fst rv)\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R481 rv) (?T476 rv fs_ret) [SKIP] (returnOk ()) (IF False THEN
  CALL emptySlot_'proc(cte_Ptr slot,finaliseSlot_ret_C.cleanupInfo_C fs_ret)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>a. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>err rv' fs_ret. \<lbrakk>finaliseSlot_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; cintr err (finaliseSlot_ret_C.status_C rv') fs_ret\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?QE310 err) (?Q''310 err rv' fs_ret) [SKIP] (throwError err) (IF finaliseSlot_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  return_C ret__unsigned_long_'_update (\<lambda>a. finaliseSlot_ret_C.status_C rv')
FI;;
(IF from_bool expo = 0 \<longrightarrow> finaliseSlot_ret_C.success_C rv' \<noteq> 0 THEN
  CALL emptySlot_'proc(cte_Ptr slot,finaliseSlot_ret_C.cleanupInfo_C rv')
FI;;
return_C ret__unsigned_long_'_update (\<lambda>a. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))
 3. \<lbrace>?R327 (from_bool expo) (cte_Ptr slot)\<rbrace> cutMon ((=) s) (finaliseSlot slot expo) \<lbrace>\<lambda>a b. (expo \<or> fst a \<longrightarrow> (valid_mdb' and valid_objs' and pspace_aligned' and untyped_ranges_zero' and (\<lambda>a. True)) b) \<and> (\<not> (expo \<or> fst a) \<longrightarrow> ?R481 a b)\<rbrace>, \<lbrace>?QE310\<rbrace>
 4. \<And>exposed slota s s'. \<lbrakk>exposed = from_bool expo; slota = cte_Ptr slot; (s, s') \<in> rf_sr; invs' s \<and> sch_act_simple s \<and> (expo \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. invs' a \<and> sch_act_simple a \<and> (expo \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot a)) and ?R327 exposed slota) s \<and> s' \<in> {s. immediate_'_update (\<lambda>_. exposed) (slot_'_update (\<lambda>_. slota) s) \<in> UNIV \<inter> \<lbrace>\<acute>slot = slota\<rbrace> \<inter> \<lbrace>\<acute>immediate = exposed\<rbrace>} \<inter> {s. \<forall>t. (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. (case rv of (success, cap) \<Rightarrow> \<lambda>a. case a of (success', cap') \<Rightarrow> success' = from_bool success \<and> ccap_relation cap cap' \<and> cleanup_info_wf' cap) (finaliseSlot_ret_C.success_C (ret__struct_finaliseSlot_ret_C_' t), finaliseSlot_ret_C.cleanupInfo_C (ret__struct_finaliseSlot_ret_C_' t)) \<longrightarrow> fs_ret_'_update (\<lambda>_. ret__struct_finaliseSlot_ret_C_' t) (s\<lparr>globals := globals t\<rparr>) \<in> {s. (expo \<or> fst rv \<longrightarrow> s \<in> {s. cleanupInfo_'_update (\<lambda>_. finaliseSlot_ret_C.cleanupInfo_C (ret__struct_finaliseSlot_ret_C_' t)) (slot_'_update (\<lambda>_. slota) s) \<in> UNIV \<inter> \<lbrace>\<acute>slot = slota\<rbrace> \<inter> \<lbrace>ccap_relation (snd rv) \<acute>cleanupInfo \<and> cleanup_info_wf' (snd rv)\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}) \<and> (\<not> (expo \<or> fst rv) \<longrightarrow> s \<in> ?T483 exposed slota t rv)})) \<and> (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. cintr err (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t)) (errstate t) \<longrightarrow> fs_ret_'_update (\<lambda>_. ret__struct_finaliseSlot_ret_C_' t) (s\<lparr>globals := globals t\<rparr>) \<in> ?Q''320 exposed slota t err))}
flex-flex pairs:
?T483 (from_bool expo) (cte_Ptr slot) \<equiv>\<^sup>? \<lambda>t rv. ?T476 rv (ret__struct_finaliseSlot_ret_C_' t)
?Q''320 (from_bool expo) (cte_Ptr slot) \<equiv>\<^sup>? \<lambda>t err. ?Q''310 err (ret__struct_finaliseSlot_ret_C_' t) (errstate t) proof (prove)
goal (4 subgoals):
 1. \<And>rv fs_ret. \<lbrakk>finaliseSlot_ret_C.success_C fs_ret = SCAST(32 signed \<rightarrow> 32) false \<and> ccap_relation (snd rv) (finaliseSlot_ret_C.cleanupInfo_C fs_ret) \<and> cleanup_info_wf' (snd rv); finaliseSlot_ret_C.status_C fs_ret = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; \<not> expo \<and> \<not> fst rv\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R481 rv) (?T476 rv fs_ret) [SKIP] (return (Inr ())) (return_C ret__unsigned_long_'_update (\<lambda>a. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>err rv' fs_ret. \<lbrakk>finaliseSlot_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; cintr err (finaliseSlot_ret_C.status_C rv') fs_ret\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?QE310 err) (?Q''310 err rv' fs_ret) [SKIP] (throwError err) (IF finaliseSlot_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  return_C ret__unsigned_long_'_update (\<lambda>a. finaliseSlot_ret_C.status_C rv')
FI;;
(IF from_bool expo = 0 \<longrightarrow> finaliseSlot_ret_C.success_C rv' \<noteq> 0 THEN
  CALL emptySlot_'proc(cte_Ptr slot,finaliseSlot_ret_C.cleanupInfo_C rv')
FI;;
return_C ret__unsigned_long_'_update (\<lambda>a. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))
 3. \<lbrace>?R327 (from_bool expo) (cte_Ptr slot)\<rbrace> cutMon ((=) s) (finaliseSlot slot expo) \<lbrace>\<lambda>a b. (expo \<or> fst a \<longrightarrow> (valid_mdb' and valid_objs' and pspace_aligned' and untyped_ranges_zero' and (\<lambda>a. True)) b) \<and> (\<not> (expo \<or> fst a) \<longrightarrow> ?R481 a b)\<rbrace>, \<lbrace>?QE310\<rbrace>
 4. \<And>exposed slota s s'. \<lbrakk>exposed = from_bool expo; slota = cte_Ptr slot; (s, s') \<in> rf_sr; invs' s \<and> sch_act_simple s \<and> (expo \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. invs' a \<and> sch_act_simple a \<and> (expo \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot a)) and ?R327 exposed slota) s \<and> s' \<in> {s. immediate_'_update (\<lambda>_. exposed) (slot_'_update (\<lambda>_. slota) s) \<in> UNIV \<inter> \<lbrace>\<acute>slot = slota\<rbrace> \<inter> \<lbrace>\<acute>immediate = exposed\<rbrace>} \<inter> {s. \<forall>t. (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. (case rv of (success, cap) \<Rightarrow> \<lambda>a. case a of (success', cap') \<Rightarrow> success' = from_bool success \<and> ccap_relation cap cap' \<and> cleanup_info_wf' cap) (finaliseSlot_ret_C.success_C (ret__struct_finaliseSlot_ret_C_' t), finaliseSlot_ret_C.cleanupInfo_C (ret__struct_finaliseSlot_ret_C_' t)) \<longrightarrow> fs_ret_'_update (\<lambda>_. ret__struct_finaliseSlot_ret_C_' t) (s\<lparr>globals := globals t\<rparr>) \<in> {s. (expo \<or> fst rv \<longrightarrow> s \<in> {s. cleanupInfo_'_update (\<lambda>_. finaliseSlot_ret_C.cleanupInfo_C (ret__struct_finaliseSlot_ret_C_' t)) (slot_'_update (\<lambda>_. slota) s) \<in> UNIV \<inter> \<lbrace>\<acute>slot = slota\<rbrace> \<inter> \<lbrace>ccap_relation (snd rv) \<acute>cleanupInfo \<and> cleanup_info_wf' (snd rv)\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}) \<and> (\<not> (expo \<or> fst rv) \<longrightarrow> s \<in> ?T483 exposed slota t rv)})) \<and> (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. cintr err (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t)) (errstate t) \<longrightarrow> fs_ret_'_update (\<lambda>_. ret__struct_finaliseSlot_ret_C_' t) (s\<lparr>globals := globals t\<rparr>) \<in> ?Q''320 exposed slota t err))}
flex-flex pairs:
?T483 (from_bool expo) (cte_Ptr slot) \<equiv>\<^sup>? \<lambda>t rv. ?T476 rv (ret__struct_finaliseSlot_ret_C_' t)
?Q''320 (from_bool expo) (cte_Ptr slot) \<equiv>\<^sup>? \<lambda>t err. ?Q''310 err (ret__struct_finaliseSlot_ret_C_' t) (errstate t) proof (prove)
goal (4 subgoals):
 1. \<And>rv fs_ret. \<lbrakk>finaliseSlot_ret_C.success_C fs_ret = SCAST(32 signed \<rightarrow> 32) false \<and> ccap_relation (snd rv) (finaliseSlot_ret_C.cleanupInfo_C fs_ret) \<and> cleanup_info_wf' (snd rv); finaliseSlot_ret_C.status_C fs_ret = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; \<not> expo \<and> \<not> fst rv\<rbrakk> \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} return_C ret__unsigned_long_'_update (\<lambda>a. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) {},{s. \<exists>(rv, \<sigma>')\<in>fst (return (Inr ()) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> (cintr \<currency> dc) rv (liftxf errstate id (K ()) ret__unsigned_long_' s)}
 2. \<And>err rv' fs_ret. \<lbrakk>finaliseSlot_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; cintr err (finaliseSlot_ret_C.status_C rv') fs_ret\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?QE310 err) (?Q''310 err rv' fs_ret) [SKIP] (throwError err) (IF finaliseSlot_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  return_C ret__unsigned_long_'_update (\<lambda>a. finaliseSlot_ret_C.status_C rv')
FI;;
(IF from_bool expo = 0 \<longrightarrow> finaliseSlot_ret_C.success_C rv' \<noteq> 0 THEN
  CALL emptySlot_'proc(cte_Ptr slot,finaliseSlot_ret_C.cleanupInfo_C rv')
FI;;
return_C ret__unsigned_long_'_update (\<lambda>a. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))
 3. \<lbrace>?R327 (from_bool expo) (cte_Ptr slot)\<rbrace> cutMon ((=) s) (finaliseSlot slot expo) \<lbrace>\<lambda>a b. (expo \<or> fst a \<longrightarrow> (valid_mdb' and valid_objs' and pspace_aligned' and untyped_ranges_zero' and (\<lambda>a. True)) b) \<and> (\<not> (expo \<or> fst a) \<longrightarrow> True)\<rbrace>, \<lbrace>?QE310\<rbrace>
 4. \<And>exposed slota s s'. \<lbrakk>exposed = from_bool expo; slota = cte_Ptr slot; (s, s') \<in> rf_sr; invs' s \<and> sch_act_simple s \<and> (expo \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. invs' a \<and> sch_act_simple a \<and> (expo \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot a)) and ?R327 exposed slota) s \<and> s' \<in> {s. immediate_'_update (\<lambda>_. exposed) (slot_'_update (\<lambda>_. slota) s) \<in> UNIV \<inter> \<lbrace>\<acute>slot = slota\<rbrace> \<inter> \<lbrace>\<acute>immediate = exposed\<rbrace>} \<inter> {s. \<forall>t. (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. (case rv of (success, cap) \<Rightarrow> \<lambda>a. case a of (success', cap') \<Rightarrow> success' = from_bool success \<and> ccap_relation cap cap' \<and> cleanup_info_wf' cap) (finaliseSlot_ret_C.success_C (ret__struct_finaliseSlot_ret_C_' t), finaliseSlot_ret_C.cleanupInfo_C (ret__struct_finaliseSlot_ret_C_' t)) \<longrightarrow> fs_ret_'_update (\<lambda>_. ret__struct_finaliseSlot_ret_C_' t) (s\<lparr>globals := globals t\<rparr>) \<in> {s. (expo \<or> fst rv \<longrightarrow> s \<in> {s. cleanupInfo_'_update (\<lambda>_. finaliseSlot_ret_C.cleanupInfo_C (ret__struct_finaliseSlot_ret_C_' t)) (slot_'_update (\<lambda>_. slota) s) \<in> UNIV \<inter> \<lbrace>\<acute>slot = slota\<rbrace> \<inter> \<lbrace>ccap_relation (snd rv) \<acute>cleanupInfo \<and> cleanup_info_wf' (snd rv)\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}) \<and> (\<not> (expo \<or> fst rv) \<longrightarrow> s \<in> UNIV)})) \<and> (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. cintr err (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t)) (errstate t) \<longrightarrow> fs_ret_'_update (\<lambda>_. ret__struct_finaliseSlot_ret_C_' t) (s\<lparr>globals := globals t\<rparr>) \<in> ?Q''320 exposed slota t err))}
flex-flex pairs:
?Q''320 (from_bool expo) (cte_Ptr slot) \<equiv>\<^sup>? \<lambda>t err. ?Q''310 err (ret__struct_finaliseSlot_ret_C_' t) (errstate t) proof (prove)
goal (4 subgoals):
 1. \<And>rv fs_ret \<sigma>. \<lbrakk>finaliseSlot_ret_C.success_C fs_ret = SCAST(32 signed \<rightarrow> 32) false \<and> ccap_relation (snd rv) (finaliseSlot_ret_C.cleanupInfo_C fs_ret) \<and> cleanup_info_wf' (snd rv); finaliseSlot_ret_C.status_C fs_ret = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; \<not> expo \<and> \<not> fst rv\<rbrakk> \<Longrightarrow> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (return (Inr ()) \<sigma>). (\<sigma>', s\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>) \<in> rf_sr \<and> (cintr \<currency> dc) rv (liftxf errstate id (K ()) ret__unsigned_long_' (s\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>))}
 2. \<And>err rv' fs_ret. \<lbrakk>finaliseSlot_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; cintr err (finaliseSlot_ret_C.status_C rv') fs_ret\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?QE310 err) (?Q''310 err rv' fs_ret) [SKIP] (throwError err) (IF finaliseSlot_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  return_C ret__unsigned_long_'_update (\<lambda>a. finaliseSlot_ret_C.status_C rv')
FI;;
(IF from_bool expo = 0 \<longrightarrow> finaliseSlot_ret_C.success_C rv' \<noteq> 0 THEN
  CALL emptySlot_'proc(cte_Ptr slot,finaliseSlot_ret_C.cleanupInfo_C rv')
FI;;
return_C ret__unsigned_long_'_update (\<lambda>a. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))
 3. \<lbrace>?R327 (from_bool expo) (cte_Ptr slot)\<rbrace> cutMon ((=) s) (finaliseSlot slot expo) \<lbrace>\<lambda>a b. (expo \<or> fst a \<longrightarrow> (valid_mdb' and valid_objs' and pspace_aligned' and untyped_ranges_zero' and (\<lambda>a. True)) b) \<and> (\<not> (expo \<or> fst a) \<longrightarrow> True)\<rbrace>, \<lbrace>?QE310\<rbrace>
 4. \<And>exposed slota s s'. \<lbrakk>exposed = from_bool expo; slota = cte_Ptr slot; (s, s') \<in> rf_sr; invs' s \<and> sch_act_simple s \<and> (expo \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. invs' a \<and> sch_act_simple a \<and> (expo \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot a)) and ?R327 exposed slota) s \<and> s' \<in> {s. immediate_'_update (\<lambda>_. exposed) (slot_'_update (\<lambda>_. slota) s) \<in> UNIV \<inter> \<lbrace>\<acute>slot = slota\<rbrace> \<inter> \<lbrace>\<acute>immediate = exposed\<rbrace>} \<inter> {s. \<forall>t. (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. (case rv of (success, cap) \<Rightarrow> \<lambda>a. case a of (success', cap') \<Rightarrow> success' = from_bool success \<and> ccap_relation cap cap' \<and> cleanup_info_wf' cap) (finaliseSlot_ret_C.success_C (ret__struct_finaliseSlot_ret_C_' t), finaliseSlot_ret_C.cleanupInfo_C (ret__struct_finaliseSlot_ret_C_' t)) \<longrightarrow> fs_ret_'_update (\<lambda>_. ret__struct_finaliseSlot_ret_C_' t) (s\<lparr>globals := globals t\<rparr>) \<in> {s. (expo \<or> fst rv \<longrightarrow> s \<in> {s. cleanupInfo_'_update (\<lambda>_. finaliseSlot_ret_C.cleanupInfo_C (ret__struct_finaliseSlot_ret_C_' t)) (slot_'_update (\<lambda>_. slota) s) \<in> UNIV \<inter> \<lbrace>\<acute>slot = slota\<rbrace> \<inter> \<lbrace>ccap_relation (snd rv) \<acute>cleanupInfo \<and> cleanup_info_wf' (snd rv)\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}) \<and> (\<not> (expo \<or> fst rv) \<longrightarrow> s \<in> UNIV)})) \<and> (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. cintr err (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t)) (errstate t) \<longrightarrow> fs_ret_'_update (\<lambda>_. ret__struct_finaliseSlot_ret_C_' t) (s\<lparr>globals := globals t\<rparr>) \<in> ?Q''320 exposed slota t err))}
flex-flex pairs:
?Q''320 (from_bool expo) (cte_Ptr slot) \<equiv>\<^sup>? \<lambda>t err. ?Q''310 err (ret__struct_finaliseSlot_ret_C_' t) (errstate t) proof (prove)
goal (3 subgoals):
 1. \<And>err rv' fs_ret. \<lbrakk>finaliseSlot_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; cintr err (finaliseSlot_ret_C.status_C rv') fs_ret\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?QE310 err) (?Q''310 err rv' fs_ret) [SKIP] (throwError err) (IF finaliseSlot_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  return_C ret__unsigned_long_'_update (\<lambda>a. finaliseSlot_ret_C.status_C rv')
FI;;
(IF from_bool expo = 0 \<longrightarrow> finaliseSlot_ret_C.success_C rv' \<noteq> 0 THEN
  CALL emptySlot_'proc(cte_Ptr slot,finaliseSlot_ret_C.cleanupInfo_C rv')
FI;;
return_C ret__unsigned_long_'_update (\<lambda>a. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))
 2. \<lbrace>?R327 (from_bool expo) (cte_Ptr slot)\<rbrace> cutMon ((=) s) (finaliseSlot slot expo) \<lbrace>\<lambda>a b. (expo \<or> fst a \<longrightarrow> (valid_mdb' and valid_objs' and pspace_aligned' and untyped_ranges_zero' and (\<lambda>a. True)) b) \<and> (\<not> (expo \<or> fst a) \<longrightarrow> True)\<rbrace>, \<lbrace>?QE310\<rbrace>
 3. \<And>exposed slota s s'. \<lbrakk>exposed = from_bool expo; slota = cte_Ptr slot; (s, s') \<in> rf_sr; invs' s \<and> sch_act_simple s \<and> (expo \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. invs' a \<and> sch_act_simple a \<and> (expo \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot a)) and ?R327 exposed slota) s \<and> s' \<in> {s. immediate_'_update (\<lambda>_. exposed) (slot_'_update (\<lambda>_. slota) s) \<in> UNIV \<inter> \<lbrace>\<acute>slot = slota\<rbrace> \<inter> \<lbrace>\<acute>immediate = exposed\<rbrace>} \<inter> {s. \<forall>t. (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. (case rv of (success, cap) \<Rightarrow> \<lambda>a. case a of (success', cap') \<Rightarrow> success' = from_bool success \<and> ccap_relation cap cap' \<and> cleanup_info_wf' cap) (finaliseSlot_ret_C.success_C (ret__struct_finaliseSlot_ret_C_' t), finaliseSlot_ret_C.cleanupInfo_C (ret__struct_finaliseSlot_ret_C_' t)) \<longrightarrow> fs_ret_'_update (\<lambda>_. ret__struct_finaliseSlot_ret_C_' t) (s\<lparr>globals := globals t\<rparr>) \<in> {s. (expo \<or> fst rv \<longrightarrow> s \<in> {s. cleanupInfo_'_update (\<lambda>_. finaliseSlot_ret_C.cleanupInfo_C (ret__struct_finaliseSlot_ret_C_' t)) (slot_'_update (\<lambda>_. slota) s) \<in> UNIV \<inter> \<lbrace>\<acute>slot = slota\<rbrace> \<inter> \<lbrace>ccap_relation (snd rv) \<acute>cleanupInfo \<and> cleanup_info_wf' (snd rv)\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}) \<and> (\<not> (expo \<or> fst rv) \<longrightarrow> s \<in> UNIV)})) \<and> (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. cintr err (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t)) (errstate t) \<longrightarrow> fs_ret_'_update (\<lambda>_. ret__struct_finaliseSlot_ret_C_' t) (s\<lparr>globals := globals t\<rparr>) \<in> ?Q''320 exposed slota t err))}
flex-flex pairs:
?Q''320 (from_bool expo) (cte_Ptr slot) \<equiv>\<^sup>? \<lambda>t err. ?Q''310 err (ret__struct_finaliseSlot_ret_C_' t) (errstate t) proof (prove)
goal (3 subgoals):
 1. \<And>err rv' fs_ret. \<lbrakk>finaliseSlot_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; cintr err (finaliseSlot_ret_C.status_C rv') fs_ret\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?QE310 err) (?Q''310 err rv' fs_ret) [SKIP] (throwError err) (return_C ret__unsigned_long_'_update (\<lambda>a. finaliseSlot_ret_C.status_C rv');;
(Cond (if from_bool expo = 0 \<longrightarrow> finaliseSlot_ret_C.success_C rv' \<noteq> 0 then UNIV else {}) (CALL emptySlot_'proc(cte_Ptr slot,finaliseSlot_ret_C.cleanupInfo_C rv')) SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>a. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))
 2. \<lbrace>?R327 (from_bool expo) (cte_Ptr slot)\<rbrace> cutMon ((=) s) (finaliseSlot slot expo) \<lbrace>\<lambda>a b. (expo \<or> fst a \<longrightarrow> (valid_mdb' and valid_objs' and pspace_aligned' and untyped_ranges_zero' and (\<lambda>a. True)) b) \<and> (\<not> (expo \<or> fst a) \<longrightarrow> True)\<rbrace>, \<lbrace>?QE310\<rbrace>
 3. \<And>exposed slota s s'. \<lbrakk>exposed = from_bool expo; slota = cte_Ptr slot; (s, s') \<in> rf_sr; invs' s \<and> sch_act_simple s \<and> (expo \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. invs' a \<and> sch_act_simple a \<and> (expo \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot a)) and ?R327 exposed slota) s \<and> s' \<in> {s. immediate_'_update (\<lambda>_. exposed) (slot_'_update (\<lambda>_. slota) s) \<in> UNIV \<inter> \<lbrace>\<acute>slot = slota\<rbrace> \<inter> \<lbrace>\<acute>immediate = exposed\<rbrace>} \<inter> {s. \<forall>t. (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. (case rv of (success, cap) \<Rightarrow> \<lambda>a. case a of (success', cap') \<Rightarrow> success' = from_bool success \<and> ccap_relation cap cap' \<and> cleanup_info_wf' cap) (finaliseSlot_ret_C.success_C (ret__struct_finaliseSlot_ret_C_' t), finaliseSlot_ret_C.cleanupInfo_C (ret__struct_finaliseSlot_ret_C_' t)) \<longrightarrow> fs_ret_'_update (\<lambda>_. ret__struct_finaliseSlot_ret_C_' t) (s\<lparr>globals := globals t\<rparr>) \<in> {s. (expo \<or> fst rv \<longrightarrow> s \<in> {s. cleanupInfo_'_update (\<lambda>_. finaliseSlot_ret_C.cleanupInfo_C (ret__struct_finaliseSlot_ret_C_' t)) (slot_'_update (\<lambda>_. slota) s) \<in> UNIV \<inter> \<lbrace>\<acute>slot = slota\<rbrace> \<inter> \<lbrace>ccap_relation (snd rv) \<acute>cleanupInfo \<and> cleanup_info_wf' (snd rv)\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}) \<and> (\<not> (expo \<or> fst rv) \<longrightarrow> s \<in> UNIV)})) \<and> (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. cintr err (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t)) (errstate t) \<longrightarrow> fs_ret_'_update (\<lambda>_. ret__struct_finaliseSlot_ret_C_' t) (s\<lparr>globals := globals t\<rparr>) \<in> ?Q''320 exposed slota t err))}
flex-flex pairs:
?Q''320 (from_bool expo) (cte_Ptr slot) \<equiv>\<^sup>? \<lambda>t err. ?Q''310 err (ret__struct_finaliseSlot_ret_C_' t) (errstate t) proof (prove)
goal (4 subgoals):
 1. \<And>err rv' fs_ret. \<lbrakk>finaliseSlot_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; cintr err (finaliseSlot_ret_C.status_C rv') fs_ret\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?QE310 err) (?P'564 err rv' fs_ret) [SKIP] (throwError err) (return_C ret__unsigned_long_'_update (\<lambda>a. finaliseSlot_ret_C.status_C rv'))
 2. \<And>err rv' fs_ret. \<lbrakk>finaliseSlot_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; cintr err (finaliseSlot_ret_C.status_C rv') fs_ret\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'564 err rv' fs_ret) return_C ret__unsigned_long_'_update (\<lambda>a. finaliseSlot_ret_C.status_C rv') {},UNIV
 3. \<lbrace>?R327 (from_bool expo) (cte_Ptr slot)\<rbrace> cutMon ((=) s) (finaliseSlot slot expo) \<lbrace>\<lambda>a b. (expo \<or> fst a \<longrightarrow> (valid_mdb' and valid_objs' and pspace_aligned' and untyped_ranges_zero' and (\<lambda>a. True)) b) \<and> (\<not> (expo \<or> fst a) \<longrightarrow> True)\<rbrace>, \<lbrace>?QE310\<rbrace>
 4. \<And>exposed slota s s'. \<lbrakk>exposed = from_bool expo; slota = cte_Ptr slot; (s, s') \<in> rf_sr; invs' s \<and> sch_act_simple s \<and> (expo \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. invs' a \<and> sch_act_simple a \<and> (expo \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot a)) and ?R327 exposed slota) s \<and> s' \<in> {s. immediate_'_update (\<lambda>_. exposed) (slot_'_update (\<lambda>_. slota) s) \<in> UNIV \<inter> \<lbrace>\<acute>slot = slota\<rbrace> \<inter> \<lbrace>\<acute>immediate = exposed\<rbrace>} \<inter> {s. \<forall>t. (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. (case rv of (success, cap) \<Rightarrow> \<lambda>a. case a of (success', cap') \<Rightarrow> success' = from_bool success \<and> ccap_relation cap cap' \<and> cleanup_info_wf' cap) (finaliseSlot_ret_C.success_C (ret__struct_finaliseSlot_ret_C_' t), finaliseSlot_ret_C.cleanupInfo_C (ret__struct_finaliseSlot_ret_C_' t)) \<longrightarrow> fs_ret_'_update (\<lambda>_. ret__struct_finaliseSlot_ret_C_' t) (s\<lparr>globals := globals t\<rparr>) \<in> {s. (expo \<or> fst rv \<longrightarrow> s \<in> {s. cleanupInfo_'_update (\<lambda>_. finaliseSlot_ret_C.cleanupInfo_C (ret__struct_finaliseSlot_ret_C_' t)) (slot_'_update (\<lambda>_. slota) s) \<in> UNIV \<inter> \<lbrace>\<acute>slot = slota\<rbrace> \<inter> \<lbrace>ccap_relation (snd rv) \<acute>cleanupInfo \<and> cleanup_info_wf' (snd rv)\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}) \<and> (\<not> (expo \<or> fst rv) \<longrightarrow> s \<in> UNIV)})) \<and> (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. cintr err (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t)) (errstate t) \<longrightarrow> fs_ret_'_update (\<lambda>_. ret__struct_finaliseSlot_ret_C_' t) (s\<lparr>globals := globals t\<rparr>) \<in> ?P'566 exposed slota t err \<inter> ?R'565 exposed slota t err))}
flex-flex pairs:
?P'566 (from_bool expo) (cte_Ptr slot) \<equiv>\<^sup>? \<lambda>t err. ?P'564 err (ret__struct_finaliseSlot_ret_C_' t) (errstate t)
?R'565 (from_bool expo) (cte_Ptr slot) \<equiv>\<^sup>? \<lambda>t err. ?R'564 err (ret__struct_finaliseSlot_ret_C_' t) (errstate t) proof (prove)
goal (3 subgoals):
 1. \<And>err rv' fs_ret. \<lbrakk>finaliseSlot_ret_C.status_C rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; cintr err (finaliseSlot_ret_C.status_C rv') fs_ret\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'564 err rv' fs_ret) return_C ret__unsigned_long_'_update (\<lambda>a. finaliseSlot_ret_C.status_C rv') {},UNIV
 2. \<lbrace>?R327 (from_bool expo) (cte_Ptr slot)\<rbrace> cutMon ((=) s) (finaliseSlot slot expo) \<lbrace>\<lambda>a b. (expo \<or> fst a \<longrightarrow> (valid_mdb' and valid_objs' and pspace_aligned' and untyped_ranges_zero' and (\<lambda>a. True)) b) \<and> (\<not> (expo \<or> fst a) \<longrightarrow> True)\<rbrace>, \<lbrace>\<lambda>a b. True\<rbrace>
 3. \<And>exposed slota s s'. \<lbrakk>exposed = from_bool expo; slota = cte_Ptr slot; (s, s') \<in> rf_sr; invs' s \<and> sch_act_simple s \<and> (expo \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. invs' a \<and> sch_act_simple a \<and> (expo \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot a)) and ?R327 exposed slota) s \<and> s' \<in> {s. immediate_'_update (\<lambda>_. exposed) (slot_'_update (\<lambda>_. slota) s) \<in> UNIV \<inter> \<lbrace>\<acute>slot = slota\<rbrace> \<inter> \<lbrace>\<acute>immediate = exposed\<rbrace>} \<inter> {s. \<forall>t. (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. (case rv of (success, cap) \<Rightarrow> \<lambda>a. case a of (success', cap') \<Rightarrow> success' = from_bool success \<and> ccap_relation cap cap' \<and> cleanup_info_wf' cap) (finaliseSlot_ret_C.success_C (ret__struct_finaliseSlot_ret_C_' t), finaliseSlot_ret_C.cleanupInfo_C (ret__struct_finaliseSlot_ret_C_' t)) \<longrightarrow> fs_ret_'_update (\<lambda>_. ret__struct_finaliseSlot_ret_C_' t) (s\<lparr>globals := globals t\<rparr>) \<in> {s. (expo \<or> fst rv \<longrightarrow> s \<in> {s. cleanupInfo_'_update (\<lambda>_. finaliseSlot_ret_C.cleanupInfo_C (ret__struct_finaliseSlot_ret_C_' t)) (slot_'_update (\<lambda>_. slota) s) \<in> UNIV \<inter> \<lbrace>\<acute>slot = slota\<rbrace> \<inter> \<lbrace>ccap_relation (snd rv) \<acute>cleanupInfo \<and> cleanup_info_wf' (snd rv)\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}) \<and> (\<not> (expo \<or> fst rv) \<longrightarrow> s \<in> UNIV)})) \<and> (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. cintr err (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t)) (errstate t) \<longrightarrow> fs_ret_'_update (\<lambda>_. ret__struct_finaliseSlot_ret_C_' t) (s\<lparr>globals := globals t\<rparr>) \<in> {s. id (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t)) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> cintr err (id (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t))) (errstate s)} \<inter> ?R'565 exposed slota t err))}
flex-flex pairs:
?R'565 (from_bool expo) (cte_Ptr slot) \<equiv>\<^sup>? \<lambda>t err. ?R'564 err (ret__struct_finaliseSlot_ret_C_' t) (errstate t) proof (prove)
goal (2 subgoals):
 1. \<lbrace>?R327 (from_bool expo) (cte_Ptr slot)\<rbrace> cutMon ((=) s) (finaliseSlot slot expo) \<lbrace>\<lambda>a b. (expo \<or> fst a \<longrightarrow> (valid_mdb' and valid_objs' and pspace_aligned' and untyped_ranges_zero' and (\<lambda>a. True)) b) \<and> (\<not> (expo \<or> fst a) \<longrightarrow> True)\<rbrace>, \<lbrace>\<lambda>a b. True\<rbrace>
 2. \<And>exposed slota s s'. \<lbrakk>exposed = from_bool expo; slota = cte_Ptr slot; (s, s') \<in> rf_sr; invs' s \<and> sch_act_simple s \<and> (expo \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. invs' a \<and> sch_act_simple a \<and> (expo \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot a)) and ?R327 exposed slota) s \<and> s' \<in> {s. immediate_'_update (\<lambda>_. exposed) (slot_'_update (\<lambda>_. slota) s) \<in> UNIV \<inter> \<lbrace>\<acute>slot = slota\<rbrace> \<inter> \<lbrace>\<acute>immediate = exposed\<rbrace>} \<inter> {s. \<forall>t. (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. (case rv of (success, cap) \<Rightarrow> \<lambda>a. case a of (success', cap') \<Rightarrow> success' = from_bool success \<and> ccap_relation cap cap' \<and> cleanup_info_wf' cap) (finaliseSlot_ret_C.success_C (ret__struct_finaliseSlot_ret_C_' t), finaliseSlot_ret_C.cleanupInfo_C (ret__struct_finaliseSlot_ret_C_' t)) \<longrightarrow> fs_ret_'_update (\<lambda>_. ret__struct_finaliseSlot_ret_C_' t) (s\<lparr>globals := globals t\<rparr>) \<in> {s. (expo \<or> fst rv \<longrightarrow> s \<in> {s. cleanupInfo_'_update (\<lambda>_. finaliseSlot_ret_C.cleanupInfo_C (ret__struct_finaliseSlot_ret_C_' t)) (slot_'_update (\<lambda>_. slota) s) \<in> UNIV \<inter> \<lbrace>\<acute>slot = slota\<rbrace> \<inter> \<lbrace>ccap_relation (snd rv) \<acute>cleanupInfo \<and> cleanup_info_wf' (snd rv)\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}) \<and> (\<not> (expo \<or> fst rv) \<longrightarrow> s \<in> UNIV)})) \<and> (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. cintr err (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t)) (errstate t) \<longrightarrow> fs_ret_'_update (\<lambda>_. ret__struct_finaliseSlot_ret_C_' t) (s\<lparr>globals := globals t\<rparr>) \<in> {s. id (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t)) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> cintr err (id (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t))) (errstate s)} \<inter> \<lbrace>True\<rbrace>))} proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'583 (from_bool expo) (cte_Ptr slot)\<rbrace> cutMon ((=) s) (finaliseSlot slot expo) \<lbrace>\<lambda>a b. (expo \<or> fst a \<longrightarrow> (valid_mdb' and valid_objs' and pspace_aligned' and untyped_ranges_zero' and (\<lambda>a. True)) b) \<and> (\<not> (expo \<or> fst a) \<longrightarrow> True)\<rbrace>, -
 2. \<And>exposed slota s s'. \<lbrakk>exposed = from_bool expo; slota = cte_Ptr slot; (s, s') \<in> rf_sr; invs' s \<and> sch_act_simple s \<and> (expo \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. invs' a \<and> sch_act_simple a \<and> (expo \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot a)) and (\<lambda>a. True \<and> ?P'583 exposed slota a)) s \<and> s' \<in> {s. immediate_'_update (\<lambda>_. exposed) (slot_'_update (\<lambda>_. slota) s) \<in> UNIV \<inter> \<lbrace>\<acute>slot = slota\<rbrace> \<inter> \<lbrace>\<acute>immediate = exposed\<rbrace>} \<inter> {s. \<forall>t. (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. (case rv of (success, cap) \<Rightarrow> \<lambda>a. case a of (success', cap') \<Rightarrow> success' = from_bool success \<and> ccap_relation cap cap' \<and> cleanup_info_wf' cap) (finaliseSlot_ret_C.success_C (ret__struct_finaliseSlot_ret_C_' t), finaliseSlot_ret_C.cleanupInfo_C (ret__struct_finaliseSlot_ret_C_' t)) \<longrightarrow> fs_ret_'_update (\<lambda>_. ret__struct_finaliseSlot_ret_C_' t) (s\<lparr>globals := globals t\<rparr>) \<in> {s. (expo \<or> fst rv \<longrightarrow> s \<in> {s. cleanupInfo_'_update (\<lambda>_. finaliseSlot_ret_C.cleanupInfo_C (ret__struct_finaliseSlot_ret_C_' t)) (slot_'_update (\<lambda>_. slota) s) \<in> UNIV \<inter> \<lbrace>\<acute>slot = slota\<rbrace> \<inter> \<lbrace>ccap_relation (snd rv) \<acute>cleanupInfo \<and> cleanup_info_wf' (snd rv)\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}) \<and> (\<not> (expo \<or> fst rv) \<longrightarrow> s \<in> UNIV)})) \<and> (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. cintr err (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t)) (errstate t) \<longrightarrow> fs_ret_'_update (\<lambda>_. ret__struct_finaliseSlot_ret_C_' t) (s\<lparr>globals := globals t\<rparr>) \<in> {s. id (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t)) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> cintr err (id (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t))) (errstate s)} \<inter> \<lbrace>True\<rbrace>))} proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P'583 (from_bool expo) (cte_Ptr slot)\<rbrace> cutMon ((=) s) (finaliseSlot slot expo) \<lbrace>\<lambda>rv. invs'\<rbrace>, -
 2. \<And>rv s. invs' s \<Longrightarrow> (expo \<or> fst rv \<longrightarrow> (valid_mdb' and valid_objs' and pspace_aligned' and untyped_ranges_zero' and (\<lambda>a. True)) s) \<and> (\<not> (expo \<or> fst rv) \<longrightarrow> True)
 3. \<And>exposed slota s s'. \<lbrakk>exposed = from_bool expo; slota = cte_Ptr slot; (s, s') \<in> rf_sr; invs' s \<and> sch_act_simple s \<and> (expo \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. invs' a \<and> sch_act_simple a \<and> (expo \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot a)) and (\<lambda>a. True \<and> ?P'583 exposed slota a)) s \<and> s' \<in> {s. immediate_'_update (\<lambda>_. exposed) (slot_'_update (\<lambda>_. slota) s) \<in> UNIV \<inter> \<lbrace>\<acute>slot = slota\<rbrace> \<inter> \<lbrace>\<acute>immediate = exposed\<rbrace>} \<inter> {s. \<forall>t. (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. (case rv of (success, cap) \<Rightarrow> \<lambda>a. case a of (success', cap') \<Rightarrow> success' = from_bool success \<and> ccap_relation cap cap' \<and> cleanup_info_wf' cap) (finaliseSlot_ret_C.success_C (ret__struct_finaliseSlot_ret_C_' t), finaliseSlot_ret_C.cleanupInfo_C (ret__struct_finaliseSlot_ret_C_' t)) \<longrightarrow> fs_ret_'_update (\<lambda>_. ret__struct_finaliseSlot_ret_C_' t) (s\<lparr>globals := globals t\<rparr>) \<in> {s. (expo \<or> fst rv \<longrightarrow> s \<in> {s. cleanupInfo_'_update (\<lambda>_. finaliseSlot_ret_C.cleanupInfo_C (ret__struct_finaliseSlot_ret_C_' t)) (slot_'_update (\<lambda>_. slota) s) \<in> UNIV \<inter> \<lbrace>\<acute>slot = slota\<rbrace> \<inter> \<lbrace>ccap_relation (snd rv) \<acute>cleanupInfo \<and> cleanup_info_wf' (snd rv)\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}) \<and> (\<not> (expo \<or> fst rv) \<longrightarrow> s \<in> UNIV)})) \<and> (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. cintr err (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t)) (errstate t) \<longrightarrow> fs_ret_'_update (\<lambda>_. ret__struct_finaliseSlot_ret_C_' t) (s\<lparr>globals := globals t\<rparr>) \<in> {s. id (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t)) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> cintr err (id (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t))) (errstate s)} \<inter> \<lbrace>True\<rbrace>))} proof (prove)
goal (2 subgoals):
 1. \<And>rv s. invs' s \<Longrightarrow> (expo \<or> fst rv \<longrightarrow> (valid_mdb' and valid_objs' and pspace_aligned' and untyped_ranges_zero' and (\<lambda>a. True)) s) \<and> (\<not> (expo \<or> fst rv) \<longrightarrow> True)
 2. \<And>exposed slota s s'. \<lbrakk>exposed = from_bool expo; slota = cte_Ptr slot; (s, s') \<in> rf_sr; invs' s \<and> sch_act_simple s \<and> (expo \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. invs' a \<and> sch_act_simple a \<and> (expo \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot a)) and (\<lambda>a. True \<and> True \<and> invs' a \<and> sch_act_simple a \<and> (\<not> expo \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot a))) s \<and> s' \<in> {s. immediate_'_update (\<lambda>_. exposed) (slot_'_update (\<lambda>_. slota) s) \<in> UNIV \<inter> \<lbrace>\<acute>slot = slota\<rbrace> \<inter> \<lbrace>\<acute>immediate = exposed\<rbrace>} \<inter> {s. \<forall>t. (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. (case rv of (success, cap) \<Rightarrow> \<lambda>a. case a of (success', cap') \<Rightarrow> success' = from_bool success \<and> ccap_relation cap cap' \<and> cleanup_info_wf' cap) (finaliseSlot_ret_C.success_C (ret__struct_finaliseSlot_ret_C_' t), finaliseSlot_ret_C.cleanupInfo_C (ret__struct_finaliseSlot_ret_C_' t)) \<longrightarrow> fs_ret_'_update (\<lambda>_. ret__struct_finaliseSlot_ret_C_' t) (s\<lparr>globals := globals t\<rparr>) \<in> {s. (expo \<or> fst rv \<longrightarrow> s \<in> {s. cleanupInfo_'_update (\<lambda>_. finaliseSlot_ret_C.cleanupInfo_C (ret__struct_finaliseSlot_ret_C_' t)) (slot_'_update (\<lambda>_. slota) s) \<in> UNIV \<inter> \<lbrace>\<acute>slot = slota\<rbrace> \<inter> \<lbrace>ccap_relation (snd rv) \<acute>cleanupInfo \<and> cleanup_info_wf' (snd rv)\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}) \<and> (\<not> (expo \<or> fst rv) \<longrightarrow> s \<in> UNIV)})) \<and> (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. cintr err (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t)) (errstate t) \<longrightarrow> fs_ret_'_update (\<lambda>_. ret__struct_finaliseSlot_ret_C_' t) (s\<lparr>globals := globals t\<rparr>) \<in> {s. id (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t)) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> cintr err (id (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t))) (errstate s)} \<inter> \<lbrace>True\<rbrace>))} proof (prove)
goal (1 subgoal):
 1. \<And>exposed slota s s'. \<lbrakk>exposed = from_bool expo; slota = cte_Ptr slot; (s, s') \<in> rf_sr; invs' s \<and> sch_act_simple s \<and> (expo \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s); s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. invs' a \<and> sch_act_simple a \<and> (expo \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot a)) and (\<lambda>a. True \<and> True \<and> invs' a \<and> sch_act_simple a \<and> (\<not> expo \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot a))) s \<and> s' \<in> {s. immediate_'_update (\<lambda>_. exposed) (slot_'_update (\<lambda>_. slota) s) \<in> UNIV \<inter> \<lbrace>\<acute>slot = slota\<rbrace> \<inter> \<lbrace>\<acute>immediate = exposed\<rbrace>} \<inter> {s. \<forall>t. (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. (case rv of (success, cap) \<Rightarrow> \<lambda>a. case a of (success', cap') \<Rightarrow> success' = from_bool success \<and> ccap_relation cap cap' \<and> cleanup_info_wf' cap) (finaliseSlot_ret_C.success_C (ret__struct_finaliseSlot_ret_C_' t), finaliseSlot_ret_C.cleanupInfo_C (ret__struct_finaliseSlot_ret_C_' t)) \<longrightarrow> fs_ret_'_update (\<lambda>_. ret__struct_finaliseSlot_ret_C_' t) (s\<lparr>globals := globals t\<rparr>) \<in> {s. (expo \<or> fst rv \<longrightarrow> s \<in> {s. cleanupInfo_'_update (\<lambda>_. finaliseSlot_ret_C.cleanupInfo_C (ret__struct_finaliseSlot_ret_C_' t)) (slot_'_update (\<lambda>_. slota) s) \<in> UNIV \<inter> \<lbrace>\<acute>slot = slota\<rbrace> \<inter> \<lbrace>ccap_relation (snd rv) \<acute>cleanupInfo \<and> cleanup_info_wf' (snd rv)\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}) \<and> (\<not> (expo \<or> fst rv) \<longrightarrow> s \<in> UNIV)})) \<and> (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. cintr err (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t)) (errstate t) \<longrightarrow> fs_ret_'_update (\<lambda>_. ret__struct_finaliseSlot_ret_C_' t) (s\<lparr>globals := globals t\<rparr>) \<in> {s. id (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t)) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> cintr err (id (finaliseSlot_ret_C.status_C (ret__struct_finaliseSlot_ret_C_' t))) (errstate s)} \<inter> \<lbrace>True\<rbrace>))} proof (prove)
goal:
No subgoals!