theory VSpace_C

lemma wordFromMessageInfo_ccorres [corres]:
  "\<And>mi. ccorres (=) ret__unsigned_long_' \<top> {s. mi = message_info_to_H (mi_' s)} []
           (return (wordFromMessageInfo mi)) (Call wordFromMessageInfo_'proc)" apply (rule ccorres_from_spec_modifies [where P = \<top>, simplified]) apply (rule wordFromMessageInfo_spec) apply (rule wordFromMessageInfo_modifies) apply simp apply simp apply (simp add: return_def wordFromMessageInfo_def Let_def message_info_to_H_def
    Types_H.msgLengthBits_def Types_H.msgExtraCapBits_def
    Types_H.msgMaxExtraCaps_def shiftL_nat word_bw_assocs word_bw_comms word_bw_lcs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>mi. ccorres (=) ret__unsigned_long_' (\<lambda>_. True) \<lbrace>mi = message_info_to_H \<acute>mi\<rbrace> [] (return (wordFromMessageInfo mi)) (Call wordFromMessageInfo_'proc) proof (prove)
goal (4 subgoals):
 1. \<And>mi. \<forall>s. \<Gamma>\<turnstile> {s} Call wordFromMessageInfo_'proc {t. ?Q mi s t}
 2. \<And>mi. \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Call wordFromMessageInfo_'proc {t. t may_not_modify_globals s}
 3. \<And>mi f s. ret__unsigned_long_' (globals_update f s) = ret__unsigned_long_' s
 4. \<And>mi s s' t'. \<lbrakk>True; s' \<in> \<lbrace>mi = message_info_to_H \<acute>mi\<rbrace>; (s, s') \<in> rf_sr; ?Q mi s' t'\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (return (wordFromMessageInfo mi) s). case x of (rv, t) \<Rightarrow> (t, s') \<in> rf_sr \<and> rv = ret__unsigned_long_' t' proof (prove)
goal (3 subgoals):
 1. \<And>mi. \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Call wordFromMessageInfo_'proc {t. t may_not_modify_globals s}
 2. \<And>mi f s. ret__unsigned_long_' (globals_update f s) = ret__unsigned_long_' s
 3. \<And>mi s s' t'. \<lbrakk>True; s' \<in> \<lbrace>mi = message_info_to_H \<acute>mi\<rbrace>; (s, s') \<in> rf_sr; ret__unsigned_long_' t' = (label_CL (seL4_MessageInfo_lift (mi_' s')) << 12) || (capsUnwrapped_CL (seL4_MessageInfo_lift (mi_' s')) << 9) || (extraCaps_CL (seL4_MessageInfo_lift (mi_' s')) << 7) || length_CL (seL4_MessageInfo_lift (mi_' s'))\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (return (wordFromMessageInfo mi) s). case x of (rv, t) \<Rightarrow> (t, s') \<in> rf_sr \<and> rv = ret__unsigned_long_' t' proof (prove)
goal (2 subgoals):
 1. \<And>mi f s. ret__unsigned_long_' (globals_update f s) = ret__unsigned_long_' s
 2. \<And>mi s s' t'. \<lbrakk>True; s' \<in> \<lbrace>mi = message_info_to_H \<acute>mi\<rbrace>; (s, s') \<in> rf_sr; ret__unsigned_long_' t' = (label_CL (seL4_MessageInfo_lift (mi_' s')) << 12) || (capsUnwrapped_CL (seL4_MessageInfo_lift (mi_' s')) << 9) || (extraCaps_CL (seL4_MessageInfo_lift (mi_' s')) << 7) || length_CL (seL4_MessageInfo_lift (mi_' s'))\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (return (wordFromMessageInfo mi) s). case x of (rv, t) \<Rightarrow> (t, s') \<in> rf_sr \<and> rv = ret__unsigned_long_' t' proof (prove)
goal (1 subgoal):
 1. \<And>mi s s' t'. \<lbrakk>True; s' \<in> \<lbrace>mi = message_info_to_H \<acute>mi\<rbrace>; (s, s') \<in> rf_sr; ret__unsigned_long_' t' = (label_CL (seL4_MessageInfo_lift (mi_' s')) << 12) || (capsUnwrapped_CL (seL4_MessageInfo_lift (mi_' s')) << 9) || (extraCaps_CL (seL4_MessageInfo_lift (mi_' s')) << 7) || length_CL (seL4_MessageInfo_lift (mi_' s'))\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (return (wordFromMessageInfo mi) s). case x of (rv, t) \<Rightarrow> (t, s') \<in> rf_sr \<and> rv = ret__unsigned_long_' t' proof (prove)
goal (1 subgoal):
 1. \<And>mi s s' t'. \<lbrakk>mi = message_info_to_H (mi_' s'); (s, s') \<in> rf_sr; ret__unsigned_long_' t' = (label_CL (seL4_MessageInfo_lift (mi_' s')) << 12) || (capsUnwrapped_CL (seL4_MessageInfo_lift (mi_' s')) << 9) || (extraCaps_CL (seL4_MessageInfo_lift (mi_' s')) << 7) || length_CL (seL4_MessageInfo_lift (mi_' s'))\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (return (wordFromMessageInfo (message_info_to_H (mi_' s'))) s). case x of (rv, t) \<Rightarrow> (t, s') \<in> rf_sr \<and> rv = (label_CL (seL4_MessageInfo_lift (mi_' s')) << 12) || (capsUnwrapped_CL (seL4_MessageInfo_lift (mi_' s')) << 9) || (extraCaps_CL (seL4_MessageInfo_lift (mi_' s')) << 7) || length_CL (seL4_MessageInfo_lift (mi_' s')) proof (prove)
goal:
No subgoals!