theory Ipc_IF

lemma do_normal_transfer_globals_equiv:
  "\<lbrace>globals_equiv st and valid_arch_state and valid_global_objs and (\<lambda>sa. receiver \<noteq> idle_thread sa)\<rbrace>
   do_normal_transfer sender sbuf endpoint badge grant receiver rbuf
   \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" unfolding do_normal_transfer_def apply (wp as_user_globals_equiv set_message_info_globals_equiv transfer_caps_globals_equiv) apply (wp copy_mrs_globals_equiv) apply (subst K_def) apply (wp | rule impI)+ apply (clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_arch_state and valid_global_objs and (\<lambda>sa. receiver \<noteq> idle_thread sa)\<rbrace> do_normal_transfer sender sbuf endpoint badge grant receiver rbuf \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_arch_state and valid_global_objs and (\<lambda>sa. receiver \<noteq> idle_thread sa)\<rbrace> do mi <- get_message_info sender;
caps <- if grant then lookup_extra_caps sender sbuf mi <catch> K (return []) else return [];
mrs_transferred <- copy_mrs sender sbuf receiver rbuf (mi_length mi);
mi' <- transfer_caps mi caps endpoint receiver rbuf;
set_message_info receiver $ MI mrs_transferred (mi_extra_caps mi') (mi_caps_unwrapped mi') (mi_label mi);
as_user receiver $ setRegister badge_register badge
od \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>mi caps. \<lbrace>?B2 mi caps\<rbrace> copy_mrs sender sbuf receiver rbuf (mi_length mi) \<lbrace>\<lambda>mrs_transferred s. globals_equiv st s \<and> valid_arch_state s \<and> valid_global_objs s \<and> valid_arch_state s \<and> receiver \<noteq> idle_thread s \<and> valid_arch_state s \<and> receiver \<noteq> idle_thread s\<rbrace>
 2. \<And>mi. \<lbrace>?B1 mi\<rbrace> if grant then lookup_extra_caps sender sbuf mi <catch> K (return []) else return [] \<lbrace>?B2 mi\<rbrace>
 3. \<lbrace>?Q\<rbrace> get_message_info sender \<lbrace>?B1\<rbrace>
 4. \<And>s. (globals_equiv st and valid_arch_state and valid_global_objs and (\<lambda>sa. receiver \<noteq> idle_thread sa)) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>mi. \<lbrace>?B1 mi\<rbrace> if grant then lookup_extra_caps sender sbuf mi <catch> K (return []) else return [] \<lbrace>\<lambda>caps s. (globals_equiv st and valid_arch_state and (\<lambda>s. receiver \<noteq> idle_thread s)) s \<and> valid_arch_state s \<and> valid_global_objs s \<and> valid_arch_state s \<and> receiver \<noteq> idle_thread s \<and> valid_arch_state s \<and> receiver \<noteq> idle_thread s\<rbrace>
 2. \<lbrace>?Q\<rbrace> get_message_info sender \<lbrace>?B1\<rbrace>
 3. \<And>s. (globals_equiv st and valid_arch_state and valid_global_objs and (\<lambda>sa. receiver \<noteq> idle_thread sa)) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>mi. \<lbrace>?B46 mi mi\<rbrace> if grant then lookup_extra_caps sender sbuf mi <catch> (\<lambda>y. return []) else return [] \<lbrace>\<lambda>caps s. (globals_equiv st and valid_arch_state and (\<lambda>s. receiver \<noteq> idle_thread s)) s \<and> valid_arch_state s \<and> valid_global_objs s \<and> valid_arch_state s \<and> receiver \<noteq> idle_thread s \<and> valid_arch_state s \<and> receiver \<noteq> idle_thread s\<rbrace>
 2. \<lbrace>?Q\<rbrace> get_message_info sender \<lbrace>\<lambda>mi. ?B46 mi mi\<rbrace>
 3. \<And>s. (globals_equiv st and valid_arch_state and valid_global_objs and (\<lambda>sa. receiver \<noteq> idle_thread sa)) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (globals_equiv st and valid_arch_state and valid_global_objs and (\<lambda>sa. receiver \<noteq> idle_thread sa)) s \<Longrightarrow> (grant \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> receiver \<noteq> idle_thread s \<and> valid_arch_state s \<and> valid_global_objs s \<and> valid_arch_state s \<and> receiver \<noteq> idle_thread s \<and> valid_arch_state s \<and> receiver \<noteq> idle_thread s \<and> globals_equiv st s \<and> valid_arch_state s \<and> receiver \<noteq> idle_thread s \<and> valid_arch_state s \<and> valid_global_objs s \<and> valid_arch_state s \<and> receiver \<noteq> idle_thread s \<and> valid_arch_state s \<and> receiver \<noteq> idle_thread s) \<and> (\<not> grant \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> receiver \<noteq> idle_thread s \<and> valid_arch_state s \<and> valid_global_objs s \<and> valid_arch_state s \<and> receiver \<noteq> idle_thread s \<and> valid_arch_state s \<and> receiver \<noteq> idle_thread s) proof (prove)
goal:
No subgoals!