theory ArchIpc_IF

lemma do_normal_transfer_reads_respects[Ipc_IF_assms]:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows
  "reads_respects aag (l :: 'a subject_label)
     (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state
                      and valid_mdb and valid_objs
                      and K (aag_can_read_or_affect aag l sender \<and>
                             ipc_buffer_has_read_auth aag (pasObjectAbs aag sender) sbuf \<and>
                             ipc_buffer_has_read_auth aag (pasObjectAbs aag receiver) rbuf \<and>
                             (grant \<longrightarrow> (is_subject aag sender \<and> is_subject aag receiver))))
     (do_normal_transfer sender sbuf endpoint badge grant receiver rbuf)" apply (cases grant) apply (rule gen_asm_ev) apply (simp add: do_normal_transfer_def) apply (wp copy_mrs_pas_refined get_message_info_rev lookup_extra_caps_rev
             as_user_set_register_reads_respects' set_message_info_reads_respects
             transfer_caps_reads_respects copy_mrs_reads_respects lookup_extra_caps_rev
             lookup_extra_caps_authorised lookup_extra_caps_auth get_message_info_rev
             get_mi_length' get_mi_length validE_E_wp_post_taut
             copy_mrs_cte_wp_at hoare_vcg_ball_lift lec_valid_cap'
             lookup_extra_caps_srcs[simplified ball_conj_distrib,THEN hoare_conjDR1]
             lookup_extra_caps_srcs[simplified ball_conj_distrib,THEN hoare_conjDR2]
          | wpc
          | simp add: det_setRegister ball_conj_distrib)+ apply (fastforce intro: aag_has_read_auth_can_read_or_affect_ipc_buffer) apply (rule gen_asm_ev) apply (simp add: do_normal_transfer_def transfer_caps_def) apply (wp ev_irrelevant_bind[where f="get_receive_slots receiver rbuf"]
            as_user_set_register_reads_respects'
            set_message_info_reads_respects copy_mrs_reads_respects
            get_message_info_reads_respects get_mi_length
         | wpc
         | simp)+ apply (auto simp: ipc_buffer_has_read_auth_def aag_can_read_or_affect_ipc_buffer_def
               dest: reads_read_thread_read_pages split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and K (aag_can_read_or_affect aag l sender \<and> ipc_buffer_has_read_auth aag (pasObjectAbs aag sender) sbuf \<and> ipc_buffer_has_read_auth aag (pasObjectAbs aag receiver) rbuf \<and> (grant \<longrightarrow> is_subject aag sender \<and> is_subject aag receiver))) (do_normal_transfer sender sbuf endpoint badge grant receiver rbuf) proof (prove)
goal (2 subgoals):
 1. grant \<Longrightarrow> reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and K (aag_can_read_or_affect aag l sender \<and> ipc_buffer_has_read_auth aag (pasObjectAbs aag sender) sbuf \<and> ipc_buffer_has_read_auth aag (pasObjectAbs aag receiver) rbuf \<and> (grant \<longrightarrow> is_subject aag sender \<and> is_subject aag receiver))) (do_normal_transfer sender sbuf endpoint badge grant receiver rbuf)
 2. \<not> grant \<Longrightarrow> reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and K (aag_can_read_or_affect aag l sender \<and> ipc_buffer_has_read_auth aag (pasObjectAbs aag sender) sbuf \<and> ipc_buffer_has_read_auth aag (pasObjectAbs aag receiver) rbuf \<and> (grant \<longrightarrow> is_subject aag sender \<and> is_subject aag receiver))) (do_normal_transfer sender sbuf endpoint badge grant receiver rbuf) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>grant; aag_can_read_or_affect aag l sender \<and> ipc_buffer_has_read_auth aag (pasObjectAbs aag sender) sbuf \<and> ipc_buffer_has_read_auth aag (pasObjectAbs aag receiver) rbuf \<and> (grant \<longrightarrow> is_subject aag sender \<and> is_subject aag receiver)\<rbrakk> \<Longrightarrow> reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs) (do_normal_transfer sender sbuf endpoint badge grant receiver rbuf)
 2. \<not> grant \<Longrightarrow> reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and K (aag_can_read_or_affect aag l sender \<and> ipc_buffer_has_read_auth aag (pasObjectAbs aag sender) sbuf \<and> ipc_buffer_has_read_auth aag (pasObjectAbs aag receiver) rbuf \<and> (grant \<longrightarrow> is_subject aag sender \<and> is_subject aag receiver))) (do_normal_transfer sender sbuf endpoint badge grant receiver rbuf) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>grant; aag_can_read_or_affect aag l sender \<and> ipc_buffer_has_read_auth aag (pasObjectAbs aag sender) sbuf \<and> ipc_buffer_has_read_auth aag (pasObjectAbs aag receiver) rbuf \<and> is_subject aag sender \<and> is_subject aag receiver\<rbrakk> \<Longrightarrow> reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs) (do mi <- get_message_info sender;
caps <- lookup_extra_caps sender sbuf mi <catch> (\<lambda>y. return []);
mrs_transferred <- copy_mrs sender sbuf receiver rbuf (mi_length mi);
mi' <- transfer_caps mi caps endpoint receiver rbuf;
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)
 2. \<not> grant \<Longrightarrow> reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and K (aag_can_read_or_affect aag l sender \<and> ipc_buffer_has_read_auth aag (pasObjectAbs aag sender) sbuf \<and> ipc_buffer_has_read_auth aag (pasObjectAbs aag receiver) rbuf \<and> (grant \<longrightarrow> is_subject aag sender \<and> is_subject aag receiver))) (do_normal_transfer sender sbuf endpoint badge grant receiver rbuf) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>grant; aag_can_read_or_affect aag l sender \<and> ipc_buffer_has_read_auth aag (pasObjectAbs aag sender) sbuf \<and> ipc_buffer_has_read_auth aag (pasObjectAbs aag receiver) rbuf \<and> is_subject aag sender \<and> is_subject aag receiver; pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> valid_objs s\<rbrakk> \<Longrightarrow> ipc_buffer_has_read_auth aag (pasSubject aag) sbuf \<and> aag_can_read_or_affect_ipc_buffer aag l sbuf \<and> ipc_buffer_has_read_auth aag (pasSubject aag) rbuf
 2. \<not> grant \<Longrightarrow> reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and K (aag_can_read_or_affect aag l sender \<and> ipc_buffer_has_read_auth aag (pasObjectAbs aag sender) sbuf \<and> ipc_buffer_has_read_auth aag (pasObjectAbs aag receiver) rbuf \<and> (grant \<longrightarrow> is_subject aag sender \<and> is_subject aag receiver))) (do_normal_transfer sender sbuf endpoint badge grant receiver rbuf) proof (prove)
goal (1 subgoal):
 1. \<not> grant \<Longrightarrow> reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and K (aag_can_read_or_affect aag l sender \<and> ipc_buffer_has_read_auth aag (pasObjectAbs aag sender) sbuf \<and> ipc_buffer_has_read_auth aag (pasObjectAbs aag receiver) rbuf \<and> (grant \<longrightarrow> is_subject aag sender \<and> is_subject aag receiver))) (do_normal_transfer sender sbuf endpoint badge grant receiver rbuf) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> grant; aag_can_read_or_affect aag l sender \<and> ipc_buffer_has_read_auth aag (pasObjectAbs aag sender) sbuf \<and> ipc_buffer_has_read_auth aag (pasObjectAbs aag receiver) rbuf \<and> (grant \<longrightarrow> is_subject aag sender \<and> is_subject aag receiver)\<rbrakk> \<Longrightarrow> reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs) (do_normal_transfer sender sbuf endpoint badge grant receiver rbuf) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> grant; aag_can_read_or_affect aag l sender \<and> ipc_buffer_has_read_auth aag (pasObjectAbs aag sender) sbuf \<and> ipc_buffer_has_read_auth aag (pasObjectAbs aag receiver) rbuf\<rbrakk> \<Longrightarrow> reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs) (do mi <- get_message_info sender;
mrs_transferred <- copy_mrs sender sbuf receiver rbuf (mi_length mi);
mi' <- do dest_slots <- get_receive_slots receiver rbuf;
case rbuf of None \<Rightarrow> return (MI (mi_length mi) 0 0 (mi_label mi)) | _ \<Rightarrow> return (MI (mi_length mi) 0 0 (mi_label mi))
od;
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) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<not> grant; aag_can_read_or_affect aag l sender \<and> ipc_buffer_has_read_auth aag (pasObjectAbs aag sender) sbuf \<and> ipc_buffer_has_read_auth aag (pasObjectAbs aag receiver) rbuf; pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> valid_objs s\<rbrakk> \<Longrightarrow> aag_can_read_or_affect_ipc_buffer aag l sbuf proof (prove)
goal:
No subgoals!