theory Ipc_IF

lemma handle_reply_globals_equiv:
  "\<lbrace>globals_equiv st and valid_objs and valid_arch_state and valid_global_refs
                     and pspace_distinct and pspace_aligned and valid_global_objs and valid_idle\<rbrace>
   handle_reply
   \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" unfolding handle_reply_def apply (wp do_reply_transfer_globals_equiv | wpc)+ apply (rule_tac Q="\<lambda>_. globals_equiv st and valid_objs and valid_arch_state and valid_global_refs
                                            and pspace_distinct and pspace_aligned
                                            and valid_global_objs and valid_idle"
                 in hoare_strengthen_post) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and valid_idle\<rbrace> handle_reply \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and valid_idle\<rbrace> do thread <- gets cur_thread;
caller_cap <- get_cap (thread, tcb_cnode_index 3);
case caller_cap of NullCap \<Rightarrow> return () | ReplyCap caller True R \<Rightarrow> fail | ReplyCap caller False R \<Rightarrow> do_reply_transfer thread caller (thread, tcb_cnode_index 3) (AllowGrant \<in> R) | _ \<Rightarrow> fail
od \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>thread. \<lbrace>?B1 thread\<rbrace> get_cap (thread, tcb_cnode_index 3) \<lbrace>\<lambda>caller_cap s. (caller_cap = NullCap \<longrightarrow> globals_equiv st s) \<and> (\<forall>x xa xb xc. caller_cap = UntypedCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x xa xb. caller_cap = EndpointCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. caller_cap = NotificationCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. caller_cap = ReplyCap x xa xb \<longrightarrow> (xa = True \<longrightarrow> True) \<and> (xa = False \<longrightarrow> (globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and valid_idle) s)) \<and> (\<forall>x xa xb. caller_cap = CNodeCap x xa xb \<longrightarrow> True) \<and> (\<forall>x. caller_cap = ThreadCap x \<longrightarrow> True) \<and> (caller_cap = DomainCap \<longrightarrow> True) \<and> (caller_cap = IRQControlCap \<longrightarrow> True) \<and> (\<forall>x. caller_cap = IRQHandlerCap x \<longrightarrow> True) \<and> (\<forall>x xa xb. caller_cap = Zombie x xa xb \<longrightarrow> True) \<and> (\<forall>x. caller_cap = ArchObjectCap x \<longrightarrow> True)\<rbrace>
 2. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>?B1\<rbrace>
 3. \<And>s. (globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and valid_idle) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>thread. \<lbrace>?B1 thread\<rbrace> get_cap (thread, tcb_cnode_index 3) \<lbrace>\<lambda>_. globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and valid_idle\<rbrace>
 2. \<And>thread rv s. (globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and valid_idle) s \<Longrightarrow> (rv = NullCap \<longrightarrow> globals_equiv st s) \<and> (\<forall>x xa xb xc. rv = UntypedCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x xa xb. rv = EndpointCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. rv = NotificationCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. rv = ReplyCap x xa xb \<longrightarrow> (xa = True \<longrightarrow> True) \<and> (xa = False \<longrightarrow> (globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and valid_idle) s)) \<and> (\<forall>x xa xb. rv = CNodeCap x xa xb \<longrightarrow> True) \<and> (\<forall>x. rv = ThreadCap x \<longrightarrow> True) \<and> (rv = DomainCap \<longrightarrow> True) \<and> (rv = IRQControlCap \<longrightarrow> True) \<and> (\<forall>x. rv = IRQHandlerCap x \<longrightarrow> True) \<and> (\<forall>x xa xb. rv = Zombie x xa xb \<longrightarrow> True) \<and> (\<forall>x. rv = ArchObjectCap x \<longrightarrow> True)
 3. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>?B1\<rbrace>
 4. \<And>s. (globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and valid_idle) s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!