theory ArchIpc_IF

lemma set_mrs_reads_respects'[Ipc_IF_assms]:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows
    "reads_respects aag (l :: 'a subject_label)
       (K (ipc_buffer_has_auth aag thread buf \<and>
           (case buf of (Some buf') \<Rightarrow> is_aligned buf' msg_align_bits | _ \<Rightarrow> True)))
       (set_mrs thread buf msgs)" apply (case_tac "aag_can_read_or_affect aag l thread") apply ((wp equiv_valid_guard_imp[OF set_mrs_reads_respects] | simp)+)[1] apply (rule gen_asm_ev) apply (simp add: equiv_valid_def2) apply (rule equiv_valid_rv_guard_imp) apply (case_tac buf) apply (rule_tac Q="\<top>" and P="\<top>" and L="{pasObjectAbs aag thread}" in ev_invisible[OF domains_distinct]) apply (clarsimp simp: labels_are_invisible_def) apply (rule modifies_at_mostI) apply (simp add: set_mrs_def) apply ((wp set_object_equiv_but_for_labels | simp | auto dest: get_tcb_not_asid_pool_at)+)[1] apply (simp) apply (rule set_mrs_ret_eq) apply (rename_tac buf') apply (rule_tac Q="\<top>" and L="{pasObjectAbs aag thread} \<union> (pasObjectAbs aag)
                                 ` (ptr_range buf' msg_align_bits)"
                in ev_invisible[OF domains_distinct]) apply (auto simp: labels_are_invisible_def ipc_buffer_has_auth_def
                 dest: reads_read_page_read_thread simp: aag_can_affect_label_def)[1] apply (rule modifies_at_mostI) apply (wp set_mrs_equiv_but_for_labels | simp)+ apply (rule set_mrs_ret_eq) by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (ipc_buffer_has_auth aag thread buf \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits))) (set_mrs thread buf msgs) proof (prove)
goal (2 subgoals):
 1. aag_can_read_or_affect aag l thread \<Longrightarrow> reads_respects aag l (K (ipc_buffer_has_auth aag thread buf \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits))) (set_mrs thread buf msgs)
 2. \<not> aag_can_read_or_affect aag l thread \<Longrightarrow> reads_respects aag l (K (ipc_buffer_has_auth aag thread buf \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits))) (set_mrs thread buf msgs) proof (prove)
goal (1 subgoal):
 1. \<not> aag_can_read_or_affect aag l thread \<Longrightarrow> reads_respects aag l (K (ipc_buffer_has_auth aag thread buf \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits))) (set_mrs thread buf msgs) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> aag_can_read_or_affect aag l thread; ipc_buffer_has_auth aag thread buf \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits)\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (set_mrs thread buf msgs) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); ipc_buffer_has_auth aag thread buf \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits)\<rbrakk> \<Longrightarrow> reads_equiv_valid_rv_inv (affects_equiv aag l) aag (=) (\<lambda>_. True) (set_mrs thread buf msgs) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); ipc_buffer_has_auth aag thread buf \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits)\<rbrakk> \<Longrightarrow> reads_equiv_valid_rv_inv (affects_equiv aag l) aag (=) ?P7 (set_mrs thread buf msgs)
 2. \<And>s. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); ipc_buffer_has_auth aag thread buf \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits); True\<rbrakk> \<Longrightarrow> ?P7 s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); ipc_buffer_has_auth aag thread buf \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits); buf = None\<rbrakk> \<Longrightarrow> reads_equiv_valid_rv_inv (affects_equiv aag l) aag (=) ?P7 (set_mrs thread buf msgs)
 2. \<And>a. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); ipc_buffer_has_auth aag thread buf \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits); buf = Some a\<rbrakk> \<Longrightarrow> reads_equiv_valid_rv_inv (affects_equiv aag l) aag (=) ?P7 (set_mrs thread buf msgs)
 3. \<And>s. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); ipc_buffer_has_auth aag thread buf \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits); True\<rbrakk> \<Longrightarrow> ?P7 s proof (prove)
goal (5 subgoals):
 1. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); ipc_buffer_has_auth aag thread buf \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits); buf = None\<rbrakk> \<Longrightarrow> labels_are_invisible aag l {pasObjectAbs aag thread}
 2. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); ipc_buffer_has_auth aag thread buf \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits); buf = None\<rbrakk> \<Longrightarrow> modifies_at_most aag {pasObjectAbs aag thread} (\<lambda>_. True) (set_mrs thread buf msgs)
 3. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); ipc_buffer_has_auth aag thread buf \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits); buf = None\<rbrakk> \<Longrightarrow> \<forall>s t. True \<and> True \<longrightarrow> (\<forall>(rva, s')\<in>fst (set_mrs thread buf msgs s). \<forall>(rvb, t')\<in>fst (set_mrs thread buf msgs t). rva = rvb)
 4. \<And>a. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); ipc_buffer_has_auth aag thread buf \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits); buf = Some a\<rbrakk> \<Longrightarrow> reads_equiv_valid_rv_inv (affects_equiv aag l) aag (=) ((\<lambda>_. True) and (\<lambda>_. True)) (set_mrs thread buf msgs)
 5. \<And>s. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); ipc_buffer_has_auth aag thread buf \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits); True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True)) s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); ipc_buffer_has_auth aag thread buf \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits); buf = None\<rbrakk> \<Longrightarrow> modifies_at_most aag {pasObjectAbs aag thread} (\<lambda>_. True) (set_mrs thread buf msgs)
 2. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); ipc_buffer_has_auth aag thread buf \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits); buf = None\<rbrakk> \<Longrightarrow> \<forall>s t. True \<and> True \<longrightarrow> (\<forall>(rva, s')\<in>fst (set_mrs thread buf msgs s). \<forall>(rvb, t')\<in>fst (set_mrs thread buf msgs t). rva = rvb)
 3. \<And>a. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); ipc_buffer_has_auth aag thread buf \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits); buf = Some a\<rbrakk> \<Longrightarrow> reads_equiv_valid_rv_inv (affects_equiv aag l) aag (=) ((\<lambda>_. True) and (\<lambda>_. True)) (set_mrs thread buf msgs)
 4. \<And>s. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); ipc_buffer_has_auth aag thread buf \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits); True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True)) s proof (prove)
goal (4 subgoals):
 1. \<And>st. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); ipc_buffer_has_auth aag thread buf \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits); buf = None\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>_. True) and equiv_but_for_labels aag {pasObjectAbs aag thread} st\<rbrace> set_mrs thread buf msgs \<lbrace>\<lambda>_. equiv_but_for_labels aag {pasObjectAbs aag thread} st\<rbrace>
 2. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); ipc_buffer_has_auth aag thread buf \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits); buf = None\<rbrakk> \<Longrightarrow> \<forall>s t. True \<and> True \<longrightarrow> (\<forall>(rva, s')\<in>fst (set_mrs thread buf msgs s). \<forall>(rvb, t')\<in>fst (set_mrs thread buf msgs t). rva = rvb)
 3. \<And>a. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); ipc_buffer_has_auth aag thread buf \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits); buf = Some a\<rbrakk> \<Longrightarrow> reads_equiv_valid_rv_inv (affects_equiv aag l) aag (=) ((\<lambda>_. True) and (\<lambda>_. True)) (set_mrs thread buf msgs)
 4. \<And>s. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); ipc_buffer_has_auth aag thread buf \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits); True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True)) s proof (prove)
goal (4 subgoals):
 1. \<And>st. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); buf = None\<rbrakk> \<Longrightarrow> \<lbrace>equiv_but_for_labels aag {pasObjectAbs aag thread} st\<rbrace> do tcb <- gets_the (get_tcb thread);
y <- set_object thread (TCB (tcb\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>reg. if reg \<in> set (take (length msgs) msg_registers) then msgs ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch tcb) reg) (tcb_arch tcb)\<rparr>));
return (word_of_nat (min (length msg_registers) (length msgs)))
od \<lbrace>\<lambda>_. equiv_but_for_labels aag {pasObjectAbs aag thread} st\<rbrace>
 2. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); ipc_buffer_has_auth aag thread buf \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits); buf = None\<rbrakk> \<Longrightarrow> \<forall>s t. True \<and> True \<longrightarrow> (\<forall>(rva, s')\<in>fst (set_mrs thread buf msgs s). \<forall>(rvb, t')\<in>fst (set_mrs thread buf msgs t). rva = rvb)
 3. \<And>a. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); ipc_buffer_has_auth aag thread buf \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits); buf = Some a\<rbrakk> \<Longrightarrow> reads_equiv_valid_rv_inv (affects_equiv aag l) aag (=) ((\<lambda>_. True) and (\<lambda>_. True)) (set_mrs thread buf msgs)
 4. \<And>s. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); ipc_buffer_has_auth aag thread buf \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits); True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True)) s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); ipc_buffer_has_auth aag thread buf \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits); buf = None\<rbrakk> \<Longrightarrow> \<forall>s t. True \<and> True \<longrightarrow> (\<forall>(rva, s')\<in>fst (set_mrs thread buf msgs s). \<forall>(rvb, t')\<in>fst (set_mrs thread buf msgs t). rva = rvb)
 2. \<And>a. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); ipc_buffer_has_auth aag thread buf \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits); buf = Some a\<rbrakk> \<Longrightarrow> reads_equiv_valid_rv_inv (affects_equiv aag l) aag (=) ((\<lambda>_. True) and (\<lambda>_. True)) (set_mrs thread buf msgs)
 3. \<And>s. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); ipc_buffer_has_auth aag thread buf \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits); True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True)) s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); buf = None\<rbrakk> \<Longrightarrow> \<forall>s t. \<forall>x\<in>fst (set_mrs thread None msgs s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (set_mrs thread None msgs t). case x of (rvb, t') \<Rightarrow> rva = rvb
 2. \<And>a. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); ipc_buffer_has_auth aag thread buf \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits); buf = Some a\<rbrakk> \<Longrightarrow> reads_equiv_valid_rv_inv (affects_equiv aag l) aag (=) ((\<lambda>_. True) and (\<lambda>_. True)) (set_mrs thread buf msgs)
 3. \<And>s. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); ipc_buffer_has_auth aag thread buf \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits); True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True)) s proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); ipc_buffer_has_auth aag thread buf \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits); buf = Some a\<rbrakk> \<Longrightarrow> reads_equiv_valid_rv_inv (affects_equiv aag l) aag (=) ((\<lambda>_. True) and (\<lambda>_. True)) (set_mrs thread buf msgs)
 2. \<And>s. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); ipc_buffer_has_auth aag thread buf \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits); True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True)) s proof (prove)
goal (2 subgoals):
 1. \<And>buf'. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); ipc_buffer_has_auth aag thread buf \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits); buf = Some buf'\<rbrakk> \<Longrightarrow> reads_equiv_valid_rv_inv (affects_equiv aag l) aag (=) ((\<lambda>_. True) and (\<lambda>_. True)) (set_mrs thread buf msgs)
 2. \<And>s. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); ipc_buffer_has_auth aag thread buf \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits); True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True)) s proof (prove)
goal (4 subgoals):
 1. \<And>buf'. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); ipc_buffer_has_auth aag thread buf \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits); buf = Some buf'\<rbrakk> \<Longrightarrow> labels_are_invisible aag l ({pasObjectAbs aag thread} \<union> pasObjectAbs aag ` ptr_range buf' msg_align_bits)
 2. \<And>buf'. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); ipc_buffer_has_auth aag thread buf \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits); buf = Some buf'\<rbrakk> \<Longrightarrow> modifies_at_most aag ({pasObjectAbs aag thread} \<union> pasObjectAbs aag ` ptr_range buf' msg_align_bits) (\<lambda>_. True) (set_mrs thread buf msgs)
 3. \<And>buf'. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); ipc_buffer_has_auth aag thread buf \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits); buf = Some buf'\<rbrakk> \<Longrightarrow> \<forall>s t. True \<and> True \<longrightarrow> (\<forall>(rva, s')\<in>fst (set_mrs thread buf msgs s). \<forall>(rvb, t')\<in>fst (set_mrs thread buf msgs t). rva = rvb)
 4. \<And>s. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); ipc_buffer_has_auth aag thread buf \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits); True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True)) s proof (prove)
goal (3 subgoals):
 1. \<And>buf'. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); ipc_buffer_has_auth aag thread buf \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits); buf = Some buf'\<rbrakk> \<Longrightarrow> modifies_at_most aag ({pasObjectAbs aag thread} \<union> pasObjectAbs aag ` ptr_range buf' msg_align_bits) (\<lambda>_. True) (set_mrs thread buf msgs)
 2. \<And>buf'. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); ipc_buffer_has_auth aag thread buf \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits); buf = Some buf'\<rbrakk> \<Longrightarrow> \<forall>s t. True \<and> True \<longrightarrow> (\<forall>(rva, s')\<in>fst (set_mrs thread buf msgs s). \<forall>(rvb, t')\<in>fst (set_mrs thread buf msgs t). rva = rvb)
 3. \<And>s. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); ipc_buffer_has_auth aag thread buf \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits); True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True)) s proof (prove)
goal (3 subgoals):
 1. \<And>buf' st. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); ipc_buffer_has_auth aag thread buf \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits); buf = Some buf'\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>_. True) and equiv_but_for_labels aag ({pasObjectAbs aag thread} \<union> pasObjectAbs aag ` ptr_range buf' msg_align_bits) st\<rbrace> set_mrs thread buf msgs \<lbrace>\<lambda>_. equiv_but_for_labels aag ({pasObjectAbs aag thread} \<union> pasObjectAbs aag ` ptr_range buf' msg_align_bits) st\<rbrace>
 2. \<And>buf'. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); ipc_buffer_has_auth aag thread buf \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits); buf = Some buf'\<rbrakk> \<Longrightarrow> \<forall>s t. True \<and> True \<longrightarrow> (\<forall>(rva, s')\<in>fst (set_mrs thread buf msgs s). \<forall>(rvb, t')\<in>fst (set_mrs thread buf msgs t). rva = rvb)
 3. \<And>s. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); ipc_buffer_has_auth aag thread buf \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits); True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True)) s proof (prove)
goal (2 subgoals):
 1. \<And>buf'. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); ipc_buffer_has_auth aag thread (Some buf') \<and> is_aligned buf' msg_align_bits; buf = Some buf'\<rbrakk> \<Longrightarrow> \<forall>s t. \<forall>x\<in>fst (set_mrs thread (Some buf') msgs s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (set_mrs thread (Some buf') msgs t). case x of (rvb, t') \<Rightarrow> rva = rvb
 2. \<And>s. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); ipc_buffer_has_auth aag thread buf \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits); True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) (pasSubject aag) \<and> (aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag thread \<notin> subjectReads (pasPolicy aag) l); ipc_buffer_has_auth aag thread buf \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits); True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True)) s