theory Ipc_AC

lemma do_normal_transfer_respects_in_ipc:
  notes lec_valid_cap[wp del]
  shows
  "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st and pas_refined aag and
    pspace_aligned and valid_vspace_objs and valid_arch_state and
valid_objs and valid_mdb and st_tcb_at can_receive_ipc receiver and
    (\<lambda>s. grant \<longrightarrow> is_subject aag sender \<and> is_subject aag receiver) and
    K ((\<not> is_subject aag receiver \<longrightarrow>
        (case recv_buf of None \<Rightarrow> True | Some buf' \<Rightarrow> auth_ipc_buffers st receiver =
                                                      ptr_range buf' msg_align_bits)) \<and>
       (case recv_buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits))\<rbrace>
   do_normal_transfer sender sbuf epopt badge grant receiver recv_buf
   \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace>" apply (simp add: do_normal_transfer_def) apply (wpsimp wp: as_user_respects_in_ipc set_message_info_respects_in_ipc copy_mrs_pas_refined
                    copy_mrs_respects_in_ipc transfer_caps_respects_in_ipc get_mi_length
                    lookup_extra_caps_authorised lookup_extra_caps_length hoare_vcg_const_Ball_lift
                    hoare_vcg_conj_lift_R hoare_vcg_const_imp_lift lec_valid_cap'
         | rule hoare_drop_imps)+ apply (auto simp: null_def intro: st_tcb_at_tcb_at) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st and pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and st_tcb_at can_receive_ipc receiver and (\<lambda>s. grant \<longrightarrow> is_subject aag sender \<and> is_subject aag receiver) and K ((pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> (case recv_buf of None \<Rightarrow> True | Some buf' \<Rightarrow> auth_ipc_buffers st receiver = ptr_range buf' msg_align_bits)) \<and> (case recv_buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits))\<rbrace> do_normal_transfer sender sbuf epopt badge grant receiver recv_buf \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st and pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and st_tcb_at can_receive_ipc receiver and (\<lambda>s. grant \<longrightarrow> is_subject aag sender \<and> is_subject aag receiver) and (\<lambda>y. (pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> (case recv_buf of None \<Rightarrow> True | Some buf' \<Rightarrow> auth_ipc_buffers st receiver = ptr_range buf' msg_align_bits)) \<and> (case recv_buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits))\<rbrace> do mi <- get_message_info sender;
caps <- if grant then lookup_extra_caps sender sbuf mi <catch> (\<lambda>y. return []) else return [];
mrs_transferred <- copy_mrs sender sbuf receiver recv_buf (mi_length mi);
mi' <- transfer_caps mi caps epopt receiver recv_buf;
y <- 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>_. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>integrity_tcb_in_ipc aag X receiver epptr TRContext st s; pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_objs s; valid_mdb s; st_tcb_at can_receive_ipc receiver s; grant \<longrightarrow> is_subject aag sender \<and> is_subject aag receiver; pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> (case recv_buf of None \<Rightarrow> True | Some buf' \<Rightarrow> auth_ipc_buffers st receiver = ptr_range buf' msg_align_bits); case recv_buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits\<rbrakk> \<Longrightarrow> (grant \<longrightarrow> tcb_at receiver s) \<and> (\<not> grant \<longrightarrow> tcb_at receiver s \<and> (\<not> null [] \<longrightarrow> is_subject aag receiver)) proof (prove)
goal:
No subgoals!