theory Ipc_C

lemma messageInfoFromWord_ccorres [corres]:
  "ccorres (\<lambda>r r'. r = message_info_to_H r') ret__struct_seL4_MessageInfo_C_' \<top> {s. w_' s = w} []
           (return (messageInfoFromWord w)) (Call messageInfoFromWord_'proc)" apply (rule ccorres_from_spec_modifies [where P = \<top>, simplified]) apply (rule messageInfoFromWord_spec) apply (rule messageInfoFromWord_modifies) apply simp apply simp apply (simp add: return_def messageInfoFromWord_def Let_def message_info_to_H_def
    Types_H.msgLengthBits_def Types_H.msgExtraCapBits_def msgMaxExtraCaps_def
    shiftL_nat msgMaxLength_def msgLabelBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (\<lambda>r r'. r = message_info_to_H r') ret__struct_seL4_MessageInfo_C_' (\<lambda>_. True) \<lbrace>\<acute>w = w\<rbrace> [] (return (messageInfoFromWord w)) (Call messageInfoFromWord_'proc) proof (prove)
goal (4 subgoals):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Call messageInfoFromWord_'proc {t. ?Q s t}
 2. \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Call messageInfoFromWord_'proc {t. t may_not_modify_globals s}
 3. \<And>f s. ret__struct_seL4_MessageInfo_C_' (globals_update f s) = ret__struct_seL4_MessageInfo_C_' s
 4. \<And>s s' t'. \<lbrakk>True; s' \<in> \<lbrace>\<acute>w = w\<rbrace>; (s, s') \<in> rf_sr; ?Q s' t'\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (return (messageInfoFromWord w) s). case x of (rv, t) \<Rightarrow> (t, s') \<in> rf_sr \<and> rv = message_info_to_H (ret__struct_seL4_MessageInfo_C_' t') proof (prove)
goal (3 subgoals):
 1. \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Call messageInfoFromWord_'proc {t. t may_not_modify_globals s}
 2. \<And>f s. ret__struct_seL4_MessageInfo_C_' (globals_update f s) = ret__struct_seL4_MessageInfo_C_' s
 3. \<And>s s' t'. \<lbrakk>True; s' \<in> \<lbrace>\<acute>w = w\<rbrace>; (s, s') \<in> rf_sr; seL4_MessageInfo_lift (ret__struct_seL4_MessageInfo_C_' t') = \<lparr>label_CL = (w_' s' >> 12) && 0xFFFFF, capsUnwrapped_CL = (w_' s' >> 9) && 7, extraCaps_CL = (w_' s' >> 7) && 3, length_CL = let v = w_' s' && 0x7F in if msgMaxLength < v then msgMaxLength else v\<rparr>\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (return (messageInfoFromWord w) s). case x of (rv, t) \<Rightarrow> (t, s') \<in> rf_sr \<and> rv = message_info_to_H (ret__struct_seL4_MessageInfo_C_' t') proof (prove)
goal (2 subgoals):
 1. \<And>f s. ret__struct_seL4_MessageInfo_C_' (globals_update f s) = ret__struct_seL4_MessageInfo_C_' s
 2. \<And>s s' t'. \<lbrakk>True; s' \<in> \<lbrace>\<acute>w = w\<rbrace>; (s, s') \<in> rf_sr; seL4_MessageInfo_lift (ret__struct_seL4_MessageInfo_C_' t') = \<lparr>label_CL = (w_' s' >> 12) && 0xFFFFF, capsUnwrapped_CL = (w_' s' >> 9) && 7, extraCaps_CL = (w_' s' >> 7) && 3, length_CL = let v = w_' s' && 0x7F in if msgMaxLength < v then msgMaxLength else v\<rparr>\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (return (messageInfoFromWord w) s). case x of (rv, t) \<Rightarrow> (t, s') \<in> rf_sr \<and> rv = message_info_to_H (ret__struct_seL4_MessageInfo_C_' t') proof (prove)
goal (1 subgoal):
 1. \<And>s s' t'. \<lbrakk>True; s' \<in> \<lbrace>\<acute>w = w\<rbrace>; (s, s') \<in> rf_sr; seL4_MessageInfo_lift (ret__struct_seL4_MessageInfo_C_' t') = \<lparr>label_CL = (w_' s' >> 12) && 0xFFFFF, capsUnwrapped_CL = (w_' s' >> 9) && 7, extraCaps_CL = (w_' s' >> 7) && 3, length_CL = let v = w_' s' && 0x7F in if msgMaxLength < v then msgMaxLength else v\<rparr>\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (return (messageInfoFromWord w) s). case x of (rv, t) \<Rightarrow> (t, s') \<in> rf_sr \<and> rv = message_info_to_H (ret__struct_seL4_MessageInfo_C_' t') proof (prove)
goal (1 subgoal):
 1. \<And>s s' t'. \<lbrakk>w_' s' = w; (s, s') \<in> rf_sr; seL4_MessageInfo_lift (ret__struct_seL4_MessageInfo_C_' t') = \<lparr>label_CL = (w >> 12) && 0xFFFFF, capsUnwrapped_CL = (w >> 9) && 7, extraCaps_CL = (w >> 7) && 3, length_CL = let v = w && 0x7F in if msgMaxLength < v then msgMaxLength else v\<rparr>\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (return (messageInfoFromWord w) s). case x of (rv, t) \<Rightarrow> (t, s') \<in> rf_sr \<and> rv = message_info_to_H (ret__struct_seL4_MessageInfo_C_' t') proof (prove)
goal:
No subgoals!