theory CSpace_RAB_C

lemma rab_failure_case_ccorres:
  assumes spec: "\<Gamma>\<turnstile> G' call_part {s. resolveAddressBits_ret_C.status_C v \<noteq> scast EXCEPTION_NONE
                                      \<and> lookup_failure_rel e (resolveAddressBits_ret_C.status_C v)
                                                           (errstate s)}"
  assumes mod:  "\<And>s. \<Gamma>\<turnstile> {s'. (s, s') \<in> rf_sr} call_part {s'. (s, s') \<in> rf_sr}"
  shows "ccorres (lookup_failure_rel \<currency> r) rab_xf \<top> G' (SKIP # hs)
   (throwError e)
   (call_part ;;
    \<acute>ret___struct_resolveAddressBits_ret_C :== v;;
    return_C ret__struct_resolveAddressBits_ret_C_'_update ret___struct_resolveAddressBits_ret_C_')" apply (rule ccorres_rhs_assoc)+ apply (rule ccorres_symb_exec_r [where R=\<top>, OF _ spec]) apply (rule ccorres_from_vcg_throws) apply (simp add: throwError_def return_def) apply (rule allI) apply (rule conseqPre) apply vcg apply (auto simp add: exception_defs errstate_def)[1] apply (rule conseqPre [OF mod]) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (lookup_failure_rel \<currency> r) (liftxf errstate resolveAddressBits_ret_C.status_C (\<lambda>v. (resolveAddressBits_ret_C.slot_C v, bitsRemaining_C v)) ret__struct_resolveAddressBits_ret_C_') (\<lambda>_. True) G' (SKIP # hs) (throwError e) (call_part;;
\<acute>ret___struct_resolveAddressBits_ret_C :== v;;
return_C ret__struct_resolveAddressBits_ret_C_'_update ret___struct_resolveAddressBits_ret_C_') proof (prove)
goal (1 subgoal):
 1. ccorres (lookup_failure_rel \<currency> r) (liftxf errstate resolveAddressBits_ret_C.status_C (\<lambda>v. (resolveAddressBits_ret_C.slot_C v, bitsRemaining_C v)) ret__struct_resolveAddressBits_ret_C_') (\<lambda>_. True) G' (SKIP # hs) (throwError e) (call_part;;
(\<acute>ret___struct_resolveAddressBits_ret_C :== v;;
return_C ret__struct_resolveAddressBits_ret_C_'_update ret___struct_resolveAddressBits_ret_C_')) proof (prove)
goal (2 subgoals):
 1. ccorres (lookup_failure_rel \<currency> r) (liftxf errstate resolveAddressBits_ret_C.status_C (\<lambda>v. (resolveAddressBits_ret_C.slot_C v, bitsRemaining_C v)) ret__struct_resolveAddressBits_ret_C_') (\<lambda>_. True) {s. resolveAddressBits_ret_C.status_C v \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> lookup_failure_rel e (resolveAddressBits_ret_C.status_C v) (errstate s)} (SKIP # hs) (throwError e) (\<acute>ret___struct_resolveAddressBits_ret_C :== v;;
return_C ret__struct_resolveAddressBits_ret_C_'_update ret___struct_resolveAddressBits_ret_C_')
 2. \<And>s. True \<Longrightarrow> \<Gamma>\<turnstile> (G' \<inter> {s'. (s, s') \<in> rf_sr}) call_part {s'. (s, s') \<in> rf_sr} proof (prove)
goal (2 subgoals):
 1. \<forall>\<sigma>. \<Gamma>\<turnstile> {s. True \<and> s \<in> {s. resolveAddressBits_ret_C.status_C v \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> lookup_failure_rel e (resolveAddressBits_ret_C.status_C v) (errstate s)} \<and> (\<sigma>, s) \<in> rf_sr} \<acute>ret___struct_resolveAddressBits_ret_C :== v;;
return_C ret__struct_resolveAddressBits_ret_C_'_update ret___struct_resolveAddressBits_ret_C_' {},{s. \<exists>(rv, \<sigma>')\<in>fst (throwError e \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> (lookup_failure_rel \<currency> r) rv (liftxf errstate resolveAddressBits_ret_C.status_C (\<lambda>v. (resolveAddressBits_ret_C.slot_C v, bitsRemaining_C v)) ret__struct_resolveAddressBits_ret_C_' s)}
 2. \<And>s. True \<Longrightarrow> \<Gamma>\<turnstile> (G' \<inter> {s'. (s, s') \<in> rf_sr}) call_part {s'. (s, s') \<in> rf_sr} proof (prove)
goal (2 subgoals):
 1. \<forall>\<sigma>. \<Gamma>\<turnstile> {s. resolveAddressBits_ret_C.status_C v \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> lookup_failure_rel e (resolveAddressBits_ret_C.status_C v) (errstate s) \<and> (\<sigma>, s) \<in> rf_sr} \<acute>ret___struct_resolveAddressBits_ret_C :== v;;
return_C ret__struct_resolveAddressBits_ret_C_'_update ret___struct_resolveAddressBits_ret_C_' {},{s. (\<sigma>, s) \<in> rf_sr \<and> resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> lookup_failure_rel e (resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' s)) (errstate s)}
 2. \<And>s. True \<Longrightarrow> \<Gamma>\<turnstile> (G' \<inter> {s'. (s, s') \<in> rf_sr}) call_part {s'. (s, s') \<in> rf_sr} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma>. \<Gamma>\<turnstile> {s. resolveAddressBits_ret_C.status_C v \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> lookup_failure_rel e (resolveAddressBits_ret_C.status_C v) (errstate s) \<and> (\<sigma>, s) \<in> rf_sr} \<acute>ret___struct_resolveAddressBits_ret_C :== v;;
return_C ret__struct_resolveAddressBits_ret_C_'_update ret___struct_resolveAddressBits_ret_C_' {},{s. (\<sigma>, s) \<in> rf_sr \<and> resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> lookup_failure_rel e (resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' s)) (errstate s)}
 2. \<And>s. True \<Longrightarrow> \<Gamma>\<turnstile> (G' \<inter> {s'. (s, s') \<in> rf_sr}) call_part {s'. (s, s') \<in> rf_sr} proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma>. \<Gamma>\<turnstile> (?P'10 \<sigma>) \<acute>ret___struct_resolveAddressBits_ret_C :== v;;
return_C ret__struct_resolveAddressBits_ret_C_'_update ret___struct_resolveAddressBits_ret_C_' {},{s. (\<sigma>, s) \<in> rf_sr \<and> resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> lookup_failure_rel e (resolveAddressBits_ret_C.status_C (ret__struct_resolveAddressBits_ret_C_' s)) (errstate s)}
 2. \<And>\<sigma>. {s. resolveAddressBits_ret_C.status_C v \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> lookup_failure_rel e (resolveAddressBits_ret_C.status_C v) (errstate s) \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> ?P'10 \<sigma>
 3. \<And>s. True \<Longrightarrow> \<Gamma>\<turnstile> (G' \<inter> {s'. (s, s') \<in> rf_sr}) call_part {s'. (s, s') \<in> rf_sr} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma>. {s. resolveAddressBits_ret_C.status_C v \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> lookup_failure_rel e (resolveAddressBits_ret_C.status_C v) (errstate s) \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. (\<sigma>, s\<lparr>ret___struct_resolveAddressBits_ret_C_' := v, ret__struct_resolveAddressBits_ret_C_' := v, global_exn_var_' := Return\<rparr>) \<in> rf_sr \<and> resolveAddressBits_ret_C.status_C v \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> lookup_failure_rel e (resolveAddressBits_ret_C.status_C v) (errstate (s\<lparr>ret___struct_resolveAddressBits_ret_C_' := v, ret__struct_resolveAddressBits_ret_C_' := v, global_exn_var_' := Return\<rparr>))}
 2. \<And>s. True \<Longrightarrow> \<Gamma>\<turnstile> (G' \<inter> {s'. (s, s') \<in> rf_sr}) call_part {s'. (s, s') \<in> rf_sr} proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> \<Gamma>\<turnstile> (G' \<inter> {s'. (s, s') \<in> rf_sr}) call_part {s'. (s, s') \<in> rf_sr} proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> G' \<inter> {s'. (s, s') \<in> rf_sr} \<subseteq> {s'. (s, s') \<in> rf_sr} proof (prove)
goal:
No subgoals!