theory Ipc_IF

lemma do_ipc_transfer_globals_equiv:
  "\<lbrace>globals_equiv st and valid_arch_state and valid_objs and valid_arch_state and valid_global_refs
                     and pspace_distinct and pspace_aligned
                     and valid_global_objs and (\<lambda>s. receiver \<noteq> idle_thread s)\<rbrace>
   do_ipc_transfer sender ep badge grant receiver
   \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" unfolding do_ipc_transfer_def apply (wp do_normal_transfer_globals_equiv do_fault_transfer_globals_equiv | wpc)+ apply (rule_tac Q="\<lambda>_. globals_equiv st and valid_arch_state and valid_global_objs and
                           (\<lambda>sa. receiver \<noteq> idle_thread sa) and
                           (\<lambda>sa. (\<forall>rb. recv_buffer = Some rb
                                 \<longrightarrow> auth_ipc_buffers sa receiver = ptr_range rb msg_align_bits) \<and>
                                 (\<forall>rb. recv_buffer = Some rb \<longrightarrow> is_aligned rb msg_align_bits))"
                 in hoare_strengthen_post) apply (wp) apply (clarsimp | rule conjI)+ apply (wp hoare_vcg_all_lift lookup_ipc_buffer_ptr_range' lookup_ipc_buffer_aligned' | fastforce)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_arch_state and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and (\<lambda>s. receiver \<noteq> idle_thread s)\<rbrace> do_ipc_transfer sender ep badge grant receiver \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_arch_state and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and (\<lambda>s. receiver \<noteq> idle_thread s)\<rbrace> do recv_buffer <- lookup_ipc_buffer True receiver;
fault <- thread_get tcb_fault sender;
case fault of None \<Rightarrow> do send_buffer <- lookup_ipc_buffer False sender;
do_normal_transfer sender send_buffer ep badge grant receiver recv_buffer
od | Some f \<Rightarrow> do_fault_transfer badge sender receiver recv_buffer
od \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>recv_buffer. \<lbrace>?B1 recv_buffer\<rbrace> thread_get tcb_fault sender \<lbrace>\<lambda>fault s. (fault = None \<longrightarrow> (globals_equiv st and valid_arch_state and valid_global_objs and (\<lambda>sa. receiver \<noteq> idle_thread sa)) s) \<and> (\<forall>x. fault = Some x \<longrightarrow> (globals_equiv st and valid_arch_state and (\<lambda>sa. receiver \<noteq> idle_thread sa)) s)\<rbrace>
 2. \<lbrace>?Q\<rbrace> lookup_ipc_buffer True receiver \<lbrace>?B1\<rbrace>
 3. \<And>s. (globals_equiv st and valid_arch_state and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and (\<lambda>s. receiver \<noteq> idle_thread s)) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>recv_buffer. \<lbrace>?B1 recv_buffer\<rbrace> thread_get tcb_fault sender \<lbrace>\<lambda>_. globals_equiv st and valid_arch_state and valid_global_objs and (\<lambda>sa. receiver \<noteq> idle_thread sa) and (\<lambda>sa. (\<forall>rb. recv_buffer = Some rb \<longrightarrow> auth_ipc_buffers sa receiver = ptr_range rb msg_align_bits) \<and> (\<forall>rb. recv_buffer = Some rb \<longrightarrow> is_aligned rb msg_align_bits))\<rbrace>
 2. \<And>recv_buffer rv s. (globals_equiv st and valid_arch_state and valid_global_objs and (\<lambda>sa. receiver \<noteq> idle_thread sa) and (\<lambda>sa. (\<forall>rb. recv_buffer = Some rb \<longrightarrow> auth_ipc_buffers sa receiver = ptr_range rb msg_align_bits) \<and> (\<forall>rb. recv_buffer = Some rb \<longrightarrow> is_aligned rb msg_align_bits))) s \<Longrightarrow> (rv = None \<longrightarrow> (globals_equiv st and valid_arch_state and valid_global_objs and (\<lambda>sa. receiver \<noteq> idle_thread sa)) s) \<and> (\<forall>x. rv = Some x \<longrightarrow> (globals_equiv st and valid_arch_state and (\<lambda>sa. receiver \<noteq> idle_thread sa)) s)
 3. \<lbrace>?Q\<rbrace> lookup_ipc_buffer True receiver \<lbrace>?B1\<rbrace>
 4. \<And>s. (globals_equiv st and valid_arch_state and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and (\<lambda>s. receiver \<noteq> idle_thread s)) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>recv_buffer rv s. (globals_equiv st and valid_arch_state and valid_global_objs and (\<lambda>sa. receiver \<noteq> idle_thread sa) and (\<lambda>sa. (\<forall>rb. recv_buffer = Some rb \<longrightarrow> auth_ipc_buffers sa receiver = ptr_range rb msg_align_bits) \<and> (\<forall>rb. recv_buffer = Some rb \<longrightarrow> is_aligned rb msg_align_bits))) s \<Longrightarrow> (rv = None \<longrightarrow> (globals_equiv st and valid_arch_state and valid_global_objs and (\<lambda>sa. receiver \<noteq> idle_thread sa)) s) \<and> (\<forall>x. rv = Some x \<longrightarrow> (globals_equiv st and valid_arch_state and (\<lambda>sa. receiver \<noteq> idle_thread sa)) s)
 2. \<lbrace>?Q\<rbrace> lookup_ipc_buffer True receiver \<lbrace>\<lambda>recv_buffer. globals_equiv st and valid_arch_state and valid_global_objs and (\<lambda>sa. receiver \<noteq> idle_thread sa) and (\<lambda>sa. (\<forall>rb. recv_buffer = Some rb \<longrightarrow> auth_ipc_buffers sa receiver = ptr_range rb msg_align_bits) \<and> (\<forall>rb. recv_buffer = Some rb \<longrightarrow> is_aligned rb msg_align_bits))\<rbrace>
 3. \<And>s. (globals_equiv st and valid_arch_state and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and (\<lambda>s. receiver \<noteq> idle_thread s)) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> lookup_ipc_buffer True receiver \<lbrace>\<lambda>recv_buffer. globals_equiv st and valid_arch_state and valid_global_objs and (\<lambda>sa. receiver \<noteq> idle_thread sa) and (\<lambda>sa. (\<forall>rb. recv_buffer = Some rb \<longrightarrow> auth_ipc_buffers sa receiver = ptr_range rb msg_align_bits) \<and> (\<forall>rb. recv_buffer = Some rb \<longrightarrow> is_aligned rb msg_align_bits))\<rbrace>
 2. \<And>s. (globals_equiv st and valid_arch_state and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and (\<lambda>s. receiver \<noteq> idle_thread s)) s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!